AI-generated proofs need a precise contract

What changed this week

On October 22, 2026, Anthropic reported work with Theorem using Claude to construct machine-checked proofs for 239 test entry points across 123 open-source libraries. The reported main experiment concerns compiled RISC-V programs and bounded inputs under specified execution assumptions. It is a research result reported by the organizations involved; Metrosion has not independently reproduced the experiment.

The public OSS Verify repository provides a smaller released collection: its current README lists 60 entry points across 25 libraries, checked using Rocq. It explicitly describes limits in its model of Linux processes. The difference matters: the released artifacts and the broader reported experiment are related evidence, with different scopes.

Our practical interpretation is that engineering teams should begin evaluating proof production as a possible part of release assurance. The immediate opportunity is a narrow, inspectable contract for an important component. A general promise that an application is safe would be much harder to justify.

Make the claim reviewable

A useful assurance record should answer four questions: which exact artifact was checked, which property was established, what assumptions were made, and what execution environment those assumptions describe. We recommend putting those answers beside the release identifier so reviewers can trace the claim without reading an entire proof.

For a hypothetical document-processing service, the first candidate might be a small parser accepting an explicitly bounded input format. The proposed claim could concern rejection of malformed lengths. The team should separately record authorization, resource consumption, and downstream rendering as concerns requiring their own evidence. This inventory prevents a narrow success from silently becoming a broader product claim.

Ask an engineer who did not write the specification to explain it in ordinary language. If that explanation differs from the intended customer behavior, resolve the disagreement before funding a larger verification effort. A mathematically precise statement can still be the wrong engineering requirement.

Keep the target stable while agents work

We recommend separating proposal authority from acceptance authority. An agent can draft a proof and suggest code changes, while a controlled checker evaluates the frozen theorem. Any proposed alteration to the specification should trigger a separate review. This makes it easier to see whether progress came from better evidence or from changing the question.

In the hypothetical parser pilot, an agent might suggest rejecting every input to make a safety property easier to establish. That would undermine the intended feature. Acceptance criteria should therefore include representative valid inputs and the business requirement that supported documents remain usable. Review code changes and the original requirement together.

The report itself cautions that its results do not establish universal absence of bugs: platform assumptions, incomplete coverage, and caller behavior limit the conclusions. Our recommendation is to maintain an explicit list of excluded behaviors and assign an owner to each remaining risk. That list should travel with the proof when the dependency is upgraded.

Budget for maintenance, not only discovery

A successful pilot should measure more than whether a proof eventually checks. Track expert review time, generation cost, checking cost, failed attempts, and the work required after a realistic code change. A result that is affordable once may still be expensive to keep current through frequent releases.

Choose a component whose boundaries are stable and whose failure would matter. A small dependency used across several services may offer more practical value than a rapidly changing interface. Keep ordinary tests, fuzzing, and operational monitoring in the pilot; each can expose concerns outside the chosen formal claim.

Our proposed release record includes the artifact digest, toolchain versions, specification revision, checking result, and documented assumptions. Rechecking that record should be reproducible by a second engineer. Treat missing or stale evidence as an incomplete assurance task, rather than carrying a previous successful label forward automatically.

A concrete next step

Select one bounded component this week and write a one-page verification contract before introducing an agent. Have the component owner identify one meaningful property, one known failure example, and three important behaviors outside scope. Then attempt a time-boxed proof exercise with a fixed spending limit.

The decision at the end is whether this technique adds useful, maintainable evidence for that component. Publish the limitations internally alongside the result. The strongest outcome may be a checked proof, a newly understood defect, or a better specification; each is more useful than an unexplained assurance badge.