Anthropic’s new formal-verification research makes a serious case for using AI to produce security evidence that a separate mathematical checker can inspect. The work could change how teams establish confidence in critical software. Understanding its value requires reading the theorem behind the claim.
In research published on October 22, Anthropic and Theorem report proofs for 239 fuzzing entry points across 123 open-source libraries. Claude produced roughly 180 million lines of accepted Rocq proof code. The guarantees concern particular compiled programs under specified conditions, including an input-size limit. Anthropic’s announcement describes a substantial engineering achievement.
There is also a consequential detail in the public release: its proofs do not establish that programs always finish running. That distinction belongs near the beginning of any serious account of this work.
My assessment is that the most promising development here is a more auditable division of labor. AI can search for proofs at enormous scale, while the acceptance decision depends on explicit statements and machine checking. The quality of those statements, and their relationship to deployed software, will determine how useful this becomes.
The reported experiment and the public release are different evidence sets
The public proof index lists 60 entry points across 25 libraries at the repository revision inspected for this article. Several entry points have proofs for more than one sanitizer configuration, so entry points and proved statements are different units.
The release includes 138 proved statements. Examples in the index include entry points in cJSON, simdjson, OpenSSL and zstd. The presence of a library in that list establishes coverage of the named targets and statements; it does not certify the whole library.
| Evidence | What it establishes |
|---|---|
| Anthropic’s reported experiment: 239 entry points, 123 libraries | The researchers’ account of the larger effort |
| Public proof index: 60 entry points, 25 libraries, 138 statements | The scope of the released proof collection inspected here |
| A statement file without a completed proof | A precisely formulated verification target |
| A successful independent checker run | Evidence that the specified proof passes in that checking environment |
Anthropic says it is withholding proofs that could expose unpatched bugs. A smaller public collection therefore does not, by itself, contradict the larger research result. It does mean outside readers must keep the two evidence sets separate.
This article inspects the announcement, appendix, public documentation and proof index. Kingy.ai has not independently rerun the Rocq proofs or reproduced the full experiment.
How a fuzz test becomes something you can prove
A conventional test supplies an input and checks an outcome. A fuzzer repeats that process with many generated or mutated inputs. A successful test campaign gives useful evidence about the cases exercised. A universal mathematical statement makes a different demand: the stated property must hold for every input within its scope.
The practical starting point is the fuzz harness, a small program that calls the library and exposes failures. Its contents matter enormously. A harness that passes arbitrary bytes to a decoder and checks for crashes asks a narrower question than one that also checks the decoded output against a reference implementation.
Theorem’s statement guide explains that correctness properties can be encoded in the harness as conditions that abort when violated. It also distinguishes statements about termination from statements about agreement between ordinary and sanitizer-instrumented builds. Inputs at least 64 MiB long are refused by the driver. MiB is the binary unit; the technical documentation is more precise here than the announcement’s shorthand “MB.”
Consider a hypothetical compression harness:
compressed = compress(input)
restored = decompress(compressed)
if restored != input:
abort()If the check survives compilation, a suitable proof that execution cannot reach the abort rules out a round-trip mismatch on covered executions. It still leaves separate questions about termination, resource consumption and what happens outside the stated environment. This example illustrates the idea; it is not a quotation from a released harness.
That suggests a useful engineering shift. Writing a better test harness can improve both testing and the proposition a future proof establishes. Teams do not need to begin with a complete formal specification of an entire application to express a valuable invariant.
Why the public proofs do not establish termination
The repository’s README is explicit: none of the proofs in this release proves a halts statement. An agreement statement can exclude errors and establish agreement between builds without excluding an execution that continues forever.
The formal statement definitions separate these obligations. Treating them as interchangeable would overstate the release.
A hypothetical parser that becomes trapped in an infinite loop could occupy a worker indefinitely without producing an invalid memory access. For a service operator, that can still be a serious availability problem. A proof of error freedom does not automatically answer it.
Even a termination proof would leave another operational question: how long does the computation take? A program that eventually finishes after an impractical amount of work may still violate a service’s latency or resource requirements. Those requirements need their own definitions and evidence.
This is a reason to be precise about security properties. “Verified” is too broad to function as a useful procurement requirement on its own. A team needs to know whether a result covers memory errors, functional behavior, termination, execution cost, or some combination of them.
The binary-level choice is powerful and restrictive
The public build contract describes reproducible builds and the artifacts that identify them. The proof release concerns static RISC-V Linux binaries; the README identifies clang 20.1.8 and musl as the compiler and C-library environment.
Working with executable bytes gives the claim a concrete target. It avoids an additional obligation to show that a manually translated source-level model faithfully describes those bytes. It also means the guarantee does not automatically follow the project name into a different build.
Suppose a company deploys the same library on an ARM server, dynamically links another C library, and enables a different optimization setting. Shared source code is useful context, but the company still needs evidence connecting its deployed artifact to the verified claim. The existing proof cannot establish that connection merely because both packages carry the same version number.
This changes what a meaningful software assurance record should contain. Alongside the package name, a reviewer should expect a source revision, build recipe, binary hash, theorem identifier, model version and checking result. Without that information, a verification badge becomes difficult to interpret after the next rebuild.
Binary verification may therefore create demand for better release provenance. That is my inference from the approach, rather than a deployment outcome demonstrated by the research.
What remains outside the guarantee
The Linux process model documentation describes a deliberately limited environment. It runs one thread and does not execute signal handlers. Its filesystem model omits features such as permissions and symbolic links. The documentation calls the model incomplete and identifies assumptions that it does not check.
These limits have direct consequences for interpretation. A claim about this model cannot establish the correctness of a concurrent application’s synchronization. Nor can it settle a real deployment’s filesystem authorization rules when those rules are absent from the model.
Memory limits are also part of the theorem. The released agreement statements use a 2 GiB plain-build budget when comparing against an AddressSanitizer build, and 16 GiB for the UndefinedBehaviorSanitizer comparison. Inputs requiring more than the applicable budget fall outside the premise, according to the release README.
The sanitizer itself defines another boundary. LLVM’s AddressSanitizer documentation describes detection of classes of memory errors, including out-of-bounds accesses and use-after-free. Such instrumentation does not define whether a calculation is correct, whether an authenticated user should see a record, or whether a protocol decision satisfies the application’s policy.
A security review should therefore connect a claimed property to a concrete failure mode. For an image-upload service, memory corruption in a decoder, excessive processing time, unauthorized file access and a wrong decoded image are separate concerns. Evidence that resolves one is valuable, but it does not silently resolve the others.
The checker changes how much we need to trust the model
The checking documentation describes a pipeline that checks binary hashes, builds the formal images and statements, compiles proof files, and checks a wrapper tying the result to the required statement. It also audits assumptions against an allowed list. An unproved admission cannot substitute for a completed proof.
That is a significant difference from asking an AI system to review code and accepting its explanation. A model may propose an invalid argument, misunderstand a helper lemma or spend a long time on a dead end. Those failures do not become accepted evidence merely because the output sounds persuasive.
There is still a trusted foundation. The release’s trust inventory includes the Rocq kernel and specified axioms, the process semantics, tools that convert executable files into memory images, the checking wrapper and the statements themselves. The correctness of the process model’s description of real Linux is not established by proving a theorem inside that model.
The resulting review task is more focused. Reviewers can scrutinize what was proved, which artifacts it concerns, what assumptions were accepted and whether those assumptions fit the intended system. They do not have to treat every line of generated proof prose as an assertion backed only by the model’s reputation.
That is the strongest reason to take this work seriously. It creates inspectable evidence and a mechanism for rejecting invalid submissions.
Hundreds of millions of proof lines are a cost signal
The technical appendix puts the proof volume in perspective. It reports about a billion lines produced during attempts, with about 180 million in successful proofs. More than half of a typical proof consists of machine-emitted material. Much of the work concerns shared runtime machinery rather than the library’s own logic. Checking a proof can take roughly 30 minutes to several hours of CPU time.
The appendix’s expert discussion identifies a scaling concern: the proofs are verbose, and better abstractions may be necessary for larger programs. Proof length is therefore a poor standalone measure of reasoning quality or economic value.
Anthropic reports about 40% fewer tokens for Opus 5.5 than Opus 5 at the halfway point of a 36-task benchmark, and a 17% token reduction when agents share proof work. These are encouraging efficiency results, not a published price for verifying an arbitrary production dependency.
The benchmark also uses deliberately reduced programs: the appendix describes 64-byte inputs, simplified runtime support and a small sanitizer. Those conditions matter when interpreting the comparison.
For a team considering adoption, I would calculate the full cost of obtaining and maintaining a useful result: proof generation, checking, specification review, failed attempts, patch review and revalidation after changes. Token savings affect one component of that bill. They do not establish the total.
The economically interesting possibility is reuse. If a well-maintained proof component can serve many projects, its initial cost can be spread across those uses. Whether that works in practice depends on stable interfaces, useful abstractions and the amount of work each update requires.
Letting the agent patch code creates a second review problem
Anthropic allowed Claude to patch bugs encountered during proof construction. It explicitly discusses the danger that an agent could simplify a program until the required statement becomes easy to prove, and describes penalties and patch audits intended to discourage that behavior.
A trivial example shows the concern. A decoder that rejects every input may avoid many dangerous execution paths while also becoming useless. A proof can be valid and the patch unacceptable if the statement does not preserve the behavior users need.
The released evidence should be read with its provenance in view. Theorem’s origin documentation explains how automated submissions were adapted to the release’s binaries and model, then checked again. The enrollment documentation separately warns that AI-generated findings and patches may be wrong or incomplete and require review.
My practical recommendation is to separate approval of a behavioral change from acceptance of its proof. A reviewer should establish what inputs now behave differently and why that change is intended. Then the proof can provide evidence about the approved result. Allowing the same optimization objective to redefine acceptable behavior without review would weaken the assurance process.
Independent reproduction needs more than a green badge
The reproduction guide explains how to rebuild a target and compare its artifact hashes. This addresses a different question from whether a proof compiles. One concerns the origin and identity of the executable; the other concerns the theorem about it.
A strong independent evaluation would retain both results, with the source revision, toolchain digest, statement revision and logs. It would then explain how closely that environment matches the evaluator’s intended deployment.
The release’s status inventory also separates available targets from projects that need additional language, build or model support. A directory full of statements is an agenda for verification work. It is not a directory full of completed guarantees.
I would resist turning the published totals into a general success rate. The larger research effort, the public subset, buildable targets and all formulated statements are different populations. Dividing one convenient number by another would produce a percentage without a defensible interpretation.
What maintainers can do with this today
Theorem has published an OSS Verify enrollment workflow. It requires a core maintainer, an eligible open-source license, a public repository, a fuzz target, a supported build and a security contact. The workflow includes reproducibility checks and controls over proof publication. That is a concrete route for eligible projects to explore the approach; it is not evidence that every submitted project can be verified immediately.
For a first evaluation, I would choose one consequential, well-understood entry point and define the decision the evidence needs to support. A parser exposed to untrusted files is easier to scope than an entire browser.
Then I would use five acceptance questions:
- Which exact executable and statement are being checked?
- Which important input cases, resource conditions and environmental behaviors are excluded?
- Does the harness test the behavior users depend on?
- Can another reviewer reproduce the artifact and checker results?
- What is the measured cost of refreshing the evidence after a realistic code change?
A successful pilot should produce answers, retained artifacts and a clear account of what remains unproved. It should also preserve ordinary regression tests and deployment-specific security checks. Those checks exercise obligations that the formal statement may not cover.
The next result I want to see is an independently reproduced proof for a widely deployed dependency, tied to the artifact people actually run, followed through a real upstream update. That would show how well this research survives the daily work of maintaining software.
Reporting note: Research and repository documentation checked October 22, 2026. Public proof figures are pinned to repository commit 8f5f46768858. This is AI-assisted research analysis, not an independent execution of the proof checker. Illustrations are original explanatory graphics; they are not screenshots of experimental results.
The Kingy Brief
Get The Kingy Brief.
AI changes, original tests and one practical thing to try. Fridays at 09:00 Vancouver time.
Free · Double opt-in · Unsubscribe anytime
Sign up for The Kingy Brief on Beehiiv.
Signup help and newsletter schedule
Signup form provided by Beehiiv. After submitting, check your inbox for "Confirm your subscription to The Kingy Brief" and open its confirmation link. Check Spam or Promotions if you cannot find it.
Fridays at 09:00 Vancouver time: source-checked AI changes, original tests and one practical thing to try. We skip a week when there is not enough verified material. Free. Unsubscribe anytime.