Claude formally verifies 123 software libraries and uncovers hundreds of bugs

Anthropic and Theorem use Claude to produce formal proofs across 123 open-source libraries and detect bugs that escape testing.

Billions of tests cannot always guarantee that a program will behave correctly. Some defects require combinations of events so rare that years of automated testing may never encounter them. Anthropic and formal verification company Theorem have used Claude to generate mathematical proofs for 239 test entry points across 123 open-source libraries, establishing that certain crashes cannot occur under precisely defined conditions. The project involved multiple agents working over several weeks, generated approximately 180 million lines of formal proof code, and uncovered hundreds of bugs, including defects that had survived trillions of test executions. Why Testing Cannot Find Every Bug

Software quality assurance relies heavily on executing tests. Developers define scenarios, inspect results, and try to trigger unexpected behavior. Fuzzing extends this process by automatically supplying programs with large numbers of randomly generated or mutated inputs. The technique is widely used by OSS-Fuzz, Google's continuous vulnerability-detection project for open-source software.

Fuzzing can reveal memory errors, crashes, and violations of properties defined by developers. Its effectiveness, however, depends on the inputs generated and the execution paths they reach. Even billions of test cases cannot guarantee that a particular combination of data capable of triggering a failure has been explored.

Formal verification approaches the problem differently. It represents a program's behavior and selected requirements mathematically, then attempts to prove that the requirements hold across all situations covered by the model. Instead of checking a finite collection of examples, it establishes a property over an entire class of inputs.

The technique has existed for decades, but implementing it requires considerable expertise. Anthropic points to the seL4 operating system kernel, which reportedly required approximately two person-years to develop and twenty person-years to formally verify. Proofs can be much larger than the programs they describe, limiting their use to systems where security requirements justify exceptional investment. Turning Existing Tests Into Mathematical Specifications

To avoid manually writing comprehensive specifications for every library, the researchers reused fuzz tests already maintained by developers. Each test defines an entry point: a portion of the program that receives data and triggers an error when an important property is violated.

Anthropic and Theorem converted those tests into formal specifications. In their principal setup, the objective was to prove that a compiled program cannot crash for any input smaller than 64 MB, across every input and operating-system response covered by the model. The guarantees include certain memory-access errors detected by AddressSanitizer and assertions embedded in the tests.

The process operates on compiled RISC-V machine instructions, rather than source code alone. Libraries and their fuzz tests are compiled into executables, then translated into mathematical representations using execution semantics developed by Theorem. Claude receives that representation, the properties to establish, and the tools required to build the proof.

This allows the researchers to examine compiled software without rewriting entire libraries in languages specifically designed for verification. Proofs are written in Rocq, formerly Coq, a proof assistant that mechanically checks whether individual steps satisfy the required logical rules. 180 Million Lines of Machine-Checked Proofs

The project covers 239 entry points across 123 libraries included in OSS-Fuzz. Anthropic reports approximately 180 million lines of Rocq proofs, generated over several weeks. A typical proof contains about 600,000 lines and concerns a binary whose median size is 18,000 RISC-V instructions.

Despite that volume, the proofs do not require line-by-line human review. Claude generates the proofs, while Rocq's checking kernel determines whether they establish the stated properties. This separates the generative model's ability to produce extensive reasoning from the formal system responsible for validating its logical correctness.

The guarantees still depend on trusted components: the exact mathematical specifications, the models of the processor and operating system, and the Rocq proof checker. An accepted proof shows that the program satisfies the defined property within the modeled environment, not that every possible defect has disappeared.

Anthropic is releasing a subset of the proofs and supporting components so they can be independently checked and reused. Materials that could reveal unpatched vulnerabilities are being withheld. Theorem is also offering its verification pipeline to additional open-source projects. Bugs Hidden in Extremely Unusual Inputs

Constructing the proofs exposed failures in the underlying software. When an agent could not establish that a program would never crash, it could investigate the conditions responsible, identify the defect, and propose a patch. The specification would then be regenerated from the modified code before another proof attempt.

One documented example involves a decompressor whose counter could underflow and cause an out-of-bounds write. Triggering the bug required approximately 20 MB of input with a particularly unusual layout. Another defect, in an image decoder, required a 64 MB input and more than 2 GB of memory. Conventional fuzzing campaigns, which often limit inputs to much smaller sizes, would be unlikely to encounter those conditions.

Claude also identified a defect requiring a particular sequence of operations involving two handles to the same file, and rediscovered CVE-2026-56132 in the libexpat XML library. Some findings did not involve crashes at all. In one case, a feature designed to restrict which files an application could access did not consistently enforce its intended limitation.

These examples show why attempting a proof can be