An AI-generated formal proof passing a checker does not mean an entire software library is bug-free. The practical question is more specific: which binary and entry point satisfy which property, for which inputs, under which machine model? Leaving out those conditions turns a strong piece of evidence into a larger claim than it supports.

Anthropic published its research on LLM-assisted software verification on October 22, 2026. The accompanying public proofs and machine model let developers inspect specific statements and their boundaries. A pinned project version and a runnable specification comparison show how to read that evidence. 中文版.

The change: models produce proofs, checkers check claims

The useful division of labor is to let a model generate a candidate proof and use a separate mechanical checker to determine whether it establishes the specified claim. Acceptance need not depend on how persuasive the model’s prose sounds. Whether that claim captures the behavior we actually need remains another question. Proof production and specification design carry different responsibilities.

The pinned checking procedure also checks binary hashes, binds the proof theorem to the intended statement, and audits its assumptions. Compiling a proof file is therefore not the only evidence to inspect: it must establish the designated claim. These steps were read, not executed here.

The technical reference here is public proof-repository commit 98e995d4, representing an October 23 project snapshot. Its README lists proofs for 60 entry points in 25 libraries and identifies Rocq 9.2.0. Those numbers describe that public release subset, not the entire research effort. A statement being present is also not the same as a proof being completed.

Engineering details and counts below use that fixed version, keeping them separate from subsequently updated research pages and project statistics. The important counting distinction is that libraries, entry points, statements, and proofs are different units. Evaluating a dependency means locating the relevant entry point and artifact, not simply finding the library name in a list.

From an entry point to a checkable statement

A test entry point receives input, calls library code, and fails when selected conditions are violated. Attempting a proof moves beyond trying many samples toward establishing a claim over its stated input set. That set and the failures to be excluded must be specified. The process does not automatically supply business requirements that nobody has defined.

The pinned build documentation associates the proofs with specific static RISC-V binaries. A review record should therefore keep artifact identity, entry point, property, and premises together. After rebuilding, changing code, or changing how the program runs, check whether the argument still applies instead of carrying forward an unversioned “verified” label.

For example, a hypothetical decoding entry point may require only that processing avoid specified errors. Does it also require every output pixel to be correct? Is expected output compared? These are questions about a specification, not allegations of defects in a particular library in this research. If the desired guarantee concerns business results, their relationship to the input needs to appear in the specification.

Eight inputs can produce two different kinds of passing

The original teaching example below defines the intended behavior as returning the input unchanged. identity returns x, while constant returns zero for every input. A weak check merely requires a non-throwing integer result between zero and eight. On inputs zero through seven, both implementations pass eight of eight cases. Requiring equality with the input yields eight of eight for identity but only one of eight for constant.

That does not show a faulty proof checker or make error-exclusion properties worthless. The checks answer different questions. Returning zero satisfies the weak requirement while violating the separately stated application requirement. The repair is to improve the specification, not expect a mechanical checker to infer an unstated need.

Now consider bounded_bug: it returns x below eight and zero otherwise. On zero through seven it passes even the stronger check eight of eight times. Expanding the input set to zero through eight produces eight of nine, with the counterexample input eight, expected eight, actual zero. A claim that really holds throughout one set does not automatically extend to a larger set.

A reproducible example and its precise scope

The program was run with Python 3.15.0 and passes eight checks. It enumerates two explicit finite sets to illustrate property strength and input scope. It does not call an LLM, run Rocq, check the released proofs, or reproduce the research results. Eight of eight is neither a model benchmark score nor a probability that real software is secure.

def identity(x):
    return x

def constant(x):
    return 0

def bounded_bug(x):
    return x if x < 8 else 0

def weak_check(fn, inputs):
    accepted = 0
    for x in inputs:
        try:
            y = fn(x)
        except Exception:
            continue
        accepted += isinstance(y, int) and 0 <= y <= 8
    return accepted

def strong_check(fn, inputs):
    return sum(fn(x) == x for x in inputs)

small = tuple(range(8))
large = tuple(range(9))
assert weak_check(identity, small) == 8
assert weak_check(constant, small) == 8
assert strong_check(identity, small) == 8
assert strong_check(constant, small) == 1
assert strong_check(bounded_bug, small) == 8
assert strong_check(bounded_bug, large) == 8
assert bounded_bug(8) == 0
assert identity(8) == 8
print('weak constant: 8/8')
print('strong constant: 1/8')
print('bounded bug, 0..7: 8/8')
print('bounded bug, 0..8: 8/9')
print('counterexample: input=8, expected=8, actual=0')
print('8 checks passed; finite enumeration, not a Rocq proof')

During a specification review, try writing an obviously wrong substitute implementation that might still satisfy a weak requirement. Ask whether the requirement excludes it. This wrong-implementation control can reveal missing conditions; it is neither an exhaustive search over faulty programs nor a replacement for a formal proof. The constant function provides a deliberately small control that a reader can inspect directly.

Error freedom is a different question from termination

The statement documentation separates agreement from halts: agreement does not exclude an execution that never ends. The pinned release README also says its released proofs do not establish halts statements. An execution can avoid errors while continuing indefinitely without delivering an application result. For a service expected to answer requests, memory safety, result correctness, and eventual return are separate questions.

No infinite loop was launched for this demonstration. The logical point is that excluding an error state alone supplies neither an end time nor a throughput or latency bound. If responsiveness matters, look separately for evidence about termination, resource budgets, and service deadlines. Formal properties and operational measurements can complement each other, but a proof label cannot be converted into an unmeasured latency guarantee.

The seam between the model and deployment

The accompanying pinned LPS scope document identifies modeling boundaries, including a single thread, restricted process and file environments, and external assumptions it does not check. Mechanical acceptance of a theorem still leaves the question of whether a deployment satisfies its premises. The checker examines the argument; it does not directly establish that every model description matches a real system.

A practical adoption record can have three columns: artifact and version; entry point and proved property; deployment premises and how they were checked. If one column is missing, limit the conclusion to what has actually been established. Do not transfer a result in a RISC-V model to another architecture, a dynamically linked binary, or a multithreaded deployment before examining that connection.

Revisit all three columns after dependency changes. Source version, build process, proof files, and deployed artifact need a traceable relationship. A previously green CI job cannot by itself show that today’s artifact falls under the same claim. No such mapping for a live project was performed here, so this article does not claim that any reader’s application has been verified.

What a developer can do with this news

The immediate benefit is a sharper review question: instead of asking whether AI-written code is trustworthy in general, ask which checkable claim is being accepted. Select an important entry point with clear boundaries, describe inputs, outputs, and failure conditions, and inspect whether existing tests express those requirements. Proof-production costs may change; missing specifications do not disappear merely because a model becomes more capable.

Before trying the public tools, follow their documentation to identify versions, build artifacts, and checking steps. Full rechecking requires the appropriate environment and resources. No proof toolchain was installed or run here, and no cost or performance estimate is offered. The contribution is an interpretation of the news and a runnable specification comparison that helps identify what deserves inspection first.

The earlier article on verifying AI-search completion claims asks what evidence establishes task completion. Formal verification makes that question more concrete through statements, artifacts, and premises. A successful check is strong evidence within the scope it actually checks.

Sources: the October 22 Anthropic report, the pre-slot public proof release, and the machine-model scope document. This analysis uses a research report and project documents; it does not independently recheck the Rocq proofs. The diagrams, finite-enumeration example, and review-record method are original. The article retains October 23, 2026 at 16:00 Beijing time and was actually published as a catch-up article on October 28, 2026.