Claude Writes Machine-Checked Proofs That 123 Open-Source Libraries Won't Crash

On October 22, 2026, Anthropic’s Frontier Red Team, working with the company Theorem, published research showing that Claude can write formal proofs about real-world software at a scale that used to be impractical.

What Claude proved

The team started from existing fuzz tests in Google’s OSS-Fuzz project. Each library and its fuzz test were compiled to a RISC-V executable, and Theorem’s formal model of RISC-V and Linux processes turned that into a specification: the program must always exit normally, with no memory-safety errors and no failed assertions.

Over a few weeks, Claude proved that 239 entry points across 123 open-source libraries never crash on any input under 64 MB. The proofs total about 180 million lines of Rocq, with a typical proof around 600,000 lines covering a binary with a median of 18,000 RISC-V instructions. Almost none of it needs human review, because the Rocq proof checker verifies each proof against the spec.

Bugs found along the way

Trying to write the proofs surfaced bugs, which Claude patched before proving the fixed code. Anthropic says some had eluded detection for years despite trillions of test runs. One was a counter underflow in a decompressor that caused an out-of-bounds write, but only on inputs around 20 MB with a rare layout. Fuzzers typically cap inputs at about 1 MB.

The caveats

Anthropic is explicit that “formally verified” does not mean “bug-free.” The proofs assume a single-threaded static binary with a fixed memory budget on RISC-V Linux, while most people run these libraries on x86 or ARM. AddressSanitizer doesn’t catch every memory bug, and not every entry point of each library was verified.

What’s next

Anthropic is publishing a subset of the proofs and the RISC-V and OS semantics, and Theorem is offering to run the pipeline for other open-source projects. Anthropic also reports that Opus 5.5 proved half of a 36-task test set using about 40% fewer tokens than Opus 5.