Claude Formal Verification: 123 Libraries, Proofs and Limits

Anthropic and verification company Theorem reported on October 22, 2026 that Claude generated machine-checked proofs for 239 fuzz-test entry points across 123 open-source libraries. The result is significant for software security, but it is not a claim that 123 libraries are now universally bug-free. The proofs cover specific properties of specific compiled binaries, with important limits on architecture, execution and input size.

What the researchers actually proved

The team took existing OSS-Fuzz entry points, compiled them as RISC-V Linux binaries and translated their behavior into formal specifications. Claude produced Rocq proofs, which an external proof checker validated against those specifications. The core target was that covered executions would not crash, trigger modeled sanitizer errors or fail assertions for inputs below 64 MB, assuming the modeled operating-system responses, memory budget and single-threaded static-binary setup.

The 123-library figure comes from Anthropic's broader experiment; it should not be confused with the smaller public release. Theorem's proof repository currently describes 60 entry points across 25 libraries, with Rocq 9.2.0 checks and a documented model of Linux process behavior. That repository allows specialists to inspect proof statements and the exact binaries they concern.

Why this matters beyond another AI coding benchmark

Anthropic also reports that attempting proofs surfaced bugs that fuzzing had missed, including unusual large-input and multi-step cases. The team allowed Claude to patch issues and then regenerate and prove the specification for the changed code. This makes patch review essential: a mathematical proof of the patched program does not by itself establish that the patch preserved every intended product behavior.

What the proof does not cover

• The main OSS-Fuzz proofs concern static, single-threaded RISC-V binaries under a modeled Linux environment, not ordinary x86 or ARM deployments.
• The properties apply to selected fuzz entry points and covered sanitizer or assertion behavior, not every function, business rule or vulnerability class in a library.
• The input bound is below 64 MB, with memory-budget and modeled system-call assumptions; a proof is only as reliable as its specification and trusted execution model.
• Theorem's public repository notes that its published agreement proofs do not establish that a program always terminates.

How maintainers can evaluate the workflow

1. Identify a high-impact library with existing fuzz targets and decide which crash or correctness property matters.
2. Review the published proof statements and model assumptions before treating the result as a security claim.
3. If eligible, follow Theorem's OSS Verify enrollment process using project.yaml, Dockerfile and build.sh; acceptance and timing are not guaranteed.
4. Keep fuzzing, conventional tests, patch review and production-architecture validation in place. Treat proofs as an additional layer, not a replacement for the rest of security engineering.

Theorem says its OSS Verify initiative is free for qualifying open-source projects, with priority for established, security-critical dependencies. It asks core maintainers to enroll and warns that generating proofs can take multiple days. That is a concrete route for maintainers to explore the technique, but it is not a general-purpose one-click verification service for arbitrary proprietary applications.