Anthropic: Claude wrote machine-checked proofs for compiled code of 123 open-source libraries

Anthropic has published research in which its Frontier Red Team, together with the formal-methods company Theorem, used Claude to formally verify security properties of 123 open-source libraries from Google’s OSS-Fuzz project, covering 239 fuzzing entry points. Notably, the proofs work on compiled RISC-V machine code, not on source code.

How it worked

Each existing fuzz test was turned into a formal specification: the compiled test must not crash (for example, with a memory error caught by AddressSanitizer or a failed assertion) on any input under 64 MB in a modelled environment. Theorem supplied formal models of the RISC-V instruction set and Linux process behaviour; Claude wrote the proofs and the Rocq proof checker validated them. According to DevOps.com, Claude produced about 180 million lines of proofs over a few weeks.

Bugs fuzzing missed

Claude was allowed to patch bugs it hit, and the effort surfaced hundreds of them. Examples cited include a counter underflow in a decompressor that only caused an out-of-bounds write on inputs of roughly 20 MB, and an image-decoder read error that needed a 64 MB input. Anthropic says it penalised large patches and audited them so the model could not simply rewrite programs into something that trivially never crashes.

Limits

Anthropic stresses that “formally verified” does not mean “bug-free”. The proofs assume single-threaded, statically linked RISC-V binaries using musl libc, while most deployed Linux software runs on x86 or ARM with glibc; AddressSanitizer does not catch every memory bug, and not every entry point was verified. Cost is another constraint: proofs can consume hundreds of millions of tokens. Efficiency gains reported for newer Claude models come from Anthropic’s own benchmarks. A subset of proofs has been released on GitHub.