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.