The Dilemma and Way Forward for Formal Verification: Lessons from 50 Years of Debate

A Debate Spanning Half a Century

In 1979, computer scientists Richard DeMillo, Richard Lipton, and Alan Perlis published a highly controversial paper, Social Processes and Proofs of Theorems and Programs, openly questioning the feasibility of formal verification as a means of ensuring software correctness. Formal verification is a technique that uses mathematical methods to rigorously prove that a system's behavior conforms to a predetermined specification—unlike traditional testing, which can only discover the presence of errors through a finite set of test cases, formal verification attempts to prove the absence of errors (for all possible inputs). This distinction stems from Edsger Dijkstra's famous dictum: "Testing can only prove the presence of bugs, never their absence."

Half a century later, this debate has returned to the spotlight—in a recent article titled The Case Against Formal Verification, 50 Years Later that sparked heated discussion on Hacker News, the author revisits the original criticisms and reflects on them against today's technological reality.

The discussion garnered 74 upvotes and 62 comments on the platform, demonstrating that formal verification—a seemingly niche topic—still strikes a nerve within the software engineering community. It touches on a fundamental question: can we truly use mathematical rigor to guarantee software correctness?

The Original Core Criticisms: Social Processes and the Specification Dilemma

Historical Context and Author Credentials

To understand the weight of this paper, one must appreciate its authors and historical context. Alan Perlis was the first recipient of the Turing Award (1966), renowned for his research in programming languages; Richard Lipton went on to make important contributions to computational complexity theory and cryptography; Richard DeMillo conducted deep research in software engineering and cybersecurity. The era in which they published this paper was significant: the 1970s "program verification" movement was at its peak, with Dijkstra, Hoare, Floyd, and others vigorously advocating mathematical methods for ensuring program correctness. Academia was permeated by optimism, believing that formal methods were about to completely solve the software crisis. It was in this academic atmosphere that three heavyweight scholars dropped a "bombshell."

Mathematical Proofs Depend on Social Processes

The sharpest argument from DeMillo et al. was this: mathematical theorems are trusted not because their formal derivation chains are flawless, but because they have undergone a "social process"—being repeatedly read, examined, cited, and corrected by large numbers of mathematicians. A proof's credibility comes from human collective consensus.

Formal proofs of programs precisely lack this social process. A hundreds-of-pages-long program correctness proof, filled with mechanical symbols, is something almost no one is willing to read, let alone verify. It is lengthy, tedious, and lacks the communicable, discussable elegance of mathematical proofs. Therefore, the authors argued, such proofs cannot earn genuine trust.

The Specification Itself May Be Wrong

Another classic criticism is that formal verification can only prove "the program conforms to the specification," but cannot guarantee "the specification itself is correct." If your formal description of the system is flawed, then even the most rigorous proof is merely proving something wrong. In other words, verification doesn't eliminate human error—it merely shifts it from code to specification.

This problem has deep philosophical roots—it resembles Wittgenstein's paradox of rule-following: how can we ensure that our formulation of a rule is itself unambiguous? In the software engineering context, this means that no matter how powerful our verification tools become, the essential difficulty of "understanding requirements" can never be automated.

The State of Formal Verification Half a Century Later

Tool Maturity Has Changed the Game

The core disagreement in the article and comments is whether the original criticisms still hold today. Opponents point out that in 1979, formal verification relied almost entirely on manual derivation, whereas today we have powerful machine-assisted proof tools like Coq, Isabelle, Lean, TLA+, and Dafny. Machine proof checkers take on the heavy lifting of "reading proofs," and humans need only trust a relatively small, well-vetted verification kernel.

Modern theorem provers are typically designed around a minimal "Trusted Computing Base." Take Coq as an example: it's based on the Calculus of Inductive Constructions, with a core type checker of only a few thousand lines of code—all proofs are ultimately verified by this small kernel. Lean 4, developed by Microsoft Research, has gained significant attention in recent years for its widespread use in mathematical formalization (e.g., the Mathlib library, which now contains over 100,000 theorems). Isabelle employs the LCF architecture, using the ML type system to ensure that only theorems verified through core inference rules can be constructed. TLA+, designed by Leslie Lamport (2013 Turing Award laureate), focuses on specification and model checking for concurrent and distributed systems.

This partially addresses the "social process" criticism—we no longer need humans to review proofs line by line; instead, trust is transferred to a proof kernel that has been validated by the community over extended periods. Real engineering cases like the CompCert compiler and the seL4 microkernel demonstrate that large-scale formal verification is feasible in critical systems.

Landmark Engineering Verification Cases

CompCert is a fully formally verified C compiler developed by Xavier Leroy's team at INRIA in France, using Coq to prove that compilation from C source code to PowerPC/ARM/x86 assembly preserves semantic equivalence. This means if the source program satisfies a certain property, the compiled target code is guaranteed to satisfy it too—fundamentally eliminating the entire class of compiler-introduced bugs. In a famous comparative study, researchers performed fuzz testing on multiple C compilers and found numerous miscompilation cases in GCC and LLVM, while CompCert's verified portions never exhibited such problems.

seL4 is a microkernel operating system developed by Australia's NICTA/Data61 team. Its complete functional correctness proof required approximately 20 person-years, with proof code roughly 10 times the size of the implementation code (approximately 200,000 lines of proof corresponding to 8,700 lines of C code). seL4 has been deployed in military drone communication systems, autonomous driving platforms, and critical infrastructure, making it a landmark case of formal verification moving from academia to industry.

But Fundamental Challenges Remain

However, those who support the original paper argue that tool improvements haven't touched the essence of the problem. The specification correctness issue persists—you still need to describe "what is correct" in some language, and that description itself cannot be verified. Furthermore, the cost of formal verification remains high: verifying the seL4 microkernel took dozens of person-years of work, an investment unrealistic for the vast majority of software projects.

Commenters pointed out that modern software's complexity, external dependencies, and rapid iteration pace make complete formal verification increasingly impractical from an engineering standpoint. A typical modern web application might depend on hundreds of third-party libraries, interact with multiple external services, and release new versions weekly or even daily—maintaining complete formal proofs in such an environment is nearly impossible. What has actually been widely adopted are lighter-weight formal methods, such as type systems, static analysis, model checking, and property-based testing.

Compromise Approaches Are Becoming Mainstream

Interestingly, the real insight from this debate may not be about "whether verification is feasible," but rather "to what degree should verification be pursued." Industry practice trends offer a pragmatic answer:

• Type Systems: Languages like Rust and Haskell use type systems to eliminate large categories of errors at compile time, essentially providing lightweight formal guarantees. Rust's Ownership System and Borrow Checker are based on affine type and region type theory, guaranteeing memory safety and freedom from data races at compile time without runtime garbage collection. Microsoft research shows that approximately 70% of security vulnerabilities in their products are memory safety issues—Rust's type system eliminates this entire class of defects by design. This is a textbook case of formal methods being "democratized" into everyday engineering practice: programmers don't need to write explicit proofs; the type system automatically enforces safety properties.

• Model Checking: Tools like TLA+ are used to verify the design logic of distributed systems, and companies like Amazon have incorporated them into their engineering workflows. Model checking was invented by Edmund Clarke, Allen Emerson, and Joseph Sifakis, who received the 2007 Turing Award for this work. Unlike theorem proving, model checking automatically verifies system properties by exhaustively exploring the state space. Amazon Web Services engineering teams have used TLA+ since 2011 to verify distributed protocol designs for core services like DynamoDB, S3, and EBS, publicly reporting that TLA+ helped them discover multiple subtle concurrency bugs that would have been nearly impossible to catch through traditional testing—bugs that might require specific combinations of event timing to trigger, which conventional testing could almost never cover. Intel also significantly increased its investment in formal methods after the 1994 Pentium FDIV floating-point division bug cost approximately $475 million.

• Property-based Testing: Sitting between testing and proof, it uses random inputs to verify program properties, balancing cost and effectiveness. Originally popularized by the Haskell community's QuickCheck tool, it has since expanded to virtually all mainstream programming languages. Unlike traditional unit tests that manually specify inputs and outputs, property-based testing requires developers to describe general properties that programs should satisfy (e.g., "a sorted list should preserve its elements" or "encrypting then decrypting should yield the original text"), then automatically generates large numbers of random inputs to verify these properties. While it cannot provide mathematical proof-level guarantees, in practice it discovers a large number of edge-case bugs at extremely low cost.

These methods don't pursue "absolute correctness" but seek a balance between cost and reliability. What DeMillo et al. opposed was the grand ideal of providing complete mathematical proofs for entire programs—an ideal that has indeed been replaced by more pragmatic approaches today. The spectrum of formal methods is very broad—from the lightest type checking to the heaviest full-program verification—and engineers can choose an appropriate position based on how critical their system is.

Lessons for Today's Engineers

This 50-year debate reminds us that software correctness has never been a black-and-white proposition. Formal verification is neither a silver bullet nor a worthless academic toy. It has proven its value in high-risk domains like aerospace (e.g., Airbus flight control software uses the Astrée static analyzer), operating system kernels, and cryptographic protocols (e.g., the miTLS implementation of TLS 1.3 was verified using the F* language)—but for most applications, the cost-benefit ratio remains unfavorable.

Perhaps the more important lesson is this: no matter how rigorous the verification, it cannot replace clear thinking about "what we actually want." The persistence of the specification correctness problem demonstrates that the core engineering challenge often lies not in "how to build correctly" but in "what is correct to build"—precisely the distinction Fred Brooks drew in No Silver Bullet between "essential complexity" and "accidental complexity": formal verification can help us eliminate errors in accidental complexity, but cannot touch the cognitive challenges within essential complexity.

Half a century on, the value of this old paper lies not in whether it "predicted correctly," but in how it forces each generation of engineers to seriously consider: upon what exactly is our trust in software correctness built? In today's world where AI-assisted programming is becoming increasingly prevalent and code generation is increasingly performed by machines, this question may be more urgent than ever—do we need a new generation of formal methods to verify AI-generated code? This conversation, begun in 1979, is far from over.