Anthropic and Theorem used Claude to prove security properties in compiled code of 123 open-source libraries. Claude found and fixed bugs that had evaded detection for years. The proofs cover 239 entry points across these libraries. Each proof operates on RISC-V assembly code under specific assumptions. The proofs total about 180 million lines of Rocq code. A typical proof is around 600,000 lines long. The work assumes single-threaded static binaries with fixed memory on Linux. The trusted components include RISC-V and Linux process models. The proofs do not guarantee the absence of all bugs. The process also discovered hundreds of bugs during attempts. Some bugs required inputs of 20 MB or more to trigger. Others involved rare memory layouts or specific call sequences. The team published a subset of the proofs for public verification.
What changed
Formal verification required years of expert effort and was impractical for most real-world projects.
What it unlocks
Proving security properties at the assembly code level for production software using LLMs.
- 123 open-source libraries
- 239 entry points proved
- 180M lines of Rocq proof code
- 600,000 lines per typical proof
What you need to act on it
- RISC-V CPU
- Linux OS
- single-threaded static binary
- fixed memory budget
- inputs under 64 MB
Sources