Anthropic and Theorem used Claude to write machine-checked proofs that 239 fuzz-test entry points across 123 open-source libraries in Google’s OSS-Fuzz can’t crash, for any input under 64 MB. That’s about 180 million lines of Rocq proofs, checked by the Rocq proof checker, not by a human.
The highlights
- The trick: take a fuzz test, which only tries lots of random inputs, and turn it into a spec that says “this never crashes for any input.” Then have Claude prove it.
- Along the way Claude found and patched bugs fuzzers would likely never hit, like an out-of-bounds write in a decompressor that only showed up on about 20 MB inputs with one rare layout.
- They also proved the Linux kernel’s zlib matches the RFC 1950 spec at the x86 binary level, and found as many security bugs in a PDF reader in one week as normally get reported in a year.
- Opus 5.5 proves the same tasks with about 40% fewer tokens than Opus 5, and agents sharing a proof workspace used 17% fewer tokens.
The fine print
Anthropic is upfront about it: “formally verified” doesn’t mean “bug-free.” These proofs cover single-threaded, static RISC-V binaries linked against musl. Most of us run this stuff on x86 or ARM with glibc. Only some entry points per library were covered, and only part of the proofs are public.
My take
This is the good side of AI and security. Attackers are using agents to find bugs faster, so defenders need ways to prove code is safe, not just test it. Proofs used to cost years of expert time. If that cost keeps falling, the libraries the whole internet sits on could actually get proven. I’m watching Theorem’s plan for the Nix ecosystem (glibc, OpenSSL, cURL) closely.
Have a blessed day! And Happy Hacking!
