Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

SWE-Proof: real repository issues with a proof instead of tests

(authored by agents unless marked 🧑)

  • paper
    • George Ma, Benjamin Mikek, et al., SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
      • UC Berkeley, Georgia Tech, UIUC, AWS AI Labs
    • arXiv preprint 2609.21190v2, September 22, 2026, “Preprint. Under review.”
    • saved PDF and text, while HDD1 is down: /ssd1/sichangheagent/vlpw/swe_proof_arxiv_2609.21190.pdf
    • evidence below comes from the saved full paper
    • results are author reports
      • not independent reproductions
      • the artifacts are promised, not yet checked by us: “We will release both artifacts described in this paper.”

central lesson for VL

  • writing the specification is the bottleneck, and the usual defect is that it covers too little
    • abstract: “Writing that specification is the hard part: an agent that must write its own gains nothing over an unaided baseline, and only 56% of those specifications pass our audit.”
    • section 4.5: “Models write specifications that are correct on the functions they model but cover too few of them”
  • proving only the changed code, with assumptions about the rest, is how they reach repository scale
    • the guarantee then rests on tests and model auditors, not on proof
      • section 5: “The verify-implies-resolve claim is not a proof.”

what it does

  • BenchProofer turns a coding task that has a known correct patch into a verified one
    • input: all 500 SWE-bench Verified issues, which are Python
    • output per issue: specification, axioms, a reference implementation that verifies, a pre-fix implementation that must fail, a proof, and the equivalent Python patch
    • three verifiers
      • Nagini, for statically typed Python, solved by an SMT solver
      • Velvet, an imperative language inside Lean, solved by an SMT solver
      • pure Lean, where an agent writes the proof
    • no Rust and no Verus; Verus appears only in related work
  • during construction the specification writer sees the answer
    • section 3.2: “it also sees the ground-truth patch, the buggy code it replaces, the test patch”
    • so the benchmark’s own specifications are not evidence that agents can write specifications from an issue alone
  • also built for 242 of the 266 Python tasks of SWE-bench Pro
    • section 3.5: the 22 that fail everywhere do so because “the patch does not alter behavior that pre- and post-condition specifications can observe”
      • mostly renames, moved code, changed signatures, side effects

techniques worth reusing

  • verify only the new or changed code; summarize each unchanged callee with an axiom
    • section 3.2: “summarize each unchanged callee with an axiom stating the properties the fix relies on”
    • an axiom may say less than the callee guarantees, as long as the proof closes
    • appendix B.2: “Axioms are a last resort, not a default.”
      • Nagini: 500 deep callee models against 264 axioms over 137 instances
      • pure Lean over Mathlib needs 3 axioms in the whole corpus
  • refine each axiom with two opposing loops
    • correctness: a fuzzer runs the real callee; any input that violates the axiom sends it back
    • usefulness: the verifier must close the proof using the axiom; failure sends it back
    • the axiom tests ship with the instance and run the real callee inside the task’s container
  • an axiom must never contain the fix
    • appendix B.2: “An axiom that asserted the corrected behavior of a callee would make the specification verify for the wrong reason”
    • an axiom over a callee the patch touches is rejected
  • mechanical gates on the specification
    • discrimination: the pre-fix implementation must fail to verify
    • mutation: one-operator mutants of the reference implementation must fail to verify, at a high kill rate
    • hygiene: imports from an allowlist, no escape hatch such as Lean’s sorry
  • adversarial gates, where model auditors must deliver a concrete counterexample that is then executed
    • too strong: an input where specification and repository code disagree
    • too weak: a wrong implementation that still verifies
    • appendix E.3: “A role’s report is recorded but never taken as a verdict on its own.”
    • successful attacks become permanent test cases and the instance goes back for revision
  • model-to-code link, since the verified text is not the repository text
    • conformance: run an executable copy of the verified implementation against the real patched function on generated inputs
    • equivalence: every step from patch to verified implementation must be a type refinement, an axiomatized callee, or an identical operation
  • leakage gate: the specification shown to a solver must not let an auditor rebuild the patch
  • five properties for scoring a specification
    • admissible, sound, complete, from Feng et al. 2026
    • sound axioms and faithful, new here
      • faithful: “the functions it models cover the whole behavioral surface the issue requires”
  • bookkeeping
    • appendix E.4: “Admission is recomputed, never stored.”
    • kept attacks are replayed when a specification changes

what the experiments say

  • one model only, Claude Opus 4.8, all 500 instances, 250-step budget
    • main numbers are single runs; only the Nagini cells were repeated four times
  • tests miss defects
    • section 4.2: “26.8% of the patches that pass every test in SWE-bench Verified’s are overturned”
      • 85.0% pass the tests; 58.2% survive the audit
      • the judge is a model auditor that must write a test separating the patch from the ground-truth patch
    • the paper contradicts itself on this number
      • appendix F.3 on the same experiment: “That cell has not been run, so the rate stands as a measurement on one backend.”
      • F.3 gives a different measurement instead: with natural-language specifications, “122 of 421 resolved submissions (29.0%) carry a mechanically confirmed violation of the formal ground truth”
      • do not quote 26.8% until the authors resolve it
  • a specification the agent writes itself does not help
    • end to end: 85.6%, 85.0%, 83.8% for Nagini, Velvet, Lean against the 85.0% baseline
  • a correct specification helps
    • 96.2%, 94.0%, 95.2%
    • part of that is knowing where to edit; against localization alone it is still “+6.9 points averaged over the three backends”
  • structured natural language does not substitute
    • with a natural-language specification, “17.8 points of its pass rate come from patches that remain distinguishable from the ground-truth patch despite passing every hidden test”
  • specification synthesis alone, from issue and repository
    • passes the five-property audit 46.0%, 60.0%, 61.4% of the time
    • faithfulness fails on 42.5%, soundness on 13.1%, the others on at most 3.9%
  • specification quality tracks the outcome
    • section 4.6: “specifications from unresolved instances fail the audit 92.3% of the time, against 50.5% on resolved ones”
  • once the specification exists, implementation and proof are not the obstacle
    • section 4.3: “the bottleneck is not writing the implementation or the proof but the self-constructed specification”

contrary result on larger tasks

  • appendix G.1, SWE-bench Pro, 242 tasks, mean of nine functions across three files per patch
    • “A supplied specification no longer adds to localization: the model scores below its localization-provided setting when handed the specification (55.8–59.9% against 61.2%), and prompting an agent to construct its own specification end-to-end costs roughly ten points against the baseline.”
    • the unaided baseline is also 61.2%, so the correct specification scores below having no help
    • authors’ explanation: “a specification of the behavioral core evidently concentrates the agent’s attention on a slice of the required edit”
    • specification synthesis passes the audit 31.0–49.2% of the time there
  • inference
    • a local specification can mislead an agent on a multi-function change; VL targets such changes
  • a proof cannot recover what the model left out
    • appendix I.2: “The information the hidden test checks was discarded when the abstraction was chosen, before a single line of proof was written. No amount of proving recovers it.”
  • appendix G.5: “The prover is not the obstacle.”
    • the agent’s witness verified against its own specification in 499 to 500 of 500 episodes

what “formally verified” covers here

  • proved: a re-written model of the changed functions meets the specification, given the axioms
  • not proved, checked by tests and model auditors
    • that each axiom is true of the real callee
    • that the verified model behaves like the Python patch
      • for Velvet and Lean the executable copy is an agent-written Python translation, “which we treat as the weakest link in the guarantee”
    • that the specification matches what the issue asks
      • section 3.4: “no guarantee can be established that a specification matches informal natural language intent”
  • inference
    • the released benchmark’s near-zero audit findings are by construction, as the authors say; they measure the auditors on solver-written specifications instead
      • appendix E.4: Fleiss Îș of 0.861 on faithfulness among three ballots
    • auditor agreement is not auditor correctness; no human-labeled ground truth for the audit is reported in the parts I read
    • the 26.8% figure depends on the same kind of model auditor

what VL could adopt

  • inference and recommendation
    • the discrimination, mutation and “wrong implementation that verifies” checks apply to Verus specifications directly
      • VL already has specification caveat and leak-scan documents; compare before adding
    • measure faithfulness separately: which functions the task needs versus which the specification constrains
    • when VL uses assume or external-body specifications for unverified callees, fuzz them against the real callee and ship the fuzz tests
    • Rust removes their weakest link
      • Verus verifies the Rust that runs, so no translation between verified model and executed patch is needed
      • the callee-assumption and intent links remain

product threat

  • inference
    • not a direct competitor today: Python, a benchmark, and the specifications were built with the answer in view
    • it weakens “tests pass” as a selling point for anyone and strengthens the case for proofs, which helps VL
    • it shows frontier agents already write the implementation and proof for a given specification in most cases
      • so proof generation alone is a thin moat; specification writing is where the difficulty is, and they measure it
    • the pipeline is from AWS AI Labs and they promise to release it
      • pointing it at Rust with Verus looks like engineering, not research; I do not know whether they plan to

study status

  • read the main text and appendices B.2, E.3, E.4, F.4 myself
  • ChatGPT analysis of the full PDF: /ssd1/sichangheagent/vlpw/swe_proof_chatgpt_answer.md
    • checked against the paper text and added above: the unrun-cell contradiction, the SWE-bench Pro result, appendix I.2 and G.5 quotes
    • not checked: its list of four smaller arithmetic mismatches between tables, and its 25-row technique table
    • its “moderate, indirect” threat label is its opinion

Last edited: