The post is a 50-years-later response to the DeMillo, Lipton, and Perlis critique of formal verification. It argues that the old paper was right about one thing in particular: verification is not just math, it is also a social process of agreeing on abstractions, requirements, and acceptable proof artifacts. But the stronger historical claim, that formal verification is fundamentally mismatched to real software and unlikely to scale, looks much weaker now that theorem provers, model checkers, SAT and SMT techniques, and compute have improved so much.
The useful landing point was not "formal verification everywhere". It was that the strongest use cases are narrow, high-value, and property-driven. People kept coming back to compilers, distributed systems, hardware, policy engines, compression, floating point, and safety-critical software. In those domains, the
spec can be much smaller than the optimized implementation, or at least much easier to reason about than the full runtime system. That is why examples like
CompCert keep carrying weight. One commenter pointed to
Csmith testing, which reportedly found no wrong-code bugs in CompCert's verified core while it found them in every mainstream compiler it tried. That does not prove formal methods beat every alternative. It does show they can carve out a class of failures that conventional testing keeps missing.
The recurring objection was the spec itself. If the specification is wrong, a proof just gives you a rigorous way to be wrong. Most people did not treat that as a fatal flaw. They treated it as the normal frontier. Verification shrinks the uncertainty surface from "implementation plus requirements" to mostly "requirements and modeling." Several comments made the practical point that this is still a win, especially when the properties are crisp, like memory safety, idempotence,
liveness, confidentiality, or preserving the semantics of an unoptimized reference implementation. The harder cases are products whose behavior is partly social, emergent, or UI-driven. Nobody had a convincing answer for "verify Facebook" as a whole, but several did for verifying the storage, permissions, consistency, and policy pieces inside it.
A second big theme was the
model-code gap. Proving a
TLA+ model safe is not the same thing as proving the Rust or C++ implementation safe. That gap is where a lot of industrial pain lives. The consensus answer was not to pretend it away. Either generate executable code from the proof environment, or use languages and toolchains where proofs attach directly to the implementation, like
SPARK or language-integrated hardware formalisms. Otherwise treat the model as architecture assurance, which is still valuable, but not the same guarantee.
AI came up mostly as an accelerator, not a substitute for judgment. Several people were skeptical that current AI changes the adoption story much, because the hard part is choosing the right abstraction and writing the right properties. People already good at formal methods get leverage. Everyone else still faces the same conceptual climb. The more grounded AI take was narrower: use it to help draft models, explore state spaces, generate proof boilerplate, or keep generated config and policy artifacts inside strongly constrained declarative systems. The thread was broadly positive about formal verification's technical progress, but blunt that adoption is still gated by specification skill, workflow friction, and the economics of where correctness actually pays for itself.
ivan-gavran.github.io