The Case Against Formal Verification, 50 Years Later
Formal verification of software is revisited in light of a famous 1979 critique, with many arguing that while full, end‑to‑end proofs remain impractical for messy real‑world systems, targeted verification of critical components (e.g., distributed datastores, compilers, policy engines) is both feasible and valuable. Commenters highlight that specifying behavior rigorously is often harder than writing code, that model–code gaps and evolving requirements limit the reach of proofs, and that most real failures stem from flawed or inconsistent specs rather than implementation bugs. There is cautious optimism that powerful type systems, better tools, and AI assistance can make formal methods more accessible, but also concern that proofs can ossify bad designs and that economic incentives still favor “good enough” software over mathematically guaranteed correctness.
Scope and practicality of formal verification
- Many see full-system verification as intractable for messy, evolving products (e.g., social networks, GUIs), but agree that verifying specific subsystems and properties is valuable.
- GUIs are viewed as especially hard to specify; some mention constraint-based GUI approaches as closer to specs, mainly to prevent obvious UI bugs.
- Several comments stress there is no need for “all or nothing”: verifying permissions, API idempotence, distributed consistency, and data-loss properties is already highly useful.
Formal verification vs testing
- Verification is framed as guaranteeing properties for all executions, whereas tests sample executions.
- Property-based testing and mutation testing are discussed as intermediate techniques; fuzzing and random testing benefit from clear specs.
- Some argue we should think of formal methods as “testing on steroids,” not as a replacement.
Specifications: benefits, difficulty, and correctness
- Disagreement on whether specs are easier to understand than code: some find formal specs more concise and closer to intent; others find them harder than implementations.
- Historical examples (floating-point ops, compression, file systems, databases, networking) are cited where specs are simple and implementations complex.
- A long subthread on “sorting” illustrates how seemingly trivial specs are easy to get subtly wrong, reinforcing that writing correct specs is itself hard.
- Question raised: why assume the spec is more correct than the program? Responses: checking is often easier than constructing; specs can be simpler; but spec errors are real and must be treated like bugs.
Economics, incentives, and regulation
- Hardware-style economics (bugs cost millions) justify heavy verification; software usually relies on cheap patching instead.
- Some argue robust software already exists where buyers pay for it (banks, aviation); others note typical consumer software remains buggy.
- Concern that regulatory “verification stamps” could become bureaucratic rubber stamps without real quality gains.
AI, tools, and the model–code gap
- Past limitations included poor notations and insufficient compute; modern SAT/SMT solvers, proof assistants, and LLMs ease some of the burden.
- AI is currently most effective in expert hands; hope exists that agents will eventually generate specs and proofs for deep modules with simple invariants.
- The model–code gap (e.g., TLA+ spec vs Rust code) is seen as a core issue; suggested mitigations include:
- Proof assistants that generate executable code.
- Languages and ecosystems (e.g., SPARK/Ada, richer type systems, verified policy engines) where specs and code are tightly integrated.
- Some worry proofs and fine-grained tests can freeze poor abstractions and hinder refactoring.
Requirements vs implementation
- Several participants argue that, in many real projects, the main failures are inconsistent or impossible requirements, not incorrect code.
- They suggest the greater need is for tools that help formalize and verify requirements against technical and business constraints, not just implementations.