Formal verification with AI: seven gates for trusting a proof

On October 22, 2026, four days before this publication in America/Lima, Anthropic described a collaboration with Theorem to bring formal verification to real binaries. The experiment turned existing OSS-Fuzz targets into propositions about RISC-V programs: under a specific Linux model, a memory budget, and inputs smaller than 64 MB, the instrumented executable must not reach errors and must preserve the observable behavior of the unsanitized binary. Claude produced the proofs and the Rocq kernel checked them. The aggregate report covers 239 entry points across 123 libraries and about 180 million lines of proof.

That result changes the bottleneck, but it does not remove human work. Previously, writing hundreds of thousands of proof lines per target made formal methods impractical for ordinary software. An agent can explore that space at scale; the team must still decide which property matters, review the statement, pin the environment, and accept the trusted base. The useful output is not persuasive model prose but a reproducible chain across binary, specification, proof, and checker.

Fuzzing searches for counterexamples: it runs many inputs and succeeds when it finds one that breaks a property. It is essential, but a finite campaign cannot traverse an infinite space. The published flow reuses the target as an executable specification. It compiles a plain version and versions with AddressSanitizer or UndefinedBehaviorSanitizer, turns the binaries and their environment into formal definitions, and states that both executions agree for every covered input. If the harness calls abort when a property is violated, proving that error unreachable also proves the property encoded by the harness.

The agent attempts to construct a proof in Rocq. If it discovers that the statement is false, it can expose a bug or propose a patch; the binary, statement, and proof must then be regenerated. If it completes the proof, Rocq does not trust the model's reputation: it checks every step against small rules. The public repository pins versions of the checker, Linux process model, binaries, and their hashes, and provides offline verification commands. That independence is the difference between an LLM answer and formal evidence.

The aggregate publication and public release are not identical. When consulted on October 26, the public README listed 60 entry points with proofs across 25 libraries, while Anthropic reported the full effort across 239 entry points and 123 libraries. The distinction matters: a research claim can include artifacts withheld because of unpatched bugs or material not yet published. A technical buyer should audit what is available rather than assume the entire announced result is reproducible today.

Imagine a company that receives signed payment webhooks and maintains a native parser for high volume. This example is hypothetical. The selected risk is not proving that every payment is booked correctly; that mixes networking, clocks, retries, and accounting rules. The pilot starts with a narrow property: for every payload up to a stated size that enters through the harness, the parser does not access memory out of bounds and the instrumented build preserves the same observable outputs as the plain binary within the accepted model.

The team pins the commit, compiler, flags, dependencies, and architecture. Security reviews the statement; engineering keeps tests and fuzzing to find failures outside the formal scope; a separate pipeline rechecks the proof in a checker pinned by digest. If the agent proposes changing the parser to make the theorem provable, the patch goes through ordinary review and the team either requires an equivalence proof or documents the difference. The proof is attached to the release as evidence for that property, not as a global certificate for the service.

First, the statement must name a property the business understands: memory safety, round-trip behavior, equivalence, or a concrete invariant. Second, scope must pin inputs, limits, architecture, operating system, memory, concurrency, and observable behavior. Third, provenance must link the commit, dependencies, compiler, flags, binaries, and hashes; a proof about different bytes does not cover the release. Fourth, the trusted base must be explicit: checker kernel, allowed axioms, machine model, and tools that turn the executable into a formal representation.

Fifth, checking must be independent from the agent and fail closed in CI if an artifact changes, a disallowed axiom appears, or the proof stops compiling. Sixth, bug, patch, and proof are separate deliverables: a model can trivialize a theorem by changing functionality, so every change needs review and, where appropriate, behavioral equivalence. Seventh, the guarantee must map to the real deployment and retain a visible scope label. If production uses dynamically linked x86, multiple threads, and glibc, a proof about a static, single-threaded RISC-V binary is useful research, not yet a release approval.

The pilot should start with one or two high-risk components with a small boundary: parsers, decoders, supporting cryptography, or transformations with a clear algebraic law. Preserve the baseline of tests, sanitizers, and fuzzing; verification does not replace them because they target different failure classes. Record how many targets were formalized, how long each attempt took, what it consumed, how many statements were proved, which counterexamples appeared, and how many findings survived human review. Do not extrapolate the result to the entire library.

The most useful comparison is not agent versus human in the abstract. Compare three decisions: continue with dynamic testing alone; add formal attempts for selected components; or require a proof as a gate for certain releases. Measure time to evidence, cost per accepted property, maintenance when code changes, coverage of the deployed binary, and reduction in the risk that actually matters. An attempt that produces no proof can still be valuable if it discovers a reproducible bug; a cheap proof can be useless if its statement does not represent the operational risk.

The primary risk is the gap between model and reality. The repository itself warns that its Linux process semantics are incomplete and that published proofs concern static RISC-V binaries, not source code or x86-64 builds. Sanitizers do not detect every failure; one target covers what is reachable from that entry point, not the entire library; and the published agreement statements do not prove termination. Concurrency, dynamic linking, hardware, unmodeled system calls, and incorrect caller usage can remain outside scope.

There is also automation risk. An agent optimized to finish the proof can reduce functionality, weaken the harness, or exploit a vacuous statement. Anthropic acknowledges this reward-hacking path and describes patch penalties and audits; a product team should add separation of duties and mutation tests showing that the harness fails when the property is broken. Finally, unpublished artifacts should not become a marketing badge: reusable evidence is what a third party can inspect and recheck.

AI-assisted formal verification already deserves a pilot when there is critical code, a bounded property, and an independent checker. It does not yet deserve to replace an AppSec program or approve an entire system by association. The prudent decision is to build a ladder: select one component, write a useful property, pin the binary, check the proof outside the agent, and compare its scope with production. Only then should the team decide whether the guarantee becomes optional evidence or a mandatory gate.

If your team needs to turn coding agents into an auditable pipeline, the valuable work starts with the evidence contract: what the agent may change, who reviews the statement, and which system preserves the decision. Wasyra designs custom agent and software workflows with explicit permissions, evaluation, and traceability. The goal is not to promise an absence of bugs; it is to put a checkable artifact behind every technical claim.