Anthropic Frontier Red Team: Claude, working with Theorem, formally proved no-crash properties at the RISC-V assembly level for 239 entry points across 123 OSS-Fuzz libraries, about 180M lines of Rocq
On 2026-10-22 Anthropicβs Frontier Red Team, working with Theorem, published research in which Claude turned OSS-Fuzz fuzz tests into formal specs and proved on the compiled RISC-V binaries that no input under 64 MB causes a crash. Over a few weeks it proved 239 entry points across 123 libraries, about 180 million lines of Rocq checked by the Rocq kernel. Along the way it found and patched hundreds of bugs, including an out-of-bounds write that needed a roughly 20 MB input with a rare layout. Anthropic says Opus 5.5 needs about 40% fewer tokens than Opus 5 to finish proofs.
β‘ Key Takeaways
- β’Scale: 239 entry points across 123 OSS-Fuzz libraries, about 180M lines of Rocq, a typical proof about 600,000 lines for binaries with a median of 18,000 RISC-V instructions
- β’Scope: no crash (including ASan memory errors and failed assertions) for any input under 64 MB, assuming a single-threaded static RISC-V binary on Linux with musl
- β’Hundreds of bugs found while proving, including an out-of-bounds write that needed about a 20 MB input, plus a rediscovery of CVE-2026-56132 in libexpat
- β’On 36 small verification tasks Opus 5.5 proves half with about 40% fewer tokens than Opus 5; a shared proof workspace cut tokens a further 17% (Anthropic figures)
- β’A subset of proofs and the RISC-V and Linux semantics are public (theorem-labs/oss-verify-proofs), and Theorem published a Claude skill to help developers start
