# Anthropic’s Claude Formal Verification Research: What the Proofs Actually Guarantee

Claude and Theorem turned fuzz tests into checked proofs, with a narrower guarantee than the headline library count might suggest.

By Paras Madan | 2026-10-23

Anthropic and Theorem published research on October 22 using Claude to prove properties of existing compiled software. Anthropic reports no-crash proofs for 239 test entry points across 123 open-source libraries. The result comes with specific assumptions, rather than a claim that those libraries are now bug-free.

## How Claude turns tests into proofs

In [Anthropic’s experiment](https://www.anthropic.com/research/formal-verification), existing fuzz tests become specifications for RISC-V binaries. Claude generates proofs; Rocq checks them. The main experiment assumes single-threaded, statically linked Linux programs, a fixed memory budget and inputs smaller than 64 MB.

Anthropic says proof generation can consume hundreds of millions of tokens. In an experiment with 36 smaller tasks, agents sharing proof work used 17% fewer tokens than agents working alone.

That suggests a different evaluation question from how quickly an agent can write code. How much effort does it take to establish a useful guarantee, and how much of that work survives the next change?

For a team considering this approach, I would start with a requirement that can be stated precisely. For example, should a parser reject malformed input without crashing, or must it also return a particular error? Those are different requirements. A successful proof of one should not be presented as evidence for the other.

## What is available to inspect

The [public proof repository](https://github.com/theorem-labs/oss-verify-proofs) lists 60 entry points across 25 libraries, a subset of the reported research. It provides Rocq 9.2.0 checking instructions and identifies the exact binaries and theorem statements.

Its released proofs establish agreement between specified ordinary and sanitizer-instrumented builds within stated limits. They do not rule out nontermination. They also do not certify an entire library or its x86-64 builds, and depend on the Linux process model being accurate.

**The useful unit of evidence is an individual theorem, not a library count.** Before attaching a guarantee to a product, an engineering team needs to connect that theorem to the executable it actually deploys.

Consider a release review. The reviewer should be able to identify the checked binary, the property established and the assumptions the deployment must satisfy. If any of those have changed since verification, the old proof should not silently carry forward as the new release’s assurance.

## Where engineering judgment still matters

A proof can answer a carefully framed question without answering every question a customer cares about. Reliability, performance and correct handling of business rules should remain separate requirements unless the verification explicitly covers them.

This is also why the review process matters. A dashboard that collapses everything into a green “verified” badge would hide the information developers need. A more useful interface would make the covered property and remaining assumptions easy to inspect alongside the code change.

The practical opportunity is to make evidence easier to maintain as software evolves. That requires more than producing a proof once. Teams need a clear way to decide what must be checked again after a dependency update, a compiler change or a new deployment target.

The next milestone worth watching is a repeatable release workflow: one that makes a precise guarantee cheap enough to refresh, rather than letting yesterday’s proof become today’s unchecked assumption.

I’m Paras. I work at the intersection of AI, engineering and distribution.

If you’re building an AI product and want help turning technical work into clear stories developers and founders read and share, I’d be happy to work with you.

[Book a 30-minute call](https://cal.com/paras-madan/30min).