The Case Against Formal Verification, 50 Years Later - Ivan Gavran
The Case Against Formal Verification, 50 Years Later | Ivan Gavran
Ivan Gavran
15.08.2026
The Case Against Formal Verification, 50 Years Later
Engineers are getting excited about software verification! This may come as a surprise, since verification has long been considered useful only in very niche cases (at best; and impractical, useless or a complete waste of time at worst). Yet, the hype around it is clearly here: Google Trends shows a large spike in searches for formal verification/formal methods in the last two years, everybody’s learning Lean, new specification languages are popping up regularly, and there are efforts to verify major applications end-to-end (e.g., the Signal Shot project).
The main driver of this excitement is AI coding. First, AI agents leave a hole in our understanding of the programs they write, thus creating the need for other means of correctness assurance. Second, they make verification itself faster and easier to incorporate into real-world software development. Third, and perhaps the most important for business, if writing programs is made super fast, all future gains will be in the area of software correctness assurance.
Will Wilson of Antithesis declares the victory for this traditionally niche area in his talk titled We won, what now? (The talk, delivered as the opening to Bug Bash 2026, is great, and it gives some good ideas for the future of verification community, given the mainstream adoption.)
In that victorious context, it is interesting to return to one of the classic papers arguing against formal verification, Social Processes and Proofs of Theorems and Programs. Writing in 1979, its authors say:
“We believe that (…) program verification is bound to fail. We can’t see how it’s going to be able to affect anyone’s confidence about programs.”
I will go through the arguments in the paper and examine what recent developments (if any) invalidate them. This is a fun exercise rather than a completely serious one: the paper does not actually claim that all formal methods efforts are doomed (but only full verification). Furthermore, it is far from clear that verification is going to become a regular part of software engineering (what we are seeing are only early signs of interest). Nonetheless, re-examining in 2026 obstacles that were seen as fundamental 50 years ago will hopefully be useful and interesting.
Argument 1: Mathematical proofs are about social processes
In this argument, the authors of the paper argue against the idea that programming should become more like mathematics in terms of each program corresponding to a theorem that needs a proof. They say: Hold on, it is not the case even in mathematics that proofs of theorems are the end of the process. Instead, the proof is the first step and a means of communication. The really important part happens when other mathematicians internalize the proof, and the claim makes contact with other branches of mathematics or physical reality. This whole process contributes to the claim’s believability.
Comment
Nothing to object to here: proofs of programs do not need to correspond to mathematics exactly. (The argument is against a particular motivation, rather than against fundamentals of software verification.)
Argument 2: Problems with the specification
The first part of the argument goes like this: There is some real-world requirement that is informal (the people involved have a shared intuitive understanding of what the requirement is). This intuitive, informal requirement needs to be translated into a formal specification, which in itself is an informal process. In that process, which is unverified, a lot can be lost or misinterpreted.
Comment
That is a fair point. The counterpoint is that specifications are closer to informal requirements than implementations are (and thus a mistake is easier to spot). Additionally, modern specification languages (such as Quint) enable examining the specification and all its edge-cases interactively, to make sure it really corresponds to our intuition.
The second part of the argument says that the specification is only valuable if it is independent of the implementation. Given the iterative nature of software development, that is almost impossible. Once the independence is lost, we are really just aligning the specification and implementation (and potentially introducing to both similar mistakes).
Comment
I don’t think this was a strong argument even in the past, and especially not with coding agents in the loop.<br>Whenever additional understanding is gained, this is good overall for the development process. Humans, as the final arbiters, decide which way to change the specification, re-examining initial assumptions.<br>Coding agents may be allowed to produce and change code, and to produce proofs. If, however, there is a need to modify the specification, only a human can do that as the final arbiter of...