Paper deep dive
Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification
Yiannis Charalambous, Rafael Menezes, Youcheng Sun, Lucas C. Cordeiro
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 7/14/2026, 6:22:30 AM
Summary
The paper introduces a novel contract-based regression verification tool that leverages Large Language Models to automatically infer partial, caller-sufficient contracts for C programs. It demonstrates that these partial contracts are sufficient to verify safety-preserving conditional equivalence without requiring full behavioral specifications. The proposed pipeline, consisting of Contractor, scribe, and regver, ensures sound verification with zero false proofs on the EqBench-C suite, matching or exceeding existing tools like AutoSpec and Preguss in verification rates while providing stronger guarantees.
Entities (10)
Relation Signals (8)
Partial Contract → enables → Safety-Preserving Conditional Equivalence
confidence 97% · a passing result certifies at least as strong a property, which we call safety-preserving conditional equivalence: enforcement plus caller-sufficiency
LLM → usedfor → Contract Inference
confidence 96% · We therefore infer them with a large language model, which has recently begun to automate contract authoring
regver → verifies → Regression Verification
confidence 96% · regver discharges the regression-equivalence checking against the enforced contracts
regver → evaluatedon → EqBench-C
confidence 95% · on the third-party EqBench-C suite it never fabricates an equivalence, returning zero false proofs
scribe → infers → Partial Contract
confidence 95% · scribe runs the LLM-based propose-and-certify contract-inference loop
judge → compares → Contract Tightness
confidence 94% · judge, a semantic comparator that decides admit-set inclusion in both directions between two contracts
regver → evaluatedon → Frama-C-Problems
confidence 94% · On Frama-C-Problems we strengthen each inferred contract past what the caller needs and measure how much tighter it becomes.
AutoSpec → comparedwith →
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Software evolves continuously, yet ensuring that a patch preserves intended behavior without re-verifying an entire codebase remains difficult. Regression verification addresses this problem, but existing techniques require expensive whole-program reasoning or rely on manually written specifications that are rarely available in practice. We present the first contract-based regression verification tool. Contract soundness is ensured by proving all function versions match the behavior. The contract then verifies program flow via assume-guarantee. We ask whether a partial, caller-sufficient contract, rather than a full behavioral specification, is enough. On Frama-C-Problems we strengthen each inferred contract past what the caller needs and measure how much tighter it becomes. It barely moves: for most targets in every model the caller-sufficient contract is already the tightest the loop reaches, and our tightness comparator rates the partial and strengthened contracts equivalent for the large majority of targets it can compare. Partial-spec contracts thus capture nearly all the attainable tightness, so stopping at caller-sufficiency costs almost nothing. The regression check underneath is sound: on the third-party EqBench-C suite it never fabricates an equivalence, returning zero false proofs and reporting an unprovable difference instead. It also surfaced nine pairs that EqBench mislabels as equivalent, more than a concurrent tool reports. The contracts themselves are inferred automatically from the checker's own counterexamples, with no separate specification step; on Frama-C-Problems and the ANSSI X509 parser this reaches a verification rate comparable to tools AutoSpec and Preguss, while a passing result certifies at least as strong a property, which we call \emph{safety-preserving conditional equivalence}: enforcement plus caller-sufficiency.
Tags
Links
- Source: https://arxiv.org/abs/2607.10291v1
- Canonical: https://arxiv.org/abs/2607.10291v1
Trouble viewing inline? Open PDF directly →
Full Text
74,792 characters extracted from source content.
Expand or collapse full text
Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification Yiannis Charalambous Rafael Menezes Youcheng Sun Lucas C. Cordeiro Abstract Software evolves continuously, yet ensuring that a patch preserves intended behavior without re-verifying an entire codebase remains difficult. Regression verification addresses this problem, but existing techniques either require expensive whole-program reasoning or rely on manually written specifications that are rarely available in practice. In this work, we present the first contract-based regression verification tool. In our approach, the contract soundness is ensured by proving that all function versions match the behavior. Additionally, to ensure the behavior, the contract is used to verify the program flow (i.e., assume-guarantee). We ask whether a partial, caller-sufficient contract, rather than a full behavioral specification, is enough. On Frama-C-Problems we strengthen each inferred contract past what the caller needs and measure how much tighter it becomes. It barely moves: for most targets in every model the caller-sufficient contract is already the tightest the loop reaches, and our tightness comparator rates the partial and strengthened contracts equivalent for the large majority of targets it can compare (18 of 20, 13 of 15, and 14 of 18 across the three models). Partial-spec contracts thus capture nearly all the attainable tightness, so stopping at caller-sufficiency costs almost nothing. The regression check underneath is sound: on the third-party EqBench-C suite it never fabricates an equivalence, returning zero false proofs on the pairs it decides and reporting an unprovable difference rather than a false proof. Used as a soundness oracle this way, it also surfaced nine pairs that EqBench mislabels as equivalent, more than a concurrent tool reports. The contracts themselves are inferred automatically from the checker’s own counterexamples, with no separate specification step; on Frama-C-Problems and the ANSSI X509 parser this reaches a verification rate comparable to the weakest-precondition (WP) tools AutoSpec and Preguss, while a passing result certifies at least as strong a property, which we call safety-preserving conditional equivalence: enforcement plus caller-sufficiency, with runtime-error freedom covered by the safety encoding. I Introduction Software changes constantly, and most changes are meant to be conservative: a refactor, a bug fix, or a small feature should preserve the behavior callers already rely on. They don’t always manage it. A fix that corrects one execution path can quietly perturb an output some other caller reads, and if no test exercises that caller the regression ships unnoticed; across major operating systems, between 14.8% and 24.4% of post-release fixes were themselves found to be incorrect [59]. Catching it means deciding whether the new and old versions still agree, and there’s no general procedure for that: deciding full input/output equivalence is undecidable [43], and even a bounded check stays expensive, since it has to reason about each function together with all its side-effects [20]. In a bug-fixing or refactoring context, full equivalence asks too much: the developer means to change some paths and leave the rest, so requiring agreement everywhere, old bugs and all, rejects the very edit being made. The useful notions form a spectrum, ordered by how much of each execution they compare, and the weaker the relation the cheaper the proof. Full equivalence is the strongest: the two versions must terminate on the same inputs and return the same outputs everywhere, preserved bugs included. Partial equivalence relaxes termination, asking the versions to agree only on the inputs where the old one terminates. Conditional, or regression, equivalence relaxes further still: it fixes a property marking the behavior worth preserving and asks for agreement only where the old version already satisfied it. Where the old version violated the property, the new one is free to differ, and that freedom is exactly where a bug fix lives. We make the three notions precise in Definition 2. Whichever notion one targets, a whole-program check re-analyzes every callee in full at each call site, which does not scale as a codebase grows. A scalable proof has to be modular: each call is discharged against an abstraction α of the callee rather than its body, so the callee is analyzed once instead of at every use. For the proof to stay trustworthy that abstraction must be sound: it has to over-approximate the callee, admitting every behavior the function can exhibit, so the check can never miss a real difference. We take that abstraction to be a function contract: a precondition and a postcondition that pin down just part of the callee’s behavior (Definition 3). A verifier enforces the contract against the old version, certifying it as a sound over-approximation, and then replaces each call by it, so one enforced contract serves every call site without re-entering the body. The contract need only be precise on the slice of the output the property observes; off that slice it may stay weak, and looseness there costs completeness, never soundness. Anchoring it to the old version’s safe behavior also folds safety in, so a newly introduced memory leak or out-of-bounds access counts as a regression even when every returned value is unchanged. Contracts like this are almost never written by hand: even safety-critical code rarely carries machine-checkable per-function specifications, and what exists tends to be system-level [57, 21, 54]. We therefore infer them with a large language model, which has recently begun to automate contract authoring, though so far only for a single version of a program [57, 21, 54]. The model is never trusted: it proposes a contract, the verifier enforces it against the old version, and only an enforced contract is used, so a wrong guess is rejected rather than believed. This is the paper’s thesis: a partial, LLM-inferred, verifier-certified contract suffices to check regression-equivalence of C, a language of large, long-lived systems where a routine change can silently regress a caller. Beyond staying safe, a change is a regression only if something that uses the function can tell. Figure 1 shows the kind of edit we target. shrink trims a box by a fixed margin; the old version forgets to shrink the height, and the new one fixes it. The caller usable_width reads only the width, so it returns the same value before and after the fix. Asking whether the two shrink versions are equivalent is the wrong question: the height really does change, so a check over the whole of *o reports a difference, flagging the fix itself. What matters is whether shrink regresses on the width, the only part usable_width observes, and the contract C in the figure captures exactly that. Enforced against the old shrink, C pins the width (ensures o->w == b->w - 2) and leaves the height free. The regression check replaces the old shrink by C and runs the new shrink concretely, comparing only the width: because C is precise exactly where the caller looks and silent elsewhere, the two agree and the height change is invisible. A full specification would have to pin the height too, the one part the fix changed and no caller reads, making the proof obligation much harder for the contract author. Caller (unchanged in both versions) ⬇ 1int usable_width(const box_t *b) 2 box_t o; 3 shrink(b, &o); 4 return o.w; // reads w, never h 5 shrink (OLD) ⬇ 1void shrink(const box_t *b, 2 box_t *o) 3 o->w = b->w - 2; 4 o->h = b->h; 5 shrink (NEW) ⬇ void shrink(const box_t *b, box_t *o) o->w = b->w - 2; o->h = b->h - 2; Inferred contract C on shrink (enforced against OLD) ⬇ requires (b) && (o); assigns o->w, o->h; ensures o->w == b->w - 2; // nothing about o->h Figure 1: A property-relative regression check. The fix corrects o->h; the caller usable_width reads only o->w, so it cannot observe the change. The partial contract C pins o->w and stays silent on o->h: it is enforced against the old shrink ([[1]]⊆[[C]][\![ shrink_1]\!] [\![C]\!]) and then replaces it in the regression check while the new shrink runs concretely, so the two agree on o->w. Comparing the whole of *o instead would flag the fix as a difference. We make three contributions: • C1 (Soundness). A verifier-independent theorem that proves abstracting only the old version by a single partial, one-sided contract suffices to prove property-relative regression-equivalence, together with a depth-bounded lift for nested calls (§IV, Theorem T1). • C2 (System). An end-to-end pipeline of three tools: Contractor itself scaffolds the regression harnesses, scribe runs the LLM-based propose-and-certify contract-inference loop, and regver discharges the regression-equivalence checking against the enforced contracts (§IV); to our knowledge the first to combine LLM-based contract inference with regression-equivalence verification. • C3 (Relative contract-tightness comparator). judge, a semantic comparator that decides admit-set inclusion in both directions between two contracts and returns a four-way verdict (equivalent, one strictly tighter, or incomparable) with counterexample witnesses; on enforced contracts this yields a refinement ordering, so we can measure how tight an inferred contract is rather than only whether it verifies (§IV-D, Theorem T2). We evaluate C1, C2, and C3 through two questions, stated and answered in §V: which counterexample modality best drives frame-condition inference (feedback modality); and whether targeting a partial, property-relative contract rather than a full specification makes inference more tractable, and where its returns plateau (tractability). The remainder of the paper is organized as follows. §I sets out the relational semantics, the three equivalence notions, and function contracts with the frame rule; §I surveys related work; §IV presents the soundness theorem (Theorem T1) and its depth-bounded lift, the system, and the contract-tightness procedure (Theorem T2); §V reports the experimental evaluation and analysis, including threats to validity (§V-G); and §VI concludes with open directions for future work. I Preliminaries I-A Program semantics Definition 1 (Program semantics). We model each version of a function as a relation [[f]]⊆X×Y[\![f]\!] X× Y from input pre-states X to output post-states Y, where (x,o)∈[[f]](x,o)∈[\![f]\!] means some terminating run of f on x yields o. The pre-state X subsumes the responses of any external nondeterministic callee the two versions share, so a single x resolves those responses identically on both sides; only nondeterminism internal to the function itself leaves [[f]](x)[\![f]\!](x) multi-valued. We write [[f]](x)≜o∣(x,o)∈[[f]][\![f]\!](x) \o (x,o)∈[\![f]\!]\ for the set of outputs on x, which is empty when f does not terminate on x. The spaces X and Y range over a common store, so a pre-state and a post-state can be compared; this is what lets the frame clause below speak of the locations a function leaves unchanged. I-B Equivalence notions Fix an old version f1f_1 and a new version f2f_2. The three notions stated informally in §I order by how much of each execution they compare [19, 20]. Definition 2 (Equivalence notions). • Full equivalence: [[f1]]=[[f2]][\![f_1]\!]=[\![f_2]\!], so the versions terminate on the same inputs and produce the same outputs everywhere, old bugs included. • Partial equivalence relaxes termination: [[f1]](x)≠∅⇒[[f1]](x)=[[f2]](x)[\![f_1]\!](x)≠ [\![f_1]\!](x)=[\![f_2]\!](x), so only inputs on which f1f_1 terminates need to agree. • Conditional (regression) equivalence relaxes further to a property ϕφ marking the behavior worth preserving (we write [[f1]](x)⊧ϕ[\![f_1]\!](x) φ when f1f_1’s runs on x satisfy it), asking for agreement only where the old version was already correct: [[f1]](x)⊧ϕ⇒[[f1]](x)=[[f2]](x)[\![f_1]\!](x) φ [\![f_1]\!](x)=[\![f_2]\!](x). Where f1f_1 violated ϕφ the new version is free to differ, and that freedom is where the fix lives. We target this conditional notion throughout. §IV makes it precise on an explicit in-scope set and relaxes the output equality to a property-relative obligation EϕE_φ, recovering the definition above as the special case where ϕφ observes the whole output. We denote this relation we target safety-preserving conditional equivalence. I-C Contracts and the Frame Rule Definition 3 (Function contract and admit set). A function contract is a Hoare-style triple [24, 32]: a precondition (requires), a postcondition (ensures), and a frame (assigns) naming the locations the function may modify. We write C≜(Pre,Post,Assigns)C (Pre,Post,Assigns), with Pre⊆XPre X a set of input states and Post⊆X×YPost X× Y relating inputs to outputs over the state spaces X,YX,Y defined above; throughout, we identify a set such as Pre with its characteristic predicate, writing Pre(x)Pre(x) for x∈Prex . Read in that relational model, the contract denotes its admit set, the input/output pairs it permits, [[C]]≜(x,o)∈X×Y∣Pre(x)⇒(Post(x,o)∧ [\![C]\!]\; \;\(x,o)∈ X× Y (x) (Post(x,o)\ oagrees withxoutsideAssigns), o\ agrees with\ x\ outside\ Assigns)\, with image [[C]](x)[\![C]\!](x) the outputs it allows on x; outside its precondition the contract permits anything, so [[C]](x)=Y[\![C]\!](x)=Y when ¬Pre(x) (x). A modular verifier supports two operations on such a contract, used here only through their effect on [[C]][\![C]\!]. Enforcement checks that the body of f satisfies its contract: every execution from a requires-state ends in an ensures-state and writes only assigns locations. This is exactly the inclusion [[f]]⊆[[C]][\![f]\!] [\![C]\!], so a passing enforcement makes C an over-approximation of f. Replacement abstracts each call to f by the contract: the call site asserts requires, havocs the locations named in assigns, and assumes ensures, so the call ranges over [[C]](x)[\![C]\!](x) in place of [[f]](x)[\![f]\!](x); since [[f]]⊆[[C]][\![f]\!] [\![C]\!] once enforced, a proof under replacement is sound for the real f. Replacement is an over-approximation: a proof obtained under it is sound for the real function, but a reported failure may be spurious, because havocking the assigned locations can hand the caller an output the real body never produces. The frame clause is what keeps replacement precise. Locations not named in assigns are snapshotted before the body and asserted unchanged after, so without an explicit assigns the verifier must havoc every reachable location, and the abstraction becomes too coarse to support a non-trivial equivalence proof. One caveat keeps enforcement honest: if a contract’s requires can never hold, the body is never entered and the check passes vacuously, testing nothing. Our pipeline guards against this by reporting such a proof as inconclusive rather than as a success, so the soundness of enforcement never rests on an empty scope. I Related Work I-A Regression Verification and Equivalence Checking Regression Verification Tool (RVT) [19, 20] pioneered modular regression verification, abstracting equivalent matched callees with shared uninterpreted functions so the proof holds for any consistent interpretation. Reve / LLREVE [16, 27] encodes paired programs as constrained Horn clauses and infers coupling predicates relating the two versions’ states with an external solver (Eldarica, Z3), while SymDiff [28] and DAC [29] relate the two versions by a relational summary in the mutual-summary tradition [22]: a single predicate over the disjoint union of both versions’ inputs and outputs that characterizes their behavioral relationship. ARDiff [6] prunes common code by iterative abstraction-refinement, but only for Java; PEQcheck and PEQtest [26, 25] target localized refactorings through segment-level encodings; and PASDA [18] adds partition-based heuristics for the undecided cases. Differential symbolic execution [38, 36, 31, 23] characterizes program differences by exploring both versions’ symbolic state spaces, usually returning concrete divergence-inducing inputs but no reusable artifact, as does LLM-driven test generation: Mokav [15] pairs it with differential testing for behavioral separation, and UnitTenX [13] drives agents over an ESBMC backend to build unit tests for legacy code, both producing tests rather than a proof certificate. Concurrent work by Sarker et al. [45] takes differential symbolic execution in an orthogonal direction, quantifying how much of the input domain a patch changes rather than proving equivalence. Run as a soundness oracle on EqBench-C our checker surfaced more mislabeled Eq pairs than they report (nine versus five), while we target a sound modular equivalence proof, not an impact measure. Throughout this line the callee abstraction is supplied or derived from both bodies in lockstep, presupposing a complete characterization of what is abstracted. The closest exception is regression verification by impact summaries [5], which restricts the proof to change-relevant behavior: a control- and data-dependence analysis marks the impacted statements and keeps only their path-condition constraints from a whole-program symbolic execution. That summary is exact, so the check is sound and complete to the depth bound, but for the same reason the analysis must see all the code it reasons about. We instead abstract the old version alone by a weak one-sided contract (one constraining the old version, never the new), a reusable and enforceable artifact rather than a path-condition partition tied to one diff, scoped to what the property observes rather than to what the change touches, and discharged once bottom-up then reused at every call site and in every later check (§IV). I-B Contract, Invariant, and Frame Inference Inferring functional specifications with LLMs has advanced quickly. The closest are ACSL-for-C tools validated by Frama-C: AutoSpec’s accept-or-reject WP feedback [57], “Specify What?” priming on EVA and Pathcrawler data [21], and Preguss’s iterative runtime-error-alarm refinement [54], the nearest analogue to our BMC-trace-driven loop on a Frama-C backend. Other LLM-based generate+validate loops [52, 44, 39]. Non-LLM inference [2, 1] and symbolic frame inference [42, 11, 49] predate these; we contribute the BMC-backed counterpart, with concrete-trace feedback drawn from ESBMC’s frame-rule pass. Two gaps separate this work from all of the above. First, every such tool targets a single version; none reuses the inferred contract as a callee abstraction in a two-version regression-equivalence proof, the gap we close. Second, they judge a specification by whether it verifies, not how tight it is [21, 10]; to our knowledge none defines a semantic notion of contract tightness or a decision procedure for contract subsumption, which §IV-D introduces. The CE-guided LLM loop is by now established for invariants [58, 12, 53, 50, 8, 40, 47, 56] and descends from counterexample-guided inductive synthesis [48, 17, 34, 46], but those target invariants, not the function-level frame conditions we infer. IV Methodology IV-A One-Sided Contracts for Regression Equivalence (C1) Recall from Definition 1 that each version is a relation [[f]]⊆X×Y[\![f]\!] X× Y of terminating runs, with image [[f]](x)[\![f]\!](x), and from Definition 3 that a contract denotes a relation [[C]]⊆X×Y[\![C]\!] X× Y, with image [[C]](x)[\![C]\!](x) the outputs it allows on x. The abstraction α of §I is just a contract: taking [[α]]=[[C]][\![α]\!]=[\![C]\!], its over-approximation requirement [[f1]]⊆[[α]][\![f_1]\!] [\![α]\!] becomes [[f1]]⊆[[C]][\![f_1]\!] [\![C]\!]. Definition 4 (Scope and equivalence obligation). A property ϕφ fixes a scope ≜x∈X∣[[f1]](x)⊧ϕSc \x∈ X [\![f_1]\!](x) φ\ of in-scope inputs (the x on which every run of f1f_1 stays within ϕφ, e.g. runs safely), and an equivalence obligation Eϕ(o1,o2)E_φ(o_1,o_2) that holds when o1o_1 and o2o_2 agree on the part of the output ϕφ observes (for example, the return value and the locations a caller reads). We work under partial correctness and three standing assumptions, made explicit because the theorem rests on them: (A1) only terminating runs populate [[⋅]][\![·]\!], so the claim is over inputs on which both versions terminate [20] (in particular, a change that makes f2f_2 diverge where f1f_1 terminated is outside the guarantee, and detecting such termination regressions is left to future work); (A2) the frame rule is sound (a body that passes enforcement writes no location outside Assigns, even under aliasing); and (A3) the verifier that discharges enforcement and replacement is sound, so every verdict it certifies holds in the relational model (Definition 3). External nondeterminism needs no separate assumption: a shared callee’s responses are part of the input x (Definition 1), so they are resolved identically on both sides by construction and cannot themselves induce a divergence. Definition 5 (Contract preserving regression-equivalence). Given two versions f1,f2f_1,f_2 of a function and a property ϕφ, a contract C preserves regression-equivalence with respect to ϕφ iff: 1. Enforcement. [[f1]]⊆[[C]][\![f_1]\!] [\![C]\!]: C over-approximates f1f_1, so every run of f1f_1 is one C permits. 2. Sufficiency for ϕφ. For every x∈x , every o∈[[C]](x)o∈[\![C]\!](x), and every o2∈[[f2]](x)o_2∈[\![f_2]\!](x), we have Eϕ(o,o2)E_φ(o,o_2): every output the replacement of f1f_1 by C may produce meets the regression obligation against f2f_2. Condition 2 mirrors replacement: the abstracted call ranges over exactly [[C]](x)[\![C]\!](x), the outputs C allows on x. We need not separately assume ⊆PreSc : dropping it only strengthens condition 2’s hypothesis (outside Pre, [[C]](x)=Y[\![C]\!](x)=Y, so the obligation ranges over more outputs, never fewer), and the soundness proof never relies on ⊆PreSc . Definition 6 (ϕφ-regression-equivalence). f2f_2 is ϕφ-regression-equivalent to f1f_1 iff for every x∈x , every o1∈[[f1]](x)o_1∈[\![f_1]\!](x), and every o2∈[[f2]](x)o_2∈[\![f_2]\!](x) the obligation Eϕ(o1,o2)E_φ(o_1,o_2) holds. For deterministic functions (each [[f]](x)[\![f]\!](x) a single output, shared external nondeterminism already folded into x by Definition 1), this coincides with the conditional equivalence [[f1]](x)⊧ϕ⇒[[f1]](x)=[[f2]](x)[\![f_1]\!](x) φ [\![f_1]\!](x)=[\![f_2]\!](x) of Definition 2, equality relaxed to EϕE_φ; for genuinely multi-valued [[f]](x)[\![f]\!](x) the pairwise form is strictly stronger. Intuitively, the contract only needs to over-approximate the old version, while being precise on the behavior observed by callers. This allows us to replace the old implementation during verification without introducing unsoundness. Theorem T1 (Soundness of one-sided contract abstraction). Let f1,f2f_1,f_2 be two versions of a function, C a contract, and ϕφ a property with scope Sc and obligation EϕE_φ. If C preserves regression-equivalence with respect to ϕφ (Definition 5), then f2f_2 is ϕφ-regression-equivalent to f1f_1 (Definition 6). Proof. Fix x∈x , o1∈[[f1]](x)o_1∈[\![f_1]\!](x), and o2∈[[f2]](x)o_2∈[\![f_2]\!](x). By condition 1, [[f1]]⊆[[C]][\![f_1]\!] [\![C]\!], so [[f1]](x)⊆[[C]](x)[\![f_1]\!](x) [\![C]\!](x) and o1∈[[C]](x)o_1∈[\![C]\!](x). Instantiate condition 2 with this x, the witness o:=o1o :=o_1, and the given o2o_2: its premises o1∈[[C]](x)o_1∈[\![C]\!](x) and o2∈[[f2]](x)o_2∈[\![f_2]\!](x) both hold, so Eϕ(o1,o2)E_φ(o_1,o_2). As x,o1,o2x,o_1,o_2 were arbitrary, f2f_2 is ϕφ-regression-equivalent to f1f_1. ∎ The proof turns on one step: enforcement (condition 1) places the real output o1o_1 inside [[C]](x)[\![C]\!](x), and replacement (condition 2) quantifies the obligation over all of [[C]](x)[\![C]\!](x), so it specializes to o1o_1. Condition 1 is what makes the proof sound; condition 2 is the only place C must be tight, and everywhere else it may stay weak. The relational-summary abstractions of SymDiff [28] and DAC [29] and the shared-uninterpreted-function abstraction of RVT [20] do not allow this freedom, since they need a complete characterization of the procedure. The remaining obligations are discharged by the standing assumptions (pointer aliasing across Assigns and non-termination) and by the semantics (external nondeterminism is folded into the shared input, Definition 1); these are standard for Hoare reasoning with a frame rule. To our knowledge this is the first such formalization for a one-sided contract inside a regression query, and it is what makes the contract small enough for an LLM to infer. How our pipeline discharges conditions 1–2 as two concrete ESBMC queries is described in §IV-C. Replacement is an over-approximation, so the converse of Theorem T1 can fail: the equivalence check may report a spurious divergence, a witness o∈[[C]](x)o∈[\![C]\!](x) that C permits but f1f_1 never produces and on which EϕE_φ fails. This is exactly why condition 2 requires C to be precise on the ϕφ-observed output: looseness there admits an observably-disagreeing o and condition 2 fails even when f1f_1 and f2f_2 genuinely agree (lost completeness, not soundness), whereas looseness off the observed projection only enlarges [[C]][\![C]\!] on locations EϕE_φ ignores and is harmless. That harmless region is the partial-spec freedom, and it keeps the LLM step practical. Remark 1 (Non-vacuity is machine-discharged). Theorem T1 is content-free if =∅Sc= : an unsatisfiable Pre makes condition 1 hold vacuously and the conclusion vacuously true. Our approach does not rely on the user to rule this out. Instead it employs a vacuity probe to ensure that the contract conditions are not vacuously true [9]. IV-B Depth-Bounded Contract Closure Theorem T1 governs the boundary between one abstracted procedure and its caller. Regression targets in legacy code transitively touch hundreds of helpers, and inferring partial contracts for all of them in a single LLM pass is intractable. We extend T1 by bounding the contract closure to a configurable depth N from the seed target g0g_0. Let d(g)d(g) be the depth of g, its distance from the seed g0g_0. Functions at distance d(g)<Nd(g)<N along the static call graph receive precise partial contracts of T1’s shape; functions at d(g)=Nd(g)=N receive deliberately weak boundary contracts Cg∂C^∂_g (precondition true, postcondition true, and a frame that havocs every location reachable from the call); functions at d(g)>Nd(g)>N receive no contract and are not analyzed in this pass. Under contract replacement, boundary contracts substitute at depth-N call sites and deeper bodies are never expanded, so the cost of verifying g0g_0 is bounded by the depth-N closure independently of the full callee depth. Write [[g∣σ]][\![g σ]\!] for the denotation of g under a callee environment σ that replaces each callee h of g by a relation. Here (⋅)h(\,·\,)_h is the family indexed by the callees h of g, so [[g∣([[h]])h]]=[[g]][\![g ([\![h]\!])_h]\!]=[\![g]\!] sends each callee to its own denotation and [[g∣([[Ch]])h]][\![g ([\![C_h]\!])_h]\!] replaces every callee by its contract. The semantics is monotone in σ (a callee relation occurs only positively): σ⊆σ′σ σ pointwise implies [[g∣σ]]⊆[[g∣σ′]][\![g σ]\!] [\![g σ ]\!]. Lemma L1 (Depth-N closure soundness). With contracts assigned as above, suppose (i) (boundary) each Cg∂C^∂_g at d(g)=Nd(g)=N havocs a superset of g’s footprint, so [[g]]⊆[[Cg∂]][\![g]\!] [\![C^∂_g]\!]; and (i) (interior) each g at d(g)<Nd(g)<N passes enforcement against its callees’ contracts, [[g∣([[Ch]])h]]⊆[[Cg]][\![g ([\![C_h]\!])_h]\!] [\![C_g]\!]. Then [[g0]]⊆[[Cg0]][\![g_0]\!] [\![C_g_0]\!]: the seed contract over-approximates the seed without expanding any body below depth N. Proof. Induct on the call relation of the depth-≤N≤ N closure, each callee before its caller. Base. A boundary node (d(g)=Nd(g)=N) is covered by (i), [[g]]⊆[[Cg∂]][\![g]\!] [\![C^∂_g]\!], with no enforcement query. Step. For an interior g, every callee h has d(h)≤d(g)+1≤Nd(h)≤ d(g)+1≤ N, so h lies in the closure with a contract ChC_h; the induction hypothesis gives [[h]]⊆[[Ch]][\![h]\!] [\![C_h]\!], monotonicity gives [[g]]=[[g∣([[h]])h]]⊆[[g∣([[Ch]])h]][\![g]\!]=[\![g ([\![h]\!])_h]\!] [\![g ([\![C_h]\!])_h]\!], and (i) gives [[g]]⊆[[Cg]][\![g]\!] [\![C_g]\!]. The order is well-founded when the closure is acyclic; an interior recursive g replaces its self-call by CgC_g in (i), sound by the standard partial-correctness contract rule (A1 makes each terminating run’s recursion finite). Take g=g0g=g_0. ∎ Lemma L1 supplies condition 1 of T1 for g0g_0 at the cost of the depth-N closure alone; condition 2 is discharged by the seed’s equivalence harness (§IV-C), independent of N. Boundary contracts need no enforcement step, so deepening the boundary trades precision, not soundness, and T1’s partial-spec relaxation carries over to each interior CgC_g. Iterative deepening re-seeds a boundary function with bound N, turning its case (i) into case (i) one stratum deeper; the single knob N trades inferred-contract precision against verification scalability. IV-C System Architecture (C2) Our tools realize the method as a three-stage pipeline. Contractor parses the C project with tree-sitter, identifies the target functions, and scaffolds their harnesses. scribe then runs the LLM contract-inference loop over the interior functions through a JSON-schema interface, closing the depth-N frontier with the mechanical havoc boundary contracts of §IV-B. Finally, regver stages the old version, either from a git commit or a directory snapshot, and renames its symbols on a temporary copy so that both versions can coexist in a single harness. From the enforced contracts, regver compiles condition 2 of Definition 5 into one equivalence harness. On a shared nondeterministic input x∈x it replaces the old version by its contract: the call site asserts requires, havocs assigns, and assumes ensures, so the result ranges over [[C]](x)[\![C]\!](x). It then runs the new version f2f_2 concretely and asserts EϕE_φ between the two outputs. That single verification condition is exactly condition 2, while enforcement (condition 1) is a separate query placing every real f1f_1-output inside [[C]](x)[\![C]\!](x). The check thus reduces to two ESBMC queries, and f1f_1’s body is never expanded inside the equivalence proof. Theorem T1 is stated over an abstract contract checker, and we instantiate its enforcement and replacement by ESBMC’s enforce and replace modes, whose documented replace-mode behavior supplies the over-approximation the proof relies on [39]. The theorem leaves the post-state property ϕφ abstract, and in the implementation we fix it to the safety properties ESBMC encodes on every harness—memory safety (spatial bounds and pointer- and dereference-validity, covering use-after-free), division by zero, arithmetic over- and underflow, memory leaks, and undefined-behavior shifts. The same instantiation inherits the non-vacuity guard of Remark 1 from ESBMC’s vacuity probe. Inference is driven by the very counterexamples the verifier already produces. When ESBMC enforces a proposed contract C(0)C^(0) against f1f_1’s body and the frame check fails, its frame-rule pass recovers the offending write (file, line, and address expression) from the counterexample trace, and scribe feeds that trace, not a bare verification-condition failure, into the next prompt. IV-D Semantic Contract-Tightness Comparison (C3) The published LLM contract-inference baselines (AutoSpec [57], “Specify What?” [21], Preguss [54]) do not measure contract tightness semantically: they report verification success rate, or at most count annotations by type. Any such syntactic proxy is inflatable: a trivially true postcondition adds to the count without adding constraint. We replace it with a decision procedure for contract subsumption. For contracts sound A,BA,B on a common function over the state spaces X,YX,Y of Definition 1, tightness is set inclusion on their admit sets: A≤tightB⇔[[A]]⊆[[B]]A _tightB [\![A]\!] [\![B]\!]. judge (C3) decides this ordering, splitting [[C]][\![C]\!] into its postcondition and frame parts. The postcondition part is two validity checks: • Check 1: ∀x,o.admitsA(x,o)⇒admitsB(x,o)∀ x,o.\;admits_A(x,o) _B(x,o) (is [[A]]⊆[[B]][\![A]\!] [\![B]\!]?) • Check 2: ∀x,o.admitsB(x,o)⇒admitsA(x,o)∀ x,o.\;admits_B(x,o) _A(x,o) (is [[B]]⊆[[A]][\![B]\!] [\![A]\!]?) where admitsC(x,o)≡¬PreC(x)∨PostC(x,o)admits_C(x,o)≡ \,Pre_C(x) _C(x,o) is membership in [[C]][\![C]\!] with the frame conjunct dropped (a superset test); frame containment on Assigns is checked separately (syntactically in v1, see §V-G). When A and B share their precondition and frame (the warm-start, partial-versus-strengthened case Theorem T2 ranges over), a passing Check 1/Check 2 establishes [[A]]⊆[[B]][\![A]\!] [\![B]\!]. These checks are sound in that direction but not complete: because admitsCadmits_C drops the frame, a failing check can be spurious (its witness may lie outside the shared precondition/frame region), so judge may under-report tightness, never over-report it. Under the same shared-precondition/frame assumption, the four outcomes of (Check 1, Check 2) classify the pair: (✓,✓)( , ) is equivalent ([[A]]=[[B]][\![A]\!]=[\![B]\!]); (✓,×)( ,×) is A strictly tighter; (×,✓)(×, ) is B strictly tighter; (×,×)(×,×) is incomparable. Each failing check yields a counterexample witness: a concrete (x,o)(x,o) admitted by one contract and rejected by the other. The incomparable case ships two witnesses, one per direction, surfacing the precise behavior each contract admits that the other does not. Each check is a pure validity query over a nondeterministic input and output, with no body of f involved (neither enforcement nor replacement); our implementation discharges each as a single SMT query. Relative ordering, not absolute completeness. judge measures the order between [[A]][\![A]\!] and [[B]][\![B]\!], not how close either is to [[f]][\![f]\!]. A contract it finds strictly tighter may still loosely over-approximate f, or not be valid for f at all; validity is settled separately by enforcement (Theorem T1, condition 1), and we always report the two together. A verdict between two enforced contracts is thus a statement about sound contracts, the tighter side admitting strictly fewer behaviors while still covering all of f’s; between unenforced contracts it is only a relative-over-approximation result, labelled as such in the evaluation tables. Tightness is the classical refinement ordering [30, 4]. When both contracts are enforcement-checked, the ordering says more than set inclusion: the tighter contract proves at least as much, discharging every obligation the looser one does. We state this as an extension of Theorem T1, reusing its scope Sc, obligation EϕE_φ, and condition 2 (sufficiency). We keep Theorem T1’s scope Sc unchanged: the hypothesis [[A]]⊆[[B]][\![A]\!] [\![B]\!] already gives [[A]](x)⊆[[B]](x)[\![A]\!](x) [\![B]\!](x) at every x, so no narrowing to the preconditions is needed (in the warm-start, partial-versus-strengthened comparison A and B share Pre anyway). Theorem T2 (Tightness refines proof power). Let A,BA,B be contracts for f1f_1 that both pass enforcement ([[f1]]⊆[[A]][\![f_1]\!] [\![A]\!] and [[f1]]⊆[[B]][\![f_1]\!] [\![B]\!]), with [[A]]⊆[[B]][\![A]\!] [\![B]\!] (judge’s Check 1: A is at least as tight as B). Then every regression-equivalence query against f2f_2 that replace(B)replace(B) discharges, replace(A)replace(A) discharges too (condition 2 of Theorem T1 for B implies condition 2 for A), and the resulting proof is sound for the real f1f_1 and f2f_2. Proof. Fix x∈x . Since [[A]]⊆[[B]][\![A]\!] [\![B]\!], also [[A]](x)⊆[[B]](x)[\![A]\!](x) [\![B]\!](x). Condition 2 for B requires Eϕ(o,o2)E_φ(o,o_2) for every o∈[[B]](x)o∈[\![B]\!](x) and o2∈[[f2]](x)o_2∈[\![f_2]\!](x); restricting to o∈[[A]](x)o∈[\![A]\!](x) gives condition 2 for A. As A passes enforcement, Theorem T1 turns condition 2 for A into the regression-equivalence of f1f_1 and f2f_2. ∎ The converse fails, and that is the point: a looser contract proves no more, and may admit an output f1f_1 never produces that raises a spurious divergence the tighter one rules out. So for enforcement-sound contracts judge’s verdict is a refinement ordering: the strictly tighter side discharges at least as many regression queries, and strictly more whenever it eliminates such a spurious counterexample. V Evaluation We evaluate the contributions of §IV around two questions: RQ1 - Feedback Modality Which counterexample modality most effectively drives frame-condition inference: concrete BMC traces, verification-condition failures (AutoSpec), or runtime-error traces (Preguss)? RQ2 - Tractability Given that the scribe loop produces a partial contract (RQ1), how much additional tightness does continued strengthening recover beyond it, and do those returns plateau? This is the practical test of the partial-spec freedom of Theorem T1: not whether a partial contract is cheaper to infer, but whether it is a good place to stop. The order is deliberate. RQ1 establishes that the inference loop works at all, and RQ2 then asks whether the partial contract it produces is already tight enough; RQ2 only makes sense once RQ1 is settled. We describe the datasets, baselines, and metrics, then report results. V-A Datasets EqBench-C. The C subset of EqBench [7]: 147 equivalent and 125 non-equivalent program pairs. EqBench is the most comprehensive public equivalence-checking dataset, built to cover the hard constructs earlier benchmarks omit (non-linear arithmetic, loops, floating point, and string and array manipulation), which makes its C subset a demanding soundness stress-test even though formal C tools have rarely reported on it. Its pairs are labelled by input-output equivalence of terminating runs, the same notion regver’s contract-free harness decides, so the labels are valid ground truth for our regression check. We use EqBench-C as a soundness baseline for regver, not a cross-tool rate ranking: the question we ask is the safe one, whether regver ever certifies a non-equivalent pair as equivalent. We evaluate on EqBench-C rather than the more recent EquiBench [55] because EquiBench labels pairs by full input-output equivalence (Definition 2), a relation finer than the safety-preserving regression equivalence our methodology targets. Frama-C-Problems. Frama-C-Problems [37] is a community set of 51 small C programs (∼ 20 LoC average), each carrying an unproven guard assertion and 1–3 ACSL specifications. AutoSpec [57] introduced it as a contract-inference benchmark and Preguss [54] reused it, so it is the standing benchmark for this task and both report per-program success rates on it. We evaluate scribe on all 51 programs. X509-parser. X509-parser is a formally verified RTE-free X.509 parser (>>1000 LoC, manually verified in ACSL by its authors over five months), against which AutoSpec [57] reports synthesized specifications for six functions, selected to span loops with buffer arithmetic, switch-case control flow, inter-procedural composition, and mixed-width integer and shift operations. We evaluate scribe on those same six functions; the depth-bounded closure of §IV-B (Lemma L1), a standing part of our C2 contribution rather than an ablation knob, handles their inter-procedural composition. V-B Baselines For frame inference (RQ1) we compare against AutoSpec [57] (LLM+WP, VC-level feedback), “Specify What?” [21] (LLM+WP+EVA/Pathcrawler prompt augmentation), Preguss [54] (LLM+WP+RTE-trace iterative refinement), and AutoDeduct [2] (CHC+Eva, no LLM). We compare against the numbers each tool reports in its published evaluation, on the inputs it reports them for: Frama-C-Problems for AutoSpec and Preguss, and the SV-COMP-derived subset and X509-parser for AutoSpec. We run scribe on those same inputs and report its success rate and iteration count alongside theirs. For regression verification we use EqBench-C only as a lightweight soundness check on regver, without a numeric cross-tool ranking: the established equivalence checkers (RVT [20], Reve [27], ARDiff [6], SymDiff [28]) decide partial rather than safety-preserving conditional equivalence, and the ones with EqBench results (ARDiff and its symbolic-execution successors) report on the Java subset, so no like-for-like EqBench-C number exists to compare against. We run regver on this set in two arms, a contract-free baseline and a treatment arm in which scribe first infers a one-sided contract for the changed function, and combine them as a sequential portfolio: the baseline runs first and the treatment arm is invoked only on the pairs it leaves undecided, the timeout and tool-error tail. Because the escalation gate is the baseline’s own abstention, observable at run time and independent of the dataset label, the combination is a portfolio and not an oracle, and it inherits every false positive the contract layer raises on that tail. V-C Experimental Setup We evaluate with three LLMs chosen for diversity: Opus 4.8 [3] (closed-source frontier), Kimi K2.6 [33] (open-weight frontier), and Qwen3.6-27B [41] (open-weight, runnable on inexpensive hardware), all at temperature 0. For the formal verifier we use ESBMC with Z3 (due to quantifier support). ESBMC runs under k-induction with no fixed unwinding bound: inductively closed loops are proved for every iteration and the rest unrolled in full, completing on finite loops and otherwise timing out. Three limits are fixed across every comparison run: a per-query ESBMC timeout and a per-call LLM timeout, both 300s, and at most 5 refinement iterations per target. ESBMC also runs under a 104GB per-process memory budget, applied as a Linux control-group limit with swap off, so a run that exceeds it stops at its memory ceiling rather than growing into swap; a stopped run is a non-result, never a pass or a failure. A non-result is a run that returns no verdict: a query timeout, a memory-ceiling stop, an ESBMC crash or solver error, an unreadable exit, or an LLM API failure. We report each success rate two ways: over the cases ESBMC decided, and with every non-result charged as a failure (to keep the lower bound conservative). V-D Metrics and Mapping to RQs Each RQ pairs a metric with the dataset it is measured on. • RQ1 (feedback modality): contract-inference success rate and iterations to convergence on Frama-C-Problems and X509-parser, read against AutoSpec’s and Preguss’s published numbers. • RQ2 (tractability): the round-by-round judge tightness verdict (the saturation curve) and pass rate of scribe’s partial contract against the warm-start hardscribe arm, on Frama-C-Problems. V-E Results We report RQ1 and RQ2 from the three-model sweep on the inputs the baselines publish, plus the EqBench-C soundness baseline. V-E1 RQ1 (feedback modality) We ran scribe in its default partial-spec mode on the two inputs the closest baselines report on, the 51 Frama-C-Problems programs and the X509 parser, across all three models. Table I gives the headline. On Frama-C-Problems, scribe infers a verifier-discharged contract for most programs on all three models, with the decided and conservative success rates shown. Non-results are few and cluster on the hard array and loop cases (20 across the three models, mostly query timeouts, the rest ESBMC crashes, unreadable exits, and one LLM API error; no run reached the 104GB ceiling). Measured the way the baselines count, with every non-result a failure, these conservative rates clear AutoSpec on every model and reach Preguss’s per-trial rate at the top of the range, from a single deterministic run at temperature 0 where Preguss averages three trials. The three tools use different success oracles: AutoSpec targets functional correctness, Preguss freedom from runtime errors, and scribe a contract that passes both enforcement and replacement, which the next paragraph shows subsumes Preguss’s condition. One feature makes the comparison fairer than the differing oracles suggest: scribe’s enforcement turns on ESBMC’s full safety set, covering the runtime-error class Preguss proves absent, while also checking a functional postcondition and caller-sufficiency, so a passing scribe result certifies at least as much as a passing Preguss one. Table I reports the per-step pass rates, with the same pattern across the three models: enforcement is the binding gate and replacement nearly always follows once it passes. postcondition toward one the body satisfies. Most targets converge in a single iteration (Figure 2). On the X509 parser, scribe verifies 5 of 6 target functions with Opus and Kimi and 3 of 6 with Qwen, against the 6 of 6 AutoSpec reports; the function set is similar but not identical, so we read this as close rather than head-to-head. RQ1 Answer Model-checker counterexamples alone provide an effective refinement signal for contract inference. Across the evaluated benchmarks scribe reaches verification rates comparable to prior approaches that additionally rely on weakest-precondition reasoning, value analysis, or runtime-error annotations, while most contracts converge after a single refinement iteration. TABLE I: RQ1 contract-inference success Tool (oracle) Frama-C-Problems X509 AutoSpec (func.) 31/51 (60.8%) 6/6 Preguss (RTE) 122/153a (79.7%) n/a scribe, Opus 4.8 36/51 (70.6% / 85.7%) 5/6 scribe, Kimi K2.6 40/51 (78.4% / 85.1%) 5/6 scribe, Qwen3.6-27B 36/51 (70.6% / 81.8%) 3/6 a Per-trial rate over three trials. TABLE I: RQ1 per-step pass rates over refinement attempts, per model. Model Enforce Replace Kimi K2.6 0.82 0.95 Opus 4.8 0.75 0.98 Qwen3.6-27B 0.75 0.93 Figure 2: RQ1 convergence histogram per model on Frama-C-Problems: the iteration at which each harness first reaches a passing enforce and replace. Most targets converge in a single iteration. V-E2 RQ2 (tractability) RQ1 leaves the loop reliably producing a verifiable partial contract. We seed the warm-start arm (hardscribe) from each model’s partial contract and apply up to five enforce-gated strengthening rounds, keeping every accepted round so judge can measure how much tighter each round is than the seed. Strengthening saturates fast in every model (Figure 3): for almost all orderable targets the contract is already at its tightest at the seed (Table I), and where strengthening helps it does so in the first round or two and then stops, its round-over-round gain reaching zero by round two or three. The endpoint comparison agrees (Table I): judging each model’s full contract against its own partial seed over the orderable pairs, the two are equivalent for the large majority of targets and only a few are strictly tighter after strengthening. The warm-start arm costs almost nothing in soundness, keeping the last contract that verifies, so its pass rate matches the partial arm to within one program in every model. The answer to RQ2 is that caller-sufficiency already captures most of the attainable tightness: a cheap partial contract is within a few targets of the strongest contract the loop can reach, a direct validation of the partial-spec stopping point. Two bounds keep this honest. About 40% of round-level comparisons involve a quantified or pointer-dereferencing postcondition judge’s signature-only harness cannot order; we hold those out and fix the denominator to the targets orderable in every round, so the saturation we report speaks only for the contracts judge can compare across all rounds. And the warm-start arm strengthens within the seed’s clause shape, so this rapid saturation shows little tightness is left within that shape, not that no tighter contract of a different shape exists, which we leave to the from-scratch study in §V-G. RQ2 Answer Continued strengthening recovers little beyond the partial contract: caller-sufficiency already captures most of the attainable tightness, and the few targets that tighten do so within a round or two before the returns plateau, so the partial contract is a sound place to stop. Figure 3: RQ2 tightness saturation on Frama-C-Problems. Per model, the share of orderable targets strictly tighter than the partial seed at round k (solid) and the round-over-round gain over the previous round (dashed). The denominator is fixed across rounds to the targets judge orders in every round (16 / 18 / 19 for Opus 4.8 / Kimi K2.6 / Qwen3.6-27B), so the solid curve is monotone by construction. TABLE I: RQ2 tightness endpoint, per model. “Partial / Full” are the per-arm pass counts (full arm of 50). Model Sat. @0 Equiv : tighter Partial / Full Kimi K2.6 43/47 13 : 2 40 / 41 Opus 4.8 40/42 18 : 2 36 / 36 Qwen3.6-27B 38/42 14 : 4 36 / 36 V-E3 Soundness and reach on EqBench-C regver runs the contract-free regression harness on all 272 pairs, producing a verdict on 70; the rest time out or hit a tool error and are held out. On the decided pairs it never fabricates an equivalence: 100% recall, zero false negatives (Figure 4). Some of its false positives are not over-detection but dataset mislabels, pairs EqBench labels Eq that are actually non-equivalent; we found nine and filed them upstream [14] , and independent work reports EqBench mislabels as well [45]. We draw no cross-tool ranking (see §V-B): the comparable checkers decide partial rather than safety-preserving conditional equivalence, so EqBench-C serves as a soundness check, not a competitive baseline. Reach with contracts. A developer runs the contract-free baseline first and escalates only the pairs it cannot decide; on that undecided tail scribe infers a one-sided contract for the changed function and regver runs again. This is where contracts earn their keep: they recover 9, 11, and 7 correct decisions for Opus, Kimi, and Qwen on pairs the baseline left as timeouts or tool errors, pushing the decided count from 70 to 105 / 106 / 102 (Table IV), and every recovered decision is a real divergence the baseline was too weak to expose. The gain comes at an expected precision cost: the inferred contracts over-approximate, so the recovered tail is false-alarm-heavy. But each false alarm lands on a pair the baseline could not decide at all, a triageable over-approximation rather than a regression. Soundness holds under the relation we target: no model fabricates an equivalence, the lone dataset-scored exception being triangularMod under Qwen, non-equivalent under full equivalence but equivalent under the safety-preserving conditional equivalence regver targets, since the two versions agree wherever the old one terminates; we report it as the dataset scores it rather than substitute our own oracle. Contracts therefore extend reach into EqBench-C’s hardest cases and fail safe: every decision they add is correct or a triageable false alarm, never a missed difference. TABLE IV: EqBench-C reach. Counts are out of 272 pairs. Arm Decided Correct FP FN Baseline (contract-free) 70 56 14 0 + contracts, Opus 4.8 105 65 40 0 + contracts, Kimi K2.6 106 67 39 0 + contracts, Qwen3.6-27B 102 63 38 1a a triangularMod: false FN under safety-preserving conditional equivalence. Figure 4: Contract-free baseline regression-verification outcomes on EqBench-C. The false-negative bucket (a non-equivalent pair called equivalent) is empty: the baseline never fabricates an equivalence. V-F Discussion The results cohere around the contributions. RQ1 supports C2, that BMC trace feedback is enough to drive frame inference: a single model checker driven by counterexamples infers verifiable contracts competitively with heavier weakest-precondition pipelines. RQ2 supports the partial-spec stopping point of Theorem T1 (C1), the cheap partial contract already close to the tightest a strengthening loop reaches, with judge (C3) supplying the tightness ordering behind that claim and reporting unorderable rounds as a scope bound. The refinement telemetry shows the mechanism, enforcement the binding gate and the loop only ever weakening an over-strong postcondition; and the EqBench-C baseline backs the soundness half of C1 directly, with zero fabricated equivalences. V-G Threats To Validity Construct validity. The cross-tool RQ1 comparison spans different success oracles, so we present it as a situating comparison rather than a head-to-head. On EqBench-C regver runs in two arms against the dataset’s full-equivalence labels as a soundness check, not a tool ranking; the reported cascade composes them post hoc, faithfully, since pairs are scored independently and the escalation gate reads only the baseline’s abstention, not the label. Because regver targets the weaker conditional equivalence, a pair the dataset scores as a miss may be correct under our notion (triangularMod); scoring against the dataset regardless, such mismatches can only count against us. judge (C3) reports a relative tightness ordering on admit sets, not whether a contract characterises f completely; we always pair its verdict with enforcement, so a tighter-under-judge contract that also enforces is unambiguously a tighter sound contract. The C1 guarantee holds under its assumptions on assigns aliasing, nondeterministic external calls, and termination; outside those it degrades to an honest unknown rather than a false proof. Internal validity. scribe runs each model once at temperature 0, a single deterministic trajectory rather than an average over LLM sampling; we mitigate by reporting three models whose refinement telemetry is near-identical, but a different seed could shift individual cases. Non-results are excluded from the pass-rate denominator, which the two-way reporting (§V) keeps honest since none is a wrong verdict. On EqBench-C the size and make-up of the undecided tail the treatment arm escalates on depend on the per-query timeout, fixed at 300s across both arms. RQ2’s warm start tightens only within the seed’s clause shape and cannot reach a structurally different contract; we frame it as the marginal value of continued strengthening and keep judge strictly post hoc, so the loop is gated on enforcement, never on the tightness measure it reports. External validity. The baseline comparison is one-way (published numbers, not re-runs), on the same full-denominator basis they report. The benchmarks are small (Frama-C-Problems averages about seventeen lines, the X509 study six functions, EqBench-C crafted rather than production code), so generalisation to large real-world C, and to C++, is future work. The supported program class is bounded by engineering gaps with known fixes: the tree-sitter call/include graph misses indirect, virtual, and macro-expanded calls (an LLVM-IR pipeline with SVF [51] or libclang closes this), the regver rename pass cannot rewrite identifiers in macro bodies (Coccinelle [35]), and its side-effect comparator sees only writes through pointer parameters (bi-abduction [11] and Infer-style footprints extend it). judge’s tightness figures exist only on its primitive-typed signature class. These are engineering scope bounds, not open research questions. VI Conclusion We asked whether a partial, caller-sufficient contract, rather than a full behavioral specification, is enough to verify regression equivalence. Theorem T1 answers yes for safety-preserving conditional equivalence: a one-sided contract that abstracts only the old version, scoped to the property worth preserving, is sound for the regression check, and a depth-bounded closure (Lemma L1) bounds the contract closure so the proof scales. The target of inference is therefore not a complete specification but the weakest contract a caller needs. An end-to-end system (scribe, contractor, regver) infers these contracts automatically from the model checker’s own counterexamples, with no separate specification step. On Frama-C-Problems and the ANSSI X509 parser this reaches a verification rate comparable to the weakest-precondition tools AutoSpec and Preguss while certifying a stronger property, enforcement plus caller-sufficiency with runtime-error freedom included, which answers RQ1: counterexample feedback alone is a sufficient signal for frame inference. Strengthening each inferred contract past caller-sufficiency barely tightens it, the partial and warm-started contracts coming out judge-equivalent for the large majority of comparable targets, so the partial-spec stopping point of Theorem T1 is close to the practical ceiling rather than a compromise (RQ2). A decision procedure for contract subsumption (judge) reports these tightness results as a real set-inclusion ordering rather than a gameable clause count. The regression check underneath is sound by construction: on EqBench-C regver never fabricates an equivalence, and run as a soundness oracle it surfaced nine pairs the suite mislabels as equivalent, more than concurrent work reports. Together these establish that sound, modular regression verification can be driven by a model checker’s own counterexamples and a partial contract, with no hand-written specification. Two directions follow naturally. LLM-driven C++ contract inference: every published LLM contract-inference tool we are aware of is C-only, so inferring functional contracts for C++ operator overloads, initializer-list constructors, RAII destructors, and template instantiations over the standard library is an unaddressed problem and the natural next target for this line of work. Regression verification across signature changes: RVT [20], Reve [27], SymDiff [28], and regver all assume the old and new versions share a signature, so aligning refactored signatures (parameter reordering, splitting, merging, type changes) for verification-grade equivalence is an open problem, naturally cast as a relational extension of Theorem T1 in which the parameter alignment is itself part of the inference. VII Acknowledgements The authors acknowledge the use of generative AI tools in both the development of the research tooling and the preparation of this manuscript. All AI-assisted content was subsequently reviewed, revised, and validated by the authors, who assume full responsibility for the integrity and accuracy of the final publication. References [1] J. Amilon, Z. Esen, D. Gurov, C. Lidström, and P. Rümmer (2024) An exercise in mind reading: automatic contract inference for frama-c. In Guide to Software Verification with Frama-C: Core Components, Usages, and Applications, N. Kosmatov, V. Prevosto, and J. Signoles (Eds.), p. 553–582. External Links: ISBN 978-3-031-55608-1, Document, Link Cited by: §I-B. [2] J. Amilon, D. Gurov, C. Lidström, M. Nyberg, G. Ung, and O. Wingbrant (2025) AutoDeduct: a tool for automated deductive verification of c code. External Links: 2501.10889, Link Cited by: §I-B, §V-B. [3] Anthropic (2026-05-28)Introducing claude opus 4.8(Website) External Links: Link Cited by: §V-C. [4] R. Back and J. von Wright (1998) Refinement calculus - A systematic introduction. Graduate Texts in Computer Science, Springer. External Links: Link, Document, ISBN 978-0-387-98417-9 Cited by: §IV-D. [5] J. Backes, S. Person, N. Rungta, and O. Tkachuk (2013) Regression verification using impact summaries. In Model Checking Software, E. Bartocci and C. R. Ramakrishnan (Eds.), Berlin, Heidelberg, p. 99–116. External Links: ISBN 978-3-642-39176-7 Cited by: §I-A. [6] S. Badihi, F. Akinotcho, Y. Li, and J. Rubin (2020) ARDiff: scaling program equivalence checking via iterative abstraction and refinement of common code. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020, New York, NY, USA, p. 13–24. External Links: ISBN 9781450370431, Link, Document Cited by: §I-A, §V-B. [7] S. Badihi, Y. Li, and J. Rubin (2021) EqBench: a dataset of equivalent and non-equivalent program pairs. In 2021 IEEE/ACM 18th International Conference on Mining Software Repositories (MSR), Vol. , p. 610–614. External Links: Document Cited by: §V-A. [8] D. Banerjee, O. Bouissou, and S. Zetzsche (2026) DafnyPro: llm-assisted automated verification for dafny programs. External Links: 2601.05385, Link Cited by: §I-B. [9] I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh (1997) Efficient detection of vacuity in actl formulas. In Computer Aided Verification, O. Grumberg (Ed.), Berlin, Heidelberg, p. 279–290. External Links: ISBN 978-3-540-69195-2 Cited by: Remark 1. [10] A. Beg, D. O’Donoghue, and R. Monahan (2026) Evaluating llm-generated acsl annotations for formal verification. External Links: 2602.13851, Link Cited by: §I-B. [11] C. Calcagno, D. Distefano, P. O’Hearn, and H. Yang (2009) Compositional shape analysis by means of bi-abduction. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’09, New York, NY, USA, p. 289–300. External Links: ISBN 9781605583792, Link, Document Cited by: §I-B, §V-G. [12] W. Cao, G. Wu, T. Xu, Y. Yao, H. Wei, T. Chen, and X. Ma (2025-06) Clause2Inv: a generate-combine-check framework for loop invariant inference. Proc. ACM Softw. Eng. 2 (ISSTA). External Links: Link, Document Cited by: §I-B. [13] Y. Charalambous, C. N. C. Jr, L. Lamb, and L. C. Cordeiro (2025) UnitTenX: generating tests for legacy packages with ai agents powered by formal verification. External Links: 2510.05441, Link Cited by: §I-A. [14] Y. Charalambous (2026) Mislabeled equivalent pairs in EqBench-C. Note: Issue #15, shrBadihi/EqBench GitHub repositoryhttps://github.com/shrBadihi/EqBench/issues/15 Cited by: §V-E3. [15] K. Etemadi, B. Mohammadi, Z. Su, and M. Monperrus (2025) Mokav: execution-driven differential testing with llms. Vol. 230. External Links: ISSN 0164-1212, Document, Link Cited by: §I-A. [16] D. Felsing, S. Grebing, V. Klebanov, P. Rü mmer, and M. Ulbrich (2014) Automating regression verification. In Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE ’14, New York, NY, USA, p. 349–360. External Links: ISBN 9781450330138, Link, Document Cited by: §I-A. [17] P. Garg, D. Neider, P. Madhusudan, and D. Roth (2016) Learning invariants using decision trees and implication counterexamples. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’16, New York, NY, USA, p. 499–512. External Links: ISBN 9781450335492, Link, Document Cited by: §I-B. [18] J. Glock, J. Pichler, and M. Pinzger (2024) PASDA: a partition-based semantic differencing approach with best effort classification of undecided cases. Journal of Systems and Software 213, p. 112037. External Links: ISSN 0164-1212, Document, Link Cited by: §I-A. [19] B. Godlin and O. Strichman (2009) Regression verification. In Proceedings of the 46th Annual Design Automation Conference, DAC ’09, New York, NY, USA, p. 466–471. External Links: ISBN 9781605584973, Link, Document Cited by: §I-B, §I-A. [20] B. Godlin and O. Strichman (2013) Regression verification: proving the equivalence of similar programs. Software Testing, Verification and Reliability 23 (3), p. 241–258. External Links: Document, Link, https://onlinelibrary.wiley.com/doi/pdf/10.1002/stvr.1472 Cited by: §I, §I-B, §I-A, §IV-A, §IV-A, §V-B, §VI. [21] G. Granberry, W. Ahrendt, and M. Johansson (2025) Specify what? enhancing neural specification synthesis by symbolic methods. In Integrated Formal Methods, N. Kosmatov and L. Kovács (Eds.), Cham, p. 307–325. External Links: ISBN 978-3-031-76554-4 Cited by: §I, §I-B, §I-B, §IV-D, §V-B. [22] C. Hawblitzel, M. Kawaguchi, S. K. Lahiri, and H. Rebêlo (2013) Towards modularly comparing programs using automated theorem provers. In Automated Deduction – CADE-24, M. P. Bonacina (Ed.), Berlin, Heidelberg, p. 282–299. External Links: ISBN 978-3-642-38574-2 Cited by: §I-A. [23] C. Helbling, G. Leach-Krouse, S. Lasser, and G. Sullivan (2025) Cozy: comparative symbolic execution for binary programs. In Proceedings 2025 Workshop on Binary Analysis Research, BAR 2025. External Links: Link, Document Cited by: §I-A. [24] C. A. R. Hoare (1969-10) An axiomatic basis for computer programming. Commun. ACM 12 (10), p. 576–580. External Links: ISSN 0001-0782, Link, Document Cited by: Definition 3. [25] M. Jakobs and M. Wiesner (2022) PEQtest: testing functional equivalence. In Fundamental Approaches to Software Engineering, E. B. Johnsen and M. Wimmer (Eds.), Cham, p. 184–204. External Links: ISBN 978-3-030-99429-7 Cited by: §I-A. [26] M. Jakobs (2021) PEQCHECK: localized and context-aware checking of functional equivalence. In 2021 IEEE/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE), Vol. , p. 130–140. External Links: Document Cited by: §I-A. [27] V. Klebanov, P. Rümmer, and M. Ulbrich (2018) Automating regression verification of pointer programs by predicate abstraction. Formal Methods in System Design 52 (3), p. 229–259. External Links: Document Cited by: §I-A, §V-B, §VI. [28] S. K. Lahiri, C. Hawblitzel, M. Kawaguchi, and H. Rebêlo (2012) SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In Computer Aided Verification, P. Madhusudan and S. A. Seshia (Eds.), Berlin, Heidelberg, p. 712–717. External Links: ISBN 978-3-642-31424-7 Cited by: §I-A, §IV-A, §V-B, §VI. [29] S. K. Lahiri, K. L. McMillan, R. Sharma, and C. Hawblitzel (2013) Differential assertion checking. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, New York, NY, USA, p. 345–355. External Links: ISBN 9781450322379, Link, Document Cited by: §I-A, §IV-A. [30] B. H. Liskov and J. M. Wing (1994-11) A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16 (6), p. 1811–1841. External Links: ISSN 0164-0925, Link, Document Cited by: §IV-D. [31] C. Luo, W. Meng, and S. Wang (2024) Strengthening supply chain security with fine-grained safe patch identification. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering, ICSE ’24, New York, NY, USA. External Links: ISBN 9798400702174, Link, Document Cited by: §I-A. [32] B. Meyer (1992) Applying ’design by contract’. Computer 25 (10), p. 40–51. External Links: Document Cited by: Definition 3. [33] Moonshot AI (2026)Moonshotai/kimi-k2.6(Website) External Links: Link Cited by: §V-C. [34] S. Padhi, R. Sharma, and T. Millstein (2016) Data-driven precondition inference with learned features. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’16, New York, NY, USA, p. 42–56. External Links: ISBN 9781450342612, Link, Document Cited by: §I-B. [35] Y. Padioleau, J. Lawall, R. R. Hansen, and G. Muller (2008) Documenting and automating collateral evolutions in linux device drivers. In Proceedings of the 3rd ACM SIGOPS/EuroSys European Conference on Computer Systems 2008, Eurosys ’08, New York, NY, USA, p. 247–260. External Links: ISBN 9781605580135, Link, Document Cited by: §V-G. [36] H. Palikareva, T. Kuchta, and C. Cadar (2016) Shadow of a doubt: testing for divergences between software versions. In Proceedings of the 38th International Conference on Software Engineering, ICSE ’16, New York, NY, USA, p. 1181–1192. External Links: ISBN 9781450339001, Link, Document Cited by: §I-A. [37] M. Patnaik (2020) A repository dedicated for problems related to verification of programs using the tool Frama-C. Note: https://github.com/manavpatnaik/frama-c-problemsAccessed: 2026-06 Cited by: §V-A. [38] S. Person, M. B. Dwyer, S. Elbaum, and C. S. Pundefinedsundefinedreanu (2008) Differential symbolic execution. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, SIGSOFT ’08/FSE-16, New York, NY, USA, p. 226–237. External Links: ISBN 9781595939951, Link, Document Cited by: §I-A. [39] M. A. A. Pirzada, W. Wang, Y. Charalambous, K. Korovin, and L. C. Cordeiro (2026) ConVer: using contracts and loop invariant synthesis for scalable formal software verification. External Links: 2605.27051, Link Cited by: §I-B, §IV-C. [40] G. Poesia, C. Loughridge, and N. Amin (2024) Dafny-annotator: ai-assisted verification of dafny programs. External Links: 2411.15143, Link Cited by: §I-B. [41] Qwen Team (2026-04) Qwen3.6-27B: flagship-level coding in a 27B dense model. External Links: Link Cited by: §V-C. [42] Z. Rakamaric and A. J. Hu (2008) Automatic inference of frame axioms using static analysis. In 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, Vol. , p. 89–98. External Links: Document Cited by: §I-B. [43] H. G. Rice (1953) Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society 74 (2), p. 358–366. External Links: ISSN 00029947, 10886850, Link Cited by: §I. [44] C. Richter and H. Wehrheim (2025) Beyond postconditions: can large language models infer formal contracts for automatic software verification?. External Links: 2510.12702, Link Cited by: §I-B. [45] L. Sarker, A. Satter, and T. BultanJ. Deshmukh, K. Havelund, and A. Pinto (Eds.) (2026) Quantitative symbolic patch impact analysis. Springer Nature Switzerland, Cham. External Links: ISBN 978-3-032-28079-4 Cited by: §I-A, §V-E3. [46] X. Si, H. Dai, M. Raghothaman, M. Naik, and L. Song (2018) Learning loop invariants for program verification. In Advances in Neural Information Processing Systems, S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (Eds.), Vol. 31, p. . External Links: Link Cited by: §I-B. [47] Á. Silva, A. Mendes, and R. Martins (2025) Inferring multiple helper dafny assertions with llms. External Links: 2511.00125, Link Cited by: §I-B. [48] A. Solar-Lezama (2008) Program synthesis by sketching. Ph.D. Thesis, University of California, Berkeley. Cited by: §I-B. [49] S. Spies, L. Gäher, M. Sammler, and D. Dreyer (2024-06) Quiver: guided abductive inference of separation logic specifications in coq. Proc. ACM Program. Lang. 8 (PLDI). External Links: Link, Document Cited by: §I-B. [50] Y. Su, T. Bu, Q. Yang, Y. Ci, and E. Tian (2026) CIll: cti-guided invariant generation via llms for model checking. External Links: 2602.23389, Link Cited by: §I-B. [51] Y. Sui and J. Xue (2016) SVF: interprocedural static value-flow analysis in llvm. In Proceedings of the 25th International Conference on Compiler Construction, C ’16, New York, NY, USA, p. 265–266. External Links: ISBN 9781450342414, Link, Document Cited by: §V-G. [52] N. Tihanyi, Y. Charalambous, R. Jain, M. A. Ferrag, and L. C. Cordeiro (2025) A new era in software security: towards self-healing software via large language models and formal verification. Vol. . External Links: Document Cited by: §I-B. [53] M. Wang, J. Wang, and X. Cheng (2025) BALI: branch-aware loop invariant inference with large language models. External Links: 2601.00882, Link Cited by: §I-B. [54] Z. Wang, T. Lin, M. Chen, H. Li, M. Yang, X. Yi, S. Qin, Y. Luo, X. Li, B. Gu, L. Lu, and J. Yin (2026-04) A tale of 1001 loc: potential runtime error-guided specification synthesis for verifying large-scale programs. Proc. ACM Program. Lang. 10 (OOPSLA1). External Links: Link, Document Cited by: §I, §I-B, §IV-D, §V-A, §V-B. [55] A. Wei, J. Cao, R. Li, H. Chen, Y. Zhang, Z. Wang, Y. Liu, T. S. F. X. Teixeira, D. Yang, K. Wang, and A. AikenC. Christodoulopoulos, T. Chakraborty, C. Rose, and V. Peng (Eds.) (2025-11) EquiBench: benchmarking large language models’ reasoning about program semantics via equivalence checking. Association for Computational Linguistics, Suzhou, China. External Links: Link, Document, ISBN 979-8-89176-332-6 Cited by: §V-A. [56] A. Wei, T. Sun, T. Suresh, H. Wu, K. Wang, and A. Aiken (2026) Quokka: accelerating program verification with LLMs via invariant synthesis. External Links: Link Cited by: §I-B. [57] C. Wen, J. Cao, J. Su, Z. Xu, S. Qin, M. He, H. Li, S. Cheung, and C. Tian (2024) Enchanting program specification synthesis by large language models using static analysis and program verification. In Computer Aided Verification, A. Gurfinkel and V. Ganesh (Eds.), Cham, p. 302–328. External Links: ISBN 978-3-031-65630-9 Cited by: §I, §I-B, §IV-D, §V-A, §V-A, §V-B. [58] G. Wu, W. Cao, Y. Yao, H. Wei, T. Chen, and X. Ma (2024) LLM meets bounded model checking: neuro-symbolic loop invariant inference. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE ’24, New York, NY, USA, p. 406–417. External Links: ISBN 9798400712487, Link, Document Cited by: §I-B. [59] Z. Yin, D. Yuan, Y. Zhou, S. Pasupathy, and L. Bairavasundaram (2011) How do fixes become bugs?. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, ESEC/FSE ’11, New York, NY, USA, p. 26–36. External Links: ISBN 9781450304436, Link, Document Cited by: §I.