What a Proof Can Leave Unfinished

The strongest aid in a new software-agent benchmark is a document the agent did not write.

On the 500 issues in SWE-Proof, researchers gave a coding agent a formal specification of the behavior a fix was supposed to produce. The specification was not another test. It described an obligation that a verifier could check across the full input domain it covered. Across four repeated evaluations using the Nagini backend, Claude Opus 4.8 rose from a mean 85.0% resolution without the specification to 96.4% with it.

The obvious lesson is that the specification was the missing thing. Write down exactly what “fixed” means, and the rest becomes easier to check.

Then the researchers tried the same idea on larger repository changes.

There, the formal specification stopped helping. On the 242 SWE-bench Pro tasks that the benchmark could model under all four of its specification backends, an agent told only where to work did better than an agent given the formal behavioral specification. In this separate evaluation, Opus resolved 61.2% of tasks with localization alone; its supplied-specification conditions across the three formal backends ranged from 55.8% to 59.9%.

The stronger checker had not made the guide sufficient.

That reversal is more useful than the simpler story that formal verification “solves” correctness. It separates three questions that ordinary coding benchmarks often collapse into one: What behavior is required? Where in the repository must the work happen? And does the resulting implementation satisfy the obligation we actually wrote down?

A machine can become very good at the third question without making the first two disappear.

A specification gives the agent two different things

SWE-Proof starts from real repository issues in SWE-bench Verified. Its construction pipeline, Benchproofer, builds a formal specification for the changed behavior, models the new or modified code, summarizes unchanged functions with explicit axioms, and admits the result only after mechanical checks and adversarial audits agree. The benchmark supports three proof-oriented backends—Nagini, Velvet, and Lean—plus a structured-natural-language condition used for comparison.

A verified implementation gets a much stronger guarantee than a test-passing one. Tests examine selected cases. A proof establishes that the implementation satisfies the specification for every input the specification admits, subject to the axioms the proof assumes.

That distinction matters because tests really do let wrong patches through. In an independent study of SWE-bench Verified, PatchDiff found that 7.8% of patches counted as correct failed additional developer-written tests. Its differential testing also found behavioral differences from the human patch in 29.6% of plausible patches, with manual review identifying a subset as certainly incorrect. A green test suite is evidence. It is not a complete description of intended behavior.

SWE-Proof makes that incompleteness visible. When the researchers took patches that had passed the ordinary hidden tests and attacked them with counterexamples derived from the formal ground truth, a substantial fraction fell apart.

But a supplied specification changes more than the correctness oracle. It also tells the agent which functions matter.

That is easy to overlook. If a contract names a function and describes its inputs and outputs, it carries both semantic information—what must be true—and localization information—where to look. SWE-Proof includes a control that supplies localization without the behavioral contract. Comparing those conditions lets the researchers separate the two effects.

Across the same four Nagini evaluations of Opus on SWE-bench Verified, the specification-provided condition gained 11.4 percentage points over the unaided baseline. Localization alone reached 92.3%, leaving a further 4.1 points for the supplied specification.

Much of that benefit came from knowing where, not just knowing what.

That does not make the formal obligation unimportant. Four points is a material residual gain. It does change the explanation. “The model needed a precise statement of intent” is too simple. The model also needed a map from that statement into the repository.

The larger repository changes exposed the missing map

SWE-bench Verified is built from relatively local fixes. In SWE-Proof’s corpus, the gold patches average 14.3 changed lines across 1.25 files. The median patch touches one file and consists of one hunk.

The full source corpus of 266 Python SWE-bench Pro tasks is much larger. Its gold patches average 145.5 changed lines across 3.42 files and 9.84 hunks. Yet their problem statements are not proportionally longer: the median issue text is about the same size as in SWE-bench Verified.

That changes what a formal contract can stand in for.

The Pro patches often spread one behavioral change across call sites, boilerplate, support code, and other coordinated edits. The formal specification, by design, models the behavioral core. The paper reports that the Pro tasks change a mean of nine functions across three files, while the specifications themselves do not grow to model all of that surrounding work.

In that setting, a precise contract can become a spotlight. It illuminates the behavior under verification while leaving the rest of the repository dimmer.

The authors interpret the Pro reversal this way: the supplied specification concentrates the agent’s attention on a slice of the required edit. That interpretation is plausible and consistent with the corpus statistics, but it is not the same thing as an isolated causal mechanism. The experiment shows that specification-provided Opus runs did worse than localization-only runs on these tasks. It does not yet show, case by case, that attentional narrowing explains every failure.

Still, the result establishes an important boundary. A behavioral specification can be correct about the behavior it states and still be incomplete as a work plan.

Call the difference the change surface: the complete set of repository regions and coordinated edits required to finish the issue. A function contract describes a behavioral surface. The two can overlap without being identical.

That distinction is what the compact benchmark hid.

On a one-file patch, naming the right behavior may almost name the whole job. On a multi-file change, the same behavioral obligation may imply edits elsewhere: a caller must adapt to a new assumption; another representation must stay synchronized; support code must carry the new state; a public interface must change with its implementation. A verifier can be perfectly decisive about the modeled relation while saying nothing about work outside it.

The proof is only as broad as its proposition

SWE-Proof is unusually explicit about this limit.

Its core guarantee begins with a specification, a set of axioms, a formal implementation, and a Python patch that is judged behaviorally equivalent to that implementation. If the implementation verifies against the specification under those axioms, then the corresponding patch resolves the benchmark instance. The benchmark spends considerable machinery checking the links between those artifacts.

But the paper names one boundary it cannot make formal: there is no guarantee that the specification itself matches informal human intent.

During benchmark construction, the system has privileged evidence. It can inspect the issue description, the known human patch, the tests, and the buggy code while building and attacking a candidate specification. During model evaluation, those gold artifacts are withheld. The result is a carefully constructed benchmark oracle, not a proof that one formal reading is the only reasonable interpretation of a user’s request.

This is not a defect peculiar to SWE-Proof. It is the old oracle problem in a sharper form. A machine can prove that program P satisfies proposition S. It cannot mechanically prove that S was what the person meant unless that relationship has itself been encoded in something the machine can check.

And if the repository change is broader than S, the proof says even less about whether the whole job is complete.

The benchmark’s own graders make the distinction concrete. Resolution says the patch passes the benchmark tests; verification says the formal implementation satisfies the submitted specification; equivalence says the formal implementation and repository patch describe the same behavior. None of those checks, by itself, makes a self-authored specification faithful to the issue. SWE-Proof needs a separate specification audit for that.

Correctness is not one gate. It is a chain of correspondences.

Writing the contract is its own hard programming problem

Once that chain is visible, another result in SWE-Proof makes more sense.

Giving an agent a ground-truth specification helps on SWE-bench Verified. Asking the agent to write its own does not. In the paper’s repeated Nagini audit, roughly half of Opus-generated specifications fail at least one property. Among those failures, the dominant problem is faithfulness: the specification constrains part of the behavior the issue requires and leaves another part free.

That pattern appears outside SWE-Proof. Verus-SpecGym turns specification writing itself into an executable benchmark. Its 581 tasks come from Codeforces problems and ask models to translate informal programming requirements into specifications for Verus. The strongest evaluated model solves 77.8% of the tasks; other frontier models land between 51.1% and 57.8%. Generated specifications omit assumptions, accept invalid outputs, and reject valid ones. An LLM judge misses 26% of the failures caught by executable tests and adversarial cases.

These are not repository-maintenance tasks, so the numbers do not transfer directly. The independent result does support the narrower mechanism: translating an informal requirement into a faithful machine-checkable obligation is itself a difficult synthesis problem, even when the implementation problem is relatively clean.

A promising response is to preserve more traceability during that translation. VeriSpecGen, on a different formal-specification benchmark, decomposes natural-language requests into atomic requirements, generates tests targeted at those requirements, records which test corresponds to which clause, and repairs failed clauses selectively. With Claude Opus 4.5 it reaches 86.6% on its VERINA specification-generation task, 27.6 percentage points above that model’s matched baseline.

That result does not prove that requirement traceability will solve multi-file repository work. It suggests a useful direction: do not ask one formal artifact to carry every relationship implicitly.

The repository case needs at least two kinds of traceability. One connects the informal request to the behavioral obligation. Another connects that obligation to the change surface where the repository must actually be edited.

SWE-Proof measures the first problem directly and exposes the second by transfer.

Some work does not fit the contract at all

The sharpest boundary appears before an agent ever gets to solve the task.

Benchproofer attempted to construct verified twins for 266 Python tasks from SWE-bench Pro. It produced bundles that passed every backend for 242. Twenty-two failed under all of the proof backends for the same basic reason: the requested change did not alter behavior that the benchmark’s pre- and post-condition specifications could observe.

Sixteen of those tasks primarily renamed or relocated code. Two changed function signatures. Two changed internal data structures. Two changed external side effects outside the value domain the contracts modeled.

There is nothing paradoxical about that once the representation boundary is visible. A precondition and postcondition can be excellent tools for saying how a function maps admissible inputs and state to outputs and state. A repository issue can also ask for something whose correctness lives in naming, placement, architecture, representation, or interaction with the outside world.

Making one relation machine-checkable does not turn every neighboring relation into the same kind of thing.

That is the practical consequence of the Pro reversal. Stronger verification can move a bottleneck upstream—from testing the patch to stating the obligation—but it can also reveal another boundary beside it: the distance between the obligation and the complete repository change.

A coding system that wants stronger guarantees therefore needs more than a better final checker. It needs to retain enough provenance to ask which requirement produced which obligation, which obligation implies which edits, and which parts of the job remain outside the verifier’s field of view.

The proof can tell you whether the code kept the contract. The repository can still be asking for more.

Sources

• George Ma et al., “SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?”, version 2, September 22, 2026.
• You Wang, Michael Pradel, and Zhongxin Liu, “Are ‘Solved Issues’ in SWE-bench Really Solved Correctly? An Empirical Study”, 2025.
• Anmol Agarwal et al., “Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization”, 2026.
• Zhe Ye et al., “Intent-aligned Formal Specification Synthesis via Traceable Refinement”, 2026.