Anthropic Uses Claude to Formally Verify 123 Open-Source Libraries: What It Means for Developers

For decades, formal verification has been the gold standard of software assurance that almost nobody could afford. Proving mathematically that a program can never crash is possible, but it has traditionally taken teams of specialists years for a single codebase. So the rest of the industry settled for testing and fuzzing: throw billions of random inputs at the code and hope the dangerous ones show up. This week Anthropic published results suggesting that trade-off may be ending. Working with the verification startup Theorem, it used Claude to write machine-checked proofs that 239 fuzz-test entry points across 123 widely used open-source libraries cannot crash on any input under 64 MB.

The catch is in the fine print, and it matters. The proofs cover specific compiled RISC-V binaries under a carefully modelled set of assumptions, not the x86 and ARM builds most of us ship. They took hundreds of millions of tokens per proof in some cases, and nobody has published a total cost. In this post we will look at what Anthropic and Theorem actually did, how the pipeline turns a fuzz test into a theorem, how this fits the wider race to make AI-written code provably safe, and what developers should do now that "verified" is becoming something an AI agent can produce in weeks rather than years.

What Happened

On October 22, 2026, Anthropic's Frontier Red Team published a research post titled "LLMs are making formal software verification feasible at a much larger scale". The work was done together with Theorem, a company building formal models of real machines and operating systems. Over a few weeks, Claude produced roughly 180 million lines of proofs in Rocq, the proof assistant formerly known as Coq, covering libraries drawn from Google's OSS-Fuzz project.

The headline numbers from the announcement:

• 123 libraries, 239 entry points. Each entry point is an existing fuzz harness that the library's own developers wrote.
• About 180 million lines of Rocq. A typical proof is around 600,000 lines, for binaries with a median size of about 18,000 RISC-V instructions.
• Every input under 64 MB. Rather than sampling inputs like a fuzzer, each proof covers the entire input space up to that bound.
• Hundreds of bugs found. Many had survived years of continuous fuzzing, including an out-of-bounds write in a decompressor triggered only by a rare layout in roughly 20 MB inputs, and a logic bug that had been latent for more than a decade.

Anthropic also described side experiments that hint at where this is going. In an effort on a widely used PDF reader, the team says it found as many security bugs in one week as are usually reported for that software in a year. It rediscovered a known libexpat vulnerability that needs deeply nested input, and it proved that the red-black tree in libc++ keeps its depth logarithmic, which was needed to rule out a stack overflow in cpp-httplib.

How It Works: The Numbers That Matter

The clever part of the project is that nobody had to write a specification from scratch. Writing specs is usually the most expensive step in formal verification, and here the developers had already done it without realizing. A fuzz harness is a function that takes arbitrary bytes and feeds them to the library. Any crash or sanitizer error counts as a bug. That is a property: "for every input, this function does not crash". A simplified harness in the OSS-Fuzz style looks like this:

#include <stdint.h>
#include <stddef.h>
#include <stdlib.h>
#include <string.h>
#include "cJSON.h"
int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
    char *buf = malloc(size + 1);
    if (!buf) return 0;
    memcpy(buf, data, size);
    buf[size] = '\0';
    cJSON *json = cJSON_Parse(buf);   /* must never crash */
    if (json) {
        char *out = cJSON_Print(json);
        free(out);
        cJSON_Delete(json);
    }
    free(buf);
    return 0;
}

#include <stdint.h>
#include <stddef.h>
#include <stdlib.h>
#include <string.h>
#include "cJSON.h"
int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
    char *buf = malloc(size + 1);
    if (!buf) return 0;
    memcpy(buf, data, size);
    buf[size] = '\0';
    cJSON *json = cJSON_Parse(buf);   /* must never crash */
    if (json) {
        char *out = cJSON_Print(json);
        free(out);
        cJSON_Delete(json);
    }
    free(buf);
    return 0;
}

A fuzzer runs this millions of times with mutated inputs. The verification pipeline instead asks for a proof that it can never fail for any input. According to Anthropic, the steps are:

1. Compile to a fixed target. The library and harness are built as a static, single-threaded RISC-V executable linked against musl libc.
2. Generate the theorem. Theorem's formal semantics for RISC-V and Linux processes, combined with a no-crash property, produce a formal statement that the binary does not crash for inputs under 64 MB. The public repository phrases this as the sanitizer build behaving like the plain build and never raising an AddressSanitizer or UndefinedBehaviorSanitizer error.
3. Let Claude write the proof. The Rocq kernel then checks it mechanically. Nobody needs to read the 600,000 lines; they either check or they do not.
4. Fix, regenerate, reprove. When Claude finds a real crash, it patches the code and starts over. Anthropic penalized patches that changed behavior and audited them, because an agent allowed to edit code could otherwise "prove" safety by deleting functionality.

That last point is the most important design decision in the whole project. The trusted parts are small and human-reviewable: the RISC-V and Linux models, the theorem statements and the Rocq checker. Everything Claude produces is untrusted until the checker accepts it. The public oss-verify-proofs repository lets anyone re-check a subset: 60 entry points in 25 libraries, including OpenSSL, zstd, simdjson, cJSON, bzip2 and mbedtls, built with clang 20.1.8 and checked with Rocq 9.2.0 inside a pinned Docker image. Anthropic is withholding proofs that could reveal unpatched bugs until fixes land.

Cost is the open question. Anthropic says individual proofs can take hundreds of millions of tokens and has not published a total. It does report fast improvement: on a benchmark of 36 small proof tasks, Claude Opus 5.5 used about 40 percent fewer tokens than Opus 5 to reach the same completion rate, and letting agents share proof work cut token use by another 17 percent.

Context and Competition

To see why this is a big deal, compare it with the most famous verified system. As The Decoder notes, verifying the seL4 microkernel took about 20 person-years, which is why formal methods have mostly stayed in places like avionics, chip design and a handful of cloud security teams. Producing proofs for 123 libraries in a few weeks is a different order of magnitude, even with all the caveats.

Anthropic is not alone in betting that proofs are the answer to unreliable AI code. In March, SiliconANGLE reported that Axiom Math raised a $200 million Series A at a $1.6 billion valuation to build "verified AI" on top of the Lean proof language, so that generated code arrives with a machine-checkable certificate. The difference in approach is telling. Axiom focuses on making new code provable as it is generated. Anthropic and Theorem went after existing, compiled C and C++ that the world already depends on, and verified the binary rather than the source, which sidesteps trusting the compiler.

It also lands in a very particular week for AI and open source. AI-powered review has been finding bugs faster than maintainers can fix them, a tension I covered in Postgres 19 Slips After AI Reviewers Flood It With Bugs. A pipeline that produces hundreds of real bugs plus patches plus proofs could relieve that pressure, or it could add to it. Theorem says it will run the pipeline for other open-source projects, and The Decoder reports its roadmap includes glibc, OpenSSL and cURL.

Why It Matters

Fuzz tests just became more valuable. Every harness your team has written is now a potential specification. The project worked because thousands of OSS-Fuzz harnesses already existed, and the same logic applies to your own code. Teams with good fuzz coverage are suddenly much closer to formal guarantees than teams with none.

The trust model shifts from reviewing code to reviewing claims. Nobody will ever read 180 million lines of proof. What humans must review is the small trusted base: the machine model, the exact theorem statement and the assumptions. That is a healthier division of labor than asking reviewers to scan endless AI-generated diffs, and it is the same principle behind keeping guardrails outside an agent's reach, which I discussed in OpenAI's Coding Agents Weakened Their Own Safety Monitoring.

"Verified" does not mean "bug-free". Anthropic says so directly. The proofs cover single-threaded static RISC-V builds with musl, a 64 MB input bound and a specific crash property. Most production software runs on x86 or ARM with glibc, often multithreaded. Dead code, uncovered entry points and logic errors that do not crash are outside the guarantee, and the public release notes that none of its proofs show termination, so an infinite loop would still count as "safe".

What It Means for Developers

1. Write fuzz harnesses for your parsers now. Anything that reads untrusted bytes, such as file formats, network protocols, config parsers and decompressors, deserves a libFuzzer or similar harness. Today it finds bugs. Tomorrow it may be the spec an AI agent proves against.
2. Keep harnesses honest and narrow. A harness that catches and swallows errors proves nothing useful. Make sure crashes, sanitizer findings and assertion failures actually surface, and keep one harness per entry point so each property is small enough to prove.
3. Update the dependencies that just got patched. Hundreds of fixes will flow into libraries like zstd, OpenSSL and simdjson as Anthropic releases findings. Watch the upstream changelogs and your dependency bot over the coming weeks, and do not pin old versions of parsers without a reason.
4. Read the theorem, not the proof. If a vendor or open-source project tells you a component is "formally verified", ask what exactly was proved, on which architecture, under which assumptions and with which trusted components. The repository's statement format is a good template for those questions.
5. Treat agent-written patches as suspect by default. Anthropic had to audit for reward hacking, where a model makes a proof easy by weakening the program. Apply the same discipline to any agent that edits code to make tests pass: review behavior changes, not just green checkmarks.
6. Experiment on something small. The oss-verify-proofs repository documents how to fetch binaries and re-check proofs, and Theorem publishes a Claude skill for adding projects. Re-checking a single proof is a cheap way to understand what these guarantees look like in practice, though a check can need up to 20 GiB of memory.
7. Budget for verification as a line item. Token costs are high but falling quickly. For security-critical components, it is worth asking whether a proof run would be cheaper than the incident it prevents, especially as costs drop with each model generation.

Final Thoughts

This announcement does not make software safe overnight. The guarantees are narrow, the architecture gap is real and independent reproduction at full scale has not happened yet. But it changes the economics of a technique the industry has long admired and rarely used. When formal proofs required years of expert labor, they were reserved for jet engines and microkernels. If they start costing weeks of compute, they become something an ordinary open-source library, or an ordinary company, can ask for.

The most practical takeaway is also the least glamorous: the teams who benefit first will be the ones who already wrote good fuzz tests. Testing is not being replaced by proofs. It is becoming the raw material for them.

Would you trust a component more if it came with an AI-generated proof that a checker accepted, or would you still want human eyes on the code? Let me know in the comments.

Sources: Anthropic, Theorem Labs on GitHub, The Decoder, Google OSS-Fuzz, Rocq Prover, SiliconANGLE