[pron]

First, the art and science of formal verification has largely moved away from proving programs correct to better/cheaper ways of catching more bugs (at least when mainstream software is concerned). So the most important question is "is a TLA+ specification a cost-effective way of catching bugs even without a formal tie to the implementation?" My opinion on that is an emphatic yes. (BTW, code reviews are an effective assurance technique even though they're not formal at all).

However, there are ways to create formal ties between a TLA+ spec and a running program. As always, the sounder the method the more costly it is (and the cost often grows faster than the increased confidence). One approach that is being research is checking execution logs against the model, perhaps online as the program is running.

At the end of this talk, https://youtu.be/TP3SY0EUV2A, I mention the technique and theory behind it, referring to this paper, Model-Based Trace-Checking [1]. I believe research is ongoing and you can find more recent papers on the subject.

[1]: https://arxiv.org/abs/1111.2825

[0x1ceb00da]

What are some of the lesser known "better/cheaper ways of catching more bugs"?

[pron]

If we look at practices that fall under formal methods, I would include things like TLA+ (or Alloy) specifications and concolic testing (https://en.wikipedia.org/wiki/Concolic_testing) (which is sometimes used as a step in the process of automatic test generation).

Practices that are not usually considered formal methods include clever semi-blackbox fuzzing (like Antithesis) and mutation testing to improve test quality.