Anthropic Uses Claude to Verify 123 Open Source Libraries

In a research post, Anthropic says it worked with Theorem to use Claude for formal verification of software at the assembly code level. Claude produced proofs for 239 test entry points across 123 open source libraries.

The proofs show that the tested programs will not crash or trigger memory safety errors for inputs under 64 MB within defined conditions. Those conditions include a static binary with one execution thread, a fixed memory budget, a RISC-V processor and Linux. The project generated about 180 million lines of proof code in Rocq, which checks whether each proof satisfies its stated specification.

Claude also found and patched hundreds of bugs while attempting the proofs. Examples included an out of bounds write that required an input of about 20 MB with a rare layout, an out of bounds read requiring a 64 MB input, and logic errors that did not cause crashes. Anthropic is publishing a subset of the proofs, specifications and formal models, while Theorem is offering the verification pipeline to other open source projects.