Claude Writes 180 Million Lines of Proofs to Verify 123 Open Source Libraries

Formal verification has long been the gold standard for software correctness. It has also been too expensive for almost everyone. New research from Anthropic suggests that’s changing.

Anthropic’s Frontier Red Team, working with formal methods company Theorem, used Claude to prove security properties in the compiled code of 123 open-source libraries from Google’s OSS-Fuzz project. The work covered 239 fuzzing entry points, and the proofs operate on RISC-V assembly, not source code. Anthropic says it’s the first large-scale effort to use AI to formally verify production software at that level.

And along the way, Claude found bugs that years of continuous fuzzing had missed.

The idea behind formal verification is simple. You build a mathematical model of your code and prove it always follows a defined set of rules. If a proof attempt fails, there may be a bug, or the proof may simply be incomplete. Fix it, try again, and eventually you have proof that no bug of that type exists.

The practice is not simple. Proofs are often far larger than the code they cover, and writing them takes a rare skill set. Anthropic points to the seL4 microkernel: two person-years to build, 20 person-years to verify. That math is why verification has mostly lived in places like avionics.

The hardest part is often defining what “correct” means. Anthropic and Theorem sidestepped that by using tests developers had already written.

OSS-Fuzz entry points crash when something goes wrong, such as a memory error caught by AddressSanitizer or a failed assertion. A fuzzer throws huge numbers of semi-random inputs at them. But it’s brute force. No fuzzer can try every input.

So the team turned each fuzz test into a formal spec: the compiled test will not crash on any input under 64 MB within the modeled environment. Theorem provided formal models of the RISC-V instruction set and Linux process behavior. Claude wrote the proofs. The Rocq proof checker validated them.

Over a few weeks, Claude produced about 180 million lines of Rocq. A typical proof ran about 600,000 lines for a binary with a median of 18,000 instructions. Nobody has to review that by hand. The checker confirms the proof satisfies the spec. Developers must trust a short list: the RISC-V and Linux models, the theorem statements, and Rocq itself.

Claude was allowed to patch bugs it hit and keep going. The effort surfaced hundreds of them.

Several show where fuzzing hits its limits. Fuzzers usually work with small inputs, often capped at 1 MB. Claude found a counter underflow in a decompressor that caused an out-of-bounds write, but only on inputs of roughly 20 MB with one rare layout. It found an out-of-bounds read in an image decoder that needed a 64 MB input and more than 2 GB of memory.

Letting an AI patch code to pass a proof carries a risk. It could rewrite a program into something that trivially never crashes. Anthropic says it penalized patches, rewarded minimal changes, and audited them for that kind of shortcut.

Mitch Ashley, vice president and practice lead for CIO & Technology Buyers and Software Lifecycle Engineering at The Futurum Group, says that’s where human attention belongs now.

“AI writes code faster than teams can review it, and machine-checked proofs change what people must review,” Ashley says. “The job shifts from reading output to checking the spec, the trusted models, and every patch the agent made to get a proof through.”

Cost is the main constraint. Proofs can take hundreds of millions of tokens, but Anthropic expects that to fall. On 36 small verification tasks, Claude Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5. And agents that shared a workspace and reused each other’s proofs needed 17% fewer tokens. These are Anthropic’s own benchmarks.

Reuse may be the bigger idea. Much of any proof covers code every C program shares, like runtime initialization, so proofs transfer well between projects. Dependencies also follow a power law. Verify a small set of widely used libraries once, and much of the software stack gets easier to prove.

Anthropic released a subset of the proofs, plus the RISC-V and OS semantics, on GitHub for anyone to check. Theorem is offering to run the pipeline for other open-source projects and has published a Claude skill to help developers start.

Anthropic is clear that “formally verified” doesn’t mean “bug-free.” The proofs assume single-threaded, statically linked RISC-V binaries using musl libc. Many deployed Linux applications run on x86 or ARM and dynamically link against glibc. AddressSanitizer doesn’t catch every memory safety bug, and the team didn’t verify every library entry point.

Ashley says the next tests are practical ones.

“Fuzzing was built for human-written code at human speed,” he says. “Watch whether these proofs reach multithreaded x86 and ARM binaries built on glibc, and whether token costs fall to a level a platform team can budget for each release.”

The near-term takeaway isn’t to drop fuzzing. Expect verification to move toward the pipeline. Anthropic predicts formal verification will soon be about as practical as fuzzing is today for most production software. That’s a vendor forecast, not a guarantee.

But the pressure is real. AI keeps getting better at finding bugs and chaining them into exploits. Testing shows bugs exist. Proofs show certain bugs don’t. And the fuzz tests many DevOps teams already maintain could become their first specs.