Formal verification sat for years on airframes and kernels such as seL4: two years to write the code, twenty to write the proofs. Anthropic’s Frontier Red Team, with Theorem, shows another scale. Claude proved security properties at RISC-V instruction level on more than a hundred open libraries. The post is dated 22 October.
What they actually proved
The spec came from existing OSS-Fuzz harnesses: “this entry point does not crash”. They lifted it onto a RISC-V binary and a Linux model. Claude closed 239 entry points across 123 libraries: a normal exit, no memory errors, no failed asserts, on any input under 64 MB — for a single-thread static binary, a fixed memory budget, RISC-V and Linux. The proofs run to about 180 million lines of Rocq; a typical one is hundreds of thousands of lines on a median 18,000 instructions.
A human does not have to read that volume. Trust sits in the RISC-V and Linux models, the theorem statement and the Rocq kernel. Other bugs are either outside that frame or in the trusted bits. Along the way the model found defects that had not shown up in trillions of test runs — and fixed them before finishing the proof.
How to look at it
This is not a stamp that “the library is safe”. It is a proof of a narrow property on a narrow machine. It matters to C/C++ maintainers in OSS-Fuzz, whom Theorem offers the same pipe and a Claude skill. It does not matter as a replacement for review and patch management. Watch how many outside teams replay the published subset of proofs, not the slogan “there are no bugs left”.
