Claude digs up bugs that survived trillions of tests across open-source software

Anthropic says its Claude model has formally verified security properties in 123 open-source software libraries, uncovering hundreds of bugs during the process. Some flaws had escaped detection for years, despite trillions of automated test runs.

The project, conducted with software verification firm Theorem, applies mathematical proofs directly to compiled machine code. Researchers say the approach could make rigorous software verification practical for a much wider range of projects.

The work targets a growing security problem. Automated tools can now discover vulnerabilities in mature software, leaving developers searching for stronger ways to prevent exploitable flaws. Formal verification offers a potential answer by proving that code follows specific rules under defined conditions.

Claude finds hidden bugs

Traditional software testing runs programs against selected inputs to expose failures. Fuzzing tools generate large numbers of unusual inputs, but they cannot exhaust every possible combination.

Anthropic used Claude to turn existing fuzz tests into mathematical specifications. The model then generated proofs showing that 239 program entry points across 123 libraries would not crash under defined conditions.

The researchers worked with RISC-V assembly code, which represents instructions executed by a processor. Claude generated roughly 180 million lines of proof code, with a typical proof spanning about 600,000 lines.

A separate tool called Rocq checked the proofs against their specifications. This independent verification step means developers do not need to manually inspect every line of generated proof code. Anthropic also allowed Claude to patch bugs discovered during verification. The model then generated new proofs for the updated code.

Flaws survived years of testing

The process exposed vulnerabilities that conventional fuzzing might struggle to find. One library contained a counter underflow that could trigger an out-of-bounds write during decompression.

The flaw required an input of roughly 20 MB with a rare arrangement of data. Another bug involved an image decoder that needed a 64 MB input and more than 2 GB of memory to expose its failure.

Claude also found an out-of-bounds read that depended on a particular sequence of operations involving two handles to the same file. In another case, it rediscovered a known vulnerability in the libexpat XML parser.

Not every issue caused a crash. The model also identified a logic flaw that could let an application bypass a feature designed to restrict which files it could load.

These findings suggest formal verification could help uncover defects that routine testing misses. The method can also establish properties that ordinary tests cannot prove across every permitted input.

Proofs have important limits

Anthropic cautioned that formally verified software is not automatically bug-free. The guarantees apply only to specific properties, inputs, and assumptions described in each proof.

The current work covers single-threaded, statically linked RISC-V programs running under a modeled Linux environment. Most deployed systems use other processor architectures or different software configurations.

The specifications also cannot guarantee properties they do not describe. Researchers must ensure their mathematical models accurately represent real processors and operating systems.

Even with these constraints, the project points toward a broader role for formal verification in software development. Anthropic expects better models and reusable proofs to reduce the cost of checking critical software components.

If developers can verify widely shared libraries once and reuse those guarantees, the approach could strengthen security across many applications that depend on them.