Anthropic says Claude wrote crash-free proofs for 123 open-source libraries

Anthropic's Frontier Red Team, working with Theorem, says Claude proved that 239 fuzz-test entry points across 123 libraries in Google's OSS-Fuzz never crash on any input up to 64 MB, after patching bugs it found along the way. The proofs, about 180 million lines checked by the Rocq proof checker, hold only under set assumptions: a single-threaded static binary on a RISC-V CPU running Linux, while most people run these libraries on x86 or ARM. Anthropic says the attempt surfaced hundreds of bugs, many of which a fuzzer would be unlikely to find, and that Opus 5.5 proved half of 36 small verification tasks with about 40% fewer tokens than Opus 5. It is publishing a subset of the proofs, and Theorem is offering to run the same pipeline for other open-source projects and publishing a Claude skill to help developers start.