Anthropic published research today showing that Claude formally verified security properties in 123 open-source libraries at the compiled assembly level. The company calls it the first large-scale effort to apply AI-driven formal verification to production software at this depth.
The work was a collaboration between Anthropic's Frontier Red Team and Theorem Labs, a San Francisco startup founded in 2025 by Jason Gross and Rajashree Agrawal. Both appear on the research's author list, alongside security researchers including Keane Lucas, Chris Rohlf, Nicholas Carlini, and Nickolai Zeldovich.
The scale of the proofs
Claude proved that 239 entry points across 123 different OSS-Fuzz libraries will never crash on any input up to 64 MB. The proofs run on compiled RISC-V binaries rather than source code, which means the verification covers what the processor actually executes. Each proof averages about 600,000 lines. The total comes to roughly 180 million lines of Rocq, the proof assistant formerly known as Coq.
Traditional formal verification of this scale would require years of expert effort. According to Anthropic, the work here took a few weeks.
Bugs found along the way
Attempting to construct proofs forced Claude to reason about edge cases that fuzzers rarely reach. The model discovered bugs that had survived years of continuous fuzzing and, in some cases, trillions of test runs. Claude patched those bugs before proving the code crash-free.
"We need ways to prove that code is free of bugs," the research states. Conventional testing produces findings but not guarantees; formal verification produces a mathematical proof that code satisfies a stated property.
What the proofs assume
The current work operates under specific constraints. The proofs assume programs run as single-threaded static binaries with a fixed memory budget on RISC-V hardware using Linux. Anthropic says expanding to other architectures and operating systems is within reach, but would require formalizing additional instruction semantics and process models.
A proof is also only as strong as its specification. Formal verification shows that code meets a stated property. Any gap in that specification remains a gap in the guarantee.
Theorem Labs and the verification toolchain
Theorem Labs builds tools to formally verify AI-generated code before deployment. The company emerged from Y Combinator's Spring 2025 batch. Its core technology, which it calls fractional proof decomposition, allocates verification effort proportionally to the risk of each code component rather than exhaustively checking every path.
For this project, Theorem provided the formal models of RISC-V instructions and Linux process semantics that let the proofs operate at the assembly level. Claude used those models to translate compiled code into mathematical form and construct the proofs.
The collaboration suggests Anthropic views formal verification as both a research capability and a tooling problem. Whether this work becomes standard infrastructure will depend on reproducibility. Anthropic has released the proofs, but the framework's complexity may limit near-term adoption outside well-resourced teams.
Context: Anthropic's defensive security push
The verification project sits inside a broader Anthropic effort on open-source security. Earlier this month, the company launched OSS Scanner, an opt-in vulnerability-finding service for open-source maintainers. Claude's earlier security work has flagged thousands of potential bugs, including vulnerabilities that survived decades of human review. Mozilla credited the Frontier Red Team with surfacing more than a dozen bugs in Firefox ahead of the recently shipped version 148.
The Frontier Red Team reports to Anthropic's policy division, led by cofounder Jack Clark, rather than to the technical safety group. That placement gives the team an explicit mandate to publish findings, a structure unusual among AI labs.
The next step, according to the research, is expanding the scope of what can be proved. More architectures, more operating systems, more specifications. For now, 180 million lines of machine-checked proof code represents a benchmark that did not exist a year ago.
