Anthropic: Claude has completed large-scale formal verification of the open-source library

On October 22, the Frontier Red Team of the artificial intelligence company Anthropic released research stating that large language models can automatically write formal proofs on a larger scale. The team collaborated with Theorem to use Claude to prove safety properties on over 100 real open-source libraries at the RISC-V assembly level, claiming this is the first known instance of using AI for large-scale formal verification of production software at the assembly level. During the proof-writing process, vulnerabilities that had gone undetected for years were also discovered.

The experiment converted existing compilable fuzz tests from Google OSS-Fuzz into specifications: under assumptions of single-threaded static binaries, fixed memory budgets, RISC-V CPUs, and Linux, for any input less than 64 MB, the program should exit normally without triggering memory safety errors or assertion failures. Within weeks, Claude proved the aforementioned properties for 239 entry points in 123 OSS-Fuzz libraries after patching the identified issues. The proofs targeted compiled RISC-V instructions, approximately 180 million lines of Rocq, and were checked by the Rocq kernel. The page states that this does not mean these libraries are free of vulnerabilities, as remaining issues may lie outside trusted components or the scope of the proofs.

The page also mentions that the team had Claude formalize RFC 1950 and proved that the zlib implementation in the Linux kernel conforms to that specification at the x86 binary level; an interpreter written in Rust covering a large subset of Python showed a 99.95% consistency with CPython behavior across over 1.7 million randomly generated programs. In 36 small verification tasks, Opus 5.5 proved that about half required approximately 40% fewer tokens than Opus 5. The team also pointed out that the proofs targeted single-threaded, statically linked RISC-V binaries, and the proof checker cannot determine whether the specifications align with reality.