Claude Used Formal Verification to Prove 123 Open-Source Libraries Won't Crash

Claude Turned Fuzz Tests Into Math

Anthropic just published the most interesting AI-for-code result in a while, and it has nothing to do with autocomplete. Its Frontier Red Team worked with the formal verification startup Theorem to have Claude generate mathematical proofs that 123 open-source libraries will not crash. The total output was roughly 180 million lines of Rocq proof code, produced over a few weeks. To Anthropic's knowledge, this is the first large-scale use of AI for formal verification of production software at the machine-code level.

Formal verification means proving mathematically that software behaves correctly under every possible input. Traditionally it has been brutally expensive: Anthropic notes that the seL4 microkernel took two person-years to build and 20 to verify. That cost is why formal proofs have been reserved for things like aircraft avionics and cryptographic kernels. Claude just collapsed that cost curve.

From Fuzz Tests to Formal Verification

The team started with Google's OSS-Fuzz project, a continuous fuzzing service that throws huge volumes of random inputs at open-source libraries hoping to trigger crashes. Fuzzing is powerful but incomplete: it can only try a sample of possible inputs, never all of them. Claude's job was to convert each fuzz test into a mathematical specification, roughly stating that an entry point never crashes on any input under 64 MB, and then prove that specification against the compiled RISC-V machine code, using Theorem's formal models of the RISC-V processor design and of a Linux process.

The Rocq proof checker then verified each proof mechanically, so almost none of the 180 million lines needed human review. Only the trusted base has to hold: the machine models, the theorem statements, and the checker itself. Over the run, Claude proved 239 test entry points across the 123 libraries.

The Bugs It Found Along the Way

The fun part is what happened before the proofs finished. Failed proof attempts kept pointing at real bugs, and Claude was allowed to patch the code itself, regenerate the specification, and prove the fixed version. The researchers say it surfaced hundreds of bugs that years of conventional testing had missed.

While verifying a widely used PDF reader, the team found as many security bugs in a single week as are typically reported for that software in a whole year. In another library, Claude caught a logical error that had sat undetected for over a decade. This was a big week for AI-found bugs generally: an OpenAI model helped track down the PHP2Shell flaws around the same time, and Anthropic separately said Claude had stripped unneeded code out of OpenSSH.

Why Formal Verification Got Practical Overnight

The headline number, 180 million lines, is less important than the economics. A proof that used to take specialists years can now be generated in days of compute. Anthropic predicts formal verification will soon be as practical as fuzzing is today, which would change how open-source security works. Instead of waiting for a researcher to stumble on a crash, maintainers could ship machine-checked guarantees that whole classes of bugs simply cannot happen.

The same trajectory that took us from autocomplete to agentic coding tools like Meta's open-weight Muse Spark and Recursive's Flint is now reaching into correctness itself. Writing the code was step one. Proving it is step two.

The Fine Print

There is precedent for skepticism here, and Anthropic published its own limitations section, which is to its credit. The proofs only hold under narrow conditions: single-threaded programs, statically linked binaries, fixed memory budgets, RISC-V CPUs, Linux environments. Your laptop is x86 or ARM and your software is multithreaded, so these particular proofs do not cover the machines most of us actually run. They also do not imply the libraries are entirely bug-free; issues can still hide in the trusted components or outside the scope of what was proved.

The compute cost is steep too. Individual proofs can burn hundreds of millions of tokens. A smaller test showed the newer Opus 5.5 model completing half its verification tasks with about 40 percent fewer tokens than Opus 5, so the economics are improving fast, but nobody is verifying an entire operating system this way yet.

Theorem is already offering to run the pipeline for other open-source projects and has released a Claude skill for it. If the cost curve keeps bending the way the last two model generations suggest, the question for maintainers will shift from "should we formally verify this" to "why didn't we." And the bugs that fuzzers cannot reach, the ones hiding behind rare 20 MB input layouts and decade-old logic errors, may finally have nowhere left to hide.