Anthropic’s Frontier Red Team published a report on 22 October that drags formal verification out of its niche. Working with a company called Theorem, the team had Claude prove security properties for 239 entry points across 123 open-source libraries, at the level of compiled RISC-V machine code.
Why nobody had done this
Formal verification translates code into a mathematical model and then proves it never breaks a given set of rules. The method is old and dependable, and expensive: the seL4 operating system kernel took two person-years to build and twenty to verify. Which is why you find it in Airbus avionics and almost nowhere else.
Anthropic starts from a different problem. Models now find bugs faster than tests cover them. The Linux kernel, one of the most heavily tested codebases in existence, recently had more than 1,000 vulnerabilities disclosed. If you do not want to spend your life catching up, you need a proof rather than a test run.
Fuzz tests as the specification
The trick here is to write no specification at all. Instead of defining what a program should do, the team takes existing fuzz tests from Google’s OSS-Fuzz and turns the rule “this test never crashes” into the spec. If the proof succeeds, fuzzing that entry point becomes pointless: there is no crash left to find.
What was proven: the programs always exit normally for any input under 64 megabytes, with no memory-safety errors and no failed assertions, assuming a single-threaded static binary with a fixed memory budget on a RISC-V CPU under Linux. The proofs come to roughly 180 million lines of Rocq, with a typical proof around 600,000 lines for a binary of about 18,000 RISC-V instructions.
None of it needs a human reviewer. The Rocq kernel checks every proof against the spec. Developers only have to trust three things: the formal models of RISC-V and of Linux processes, the exact theorem statements, and the Rocq checker itself.
The bugs no fuzzer finds
Hundreds of bugs surfaced along the way, and some of them are the real payoff. Fuzzers mutate small inputs, typically up to one megabyte. In a vendored decompressor Claude found a counter underflow leading to an out-of-bounds write, but only at around 20 megabytes of input with one rare layout. Another out-of-bounds read needed a 64-megabyte input and over two gigabytes of memory. Add a rediscovery of CVE-2026-56132 in libexpat and a logic bug that never crashes at all: a feature meant to restrict which files an application may load was not always enforced.
Expertise is no longer the bottleneck
Anthropic is publishing a subset of the proofs along with the RISC-V and OS semantics, and Theorem offers to run the same pipeline for other open-source projects, with a Claude skill to get people started.
The line worth noting sits at the end of the report: if you tried formal verification with weaker models and gave up, try again. The 493 findings from Attack Surface Reduction the day before point the same way. Proving things is still expensive, but the cost has moved from person-years to compute time, and compute time scales.