# Claude Produces Proofs for 239 Entry Points Across 123 Open-Source Libraries

By Simon Yoon

Canonical URL: https://www.tokenpost.com/news/technology/39113
Published: 2026-10-23T16:03:47.000Z
Updated: 2026-10-23T16:03:47.000Z
Section: Technology

> The work covers defined, single-threaded RISC-V binaries; a public repository contains proofs for a smaller set of 60 entry points across 25 libraries.

A collaboration between Anthropic and Theorem produced machine-checkable proofs for 239 fuzz-test entry points across 123 open-source libraries in a few weeks, documenting software guarantees under specific conditions.

The process starts with existing fuzz tests, which generate inputs to probe software behavior, and turns them into formal specifications. A proof checks every input within its defined limits rather than only the inputs sampled during fuzzing. Claude generated proofs in Rocq, and Rocq’s kernel checked them against the specifications. The research post describing the work was published Thursday, Oct. 22.

For inputs smaller than 64 MB, the proofs establish that the covered programs exit normally, trigger no failed assertions and have no memory-safety errors detected by the modeled checks under specified Linux behavior and memory layouts. The guarantee applies to single-threaded, statically linked RISC-V binaries linked with musl and run within a fixed memory budget. It does not cover every entry point or all possible memory-safety flaws, and it does not apply directly to common x86 or ARM builds.

“Formally verified” does not mean “bug-free,” Anthropic’s Frontier Red Team wrote. Attempts to prove the specifications surfaced hundreds of bugs. Claude changed code to address bugs in some cases, and the specifications were regenerated for patched versions.

The full proof set totals about 180 million lines of Rocq. A public repository contains proofs for 60 entry points across 25 libraries, checked with Rocq 9.2.0. The public repository makes the smaller set available for checking but does not contain the full 239-entry-point set. The proofs describe compiled binaries, not the libraries’ source code as a whole. A typical proof contains about 600,000 lines, and the binaries had a median length of 18,000 RISC-V instructions.

Proof generation can require hundreds of millions of tokens. In a separate evaluation of 36 smaller verification tasks, Opus 5.5 proved half using about 40% fewer tokens than Opus 5; those results do not establish the cost of the 123-library project. For comparison, seL4’s implementation took two person-years, while its formal verification took 20.