Anthropic Uses Claude to Prove No-Crash Rules Across 123 Libraries

Anthropic and Theorem used Claude to produce formal proofs for no-crash behavior at 239 software-library entry points, examining a limited property under strict assumptions rather than establishing that the libraries are bug-free.

The work, completed over a few weeks, covered 123 open-source libraries in OSS-Fuzz. The proofs applied to inputs smaller than 64 megabytes and assumed each program ran as a single-threaded static binary with a fixed memory budget on RISC-V hardware. Linux behavior was modeled.

The project generated about 180 million lines of Rocq proof code. A typical proof contained about 600,000 lines, while the median binary measured 18,000 RISC-V instructions.

The results apply only to the specified no-crash properties under the project’s assumptions. They do not show that the libraries are free of every bug. The work examined open-source libraries, not blockchain networks or smart contracts.