Top stories

Anthropic and formal-verification company Theorem used Claude to generate machine-checkable proofs for security properties in open-source software at the RISC-V assembly level. Over several weeks, Claude patched bugs and proved that 239 OSS-Fuzz entry points across 123 libraries would not crash for any input below 64 MB, under assumptions including a single-threaded static RISC-V binary, Linux, and a fixed memory budget. The proofs cover normal exits without assertion failures or modeled memory-safety errors, rather than proving that the libraries are entirely bug-free. The effort produced roughly 180 million lines of Rocq proof code, with a typical proof about 600,000 lines for a binary containing a median 18,000 RISC-V instructions. Claude found hundreds of bugs while attempting the proofs, including out-of-bounds reads and writes requiring unusual or large inputs, a rediscovery of CVE-2026-56132 in libexpat, and a logic flaw in a file-loading restriction feature. Anthropic is publishing a subset of the proofs, relevant RISC-V and Linux semantics, and specifications that it could not prove; Theorem plans to offer the pipeline for other open-source projects. The guarantees depend on the correctness and scope of the formal specification, processor and operating-system models, and the Rocq proof checker. The current proofs do not model common deployments such as x86 or ARM systems with dynamically linked glibc, and AddressSanitizer-based fuzz targets do not capture every possible vulnerability.