Claude wrote software proofs. Here is what they actually guarantee

A software proof can rule out an entire class of failures within a defined boundary. It can also be described so loosely that readers think an application has guarantees nobody established. Anthropic and Theorem’s recent work makes that boundary a practical issue for teams using AI to write and inspect code.

Their 22 October account reports Claude-assisted proofs of properties of compiled open-source software, with a public subset available for inspection. The result concerns specified executions and assumptions, rather than every possible bug in the underlying libraries. The research announcement describes a broader effort than the released artefacts alone.

The important development is a division of labour: a model helps produce a formal argument, and a separate checker assesses that argument against a statement. The difficult human question moves toward the statement itself. Is the property useful, does the model of execution match the intended environment and does the deployed binary fall inside the evidence?

A proof begins with a sentence that could be wrong

Consider a hypothetical image-processing service receiving files from users. “This service is secure” is too broad to serve as a useful first specification. The service has parsers, authentication, storage, scheduling and output handling. Different failures across those components need different properties and evidence.

A narrower sentence might say that a particular parsing entry point does not trigger specified error conditions for eligible inputs in a defined execution model. That sentence is less glamorous, but it can become a formal obligation. It identifies what must hold, where it must hold and which cases are outside the claim.

The distinction is not rhetorical modesty. A customer deciding whether to accept untrusted files needs to know whether the result concerns a parser, its caller or the complete service. A theorem about one entry point cannot automatically justify an assumption about authentication or the handling of uploaded files after parsing.

Imagine that the parser correctly rejects an invalid image, but the service stores it in a publicly accessible bucket. The parsing property may remain true while the application has a serious problem. Formal verification has not failed to catch a violation of its statement; the organisation asked it a narrower question than the application’s full security requirement.

A useful review therefore starts with a plain-language version of the theorem. A domain owner should be able to explain why the property matters. A formal-methods reviewer should confirm that the formal statement represents that property. A systems owner should identify whether the real deployment satisfies its premises. These are complementary responsibilities.

This is relevant to our coverage of AI guardrails, where controls operate at particular points in a system. A guarantee cannot exceed the boundary it controls. The difference here is that a formal proof can establish a strong mathematical relationship inside a deliberately specified boundary, rather than merely observe a collection of successful examples.

Quantifiers carry the strength and the limit

“Every eligible input” is much stronger than “every input tested so far”. But “eligible” has to be defined. An input-size bound, a launch configuration or a modelled environmental condition can determine which executions belong to the theorem. Removing those words from the public explanation changes the claim.

A reviewer should look for both the universal statement and its domain. A proof over a bounded set of inputs can be very useful. It is not made less valuable by stating the bound. The misleading step is to remove the bound while keeping the rhetorical force of universality.

The same discipline applies to outputs. “Terminates with an allowed status” and “returns the correct image” are different properties. A program could return a permitted error on every input and satisfy an inadequately chosen status requirement while doing no useful work. The specification needs to exclude behaviour the application would consider unacceptable.

The public release is a set of particular artefacts

The OSS Verify repository inspected on 5 November lists proofs for 61 entry points in 26 libraries. It describes statements about compiled fuzz targets, including relationships between sanitizer and plain builds or allowed execution outcomes. Those public artefacts are narrower than a claim about entire libraries or all results in the announcement.

The repository also identifies the proof environment and formal process model. A reader evaluating the release should inspect those artefacts directly rather than assume that the headline count corresponds to a downloadable proof for every named case. Publicly inspectable evidence and an author’s report of a broader effort have different roles in verification.

For our hypothetical image service, the first task would be to identify a relevant entry point and binary. A package name alone is not enough. Which version was built? What code path does the target call? What checks does it assert? Which execution outcomes are allowed? The answers determine whether the proof concerns a property the service needs.

A proof package should therefore be treated like a reproducible technical record. It contains a statement, dependencies, an identified artefact and checking instructions. A successful recheck supports the derivation in that environment. It does not mean the reviewer has independently validated every component of the execution model or matched it to the production service.

This division is useful for procurement. A supplier can provide a precise artefact and explain the intended application. A buyer can review the scope rather than negotiate around an undefined “verified” badge. If the supplier changes the binary, the record should make it obvious that a previous proof needs an applicability review.

The practical value can be substantial even when coverage is partial. A widely used parser entry point may be important enough to justify strong assurance on its own. But that value should be described through the entry point and property, not enlarged by association with the entire library’s reputation.

The table is a reading guide for the released evidence. It is not a claim that our hypothetical service has been verified.

The machine model is part of the result

The Linux process semantics repository describes a Rocq model for a Linux process running a 64-bit RISC-V binary. It explicitly calls the model incomplete and points readers to assumptions and gaps. A proof about a formal execution has to be interpreted through that model before it becomes evidence about a real machine.

The separate scope document identifies supported systems and restrictions including a single-threaded model without shared-memory interleaving or signal-handler execution. It also records cases outside the model. These are not incidental implementation notes: they decide which real-world uses a statement can address.

A hypothetical web service might run on another architecture with dynamic linking and concurrent requests. It could use the same source library while differing in precisely the conditions relevant to the proof. The source relationship is useful context, but it is not an argument that the verified binary and deployed service behave identically.

The release semantics documentation further pins the model version used by the proof release and warns that a proof about one version says nothing about another automatically. It documents a known divergence involving memory remapping behaviour. That specificity is a strength of the evidence record because it directs reviewers to a concrete limitation.

A sensible applicability review should therefore compare the production environment against a written assumption list. Mark each condition as satisfied, unsatisfied or unresolved. Where the environment differs, identify whether a separate theorem or validation step closes the gap. Do not replace the unresolved column with a general statement that the technology is promising.

This approach also helps prioritise research. If many important deployments differ at the same boundary, expanding the execution model could be valuable. If a deployment already lies inside the supported conditions, the next task may instead be proving another property or covering another entry point. A clear boundary tells engineers where additional effort could change the conclusion.

An assumption deserves an owner

Some assumptions are technical statements a specialist can inspect. Others concern how the software will be operated. A production team should assign responsibility for keeping the latter true. If a deployment later enables concurrency or changes a linked component, someone needs to recognise that the assurance argument may have changed.

An assumption register should travel with release configuration. It should identify which changes require review and how those changes are detected. Otherwise, a proof can remain mathematically valid while the organisation quietly stops running the system it describes. The problem is stale applicability, rather than a broken mathematical argument.

This is why proof maintenance belongs in ordinary engineering change control. A verified artefact is a valuable dependency with explicit conditions. It should not live only in a research folder disconnected from the people who build and deploy the application.

Fuzzing and proof search ask related but different questions

Fuzzing searches for executions that expose a problem. A proof attempts to establish a statement over the specified set of executions. A long unsuccessful search for a counterexample and a checked derivation are therefore different kinds of evidence, even if both concern a similar failure condition.

The libFuzzer documentation describes a coverage-guided engine that feeds inputs through a target and uses observed code coverage to guide mutations. The target is an intentionally chosen interface into the software. Its design affects what behaviour the search can reach, which is why a passing campaign does not establish that every library operation was exercised.

AddressSanitizer’s documentation describes compiler instrumentation and a runtime for detecting specified memory-error classes. It also states that its runtime is a bug-detection tool, not designed as a security-sensitive production runtime. Its useful checks should not be transformed into an assertion that every possible memory or logic error has been represented.

OSS-Fuzz combines fuzzing techniques, sanitizers and distributed execution for open-source projects. The service illustrates the infrastructure already built around target functions, corpora, reports and regression handling. Formal work on related targets can build on that practical investment while adding a different form of assurance.

The relationship is complementary at the system level. Tests can find counterexamples, expose a bad specification or investigate behaviour outside an existing proof. Proofs can eliminate a search question within an established domain. An engineering team should decide what remains useful after a particular theorem is checked, rather than treating the methods as rival brands.

For the image service, ordinary integration testing still answers whether the uploaded file reaches the intended parser and whether the response is handled correctly. A parsing proof does not exercise the network endpoint. Load testing still addresses the service’s capacity under demand. A theorem about an entry point does not establish an acceptable response time or operational recovery procedure.

A counterexample is a result, not a failed project

If an attempted proof reveals that the proposed property is false, the investigation can still be valuable. The team might have found a bug, a missing precondition or an overly broad specification. The next action depends on which explanation is correct. Patching code to satisfy a mistaken property can be as unhelpful as dismissing a genuine counterexample.

The review should preserve the distinction between a proof-construction failure and a discovered violation. An AI agent may simply fail to find a derivation within its budget. That does not establish that no proof exists. Conversely, a concrete violating execution needs substantive investigation, even if another agent produces confident prose saying the code is probably safe.

Record both outcomes honestly. A release report should identify checked proofs, counterexamples, incomplete attempts and cases outside the method’s scope. That prevents the successful subset from being mistaken for an exhaustive audit of every attempted project.

AI changes proof construction without choosing the requirement

A coding model can explore strategies, reuse lemmas and write formal text. A proof checker evaluates the resulting derivation against the formal statement. The model’s confidence is not the acceptance rule. This difference is central to understanding why AI-assisted formal work can provide stronger evidence than an AI-generated code review alone.

The Rocq documentation provides the language and proof-environment background for inspecting such work. A reviewer can examine the definitions, assumptions and checking process. That inspection is different from asking another model whether the first model’s argument sounds convincing.

The strongest use of automation is to move repetitive construction work into a process with a checkable endpoint. But the endpoint must remain meaningful. If an agent weakens the statement, adds an unjustified assumption or proves a nearby theorem, the resulting derivation can be valid while failing the original engineering requirement.

Our hypothetical team should therefore separate authority to propose from authority to approve. An agent could suggest a specification and a proof. A reviewer would compare the statement with the intended requirement, inspect dependencies and establish the connection to the chosen artefact. The team should not allow a successful checker exit to erase the need for that comparison.

seL4’s verification overview offers a mature example of communicating strong proof results alongside explicit assumptions about the surrounding machine. Its kernel guarantees are not results of this Claude collaboration. The relevant lesson is how assurance documentation can state a powerful property without claiming that the entire real-world system has no remaining trust boundary.

A useful production process can adopt that habit. Publish a plain-language property, link the precise statement, identify the artefact and state the important assumptions. Explain what the result means for a particular deployment. An honest narrow guarantee can support a stronger decision than a broad label whose scope nobody can reconstruct.

A proposed adoption path for a small engineering team

Start with a component that has a clear entry point and a consequential property. A parser or transformation function may be easier to specify than an entire interactive application. Choose the target because the property matters, not because a demonstration happens to be available.

Write a threat or failure scenario in ordinary language. For the hypothetical image service, it might concern malformed files reaching a parsing function. Identify what failure must be excluded and what remains out of scope. A reviewer should understand why that property improves the service before the team spends time on formalisation.

Next, inventory the build. Record source revision, compiler, configuration, linked dependencies and produced binary identifiers. Identify the deployment environment separately. This prevents a later reviewer from confusing source similarity with artefact identity. The proof statement should make its target discoverable without relying on a maintainer’s recollection.

Inspect the execution model and its assumptions before interpreting success. If the proposed target requires features the model does not cover, either narrow the deployment deliberately or choose another verification route. Do not silently reinterpret the deployed service to fit the available proof after the fact.

Run the checking procedure in a documented environment. Save the result and enough provenance for an independent reviewer to repeat it. We have not performed that recheck for the released research artefacts; this is a proposed adoption procedure. A report should distinguish reading the public code from executing and validating it.

Then test the integration boundary. Confirm that the application actually invokes the intended component under the conditions the assurance review assumes. Confirm that failures and rejected inputs are handled appropriately. This work supplies a connection between the theorem and the application rather than asking the theorem to establish unrelated operational behaviour.

Finally, rehearse a change. Modify a relevant build setting or update a dependency in a controlled branch and observe which checks require renewal. A proof pipeline that works only for one frozen demonstration may still be useful research, but a maintained component needs an update process. The cost of that process belongs in the adoption decision.

Coverage should be displayed where people rely on it

A dashboard should not mark an entire repository “verified” when only selected targets carry proofs. Show the target, property, build and check date near the status. Indicate uncovered interfaces explicitly. The display should help someone deciding whether a proposed use falls inside the result, rather than merely advertise that formal methods were involved.

The same care applies to release notes. If a change alters code outside the covered target, say so without implying that the old proof evaluates the new code. If it changes the target itself, identify the new evidence or the temporary assurance gap. Versioned claims let users make informed decisions during ordinary software maintenance.

A supplier could also provide a short applicability worksheet for downstream consumers. The worksheet would ask about architecture, linking, process features and the calling pattern relevant to the theorem. It would not replace specialist review, but it would make common mismatches visible before a customer relies on the result.

Work through three changes before relying on the badge

The easiest way to expose an assurance boundary is to change one condition deliberately. In a proposed applicability review for the hypothetical image service, keep the proved artefact as the reference and consider three changes: a new caller, a new binary and a new deployment environment. Each asks a different question, so one generic regression checklist may not be sufficient.

First, introduce a new caller that passes data through an additional conversion before parsing. The old property might still apply to the parser’s eligible inputs, but the new conversion could mishandle lengths or ownership. A proof of the callee does not automatically establish that its caller meets the required preconditions. The review should identify the exact interface contract and check the new caller against it.

The application may need a separate property about that conversion, or ordinary tests may be appropriate for the remaining risk. The important point is to name the gap. Saying the application uses a verified parser would be factually compatible with an unsafe integration, so the phrase alone cannot carry the complete assurance argument.

Second, rebuild the same source with a changed toolchain or configuration. The new binary can differ even when the source diff is empty. If the statement concerns a particular binary, the team needs evidence connecting the new artefact to the old result or a new proof. A successful source review does not establish that connection by itself.

This is where reproducible builds can help an investigation: they make it easier to identify whether the artefact being discussed is the one produced by a known process. They do not prove the program’s desired behaviour. Build provenance, behavioural verification and release approval are separate pieces that should agree about the artefact’s identity.

Third, move the component into a different process environment. A previously single-threaded path may now share mutable state, receive signals or invoke different system services. The relevant question is whether those behaviours remain inside the model and theorem. An application owner should not assume that a stable library version makes every deployment context equivalent.

The review can reach several legitimate outcomes. The change may remain inside the original scope. It may require additional evidence. It may be deliberately prohibited by deployment policy. Or the team may accept a documented residual risk for a low-impact use. The unacceptable outcome is to leave the applicability question unanswered while continuing to display the same broad guarantee.

Functional correctness asks another question again

Even a program that avoids the specified crashes can return an incorrect result. In the hypothetical image service, a decoder might produce the wrong colours, omit a region or mishandle metadata without triggering the failure condition under discussion. Whether those behaviours matter depends on the service’s job. They are not made irrelevant because a stronger guarantee exists for another property.

A team choosing a first verification target should distinguish safety properties from the application’s functional contract. It might begin with memory-error exclusions because those are broadly important and easier to state. A later project could address a transformation’s mathematical result. Progress can be incremental without pretending that the first property subsumes the second.

Performance is another independent concern. A valid result produced too slowly can still make a service unusable. A no-crash property does not automatically bound resource consumption in the way the application needs. If denial of service is a concern, the team should specify which time or space behaviour it intends to establish and seek evidence for that claim separately.

The same principle applies to confidentiality. A program could compute the correct output and terminate normally while revealing information the application should keep private. A security review should identify the desired information-flow property rather than infer confidentiality from the absence of crashes. Formal methods can address powerful properties, but only when those properties are actually represented.

Our AI governance framework guide places technical controls in a wider accountability process. For software proofs, the governance job is concrete: keep claims attached to their evidence, assign responsibility for assumptions and review changes that alter applicability. This is how a mathematically precise result remains useful after it enters an ordinary engineering organisation.

The adoption question is what you can now rule out

The collaboration is interesting because proof construction may become a more accessible engineering activity. That does not require claiming that specifications are complete or that deployment differences have disappeared. The practical benefit comes from ruling out a precisely identified failure within a boundary an organisation can understand and maintain.

A team should ask what decision changes after the proof is checked. Does it permit accepting a broader input class? Does it reduce the need for a particular search campaign? Does it clarify which remaining component deserves review? If the answer is only that the repository gains a reassuring label, the assurance work has not yet reached its user.

The public artefacts make that assessment possible for selected cases. Read the property, identify the binary, examine the model and retain the assumptions. Keep ordinary testing for the questions it still answers. An AI-written proof earns trust through the checked statement and its applicability, rather than the sophistication of the agent that produced it.