What a Software Proof Covers in an Agent Deployment

A formal proof can establish a software property across every input within its stated bounds. Using that result in an agent deployment requires knowing which executable, entry point and operating conditions the proof actually covers.

Anthropic's October 22 report, LLMs are making formal software verification feasible at a much larger scale, makes that connection concrete. Working with Theorem, the team used Claude to produce proofs checked by external verification software, rather than asking a model to judge whether its own code looked correct.

From testing examples to proving a stated property

The researchers start with existing OSS-Fuzz entry points: developer-written ways to feed inputs into a library and detect failures. They compile these test programs into RISC-V machine code and express a property over a formal model of the processor and Linux processes.

Claude writes the proof; the Rocq proof checker checks it. Anthropic reports completed proofs for 239 entry points across 123 libraries, sometimes after patching bugs found during the work.

That can establish more than passing many sampled tests. A proof covers all inputs within the theorem's bounds, provided its trusted models and checker are correct.

The bounds remain important. The reported OSS-Fuzz work concerns specified single-threaded, statically linked RISC-V Linux binaries, fixed memory budgets and inputs below 64 MiB. It does not cover every library entry point or every kind of memory error.

The tested program and the deployed program can differ

Consider a hypothetical insurance agent extracting information from uploaded claim documents. A parsing library may have a proof for one input entry point in a particular build. The deployed tool might call a different entry point, link different dependencies or run on another processor.

Those differences determine whether the proof applies. A proof about crash-freedom also does not establish that the agent extracted the correct claim number or was permitted to disclose the document. Those require different properties and evidence.

The report's technical appendix goes further. AddressSanitizer adds runtime checks that expose certain memory errors, but ordinary users generally run a build without that instrumentation. The team therefore proves properties of both builds and their relationship.

Matching observable traces alone is insufficient: under the appendix's definition, a crash in one program and a silent infinite loop in the other can look equivalent. Separate crash-freedom proofs are needed for both. The exact theorem matters more than a broad label such as verified software.

Improving the program must preserve its purpose

The work also connects to governed improvement. When Claude found a bug, it could patch the program, regenerate the specification and continue proving the revised binary.

Anthropic explicitly identifies the risk in that loop: replacing useful code with code that trivially never crashes could satisfy the narrow objective. It reports penalizing patches, rewarding evidence about the inputs whose behavior changed, and auditing the changes.

For WTK, the question is how qualification evidence could retain the proved property, exact software version, modeled environment and caller obligations alongside the deployed package. A changed dependency or build needs an explicit assessment of whether the earlier evidence still applies.

The factory also needs to distinguish repairing an implementation from weakening its required behavior. Our success-definition approach places those requirements and delegated limits outside the candidate's unilateral control.

That could move human effort toward choosing properties, reviewing assumptions and handling consequential changes, while agents construct proofs and automated checkers validate them. The proof-writing model can be fallible without making its accepted proofs mere model opinions. The remaining question is whether the checked theorem describes the software and behavior the deployment needs.

Sources

Anthropic Frontier Red Team and collaborators with Theorem, LLMs are making formal software verification feasible at a much larger scale, October 22, 2026, and its six-page technical appendix. See Turning tests into proofs, Limitations, footnotes 5–6, and appendix pages 1–2. The insurance example and WTK interpretation are ours.