Anthropic and Theorem use Claude to formally verify 123 open-source libraries

Anthropic and formal-verification startup Theorem had Claude write mathematical proofs showing that parts of 123 open-source libraries cannot crash under certain conditions. The proofs cover 239 test entry points and work at the level of compiled RISC-V assembly code, checking that programs exit normally without memory-safety errors or failed assertions for inputs under 64MB, assuming a single-threaded static binary on Linux.

The team's method converts existing fuzz tests, which only sample inputs, into formal specifications covering every possible input. According to Anthropic, Claude produced about 180 million lines of proof code in the Rocq proof checker, with a typical proof running to around 600,000 lines for binaries containing a median of 18,000 RISC-V instructions. While writing these proofs, Claude also found and patched real bugs, including a rediscovery of a known vulnerability in the libexpat library, that had not been caught despite years of fuzz testing.

Anthropic is publishing a subset of the proofs along with the RISC-V and OS semantics used to build them, and Theorem is offering to run the same process on other open-source projects and publishing a Claude skill so developers can try it themselves. All performance figures and bug counts in this story come from Anthropic and Theorem.

Why it matters

It suggests formal software verification, long too expensive for most projects, could become a practical way to prove code is free of entire classes of bugs.

Source: Anthropic