Claude finds hidden bugs in open-source code using mathematical proofs

Beyond traditional testing

Software developers typically use automated testing to find bugs, which involves running programs against various inputs to see if they fail. A common technique is fuzzing, where tools generate a massive volume of unusual inputs to try and trigger a crash. However, these methods cannot test every possible combination of data or actions.

Anthropic recently demonstrated a more rigorous approach by using its Claude model to perform formal verification. This process involves creating mathematical proofs to show that code follows specific rules under defined conditions. By using math instead of just trial and error, researchers can identify flaws that might remain hidden during trillions of standard test runs.

The project, conducted with the software verification firm Theorem, targeted 123 open-source software libraries. The goal was to see if Claude could turn existing fuzz tests into mathematical specifications. This transition allows the model to prove that specific program entry points will not crash, providing a much higher level of certainty than standard testing.

How Claude generates proofs

To conduct the verification, the team worked with RISC-V assembly code, which consists of the basic instructions executed by a processor. Claude was tasked with generating the proof code necessary to verify these instructions. During the process, the model produced roughly 180 million lines of proof code, with individual proofs often spanning about 600,000 lines.

Because the amount of code is so vast, the researchers did not rely on the AI alone to confirm the results. They used a separate tool called Rocq to check the Claude-generated proofs against their original specifications. This independent verification step ensures that developers do not have to manually inspect every single line of the massive proof output.

The model was also capable of more than just finding errors; it could actively repair them. When Claude identified a bug during the verification process, it was allowed to generate a patch for the code. Once the patch was applied, the model then generated new proofs to confirm that the updated software functioned correctly and safely.

Uncovering hidden vulnerabilities

The formal verification process successfully exposed several vulnerabilities that had escaped detection for years. One library contained a counter underflow that could lead to an out-of-bounds write during decompression. This specific flaw was difficult to find because it required a very specific 20 MB input with a rare arrangement of data.

Other bugs discovered by Claude were even more complex and required significant resources to trigger. One instance involved an image decoder that needed a 64 MB input and more than 2 GB of memory to cause a failure. Claude also identified an out-of-bounds read that occurred only during a specific sequence of operations involving two handles to the same file.

The model even rediscovered a known vulnerability in the libexpat XML parser. Beyond simple crashes, it also identified a logic flaw that could allow an application to bypass a feature meant to restrict file loading. These findings suggest that formal verification can uncover defects that routine testing misses while establishing properties that ordinary tests cannot prove across every permitted input.

Limitations of the current model

Anthropic noted that formally verified software is not automatically free of all bugs. The guarantees provided by these proofs are strictly limited to the specific properties, inputs, and assumptions described in each individual proof. If a property is not described in the mathematical model, the verification cannot guarantee its safety.

The current research focused on single-threaded, statically linked RISC-V programs running in a modeled Linux environment. However, most modern systems use different processor architectures or different software configurations. For these proofs to be useful in the real world, researchers must ensure that the mathematical models accurately represent the actual processors and operating systems being used.

Despite these constraints, the project highlights a path toward making rigorous verification more practical for a broader range of projects. The researchers believe that as models improve, the cost of checking critical software components will decrease. This could allow developers to verify widely shared libraries once and reuse those safety guarantees across many different applications.