From Mexico, I’ve always treated fuzzing as the best we can do: throw millions of random inputs at a parser and hope the bad one shows up. On October 22, Anthropic and the verification company Theorem published a study that goes further. They say Claude wrote machine-checked proofs that 239 fuzz entry points across 123 open-source libraries from Google’s OSS-Fuzz project can’t crash, for every input under 64 MB, after patching the bugs it found along the way.
What they actually proved
Here “crash” means a memory-safety error caught by AddressSanitizer or a failed assertion. The team took existing OSS-Fuzz tests and turned each one into a formal statement about the compiled RISC-V binary, using Theorem’s models of the RISC-V instruction set and a Linux process. Claude then wrote the proofs in Rocq, and Rocq’s small kernel checks them. You don’t have to trust the AI’s reasoning, only the machine and OS models, the theorem statements and the checker (plus the hardware and software the checker itself runs on).
The scale is the striking part. Anthropic says the work took a few weeks and produced about 180 million lines of Rocq, with a typical proof around 600,000 lines for a binary with a median of about 18,000 instructions.
What it found on the way
A proof can’t go through while a bug is still there, so the process works as a bug hunt. Anthropic says it surfaced hundreds of bugs. Its examples include a counter underflow that leads to an out-of-bounds write on inputs around 20 MB, an out-of-bounds read in an image decoder that needs a 64 MB input and more than 2 GB of memory, an out-of-bounds read that needs a particular sequence of calls across two handles to the same file, and a rediscovered libexpat CVE. Huge, oddly shaped inputs like these are the kind random fuzzing rarely gets to.
The post also covers side experiments: zlib inside the Linux kernel proved against the RFC 1950 spec at the x86 binary level, and a Python interpreter written in Rust and proved with Verus that matched CPython’s behavior on 99.95% of 1.7 million random programs. Theorem has put an OSS Verify enrollment repo on GitHub for maintainers of established open-source projects that already have fuzz targets.
The fine print
Anthropic’s own limitations section opens with the line that matters most: “formally verified” doesn’t mean “bug-free.” The proofs cover single-threaded, statically linked RISC-V binaries built against musl, while most of us run x86 or ARM with glibc. AddressSanitizer doesn’t catch every memory bug, even verifying every entry point wouldn’t cover everything, and a caller can still misuse a library. Anthropic also notes that letting the model patch code opens the door to reward hacking, so patches were penalized and audited.
The independent write-ups add more. The Decoder points out that the tools and formal foundations were built by people at Theorem, and that Anthropic doesn’t report what the whole project cost. Anthropic itself says a proof can take hundreds of millions of tokens. XenoSpectrum stresses that the proofs only cover what the fuzz tests check, not the whole library, and don’t guarantee the code terminates. Almost every number here comes from Anthropic.
My take
I don’t read this as “AI made software safe.” I read it as a cost curve moving. Formal proofs used to be something only a few teams could afford for a few critical components. If a model can write them and a small, boring checker can confirm them, the expensive part shifts to writing the right spec and trusting the models underneath. That’s where I’d put my attention as an engineer.
For everyday work, the practical lesson is that good fuzz targets are now worth more than before, because they can become specs. If you maintain a parser or a decoder, I’d make sure your fuzz harnesses are clean and meaningful. Just don’t take “proved” to mean your production build on a different CPU and libc is covered. It isn’t, yet.
Featured image: “Plumb bob with string 1” by Salil Kumar Mukherjee, Wikimedia Commons, CC BY-SA 4.0. Cropped, resized to 1400×900 and lightly sharpened; the modified image is shared under the same license.
