The trouble with formal specification, from someone who used to do it, is that only for some problems is the specification simpler than the code.

Some problems are straightforward to specify. A file system is a good example. The details of blocks and allocation and optimization of I/O are hidden from the API. The formal spec for a file system can be written in terms of huge arrays of bytes. The file system is an implementation to store arrays on external devices. We can say concisely what "correct operation" means for a file system.

This gets harder as the external interface exposes more functionality. Now you have to somehow write down what all that does. If the interface is too big, a formal spec will not help.

Now, sometimes you just want a negative specification - X must never happen. That's somewhat easier. You start with subscript checking and arithmetic overflow, and go up from there.

That said, most of the approaches people are doing seem too hard for the wrong reasons. The proofs are separate from the code. The notations are often different. There's not enough automation. And, worst of all, the people who do this stuff are way into formalism.

If you do this right, you can get over 90% of proofs with a SAT solver, and the theorems you have to write for the hard cases are often reusable.

Some realized that building the tests was the more important part of writing the software long ago...

Test tables and scenarios may not cover all the things that can go wrong (a la Goëdel), but not doing them almost guarantees broken software.

Whenever you look closely at what these proof nerds have actually built you typically find… nothing. No offense to them, it’s simply reality.