# Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification

arXiv: https://arxiv.org/abs/2607.10291 · HTML: https://mlsanity.com/paper/2607.10291/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 20 of its 58 references that are in the map.
- First posted on arXiv 11 Jul 2026.

## Builds on (most cited first, 20 of 20)

- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking](https://mlsanity.com/paper/2502.12466/) (2025)
- [DafnyPro: LLM-Assisted Automated Verification for Dafny Programs](https://mlsanity.com/paper/2601.05385/) (2026)
- [dafny-annotator: AI-Assisted Verification of Dafny Programs](https://mlsanity.com/paper/2411.15143/) (2024)
- [Mokav: Execution-driven Differential Testing with LLMs](https://mlsanity.com/paper/2406.10375/) (2024)
- [Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods](https://mlsanity.com/paper/2406.15540/) (2024)
- [Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?](https://mlsanity.com/paper/2510.12702/) (2025)
- [A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs](https://mlsanity.com/paper/2512.24594/) (2025)
- [Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis](https://mlsanity.com/paper/2509.21629/) (2025)
- [Inferring multiple helper Dafny assertions with LLMs](https://mlsanity.com/paper/2511.00125/) (2025)
- [AutoDeduct: A Tool for Automated Deductive Verification of C Code](https://mlsanity.com/paper/2501.10889/) (2025)
- [CIll: CTI-Guided Invariant Generation via LLMs for Model Checking](https://mlsanity.com/paper/2602.23389/) (2026)
- [PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)](https://mlsanity.com/paper/2101.09042/) (2021)
- [PASDA: A Partition-based Semantic Differencing Approach with Best Effort Classification of Undecided Cases](https://mlsanity.com/paper/2311.08071/) (2023)
- [cozy: Comparative Symbolic Execution for Binary Programs](https://mlsanity.com/paper/2504.00151/) (2025)
- [UnitTenX: Generating Tests for Legacy Packages with AI Agents Powered by Formal Verification](https://mlsanity.com/paper/2510.05441/) (2025)
- [BALI: Branch-Aware Loop Invariant Inference with Large Language Models](https://mlsanity.com/paper/2601.00882/) (2025)
- [Evaluating LLM-Generated ACSL Annotations for Formal Verification](https://mlsanity.com/paper/2602.13851/) (2026)
- [Quantitative Symbolic Patch Impact Analysis](https://mlsanity.com/paper/2605.13885/) (2026)
- [ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification](https://mlsanity.com/paper/2605.27051/) (2026)

## Abstract (arXiv)

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 safety-preserving conditional equivalence: enforcement plus caller-sufficiency.