Formal verification works. The evidence is not contested. The question has always been whether it is worth the cost.
The seL4 microkernel — the most comprehensively verified operating system kernel ever produced — took approximately 20 person-years to verify 8,700 lines of C code, producing around 1.3 million lines of Isabelle/HOL proof. In exchange: zero functional correctness defects in verified code in over 15 years of deployment. No buffer overflows. No null pointer dereferences. No memory leaks. No undefined behaviour. For a security-critical kernel running in aircraft, medical devices, and classified government systems, this is exactly the guarantee you want. The original SOSP 2009 paper and the comprehensive 2014 TOCS paper document what was built.
The same pattern holds wherever formal verification has been applied seriously. CompCert, the formally verified C compiler, produced zero wrong-code errors in its middle-end under extensive CPU-year-scale fuzzing — while GCC and LLVM had hundreds. Yang et al. (PLDI 2011) ran the comparison; Leroy’s original POPL 2006 paper describes the verification. Airbus applied the Astrée static analyser to the A340 primary flight control software (132,000 lines of C) in 2003, proving the complete absence of runtime errors with zero false alarms — and then applied it to the A380 before its maiden flight in 2005. Blanchet et al. (PLDI 2003) describes the approach. Amazon Web Services has used TLA+ for critical distributed systems since 2011, finding serious design bugs in S3, DynamoDB and EBS that testing had missed; Newcombe et al. (CACM 2015) documents the experience.
The evidence is consistent: formal verification eliminates whole classes of bugs that testing cannot catch. It has been worth doing wherever the stakes were high enough to justify the cost. The problem is that the cost — roughly 10–20× the effort of writing the code — has placed it out of reach for the overwhelming majority of software engineering. Not because the guarantees were not valuable, but because the economics did not work.
What Changes with AI
Two traditions in software engineering have both tried to address the problems of correctness and scale. Software verification gives strong, machine-checked guarantees but requires specialist expertise and enormous effort. Design by contract annotates functions with preconditions and postconditions in readable, practical form, but has relied on testing rather than proof to check them. Each addressed part of the problem.
With AI discharging proof obligations, these become a single approach. An LLM writes the code and the contracts; a theorem prover checks them. The human writes the specification. The cost of obtaining machine-checked guarantees falls from 20 person-years to the cost of a proof run — cents to dollars, minutes to hours.
This changes what is economically rational. When verification costs less than the incident it prevents, it becomes routine infrastructure rather than a specialised investment. The guarantees seL4 spent 20 years earning are the same guarantees that vericoding makes available to any function with a contract.
The value was always there. The cost is what is changing.