Anthropic said Claude has written machine-checked proofs that 239 fuzz-test entry points across 123 libraries in Google’s OSS-Fuzz program cannot crash on any input under 64 MB under a fixed set of hardware and operating system assumptions. The Frontier Red Team post went up Thursday evening, and the work was done with Theorem, a formal verification startup that is now offering the same pipeline to open-source maintainers for free.

The project took a few weeks. Claude’s proofs come to about 180 million lines of Rocq, with a typical proof running about 600,000 lines for a binary with a median of 18,000 RISC-V instructions. For scale, the post notes that the seL4 operating system kernel took two person-years to build and 20 to verify, which is why this kind of proof has mostly been limited to code like Airbus avionics.

Almost none of the proof code needs a human reviewer.…