I'm not sure that is necessarily true. I think of the modern typechecker (especially with generics, algebraic data types, and other advanced features, including sometimes dependent tpes) as basically formal-verification-lite, and it tends to work really well with changing specs. You can aggressively refactor and change code and just let the compiler catch errors as you go. A practical formal verification language would function much the same way.
This! I'd also argue that your formal verification language and your coding language are one and the same. This leads to the case where if you can specify your language, it is written.
Obviously there are scenarios where it's not practical to prove a part of the program, but you can simply use an unsafe dialect as per Rust or Maude (system modules).
This works well with agile development in that you can spec out the underlying communications protocols, parallel operations etc. and layer unsafe stuff on top.
While we're here then, being able to publish these proven modules for other people should lead to a situation where we can build incrementally on code proofs.
Lastly, you can consider this system to be the equivalent of unit tests, but better in that there are guaranteed to be no edge cases you haven't tested (subject to coverage, but again publishing modules should help bullet-proof them).
For integration testing, you can use behavioural proofs - see Maude or BOBJ.
