Anthropic’s artwork for its formal verification research. Image: Anthropic
Anthropic says Claude can now do something that used to take experts years: write mathematical proofs that real software won’t crash. In research published on Thursday, its Frontier Red Team and the formal verification start-up Theorem say Claude proved that 239 test entry points across 123 open-source libraries will never crash on any input under 64 MB, and found and patched hundreds of bugs along the way.
It lands in a week of AI-found bugs: an OpenAI model helped find the PHP2Shell flaws, and on Tuesday Anthropic said Claude had stripped unneeded code out of OpenSSH. Now Anthropic argues that “we need ways to prove that code is free of bugs.”
From fuzz tests to proofs #
Formal verification means proving mathematically that code always follows a set of rules, with a computer checking every step. It has stayed rare because it is slow: Anthropic notes the seL4 kernel took two person-years to build and 20 to verify.
The team started with Google’s OSS-Fuzz, whose “fuzz tests” throw huge numbers of random inputs at an entry point developers wrote for testing, hoping one causes a crash. Fuzzing can never try every input. Claude instead turned each fuzz test into a specification (the test never crashes on any input under 64 MB) and proved it against the compiled RISC-V machine code, using Theorem’s formal models of the RISC-V chip design and of a Linux process. The Rocq proof checker then confirms each proof mechanically.
Over a few weeks the finished proofs came to about 180 million lines of Rocq, with a typical proof running to about 600,000 lines for a program with a median of 18,000 RISC-V instructions. The appendix says Claude wrote around one billion lines in all. Anthropic says “virtually none of it needs to be manually reviewed”, because only the machine models, the theorem statements and the checker itself have to be trusted.
Bugs a fuzzer would probably never hit #
When a proof wouldn’t go through, the reason was often a real bug, and Claude was allowed to patch the code and carry on. Anthropic says the attempts turned up hundreds of bugs. Fuzzers usually cap inputs at about 1 MB, but Claude found a counter underflow in a decompressor that caused an out-of-bounds write only on inputs of around 20 MB with one rare layout, and an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory. It also rediscovered CVE-2026-56132 in libexpat and noticed that one library didn’t always enforce a feature meant to limit which files an app can load.
To stop Claude cheating by rewriting a program so that it trivially never crashes, a form of reward hacking, the team penalised patches and audited them. Anyone can check some of it: Theorem’s public repository holds proofs for 60 entry points in 25 libraries, including bzip2, cJSON and json-c. Proofs that could reveal unpatched bugs are held back.
Zlib, Python and a PDF reader #
Claude also wrote a formal specification of RFC 1950, the zlib compression format, and proved the Linux kernel’s zlib code meets it, on the x86 binary, using x86 models it generated itself. Half a dozen other libraries turned up only minor, unexploitable bugs.
It built a Python interpreter in Rust and proved with the Verus tool that it follows a formal model of Python; on 1.7 million random programs it matched CPython 99.95% of the time. When the team planted seven bugs in an early version, five slipped past random testing and all seven broke the proof. Anthropic also says an effort on an unnamed, widely used PDF reader found “as many security bugs in one week as are typically reported in a year”, and that elsewhere it found a logic bug that had sat unnoticed for more than a decade. Those claims come from Anthropic alone.
Cheaper proofs, clear limits #
The big cost is compute: Anthropic says proofs can take hundreds of millions of tokens. On 36 small verification tasks built from OSS-Fuzz code, Claude Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5.
“‘Formally verified’ does not mean ‘bug-free’,” Anthropic writes. The proofs cover single-threaded RISC-V programs; most people run these libraries on x86 or Arm. Not every entry point was proved, and an expert’s notes in the appendix warn Claude’s wordy proofs may hit “a complexity wall” on bigger programs.
Why it matters #
AI is making bugs cheaper to find for attackers as well as defenders, as Anthropic’s own warning that a downloadable model can now build working hacks showed. A machine-checked proof that a whole class of crash can’t happen is a far stronger defence than patching flaws one by one, and if costs keep falling Anthropic expects verification to become as routine as fuzzing.
Sources: Anthropic, “LLMs are making formal software verification feasible at a much larger scale” and appendix (PDF); Theorem, oss-verify-proofs (GitHub).