What happened

Anthropic said it used its Claude model, together with software verification firm Theorem, to formally verify 123 open-source libraries. The project produced mathematical proofs for 239 program entry points and uncovered hundreds of bugs.

What formal verification means

Traditional testing runs a program against selected inputs, and fuzzing tools generate many unusual inputs, but neither can exhaust every possible combination. Formal verification instead tries to prove mathematically that code follows specific rules under defined conditions. Anthropic used Claude to turn existing fuzz tests into mathematical specifications; the model then generated proofs showing those entry points would not crash under defined conditions.

Notable findings

  • One library contained a counter underflow that could trigger an out-of-bounds write during decompression; triggering it required roughly a 20 MB input with a rare data arrangement.
  • An image decoder bug needed a 64 MB input and more than 2 GB of memory to surface.
  • An out-of-bounds read depended on a particular sequence of operations involving two handles to the same file.
  • A known vulnerability in the libexpat XML parser was rediscovered.
  • A logic flaw could let an application bypass a feature restricting which files it could load.

Limits of the proofs

Anthropic cautioned that formally verified software is not automatically bug-free. The guarantees apply only to the properties, inputs and assumptions described in each proof. The current work covers single-threaded, statically linked RISC-V programs running in a modeled Linux environment; most deployed systems use other architectures or configurations. Researchers must ensure their mathematical models accurately represent real processors and operating systems.

Why it matters

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, so developers do not need to manually inspect every line. Anthropic expects better models and reusable proofs to lower the cost of verifying critical software components.