From fuzz tests to proofs: inside an AI verification workflow

An AI-written proof becomes useful to a software maintainer when someone else can identify the exact program, inspect the promised property and check the argument without trusting the model that produced it. That is the practical standard for assessing the verification workflow Anthropic and Theorem published in October. The interesting artifact is neither a confident explanation nor a large proof file. It is the connection between a specific executable and a statement a maintainer actually needs.

TL;DR

• Treat the executable, property, execution model and proof checker as separate artifacts.
• A successful theorem can cover all inputs within its stated domain while leaving important product behaviours outside that domain.
• This article inspects documentation. The Frontier Wire has not rerun the proof toolchain or measured its costs.

Anthropic’s October 22 report describes Claude-generated, Rocq-checked proofs for security properties of compiled RISC-V programs. The work begins from existing fuzz targets. Its no-crash results are conditional on input bounds and a model of execution; they are not a declaration that entire libraries contain no bugs.

The published artifacts make a more useful story possible: following a prospective maintainer from a test harness to a release decision. The walkthrough below is a proposed assessment procedure, not an account of a reproduction we performed. It also explains why a narrower, well-understood theorem can be more valuable than an expansive claim that nobody can connect to a deployed system.

The harness is part of the specification

A fuzz target is a small program that passes generated input into an interface under test. LLVM’s libFuzzer documentation describes coverage-guided mutation: the engine uses information about reached code to guide the creation of further inputs. The target determines which interface those inputs exercise. Coverage of that target therefore differs from coverage of everything the library can do.

Consider a hypothetical image library with three entry points: read a file, resize a decoded image and write a file. A harness that only calls the reader cannot establish properties of the writer merely because both belong to the same project. It might also call the reader with a restricted configuration that disables a difficult format. These choices can be reasonable. They must become visible when the evidence is described.

For a maintainer, the first review question is consequently about the harness, before the proof language. Which public interfaces does it invoke? Which configuration values come from the generated input? Which are fixed? Does it check an output, or merely wait for the program to return? A proof can faithfully establish a weak harness property. More generated proof text cannot strengthen the underlying specification.

A useful exercise is to translate the harness into plain language without using the word correct. For example: for any admitted byte string, attempt to parse one document with these flags, then release all returned objects, without triggering this class of failure. This is intelligible enough for a product engineer to compare against an actual use case. If nobody can write that sentence, reviewing the theorem’s implementation is premature.

OSS-Fuzz’s integration guidance recommends keeping fuzz targets with the project, maintaining a seed corpus and running regression checks. Those habits also help a proof project: a maintained harness is less likely to quietly drift away from the interface users depend on. They do not, by themselves, establish that the harness expresses every important requirement.

A failure detector supplies a particular property

Many developers encounter memory errors through a sanitizer. Clang documents AddressSanitizer as compiler instrumentation combined with a runtime, with detection for categories including out-of-bounds access and use-after-free. That is a concrete failure detector, not a complete definition of program quality.

The distinction becomes clear in a hypothetical decimal parser. It might safely read every input and return zero for all of them. Such an implementation could avoid memory errors while failing every useful business requirement. Conversely, a parser might calculate the expected answer on familiar inputs while reading outside an allocated buffer on an unusual one. Functional behaviour and memory safety answer different questions.

A serious assessment therefore records what produces a failing execution. Is the relevant property absence of a sanitizer report, absence of a failed assertion, agreement between two binaries, or allowed termination? A label such as verified parser is too coarse to answer that question. The meaningful sentence names the detector and the relationship the proof establishes.

Assertions can add semantic content. In a hypothetical encoder, a harness could encode an object, decode the result and compare the recovered object with the original. But the comparison itself becomes part of the specification. Does it compare every field? Does it ignore ordering appropriately? Does it silently discard unsupported values before testing? Each answer changes what success means.

This creates a practical division of labour. The AI can help search for a proof, but a maintainer still has a reason to review the property. A model can be extremely effective at proving the wrong statement if the task points it there. The safeguard is not to demand a more persuasive explanation. It is to make the relevant program behaviour explicit enough that an independent checker can assess a precise claim.

The executable carries the identity

Theorem’s build contract describes a cross-compilation workflow for static RISC-V Linux programs and manifests containing binary hashes. It explicitly distinguishes that environment from an ordinary OSS-Fuzz build. Compilation runs without network access after image construction. The contract is a useful place to inspect what is actually being proved.

This matters because a source repository name does not uniquely identify an executable. Imagine two releases from the same commit. One enables a rarely used parser extension; another disables it. They may differ in reachable behaviour even though their source revision is identical. Compiler options, dependency versions and generated files can introduce further differences. A theorem about one executable needs a clear connection to the artifact being distributed.

The assessment record should therefore include the source revision, dependency inventory, compiler and linker configuration, build image identity and digest of each relevant executable. These fields support a chain of questions rather than a decorative provenance section. Can another person rebuild the artifact? If the bytes differ, is the difference understood? Does the theorem refer to the bytes the maintainer plans to trust?

Suppose a release pipeline later rebuilds the source using a new optimisation setting. Even if the new build appears to work, the old executable identity no longer establishes that the new bytes satisfy the same theorem. The team can decide to recheck, prove an appropriate equivalence or retain the originally verified artifact. What it cannot establish by naming the same library is that the old result automatically transfers.

This is why verification work belongs near release engineering. A proof stored in a research branch is evidence about that branch’s artifacts. To influence production assurance, the project needs a durable way to associate release artifacts with the properties established for them. Our guide to software benchmarking and version parity examines a related identity problem: conclusions weaken when the tested and described builds diverge.

The execution model defines the world

A formal proof reasons within definitions. Theorem’s Linux process semantics repository supplies a model for a Linux process running a RISC-V binary and warns that the model is incomplete. Its scope document identifies restrictions including single-threaded execution, no signal-handler execution and limitations in filesystem modelling. These are material conditions, not footnotes to erase in a summary.

For a hypothetical command-line converter, a single-threaded model might align with the executable’s normal design. For a multithreaded service using the same underlying library, it does not establish the behaviour of interleaved requests. The right response is to identify the boundary, rather than treating the narrower result as either useless or universally applicable.

A maintainer can make this comparison using a two-column document. The left column describes the theorem’s environment. The right describes the actual product environment. Any mismatch becomes a question requiring a separate argument or additional evidence. The exercise is especially useful because a product team may assume that common words such as Linux or memory imply more environmental coverage than the formal definitions provide.

This table is a suggested maintainer worksheet. It is not a claim that every published project has completed those checks. Its purpose is to prevent the binary question of whether a project is verified from replacing the more informative question of which behaviour has evidence behind it.

The public subset needs its own description

The published proof repository lists the entry points available for inspection and describes the theorem forms used in the release. At inspection, its README listed 61 entry points across 26 libraries, with proofs checked using Rocq 9.2.0. That public inventory is a different object from the broader experiment described in the announcement. Readers should follow the artifact list when asking what they can check themselves.

The repository explains both agreement-style statements, relating instrumented and plain binaries, and allowed-termination statements. Rather than collapse them into a single no-bugs category, a reviewer should follow the statement associated with the chosen entry point. The proof name is a starting point; the definitions and premises establish the claim.

A useful documentation convention would give every release three separate summaries: the overall research campaign, the public artifacts included in this release and the properties relevant to a particular downstream use. This is a proposed reporting practice. It prevents a large campaign total from being mistaken for the smaller set a reader has actually downloaded or inspected.

For example, imagine that a library provides twelve public interfaces, two harnesses have public proofs and only one harness matches a downstream application. The campaign, repository and application can all be accurately described, but their counts answer different questions. Advertising the largest number at every layer makes the evidence less useful to the person deciding whether an application risk has changed.

The same discipline applies to unsuccessful work. A proof failure can reflect a real defect, an inadequate lemma, a modelling limit or an exhausted search budget. Without investigation, it does not identify which explanation is correct. A publication that reports only completed theorems can still provide valuable artifacts, but it does not establish the cost or success rate for an arbitrary new codebase.

Checking is a reproducible task with prerequisites

The essential separation is between generating an argument and checking it. In the published workflow, the model produces proof material; the proof system assesses whether that material establishes the specified theorem. A maintainer should be able to evaluate the latter step without accepting the former agent’s confidence as evidence.

For an actual reproduction, the record should begin before running commands. Fix the release revision, record the host environment, identify the documented toolchain and decide which theorem will be checked. Save the output and final status. If dependencies or commands differ from the release instructions, record those deviations explicitly. A failed run should remain a failed run until the cause is understood.

The release semantics document adds an important qualification: proofs attach to a particular version of the execution model. It also documents a known divergence involving a memory-remapping case. This shows why a successful local build and an applicable real-world claim are separate reviews. The model’s stated boundary must still match the execution one cares about.

There is no need to pretend that a newsroom’s documentary review performed this engineering work. This article has not installed Rocq, rebuilt the binaries or checked the proofs. Its findings concern what the documents make available and what a responsible reproduction would need to demonstrate. That distinction lets a reader use the worksheet without interpreting it as an endorsement of unperformed tests.

For a maintainer commissioning such work, an economical pilot would choose one important interface and one clear property. It would aim to establish a complete chain from artifact identity to checked statement, then inspect the cost of maintaining that chain across a change. A very large first pilot can obscure whether difficulty came from the software, toolchain, specification or operational setup.

Changes create different maintenance obligations

Consider a hypothetical patch that alters an error message but leaves the parser untouched. The executable may still change. A team needs a policy for deciding whether to regenerate a proof, establish equivalence at the relevant boundary or treat the result as pending. This is a maintenance policy, not something a prior theorem can choose on the team’s behalf.

Now consider a different patch that adds a compressed-input mode. Even if existing proofs still check for the original harness, they may say nothing about that new interface. A green check on an unchanged theorem would be accurate while the release’s practical attack surface expands. The assessment should track feature coverage as well as theorem health.

A third change widens an allowed input limit. If the original claim included a bound, widening product acceptance changes the comparison between specification and deployment. The team might keep the old limit at the product boundary or seek a result covering the larger domain. These are concrete decisions the theorem helps expose. Neither requires dismissing the earlier work.

Theorem’s enrollment workflow asks maintainers about entry points, attacker-controlled inputs, expected outcomes and properties beyond no crash. It also asks about contribution policies and preferences for findings. Those questions locate ownership where it belongs: the project decides what behaviour matters and how suggested changes enter its maintenance process.

An effective release checklist should consequently name an owner for the harness, an owner for the deployment comparison and an owner for proof-toolchain updates. These responsibilities may belong to one person in a small project. The point is that a model’s ability to produce a theorem does not itself assign responsibility for keeping the claim relevant next month.

A useful disagreement about expected failure

A final hypothetical case shows why specification review needs a maintainer rather than a popularity vote on model answers. Imagine an archive reader that rejects an unusually large expansion. One contributor calls the rejection a bug because the archive is syntactically valid. Another calls it essential protection because accepting the archive would exceed the service’s resource budget. Both can agree on the bytes and disagree about the desired behaviour.

The verification task cannot settle that product decision without being told which outcomes count as acceptable. If rejection is permitted, a proof might faithfully establish a safe refusal. If every syntactically valid archive must expand, the requirement is stronger and may conflict with the chosen resource limit. The useful work is to expose that conflict before an agent spends effort proving a statement nobody intended to ship.

This example also distinguishes a programme’s own limit from a theorem’s analysis limit. A service can reject larger inputs at its boundary. Separately, a proof may cover only a bounded domain because of how the formal task was constructed. The two limits should be compared explicitly. A bounded proof does not imply the service actually enforces its presumed bound, and an enforced bound does not establish that every admitted request behaves safely.

There is a straightforward acceptance test for the documentation, even before anyone checks a proof: ask two engineers to describe which requests the guarantee covers. If one includes compressed payloads, background threads or a different executable and the other does not, the release note is ambiguous. Tightening the wording resolves a communication defect that no additional proof generation can fix.

This is also where a maintainer can preserve the value of an incomplete result. Rather than postpone every benefit until the whole application is formalised, the team can isolate an important conversion step with a documented interface, enforce its input contract and retain separate evidence for the surrounding system. That is a proposed design option, not a measured result of the published campaign. It gives the theorem a well-defined role instead of turning it into a claim about everything nearby.

Tests and proofs cover different uncertainty

The useful decision is rarely whether to choose tests or proofs in the abstract. Testing can exercise actual integrations and environments that a formal model does not cover. A proof can establish a property over a stated domain without sampling every input. Their value depends on the question, the harness and the connection to the real deployment.

The seL4 verification overview provides a broader example of reporting assurance together with assumptions. It describes machine-checked properties and separately points readers to assumptions about matters such as hardware and boot code. It is not evidence that this newer workflow inherits seL4’s guarantees. It illustrates a useful reporting habit: make the trusted boundary as discoverable as the positive result.

For the hypothetical image service, a sensible assurance plan might combine a checked parser property, integration tests for request handling, load tests for resource exhaustion and review of access control. Those are proposed layers, not measurements from the Anthropic project. Each layer answers a different failure question. Calling the parser verified should not cause the others to disappear from the release plan.

This also changes what a manager should ask an AI verification vendor. Request the artifact manifest, the plain-language property, the theorem’s premises, the checker instructions and a maintenance story. Ask which parts remain human assertions. Ask what changes invalidate the evidence. A lengthy proof and a successful demonstration are less informative without those details.

For readers approaching this from model evaluation, the connection to reading a model card like an auditor is direct. A capability description becomes useful when it identifies the object assessed, the conditions and the missing evidence. Formal methods can make one part of that evidence unusually strong. They do not eliminate the need to describe its scope.

There is one further advantage to keeping these claims separate: a negative finding becomes actionable. If a deployment mismatch is discovered, the team can identify whether the gap concerns the executable, the property or the environment. It need not throw away every existing artifact. A missing writer harness calls for a different addition than an unsupported operating-system feature. Those distinctions let a small project spend scarce review time on the part of its assurance case that actually changed.

A maintainer can also ask for a release note written before the proving work starts. Drafting the intended sentence in advance exposes whether the project wants a memory-safety result, a functional guarantee or a compatibility claim. It discourages a common evaluation mistake: measuring whatever the tool can most easily establish, then redescribing it as the original objective. The eventual note can narrow or expand with evidence, but the original question remains available for comparison.

The practical outcome is a smaller, sharper sentence a maintainer can defend: this identified executable satisfies this checked property under these stated conditions. That is a meaningful improvement over believing that a library is probably safe because many generated tests have passed. It is also a claim precise enough to survive contact with the next release.