Anthropic's Frontier Red Team, working with verification startup Theorem, used Claude to prove security properties in 123 real-world open-source libraries. The proofs target compiled RISC-V assembly rather than source code, which means the team did not need a formally verified compiler to reason about what the software actually does when it runs. Anthropic calls it the first large-scale effort to apply formal verification to production software at the assembly level with AI.
The results are concrete. Claude proved that 239 fuzz entry points across those libraries always exit normally, without memory-safety errors or failed assertions, for every input under 64 MB and every modelled Linux response and memory layout, assuming single-threaded static binaries on a RISC-V CPU. That took roughly 180 million lines of Rocq proofs, machine-checked by the Rocq kernel. Along the way, Claude found bugs that had survived trillions of fuzz runs, patched them, and then proved the patched code crash-free. The team also formalised RFC 1950 and proved the Linux kernel's zlib implementation conforms to it, and checked a Rust interpreter for a large subset of Python against CPython across 1.7 million generated programs.
Why it matters for founders: verification is moving from a research curiosity to something a small team can buy. Theorem is launching OSS Verify, a free programme that enrolls open-source projects and either proves them crash-free or sends the patches they need. On 36 smaller verification tasks, Opus 5.5 proved about half using roughly 40 percent fewer tokens than Opus 5. One estimate from the Theorem side put patching and proving an entire production stack in the tens of millions. The caveats still matter: the proofs cover specific properties under stated assumptions, say nothing about bugs outside those boundaries, and the checker cannot confirm the specification matches reality.