Formal verification with Claude: proofs for 123 open source libraries

On October 22, Anthropic’s Frontier Red Team, together with the company Theorem, published a study in which Claude wrote formal security proofs for 123 open source libraries from the OSS-Fuzz project. The proofs cover compiled RISC-V code, not source code. According to the authors, it’s the first formal verification of production software at the assembly level, using AI, on this scale.

How does formal verification with Claude work?

Formal verification is a mathematical proof that a program has a given property for every possible input, not just the ones someone tested. The problem is that until now it took years of expert work. A comparison from the study: verifying the seL4 kernel took about 20 person-years, while writing it took two.

The pipeline from the study looks like this:

1. The starting point is existing fuzz tests from OSS-Fuzz (a Google project that constantly bombards libraries with random data).
2. The library and its test are compiled into a RISC-V executable.
3. From Theorem’s semantics of the RISC-V processor and a Linux process, a specification is generated automatically: the program must always exit normally, with no memory errors and no failed assertions.
4. Claude writes the proof, and the Rocq proof checker confirms that the proof meets the specification.
5. When Claude hits a bug, it patches the code, the specification is regenerated, and the proof is built again from scratch.

The guarantee covers every input under 64 MB and every modeled system response and memory layout (assuming a static, single-threaded program on RISC-V and Linux).

What numbers did Anthropic share?

1. 239 entry points in 123 libraries.
2. About 180 million lines of Rocq proofs in total; a typical proof is about 600,000 lines long and covers a program with a median of 18,000 RISC-V instructions.
3. The whole effort took a few weeks.
4. On 36 small tasks, Opus 5.5 proved half while using about 40% fewer tokens than Opus 5, and agents working in a shared workspace used 17% fewer than alone.

Interestingly, the proof for cpp-httplib required showing that the red-black tree in libc++ has logarithmically bounded depth, because that was the only way to rule out a stack overflow in the std::set destructor.

What bugs did Claude find?

According to the authors, the process uncovered hundreds of bugs that had survived years of fuzzing. Examples from the post:

1. A counter underflow in a decompressor that led to an out-of-bounds write, but only with an input of about 20 MB with a rare layout.
2. An out-of-bounds read in an image decoder that required a 64 MB input and over 2 GB of memory.
3. An out-of-bounds read that appeared only with a specific sequence of calls on two handles to the same file.
4. A rediscovery of CVE-2026-56132 in libexpat (it required deeply nested input).
5. A logic bug: a function restricting file access didn’t always work, even though nothing crashed.

On top of that, three extra experiments. Claude wrote a formal specification of RFC 1950 and proved on x86 binaries that the Linux kernel’s zlib implements it correctly. It also built a Python subset interpreter in Rust that behaved like CPython in 99.95% of 1.7 million random programs. And an attempt to verify a popular PDF reader found as many security bugs in a week as are usually reported in a year.

It’s the same direction as with PHP2Shell and Claude Mythos at Bank of America: AI models find bugs that people and classic tools missed for years. Only this time it ends not just with a patch, but with a proof.

What to watch out for?

First, what “verified” means. The authors say it plainly: “»Formally verified« does not mean »bug-free.«” A proof is only as good as the specification, the RISC-V and Linux models, and the Rocq checker itself.

Second, the scope. The proofs cover static, single-threaded RISC-V binaries with musl, while most of us run code on x86 or ARM with glibc. They also don’t cover dead code or cases where the program calling the library corrupts memory.

Third, the cost. Single proofs can consume hundreds of millions of tokens, which the authors themselves call the main limitation.

Some of the proofs are already on GitHub (oss-verify-proofs), along with the RISC-V and Linux semantics. The rest are held back because they could reveal unpatched bugs.

FAQ

What is formal verification?

It’s a mathematical proof, checked by a program, that code has a given property for all inputs, e.g. that it never writes out of bounds. Tests and fuzzing only check selected cases.

Are the verified libraries bug-free?

No. The proof guarantees no crashes only within the described model (RISC-V, Linux, input under 64 MB, a single thread). Bugs can hide in the specification, in the machine model or outside that scope.

Can I verify my own project?

Theorem runs OSS Verify, a free program for selected open source projects. A project maintainer applies through a pull request with project.yaml, Dockerfile and build.sh files, much like in OSS-Fuzz. Expect to move the build to static riscv64 binaries.