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

By Simon Yoon

Canonical URL: https://www.tokenpost.com/news/technology/39863
Published: 2026-10-24T10:34:54.000Z
Updated: 2026-10-24T10:34:54.000Z
Section: Technology

> The project covered 239 fuzz-test entry points and inputs under 64 MB, with proofs based on a defined hardware and software model.

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.