We have strong evidence that formal verification works. The problem has really not been about its effectiveness, but rather 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 — from dollars to cents, from hours to seconds.
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.
What We Have Been Measuring
This is not merely a theoretical claim. We have been running systematic experiments using rocq-piler, our open-source Rocq proof assistant, to measure how reliably LLMs can discharge non-trivial proof obligations automatically.
The benchmark suite includes problems that require genuine induction — historically one of the hardest things to automate, because it requires guessing the right induction principle and invariants. Some results from DeepSeek v4:
| Problem | What it proves | Time | Cost |
|---|---|---|---|
| Insertion sort correctness | Output is sorted (induction on list) | ~4 min | $0.03 |
| Dependent typed vector operations | Progress + preservation for a dependent type system | ~5 min | $0.03 |
| Merge sort correctness | Output is sorted AND is a permutation of input | ~23 min | $0.21 |
| PCF type preservation | Type safety for a lambda calculus with mutable references | ~20 min | $0.06 |
These are not toy examples. Merge sort requires two separate inductive theorems — that the output is sorted, and that it contains exactly the same elements as the input. PCF type preservation, which we have written about separately, requires handling variable binding, substitution, and store typing — a proof that in the seL4 style would take days of expert time.
Not every problem closes on every attempt. Indexed inductive families and applicative bisimilarity remain harder, and we have been using those as the frontier to push against as the tooling improves. But the easier problems close reliably and cheaply, and the harder ones are closing more often as the tools develop.
This is what the cost curve looks like in practice: routine inductive proofs for cents, harder theorems for dollars, with the boundary moving as models and tooling improve. The economics are already there for a large fraction of the proof obligations that real software contracts generate.