Software teams that want mathematical proof their code is safe have long faced a brutal cost barrier. Anthropic’s Frontier Red Team says that barrier just dropped. In research published October 22, 2026, with verification firm Theorem, Claude wrote formal proofs for open-source code at a scale no one had attempted with AI.
What Did Anthropic’s Formal Verification Project Prove?
Claude proved that 239 entry points across 123 open-source libraries never crash on any input under 64 MB. The proofs cover compiled RISC-V assembly, not just source code, and Anthropic calls it the first large-scale AI effort of this kind on production software.
The proofs total about 180 million lines of Rocq. A typical one runs roughly 600,000 lines.
How Does AI Formal Verification Turn Tests into Proofs?
Researchers converted existing fuzz tests from Google’s OSS-Fuzz into specifications stating “this test never fails.” Claude then proved that statement holds for every possible input, which a fuzzer, limited to sampling, cannot do.
|
Method |
Coverage |
Guarantee |
|
Fuzzing |
Samples inputs |
Finds bugs, proves nothing |
|
Claude’s proofs |
Every input under 64 MB |
No crash on that entry point |
A Rocq proof checker validates each proof automatically, so humans do not need to review the millions of lines.
What Bugs Did Claude Find That Fuzzers Missed?
Claude found bugs that need unusually large or oddly structured inputs, which fuzzers rarely produce because they typically cap inputs near 1 MB.
- A decompressor counter underflow triggered only by roughly 20 MB inputs with a rare layout
- An image decoder out-of-bounds read requiring a 64 MB input and over 2 GB of memory
- A rediscovery of CVE-2026-56132 in libexpat
- A PDF reader effort that surfaced as many security bugs in one week as are typically reported in a year
Does “Formally Verified” Mean Bug-Free?
No. Anthropic states plainly that a verified program can still contain bugs if the spec or the assumed machine model differs from reality.
The proofs assume single-threaded, static RISC-V binaries on Linux. Most people run x86 or ARM with dynamic linking. Trust also rests on three components: the RISC-V and Linux models, the theorem statements, and the Rocq checker.
The team also flagged reward hacking, where Claude could “prove” a patched program that trivially never crashes. They penalized broad patches and audited every change.
How Much Does AI Formal Verification Cost?
Still a lot, but falling. Proofs can consume hundreds of millions of tokens. Opus 5.5 completed half of 36 test tasks with about 40% fewer tokens than Opus 5, and agents sharing proofs used 17% fewer tokens than agents working alone.
For context, the seL4 kernel took two person-years to build and 20 to verify.
What Happens Next?
Anthropic is publishing a subset of the proofs and the machine models on GitHub. Theorem offers to run the pipeline on other open-source projects and plans to extend verification across the Nix ecosystem, including glibc, OpenSSL, and cURL.
The takeaway for developers: verification now looks less like a niche academic exercise and more like a testing step that scales with model capability.
