Anthropic said Claude has written machine-checked proofs that 239 fuzz-test entry points across 123 libraries in Google’s OSS-Fuzz program cannot crash on any input under 64 MB under a fixed set of hardware and operating system assumptions. The Frontier Red Team post went up Thursday evening, and the work was done with Theorem, a formal verification startup that is now offering the same pipeline to open-source maintainers for free.
The project took a few weeks. Claude’s proofs come to about 180 million lines of Rocq, with a typical proof running about 600,000 lines for a binary with a median of 18,000 RISC-V instructions. For scale, the post notes that the seL4 operating system kernel took two person-years to build and 20 to verify, which is why this kind of proof has mostly been limited to code like Airbus avionics.
Almost none of the proof code needs a human reviewer. The Rocq proof checker confirms each proof meets its specification, so a developer has to trust the checker, the exact theorem statements, and Theorem’s formal models of RISC-V and Linux processes. A subset of the proofs is on GitHub under an MIT license.
Bugs past the fuzzer’s reach
Where a target had bugs, Claude patched them first and then proved the patched code. Some were out of a fuzzer’s reach, since fuzzers typically cap inputs at 1 MB. One decompressor had a counter underflow that caused an out-of-bounds write, but only on inputs of around 20 MB with one rare layout. An image decoder had an out-of-bounds read that needed a 64 MB input and more than 2 GB of memory. Claude also rediscovered CVE-2026-56132 in libexpat.
A model that can edit the code it is proving could cheat by rewriting the program so it trivially never crashes. Anthropic said it penalized every patch, gave extra credit for proving which inputs a patch changed and how few they were, and logged and audited the patches.
The post is direct about the limits. “‘Formally verified’ does not mean ‘bug-free,’” it says. The proofs cover single-threaded, static RISC-V binaries linked against musl libc, while most people run these libraries on x86 or ARM with glibc. AddressSanitizer, the tool that turns memory errors into crashes, doesn’t catch every memory-safety bug, and Anthropic didn’t verify every entry point in each library.
An expert review in the appendix found Claude’s proofs verbose. They spell out register contents and every branch where a human proof engineer would have built abstractions, and the reviewer left open whether that style will work on more complex programs.
Haseeb Qureshi, managing partner at Dragonfly, was more upbeat on X. “It’s not a panacea, but a formally verified program is way more robust than one that’s vibe-tested,” he wrote.
How maintainers sign up
Qualifying open-source projects pay nothing for Theorem’s OSS Verify. A core maintainer opens a pull request with a project.yaml, a Dockerfile and a build.sh, and the build has to produce static riscv64 binaries. Bugs go to maintainers privately, with no disclosure deadline. “Findings and patches are generated by AI models, and we don’t promise that a person reviews them before we send them,” Theorem’s FAQ says.
Anthropic took the same unreviewed approach with OSS Scanner, the opt-in service it launched earlier this month that sends maintainers model-generated vulnerability reports.
Anthropic calls cost one of the key limitations, since a single proof can take hundreds of millions of tokens. On a 36-task test set, Opus 5.5 proved half the tasks with about 40% fewer tokens than Opus 5. Theorem estimated last month that 95% of the machine code in the Nix package collection could be verified for about $134 million by the end of 2027, if models can be made to improve at verification much faster than they improve overall. At today’s rates, Theorem puts the proof for OpenSSL at about $220,000. Nearly 16,000 packages reuse OpenSSL, which works out to about $14 each.