Claude Formally Proves Crash-Freedom Across 123 Open-Source Libraries

Anthropic and Theorem Labs used Claude to formally prove that 239 fuzz-test entry points across 123 open-source libraries never crash on any input under 64 MB, generating roughly 180 million lines of Rocq proofs operating on compiled RISC-V binaries. The proofs were machine-checked by the Rocq proof assistant for correctness. Along the way, Claude discovered bugs that had survived years of fuzzing, including trillions of fuzzing runs, and patched them before completing the proofs. 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. The approach works at the RISC-V assembly level rather than source code, which eliminates the need for a formally verified compiler, though the current scope is limited to single-threaded static binaries. Theorem Labs is launching OSS Verify, a free program where open-source maintainers can enroll their projects to receive crash-freedom proofs or the patches needed to achieve them.