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.

Source: TokenPost