Anthropic and formal-verification startup Theorem say Claude has done something that used to take experts years: it wrote mathematical proofs that real software will not crash. In research published on October 22, Claude proved that 239 test entry points across 123 open-source libraries from Google's OSS-Fuzz programme never crash on any input under 64 MB, working at the level of compiled RISC-V machine code.

The proofs run to roughly 180 million lines of Rocq, a proof language checked mechanically by computer, with a typical proof around 600,000 lines for a binary with a median of 18,000 instructions. Along the way Claude found bugs that trillions of fuzzing runs had missed, patched them, and then proved the patched code crash-free. Anthropic is publishing a subset of the proofs and the trusted components underneath them, so the checking does not depend on trusting the lab.

The bounds matter: the proofs cover single-threaded, static RISC-V binaries, not the x86 or ARM builds most software actually ships as, and 'formally verified' here means crash-freedom for the stated property, not bug-free in general. Even so, Anthropic frames it as the first large-scale use of AI for formal verification of production software at assembly level — arriving in the same week AI models helped surface the PHP2Shell flaws and Claude stripped unneeded code out of OpenSSH.