Claude Writes 180 Million Lines of Proofs to Verify 123 Open Source Libraries
The notable shift here is not just that an LLM generated proofs, but that it turned an artifact many teams already own—the fuzz harness—into a machine-checkable specification. That creates a plausible adoption path for engineering teams that will never staff formal-methods specialists. The practical question is whether existing fuzz targets are precise enough to serve as security contracts, or whether they mainly encode “doesn’t crash” properties that leave logic flaws, concurrency defects and environment-specific behavior out of scope.
For practitioners, the architectural boundary matters as much as the result. These proofs apply to compiled RISC-V binaries under a modeled Linux environment, which is powerful because it reduces trust in source-level assumptions, but it also narrows portability. Teams running x86_64 or ARM fleets, dynamic linking, glibc, kernel-dependent behavior or multithreaded services should treat this as a verification pipeline pattern, not a directly transferable assurance claim. The first implementation task is mapping where binary-level verification fits alongside CI builds, sanitizer-based testing, SBOM tracking and release gates.
There is also an emerging governance issue: if AI is allowed to patch code in order to complete proofs, review shifts from line-by-line implementation reading to validating specs, trusted models and patch intent. That is a different control framework than most AppSec and platform teams use today. Organizations considering this approach should define up front which proof assumptions are acceptable, what classes of fixes an agent may apply autonomously, and how proof artifacts are retained for audit, regression analysis and dependency reuse.
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.
Enjoyed this article? Sign up for our newsletter to receive regular insights and stay connected.