Research #Anthropic #Coding agents Oct 24, 2026 · Originally published Oct 22

Claude proves 239 entry points across 123 open-source libraries won't crash on any input up to 64 MB, at the RISC-V assembly level

Working with Theorem, Anthropic turned open-source libraries' existing fuzz tests into formal specs and had Claude write the proofs. The scale, the bugs found along the way, and the cost.

Primary source Anthropic Research · anthropic.com Read the original ↗

// Key points

The method turns developer-written OSS-Fuzz entry points into a spec over the compiled RISC-V instructions: this test never crashes on any input. Once proved, fuzzing that entry point can never find a bug.
Claude patched the bugs it hit along the way and proved no crashes on any input up to 64 MB for 239 entry points across 123 libraries. Attempting the proofs surfaced hundreds of bugs, among them an out-of-bounds write triggered only by inputs of around 20 MB with one specific layout.
While verifying a widely used PDF reader, the team found as many security bugs in one week as are typically reported in a year, and a logic bug that had been latent for more than a decade.
The main limit is cost: a proof can take hundreds of millions of tokens. Theorem is offering to run the same pipeline for other open-source projects and has published a subset of the proofs.

Builder's takeAt hundreds of millions of tokens a proof, this isn't something every team can afford yet. The idea is worth copying now, though: treat existing tests as the spec and have an agent prove they always pass, or at least push hard on edge-case inputs. I'd start with the code that parses uploaded files, like the PDF and image handling in an AI cloud drive, since that's what oversized or malformed files break first.

// Background · from #Anthropic

Full timeline →