Claude finds hidden bugs in 123 widely used software libraries

Anthropic says its Claude AI model has formally verified security properties in 123 open-source software libraries. Along the way, it uncovered hundreds of bugs. Some had hidden for years, even though automated tools had run trillions of tests on the code.

What changed

Normal testing feeds a program chosen inputs and watches for failures. Fuzzing goes further by throwing huge numbers of odd inputs at the code. But it cannot try every possible input.

Anthropic worked with a software verification firm called Theorem. Claude turned existing fuzz tests into mathematical specifications, which are precise statements of what the code must never do. It then wrote proofs that 239 entry points across the 123 libraries would not crash under defined conditions.

Those proofs are huge. Claude wrote about 180 million lines of proof code, with a typical proof running about 600,000 lines. A separate tool called Rocq checked them, so people do not have to read every line.

The bugs it found

Several flaws were the kind routine testing struggles to reach.

• A counter underflow in one library could cause an out-of-bounds write during decompression. It needed an input of about 20 MB with a rare data pattern.
• An image decoder failed only with a 64 MB input and more than 2 GB of memory.
• An out-of-bounds read depended on a particular sequence of operations on two handles to the same file.
• A logic flaw could let an application bypass a feature meant to limit which files it could load.

Claude also rediscovered a known vulnerability in the libexpat XML parser. Anthropic let the model patch the bugs it found, then generate new proofs for the fixed code.

Why it matters

Many apps and services lean on the same shared open-source libraries. A flaw in one can touch a lot of products. If a library can be verified once and that proof reused, the protection could reach many programs that depend on it. Anthropic expects better models and reusable proofs to bring the cost down.

The limits

Verified does not mean bug-free. A proof covers only the specific properties, inputs and assumptions it describes. It cannot promise anything the specification leaves out.

The work also covers a narrow setup: single-threaded, statically linked RISC-V programs running under a modeled Linux environment. Most deployed systems use other processor types or configurations. Researchers must also make sure their models match real processors and operating systems.