The Case Against Formal Verification, 50 Years Later: Do the Old Arguments Still Hold?

In 1979, DeMillo, Lipton, and Perlis argued that formal program verification was “bound to fail.” With AI coding agents driving renewed interest in formal methods, their objections deserve a fresh look.

Why Verification Is Having a Moment

Three forces are pushing formal verification into the mainstream. AI agents create gaps in human understanding of generated code, demanding other correctness assurances. New tooling makes verification faster to incorporate into real workflows. And as code generation accelerates, correctness becomes the remaining competitive frontier.

The result: Google Trends shows a sharp spike in formal verification searches over the past two years, Lean is attracting new learners, and projects like Signal Shot aim for end-to-end verification of major applications.

The Six Original Arguments, Revisited

1. Mathematical proofs are social processes

The paper argued that proofs gain credibility through community internalization, not formal derivation alone. This critique targets a specific motivation for verification, not its foundations. It holds up—but it was never a reason to abandon verification entirely.

2. Specifications are unreliable

Two sub-claims here. First, translating informal requirements into formal specs is itself an unverified, lossy process. This remains true, but modern specification languages like Quint let you explore edge cases interactively, closing the gap between intent and spec.

Second, specs only have value independent of implementations—and iterative development makes that independence impossible. This argument was weak in 1979 and is weaker now. When a conflict arises between spec and code, humans decide which to change. AI agents can write code and generate proofs, but only humans define what “correct” means.

3. Fully automatic verification is out of reach

This was plausible in 1979. Today, LLM-powered tools are closing the gap rapidly. Igor Konnov’s recent work proving the safety of the Ben-Or protocol in Lean illustrates how quickly AI assistance is changing what’s feasible.

4. Automatic verification would harm understanding

The authors worried that a black-box “VERIFIED” stamp would leave programmers unable to modify programs and reduce investment in other defenses. This assumes the worst about both the tools and the engineers using them. It doesn’t hold.

5. Real-world systems are too messy to specify

Algorithms have clean specs; production systems don’t. This remains partly true—not every system warrants full verification. But two trends shift the calculus: software now runs critical infrastructure and financial systems where stakes are high, and working with AI coding agents demands precise descriptions of intent even when full formal proof isn’t the goal.

6. Verification is not the whole of reliability

The paper’s strongest point: engineering reliability requires economic tradeoffs, design reuse, peer review, and layered defenses—none of which verification replaces. This still holds, and the verification community largely agrees. Full verification is rarely the optimal path to reliability.

What the Paper Gets Wrong

The authors focus exclusively on full verification and miss how partial formal methods improve design, accelerate understanding, and increase development velocity. AI coding agents sharpen this value further: they write the code, humans specify the requirements, and verification closes the loop—giving agents a way to confirm whether their output is correct.

The Bottom Line

The 1979 objections were reasonable for their time, but AI tooling has weakened the strongest technical ones. The philosophical objections—specs are hard, reliability requires more than proofs—remain valid and useful reminders against over-reliance on any single technique.

Start exploring formal methods not as a replacement for good engineering practice, but as one more tool that AI makes increasingly accessible.