Anthropic says Claude formally verified code in 123 open-source libraries

Anthropic says Claude has produced machine-checked security proofs for compiled code across 123 open-source libraries, a scale that could move formal verification beyond a small set of safety-critical systems.

Working with Theorem, the researchers converted existing Google OSS-Fuzz tests into specifications and had Claude write proofs checked by the Rocq kernel. Over several weeks, the system patched bugs it encountered and proved that 239 fuzzing entry points would not crash on any input up to 64 MB. The resulting proofs total roughly 180 million lines.

The attempt also surfaced bugs that conventional fuzzing was unlikely to reach, including memory errors requiring unusually large or specially structured inputs. Anthropic is releasing a subset of the proofs and supporting components for independent inspection and reuse.

The limits matter. The proofs cover single-threaded, statically linked RISC-V binaries running under a specified Linux model, not the common x86 or ARM deployments. They also prove only the properties encoded in the specification and do not cover every entry point or every class of bug. Still, the work suggests AI can reduce the expert labor that has historically made formal verification too expensive for routine software.