180 Million Lines of Proof, and the Assumptions That Make It Useful

The sentence "AI formally verified 123 open-source libraries" slides very easily into "those libraries are now bug-free." What was actually proved is much narrower, and the narrowness is the useful part. Anthropic and Theorem published proofs that 239 fuzz entry points cannot crash under a specific execution model. The 180 million lines describe the size of the Rocq development, not the size of the guarantee.

Applying the October 22 result requires pinning both a property and a binary. Rechecked October 26, Theorem's scope document distinguishes current and next-toolchain exit contracts. The latest prose cannot simply be projected onto an older proof. This article did not re-check the complete proof corpus.

What was proved, and what was not

Read Anthropic's research post next to Theorem's what-gets-proven document and the boundary becomes clear.

The unit is the fuzz entry point, not the library. One library can have several entry points, and only some of them were proved. Code outside those entry points, misuse by a caller, and a binary built for another architecture all sit outside the statement.

Why the proof targets assembly

Source-level verification proves something about the source. What runs is the output of a compiler and linker. Change the optimizer, the runtime library, or the link mode and the same source can behave differently.

Binary-level verification closes part of that gap. Theorem builds each project twice, checks that the bytes match, and pins the binary's SHA-256 in a lock file. The proof is about that binary. Reproducible builds are a precondition, so the source commit, build files, and toolchain image are published together.

The cost is coupling. A proof is tied to one architecture and one compiler. An x86-64 OSS-Fuzz binary, a dynamically linked glibc build, and a different optimization level are different subjects. The accurate sentence is not "this library is verified" but "this entry point of this binary, built from this commit with this toolchain, satisfies this statement."

The specification lives inside the fuzz target

The most important warning in Theorem's documentation is that a proof is only as strong as its fuzz target. A weak fuzz target makes the theorem vacuous. In this style of verification the specification is not a separate document. It is the code that feeds input in and decides when to fail.

The contract differs from a normal fuzzer. The halts statement accepts only exit status 0 or 2. Zero means the target returned normally. Two means the driver rejected the input, for example because it was 64 MiB or larger. Expected errors therefore end with return 0, and a real property violation must end with abort().

For the driver pinned by the current proofs, returning -1 is not a failure. It is read as "do not add this input to the corpus" and counts as a pass. assert() is also the wrong tool, because the check disappears in a release build with NDEBUG defined.

The snippet below is an illustrative decode API, not code that was compiled or verified for this article.

// Wrong: the property failure is reported as -1.
// The halts statement counts -1 as a pass, so the proof survives a broken property.
int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
  if (size < 4) return -1;
  if (!decode_is_valid(data, size)) return -1;
  return 0;
}

// Better: expected errors return 0; property violations call abort().
// Single-threaded, no state beyond the input, explicit size ceiling.
int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
  if (size < 4) return 0;
  if (size >= 64u * 1024u * 1024u) return 0;

  struct decoded out = {0};
  if (!decode(data, size, &out)) return 0;   // invalid input is a normal outcome
  if (out.len > MAX_DECODED) abort();        // specification violation
  if (!roundtrip_matches(data, size, &out)) abort();
  free_decoded(&out);
  return 0;
}

The conditions that reach abort() are the real specification: the things that must never happen. If out.len > MAX_DECODED is in fact an allowed outcome, the proof will be a flawless proof of the wrong statement. This illustrates a specification error that can remain even when the proof checker is sound.

Before adopting this workflow, I recommend two checks against vacuity. These are editorial review criteria, not an audit result for all published proofs. A coverage witness means the example inputs execute every API call and every property check at least once. A distinguishing mutant means that when one line of the property is deliberately broken, the fuzz target finds an input that actually calls abort(). Without both, you can prove a specification whose checks never run.

A changed build needs a new evidence link

An adoption record can use the following four fields. This is a documentation example, not a completed verification of a real project.

The current document also describes a next-toolchain change: some language drivers will distinguish a -1 return with exit status 3. Existing proofs keep their pinned driver. “Only statuses 0 and 2 are accepted” must not be generalized to every future build. Nor does the normal target establish resilience to arbitrary allocation failures: that needs a separate allocation-failure target.

Choosing a first target

You cannot verify everything at once. Narrow the candidate list with these questions.

A small parser or decoder is a good first target: a config-format parser, an image header parser, a decompression function. A plugin loader, a network server, or a multithreaded runtime is outside the current model.

Budget realistically. Theorem does not promise a fixed duration per project and says a single proof can take days or more. The build needs Docker, buildx, Python 3, and about 10 GB of free space; the first run pulls a roughly 1.1 GB toolchain image that expands to about 5 GB. tools/check builds Dockerfiles that can reach the network, so run it only against repositories you trust.

What the proof does not cover

An adoption note should state these limits explicitly.

• Other builds. A different compiler, flag set, architecture, or the usual x86-64 OSS-Fuzz build is a separate subject.
• Other link modes. The proof assumes a statically linked RISC-V binary with musl. Most production deployments link glibc dynamically on x86 or ARM.
• The whole library. The 239 entry points are a subset of 123 libraries. Code outside them, dead code, and memory corruption on the caller's side are out of scope.
• Sanitizer gaps. LeakSanitizer is disabled and MemorySanitizer is absent. Uninitialized reads are not checked.
• Large inputs and memory. Inputs of 64 MiB or more, or over the memory budget, are not part of the statement.
• The trusted base. Errors in the checker, semantics, or statement can invalidate the intended guarantee. People still have to review that layer.
• Patch quality. Fixes produced during proving were written by AI, with no guarantee of human review. Theorem also tells recipients to review patches before taking them.

Do not translate "formally verified" into "bug-free." The accurate sentence is "this entry point of this binary satisfies this specification."

Reading 180 million lines as a cost signal

Line count shows scale, not cost. Divide 180 million by 239 entry points and you get roughly 750,000 lines each, close to the "typically 600,000" figure in the announcement. Proofs being much larger than the code is normal in formal verification.

The efficiency signals are separate. On 36 small verification tasks, Opus 5.5 proved half and used about 40% fewer tokens than Opus 5. Letting agents copy each other's proofs cut total tokens by 17%. That supports a direction, cheaper proofs as models improve, but it is not a quote for your project.

For a team, the bottleneck is not proof volume. It is writing the specification and reviewing the patches. Deciding which properties to state, how large an input you are willing to be responsible for, and whether a failing input is a real bug are not automated. Budget that design time before you budget model tokens.

Put the scope of the guarantee in the contract

The Anthropic and Theorem result shows more than "AI can write proofs." It shows that the boundary of a proof can be written down and pinned. The important part is not the number 123. It is 239 entry points, 64 MiB, single-threaded, a static RISC-V binary, and the Rocq kernel.

If you adopt this, write three sentences first. Which binary is being verified. Which property is being proved. Which execution conditions are assumed. If you cannot answer those three, 180 million lines are not a reason for confidence. They are a contract you have not read.

The linked paid course covers agent harness, loop, and graph design. Readers seeking Rocq or C/C++ formal verification practice will need separate learning material.

Related reading

• Claude Security's continuous scanning: the gap between "fixed" and deployed
• AI agent security basics: why permission design comes before prompts

Sources

• Anthropic: LLMs are making formal software verification feasible at a much larger scale
• Theorem: OSS Verify — What gets proven
• Theorem: OSS Verify README
• Theorem: OSS Verify proofs
• Theorem: RISC-V and Linux process semantics