From tests to proofs: formal verification with LLMs across 123 open source libraries

For a few weeks now, almost every day has brought news of security bugs found with AI, and this very week we had PHP2Shell, discovered with the help of models. If finding bugs has become cheap, the question is what the defence is. Anthropic has published LLMs are making formal software verification feasible at a much larger scale, in collaboration with Theorem, and its answer is ambitious: prove that code is free of certain bugs, instead of hunting for them one by one.

What formal verification is and why almost nobody uses it

Formally verifying a program means translating it into a mathematical model and proving that it always follows some rules, for example, that it never accesses memory out of bounds. If the proof fails, the point where it fails shows where a bug might be. You fix it and try again, until the proof goes through.

The problem is cost. Proofs can be many times larger than the code, and writing them requires a very rare specialisation. The classic example is seL4, an operating system kernel: writing it took two person-years and formally verifying it, twenty. That’s why formal verification has stayed in niches like avionics.

Turning fuzz tests into specifications

The first obstacle is deciding what “correct” means. For a PNG decoder there’s a clear specification, the RFC, but for most programs there isn’t. The project’s trick is to use something that already exists: fuzz tests.

A fuzzer generates millions of semi-random inputs against an entry point in the code, and any input that causes a crash is a bug the authors care about. But it’s brute force: however long it runs, it never guarantees having tried every path. The idea is to turn that test into a specification: “this test doesn’t crash on any input smaller than 64 MB”. If that’s proven, the fuzzer has nothing left to find at that entry point.

flowchart LR
    A["Library and its fuzz test"] --> B["RISC-V binary"]
    B --> C["Specification · never crashes on any input"]
    D["RISC-V and Linux semantics"] --> C
    C --> E["Claude writes the proof"]
    E --> F["Rocq checks the proof"]
    E -->|"bug found"| G["Patch and new specification"]
    G --> C

They did it with projects from OSS-Fuzz, Google’s continuous fuzzing programme for open source projects, which also builds C and C++ code with AddressSanitizer so that any improper memory access causes a crash. So proving the test doesn’t crash also proves a form of memory safety.

And they did it on the compiled binary, not on the source code: the proofs reason about RISC-V instructions, using a formal model of that architecture and of Linux processes.

The numbers

These are huge figures, but the interesting part is that almost none of it needs human review. The Rocq proof checker guarantees that the proof satisfies the specification. The only things you need to trust are the formal models of RISC-V and Linux, the exact statement of what was proven, and Rocq itself. It’s the same principle I mentioned with the NIST curve seeds or with hardware reverse engineering: when the result can be checked objectively, it doesn’t matter how many lines the model wrote.

The bugs found along the way

Attempting the proofs uncovered hundreds of bugs, many of them ones a fuzzer would be unlikely to find, because fuzzers usually work with small inputs, typically up to 1 MB:

• A counter underflow in a decompressor that led to an out-of-bounds write, but only with inputs of about 20 MB with a specific, rare layout.
• An out-of-bounds read in an image decoder that needed a 64 MB input and more than 2 GB of memory.
• An out-of-bounds read that only appeared with a specific sequence of calls across two handles to the same file.
• The rediscovery of a libexpat CVE that needed deeply nested input.
• Logic bugs that never crash, such as a feature to restrict which files an application can load that wasn’t always enforced.

Claude fixed the bug, the specification was regenerated with the fixed code, and it carried on with the proof. There’s an obvious risk, which the report itself acknowledges: the model could “cheat” by rewriting the program so it trivially never crashes. To prevent that, they penalised patches, rewarded proving which inputs each patch changed, and audited every change.

One detail I liked: proving a test doesn’t crash sometimes forces you to prove much more. For cpp-httplib, they had to rule out a stack overflow from recursion in the std::set destructor, so Claude had to prove, on machine code, that libc++’s red-black tree keeps its depth logarithmically bounded.

Other experiments

The report describes other formal verification trials:

• zlib in the Linux kernel: Claude wrote a formal specification of RFC 1950 and proved, on the x86 binary, that the implementation follows it. To do that it also generated the formal semantics of x86, complete enough to boot an Ubuntu userspace, and which along the way found hundreds of mistakes in the official reference documentation.
• A Python interpreter in Rust, proven with Verus against CPython’s semantics. Across 1.7 million random programs, it behaved like CPython in 99.95% of cases.
• A widely used PDF reader, where they found as many security bugs in one week as are usually reported in a year.

The cost, and why it will go down

The big limitation is price: a proof can cost hundreds of millions of tokens. But two trends help:

• Newer models need fewer tokens. On 36 verification tasks taken from OSS-Fuzz, Opus 5.5 proves half of them using about 40% fewer tokens than Opus 5.
• Proofs can be reused. A large part of each proof concerns code every program has, like C runtime initialisation. When agents could copy each other’s proofs, they needed 17% fewer tokens, and some succeeded at proofs they had failed working alone.

Reuse is the long-term key. Just as Mathlib, Lean’s library of formal mathematics, has grown to nearly 300,000 theorems by building on one another, each software dependency would only need to be verified once. Theorem even has a roadmap for verifying the whole Nix ecosystem, including glibc, OpenSSL and cURL.

The limits

The report is honest about what all this does not mean: “formally verified” doesn’t mean “bug-free”. A proof guarantees that the program meets the specification on the machine model used, and reality may differ:

• The model isn’t the real machine. The proofs are about static, single-threaded RISC-V binaries linked against musl. Most people use these libraries on x86 or ARM, dynamically linked against glibc.
• The specification doesn’t cover everything. AddressSanitizer doesn’t detect every memory problem, not every entry point of each library was verified, and a program can misuse a correct library.

The upside is that you know exactly where to look: any remaining bugs will be in the trusted models or outside what was proven.

My takeaway

This seems to me one of the most interesting pieces I’ve read on AI and security, precisely because it isn’t about finding more bugs, but about being able to stop looking for them. And the idea of starting from fuzz tests is very clever: no new specifications need to be written, it builds on what the developers themselves had already decided was a bug.

The report’s conclusion is that formal verification will soon be as practical as fuzzing is today. At current cost, it’s still for critical libraries and well-resourced teams. But if the tokens needed keep falling and proofs are reused across projects, verifying the most widely used dependencies once could change the security of the software we all use a great deal. They’ve published part of the proofs and the formal models so anyone can check them, and Theorem is offering to apply the same process to other open source projects.

Source: LLMs are making formal software verification feasible at a much larger scale, Anthropic and Theorem.