Specifications Don't Exist: Why Formal Verification Hits a Wall

Galois researcher Mike Dodds argues that while formal verification works for naturally formalizable systems like compilers and microkernels, most real-world software—from web browsers to PDFs—lacks a precise, coherent specification. Drawing on his experience with DARPA's SafeDocs project, he shows how informal specs (docs, tests, slide decks) are ambiguous and contradictory, making formal verification impossible for most systems. As AI makes proofs cheap, the bottleneck shifts to specification, and we still don't know how to write one for a web browser.