Claude's formal verification of open-source libraries

Anthropic's Frontier Red Team, working with Theorem Labs, used Claude to generate machine-checked formal proofs covering 239 entry points across 123 open-source libraries, proving crash-freedom for any input under 64 MB. The proofs operate at the compiled RISC-V assembly level, translating binaries into a mathematical model using Theorem's RISC-V instruction and Linux process semantics, with Claude writing the proofs in the Rocq proof assistant for kernel-checking. A typical proof spans about 600,000 lines of Rocq for binaries with a median length of 18,000 RISC-V instructions. The work was completed in a few weeks. Anthropic claims this is the first large-scale effort to use AI for formal verification of production software at the assembly code level. While generating proofs, Claude found bugs that had survived trillions of fuzzing runs. Anthropic's Frontier Red Team also separately used Claude to find 493 security issues across 25 open-source codebases. The current scope is limited to single-threaded static RISC-V binaries. Theorem Labs launched OSS Verify, a free opt-in program for open-source maintainers to receive crash-freedom proofs or the patches their projects need to achieve them.