Proof is getting cheap: AI and formal verification

Proving that code cannot fail used to be reserved for chips, aircraft and cryptography. New research suggests language models can bring it to ordinary open-source libraries.

Testing shows that code works on the inputs you tried. Formal verification goes further: it proves, with a machine checking every step, that a property holds for every input within stated limits. It is how chip designers, avionics teams and cryptographers get guarantees that testing alone cannot give. It has also been slow, specialist work, which is why almost nobody uses it on everyday software.

Research Anthropic published on 22 October suggests that is starting to change. Using Claude, the researchers produced machine-checked proofs that programs from 123 open-source libraries will not crash on any input up to a set size, under stated assumptions about the environment the code runs in. Along the way, writing the proofs turned up real bugs that extensive fuzz testing had missed.

Why the bugs matter more than the proofs

Fuzzing throws huge volumes of random input at a program and watches for failures. It is one of the best tools we have, and it still misses things, because random search rarely lands on the exact combination that breaks a rare path. A proof has to account for every path, so the awkward corners surface as the steps that will not go through. The bugs are the evidence that this is not a paper exercise.

Read the small print

A proof is only as strong as what it assumes. These results hold up to a bounded input size, depend on assumptions about the runtime environment, and show that programs do not crash, not that they do the right thing. That is still a meaningful guarantee, but a specific one. When someone tells you code is verified, the useful questions are: verified to do what, for which inputs, assuming what?

What it means for product teams

Most products have a small amount of code where a mistake is expensive: payments and refunds, permissions, pricing rules, data migrations. If the cost of proving properties keeps falling, those paths are the first candidates, alongside the tests you already run rather than instead of them.

• Write the rules down as properties now. 'A refund can never exceed the original charge' is useful to a tester today and to a prover tomorrow.
• Keep critical logic small and separate, so it can be checked on its own.
• Ask suppliers what is tested, what is proven and what is assumed.

We do not expect proofs to replace tests on a typical website or SaaS build any time soon. But the line between research technique and engineering budget is moving, and the parts of a product that handle money and access are where it will cross first.