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. 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. 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 what correct means - which brings us back to the first part of Argument 2.
Argument 3: Fully automatic verification is out of reach
Having argued for why verification is bad as a means of communication, the authors shift their attention to the potential of fully automatic verifiers (in which case, we could be happy with the fact that a program was proven correct, even if the proof did not trigger a social process among colleagues). Fully automatic verifiers, the authors argue, are very unlikely to ever be built.
Comment
In the meantime, there has been some in developing automatic verifiers, though human effort (either writing proofs, or writing a suitable model to be model checked) remains crucial. However, LLM-powered tools are closing this gap quickly. Igor Konnov, in his post Formal proofs for distributed protocols with AI may be closer than you think, describes his experience proving the safety of the Ben-Or protocol in Lean.
Argument 4: Even if fully automatic verification were within reach, it would be detrimental
The authors claim that verifiers that simply respond with “VERIFIED” or “NOT VERIFIED” do not contribute to understanding and would leave programmers clueless about how to modify the program further. Furthermore, they argue, having a verified program may reduce the incentive for other layers of defense (e.g., monitoring, rate-limiting and similar).
Comment
This is a weak argument, relying on the worst possible assumptions about how verification tools and programmers’ behaviors would look in the presence of automatic verification.
Argument 5: Real-world systems are too messy to be specified
There is a huge difference, it is correctly noted, between algorithms and real-world systems. Whereas a specification for an algorithm can often be concise and tidy, specifications of real-world systems are ad-hoc, unstable, and messy. Furthermore, in most real-world systems, the algorithms are simple and easy (and thus verifying them is not of great value).
Comment
It is true that not all systems need to be verified. However, in last decades and years, there are changes that push for more verification:
- As software is entering critical infrastructure and the world of finance, the stakes get higher.
- If we have any hope that a coding agent creates what we want, we should better be able to describe what we want. Of course, this does not always need to be a formal specification, but the goal of precisely specifying our intent becomes more important when we work with coding agents. (This does not imply full verification, but the art of specification too is one of the formal methods tools.)
Argument 6: Software reliability is much more than verification
“The desire to make programs correct is constructive and valuable. But the monolithic view of verification is blind to the benefits that could result from accepting a standard of correctness like the standard of correctness for real mathematical proofs, or a standard of reliability like the standard for real engineering structures. The quest for workability within economic limits, the willingness to channel innovation by recycling successful design, the trust in the functioning of a community of peers–all the mechanisms that make engineering and mathematics really work are obscured in the fruitless search for perfect verifiability.”
Comment
I am fully onboard with this argument. Indeed, full verification of a system is rarely the best way to go about reliability. All other efforts towards software correctness are equally valuable. And those two are not competitors: the increased focus on best methods to bring about correctness is what matters.
## Conclusion This was quite a fun paper to read. The authors make a good point that formal verification is not a magic wand that solves all the correctness issues. Indeed, as they point out, there is much more to software correctness than verification: engineering processes, business considerations, additional layers of defense, and so on.
Because of their focus on full verification, the authors of the paper wrongly dismiss how useful different parts of formal methods are for overall understanding, better design choices, or higher velocity. All that gets amplified with AI coding agents writing the code, leaving humans with the task of specifying what needs to be written and checking that it was written according to the given specification. This makes the work of coding agents easier, too: verification gives them a way to close the loop and tell whether what they wrote was correct.
Thanks to two fellow FM practitioners, Thomas Pani and Ranadeep Biswas, for useful discussions about the paper and this post. It would also be interesting to hear from people outside the bubble who still find formal methods useless.