This week: Anthropic says Claude wrote machine-checked proofs that over a hundred open-source libraries won't crash on huge ranges of inputs, and found old bugs along the way.

Elsewhere: What a "proof" actually covers here, the fine print Anthropic spells out itself, and how open-source maintainers can sign up for free.

The New Prime Signal

Most software gets checked the way you check a parachute you bought online: you try it a bunch of times and hope the next time goes the same way. Fuzzers, tools that hurl millions of random inputs at code to see what breaks, are great at this, but they can never try everything. Anthropic's new research post argues that AI can now do the slower, stricter thing: write a mathematical proof that a program behaves, for every input in a defined range. Historically that was so expensive almost nobody bothered. In the post's example, "it took two person-years to implement the seL4 operating system kernel, but 20 person-years to formally verify it."

What happened: On October 22, Anthropic's Frontier Red Team, working with the formal verification company Theorem, published results from using Claude to write formal proofs about real open-source code. Starting from fuzz tests in Google's OSS-Fuzz program, Claude "successfully patched the bugs it found and then proved that there are no crashes on any input (up to 64 MB) for 239 entry points across 123 different OSS-Fuzz libraries." The proofs work on the compiled RISC-V machine code, not the source, and "comprise about 180 million lines of Rocq, with a typical proof running to about 600,000 lines." Nobody reads all that by hand. A program called the Rocq proof checker does, and Anthropic says the only things you need to trust are its models of RISC-V and Linux, the exact theorem statements, and the checker itself.

Why it matters: AI is getting better at finding bugs, and attackers know it. The post notes the Linux kernel "recently had over 1,000 vulnerabilities disclosed." Proofs flip the game from "find the next bug" to "show there isn't one of this kind." The side effect was arguably the best part: the proof attempts "discovered hundreds of bugs," including an out-of-bounds write in a decompressor that only showed up "on inputs of around 20 MB that had one rare, specific layout." Fuzzers usually cap inputs at around 1 MB, so they would likely never have stumbled on it.

The fine print: Anthropic is unusually blunt about the limits, starting with its own heading: "Formally verified" does not mean "bug-free." The proofs assume the program "runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU using Linux OS," while most people run these libraries on x86 or ARM with different system libraries. The team didn't verify every entry point in each library, and the AddressSanitizer tool it leaned on doesn't catch every memory bug. Cost is real too: proofs "can take hundreds of millions of tokens to produce." And because Claude was allowed to patch code, it could in theory cheat by rewriting a program into one that trivially never crashes. Anthropic says it penalized patches and audited them for that. All of this is Anthropic and Theorem reporting on their own work. They're publishing a subset of proofs and invite independent checking, which is the right move, but outside experts haven't had long to dig in.

Formal verification has long been the vegetables of software engineering: everyone agrees it's good for you, almost nobody eats it. If AI makes the proofs cheap enough to be routine, the payoff isn't a flashy demo. It's boring, important libraries (the ones that unzip files and decode images inside everything you use) quietly getting a lot harder to break. The caveats are big enough that "proven" should still come with an asterisk, but it's a nice change to read an AI security story where the AI is mostly patching holes instead of finding new ways in.

The clever trick is that nobody had to write a fresh description of what "correct" means for each library. The developers already had.

How it works: A fuzz test is a front door into the code where any crash counts as a bug. Anthropic turned each one into a formal claim: this test never crashes for any input under 64 MB. Claude then writes a proof of that claim against the compiled binary, and the Rocq checker either accepts it or doesn't. When the proof gets stuck, that's often because there's a real bug, so Claude patches it and tries again. Proofs also turn out to be reusable. When agents could copy each other's finished work, Anthropic says they "needed 17% fewer tokens than when they worked alone." And newer models are cheaper at it: on 36 small test tasks, Opus 5.5 proved half of them "with about 40% fewer tokens than Opus 5."

Try it: If you maintain an established open-source project, Theorem's OSS Verify program offers this for free to qualifying projects. You enroll by opening a pull request, much like joining OSS-Fuzz, and Theorem has published a Claude skill to help set it up. Curious rather than maintaining? The released proofs live in Theorem's oss-verify-proofs repository on GitHub, and Anthropic's full appendix goes deeper on some of the side experiments. Fair warning: a typical proof is longer than most novels.