[jffhn]

Yes, I guess the proof is only relative to the formal spec, if the spec (formal or not) is nonsense it's another problem (so you might not have to test the program, but still have to test the complete system).

But I guess (again) that having formal specs getting proven helps to avoid inconsistent specs. I recall a talk by Martyn Thomas where he said that with these methods it was harder to get programs to compile (for example, the compiler could complain if it detected an inconsistency, either between the spec and the program or within the spec itself).