Ivan Gavran's recent post, The Case Against Formal Verification, 50 Years Later, revisits DeMillo, Lipton, and Perlis's 1979 paper Social Processes and Proofs of Theorems and Programs against the backdrop of a genuine resurgence of interest in formal methods. The timing is striking. Formal verification has spent most of its life as a niche discipline, respected in certain corners of safety-critical systems engineering and academic PL theory, but largely invisible to mainstream software practice. Something has shifted. Whether that shift is durable is the more interesting question.
Why the Resurgence Is Happening Now
The proximate cause is AI-assisted code generation. When a large language model writes a function, the developer who accepts that output carries a reduced epistemic relationship to it. They did not construct it; they evaluated it, perhaps cursorily. This creates a structural gap between the artifact and human understanding of its correctness properties, a gap that testing alone cannot reliably close. Formal specification and verification offer one principled way to address that gap, and this is not lost on practitioners.
There is a second, more commercially legible driver. If code generation velocity approaches some asymptote through AI tooling, the competitive differentiator shifts toward correctness assurance. Will Wilson's framing at Bug Bash 2026, that verification has effectively "won" and the community should now think about what comes next, reflects this logic. It is a plausible argument, though it elides how far the field still is from routine industrial deployment outside of a small number of high-stakes domains like cryptographic protocol verification and hardware model checking.
The third driver is the maturation of tooling. Lean 4, Dafny, TLA+, Quint, and a growing ecosystem of LLM-assisted proof assistants have meaningfully reduced the activation energy required to engage with formal methods. Igor Konnov's reported experience proving the safety of the Ben-Or protocol in Lean with AI assistance is an early data point, not a trend, but it gestures at a possible trajectory.
Reassessing the 1979 Arguments
Gavran's structured walk through the six main arguments in DeMillo et al. is useful and fair. A few of them deserve closer scrutiny than the post provides.
The specification problem remains underrated as a difficulty. Argument 2, concerning the informal-to-formal translation gap, is dismissed somewhat quickly. The claim that specifications are "closer to informal requirements than implementations are" is true in some sense, but it understates the degree to which formal specifications can be subtly wrong in ways that are harder to detect than implementation bugs. A specification is a theory of the system's intended behaviour. Theories can be internally consistent and externally wrong. The history of verified systems includes cases where the specification was faithfully implemented and the resulting system still failed to meet actual requirements, because the specification encoded a misunderstanding rather than a mistake. Quint's interactive exploration of edge cases is a genuine improvement, but it addresses the tractability of specification examination, not the fundamental epistemological problem of specification validity.
The independence of specification and implementation is a real constraint. The dismissal of the co-evolution problem is too quick. When specifications and implementations are developed and refined together, as they almost always are in practice, the verification guarantee weakens. The proof establishes consistency between two artefacts, not correspondence between either artefact and the world. This is not an argument against verification; it is an argument for being precise about what verification actually guarantees. The field has grappled with this honestly, through notions like refinement and abstraction hierarchies, but the 1979 critique retains some bite.
The fully automatic verification argument has aged worst. DeMillo et al. were sceptical that fully automatic verifiers would ever be practical. This was reasonable in 1979, when even propositional satisfiability was not yet practically tractable for real-world instances. The subsequent development of SAT solvers, SMT solvers, and model checkers has substantially changed the picture for bounded and finite-state verification. The remaining question, whether LLM-assisted proof generation will extend this to unbounded, higher-order reasoning at scale, is genuinely open. The early evidence is suggestive but not conclusive.
The Human-in-the-Loop Question
Gavran makes a structurally important point about the division of labour between humans and coding agents. The proposal is roughly: agents write code and proofs; humans retain authority over specifications. This is a coherent position, and it maps onto a plausible near-term workflow. But it raises questions the post does not fully address.
- Specifications written by humans will inherit human cognitive limitations, including the tendency to under-specify concurrency behaviour, exception handling, and failure modes that are difficult to reason about informally.
- If agents are generating proofs, the social process that DeMillo et al. identified as essential to mathematical confidence, peer review, internalisation, contact with other results, is absent from the proof artefact. A machine-generated proof of a machine-generated program, checked by a proof assistant, provides a certain kind of assurance but not the same kind as a proof that has been read and understood by multiple competent humans.
- The boundary between "modifying the specification" and "modifying the code" is not always crisp. Specifications often contain executable or near-executable content, and the line between refining a spec and writing an implementation is context-dependent.
None of these are fatal objections. They are constraints that a mature methodology will need to accommodate. The field of certified compilation, exemplified by CompCert, offers a useful existence proof: it is possible to build verified systems that are genuinely useful in practice, but the effort required and the scope of what is verified remain significant constraints.
What the 1979 Paper Got Right That Still Matters
The most durable argument in DeMillo et al. is Argument 6, the one Gavran endorses most fully. Software reliability is an ensemble property. It arises from testing, monitoring, redundancy, operational practices, code review, architectural choices, and yes, formal methods, in combination. The risk of the current hype cycle is not that formal verification will fail; it is that enthusiasm for one technique will crowd out investment in the others, or that verification will be treated as a binary property (verified versus unverified) rather than as one input into a probabilistic assessment of system trustworthiness.
The analogy to structural engineering is apt and worth extending. Civil engineers do not consider a bridge safe because its design calculations were formally verified. They consider it safe because the calculations were verified, the materials were tested, the construction was inspected, the design includes safety margins, and the bridge is monitored in service. Formal verification is the calculation step. It is necessary but not sufficient, and the profession has known this for a long time.
Where This Leaves the Field
The current moment is genuinely interesting. The combination of AI-generated code creating demand for stronger correctness assurance, LLM-assisted proof generation reducing the cost of supplying that assurance, and maturing specification tooling making the process more accessible is a coherent story about why formal methods might achieve broader adoption than they have managed in the previous five decades.
The caveats are real, though. Broader adoption of formal methods will require:
- Better tooling for specification validation, not just specification writing. The gap between a formal spec and the actual requirement remains the hardest part.
- Clearer communication about what verification guarantees and what it does not. Overselling will produce backlash when verified systems fail for reasons outside the verification scope.
- Integration with existing engineering practices rather than replacement of them. Verification should sit alongside testing, monitoring, and operational discipline, not substitute for them.
- Empirical evidence at scale. The field needs more data on where formal methods provide the best return on investment, and under what conditions the cost is justified.
Gavran's post is a thoughtful and well-structured engagement with a classic paper. The exercise of revisiting foundational critiques as conditions change is exactly the kind of intellectual housekeeping the field needs. The 1979 arguments have not all been invalidated; some have been weakened, some have been partially addressed by tooling, and some remain as live constraints. The honest conclusion is that formal verification is more useful than DeMillo et al. believed it would be, less transformative than the current hype cycle suggests, and most valuable when understood as one component of a broader correctness engineering practice rather than as a solution in itself.