> That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.

But that doesn't have much to do with formal methods. You can achieve the same effect grabbing a colleague and explaining your spec to them, it will trigger the same rigorous thought because you want them to understand you.