Claude formally verifies 123 open-source libraries

Your AI and this story

Key facts

• Authors (Anthropic Frontier Red Team): Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal, Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich, Nicholas Carlini, Rajashree Agrawal and Jason Gross; collaborator Theorem, which offers to run the pipeline on other open-source projects and published a Claude skill for it
• Main result: no-crash proofs for 239 fuzz entry points in 123 libraries from Google’s OSS-Fuzz, at the level of compiled RISC-V binaries (median ~18,000 instructions), for inputs under 64 MB; assumptions: single-threaded static binaries, fixed memory budget, RISC-V, Linux with musl libc
• Scale: ~180 million lines of Rocq in total, a typical proof ~600,000 lines; proofs can take hundreds of millions of tokens; whole effort ‘a few weeks’ (Anthropic contrasts seL4: ~2 person-years to implement, ~20 to verify)
• Bugs: hundreds surfaced, e.g. a decompressor counter underflow causing an out-of-bounds write only on ~20 MB inputs with one rare layout; an image-decoder out-of-bounds read needing a 64 MB input and 2 GB+ memory; a rediscovery of CVE-2026-56132 in libexpat; a logic bug latent for over a decade; a review of a widely used PDF reader found as many security bugs in one week as are typically reported in a year
• Other case studies: the Linux kernel’s zlib proven against a spec written from RFC 1950 at the x86 binary level; a Claude-written Rust interpreter for a Python subset proven (Verus) to follow CPython semantics, matching CPython on 99.95% of 1.7M random programs
• Model efficiency: on 36 small verification tasks Opus 5.5 needed ~40% fewer tokens than Opus 5 to prove half of them; sharing proofs in a common workspace cut tokens by 17%
• Reward hacking: Claude could make a proof go through by rewriting code so it never crashes; the team penalised patches, required proofs of how much patches changed behaviour, and audited them
• Limitations stated: specs may not match the real machine; RISC-V/musl differs from the x86/ARM, glibc, dynamically linked builds most people run; ASan does not catch every memory-safety bug; dead code and unverified entry points are not covered; callers can still misuse libraries; the trusted base includes Rocq, the RISC-V and Linux semantics, hardware and the OCaml compiler