Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification

• URL: http://arxiv.org/abs/2607.10291v1
• Date: Sat, 11 Jul 2026 12:40:22 GMT
• Title: Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification
• Abstract summary: We present the first contract-based regression verification tool.<n>Contract soundness is ensured by proving all function versions match the behavior.<n>We ask whether a partial, caller-sufficient contract, rather than a full behavioral specification, is enough.
• Score: 7.004725450780227
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Dead text or binding clause? Measuring and restoring constraint influence in black-box LLM dialogues [0.0]
  Multi-turn dialogues let users revoke constraints as easily as impose them, but revocation does not reliably take effect.<n>No existing instrument measures this influence per clause, predicts it before delivery, or repairs it under matched budgets.<n>sysname closes the three gaps through the model API alone.
  arXiv  Detail & Related papers  (2026-08-12T21:12:32Z)
• What Can Verifiable Decapsulation Tests Certify? Pass Bounds and Fault-Recognition Limits for FO-Based KEMs [0.0]
  Black-box tests for Fujisaki-Okamoto decapsulation observe the sampled execution seen by the harness.<n>We study confirmation-code-augmented KEM variants under an honest-reference harness.
  arXiv  Detail & Related papers  (2026-06-03T04:46:17Z)
• Scaling Laws for Agent Harnesses via Effective Feedback Compute [53.68149869349268]
  emphEffective Feedback Compute (EFC) is a trace-level scaling coordinate that credits feedback only when it is informative, valid, non-redundant, and retained for subsequent decisions.<n>EFC-based coordinates consistently predict failure rates better than raw-compute baselines.
  arXiv  Detail & Related papers  (2026-05-28T09:45:47Z)
• RubricRefine: Improving Tool-Use Agent Reliability with Training-Free Pre-Execution Refinement [0.36165327398913766]
  Iterative self-refinement is a popular inference-time reliability technique.<n>But its effectiveness in code-mode tool use depends heavily on the structure of the feedback signal.<n>We introduceRefine, a training-free method for pre-execution semantic contract verification.
  arXiv  Detail & Related papers  (2026-05-10T19:57:32Z)
• Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon [0.0]
  ML kernels ship with an implicit contract about what it computes.<n>Recent empirical work has measured the gap across silicon platforms, but none of it specifies the contract being violated.<n>We present a specification language for kernel contracts.
  arXiv  Detail & Related papers  (2026-04-23T19:46:52Z)
• IMPACT-CYCLE: A Contract-Based Multi-Agent System for Claim-Level Supervisory Correction of Long-Video Semantic Memory [73.22944697933603]
  Existing pipelines produce opaque, end-to-end outputs that expose no intermediate state for inspection.<n>We present IMPACT-Cycle, a supervisory multi-agent system that reformulates long-video understanding as a multimodal iterative claim-level maintenance.
  arXiv  Detail & Related papers  (2026-04-22T03:03:33Z)
• Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
  We propose a paired-outcome measurement interface for auditing a single protocol step on exact-match tasks.<n>For each instance, the interface records a baseline correctness bit and a post-step correctness bit.<n>These rates predict accuracy changes and define a reusable empirical interface testable across seeds, mixtures, and pipelines.
  arXiv  Detail & Related papers  (2026-04-20T13:25:40Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• SABER: Small Actions, Big Errors -- Safeguarding Mutating Steps in LLM Agents [52.20768003832476]
  We analyze execution traces on $$-Bench (Airline/Retail) and SWE-Bench Verified.<n>We formalize emphdecisive deviations, earliest action, level divergences that flip success to failure.<n>We introduce cm, a model-agnostic, gradient-free, test-time safeguard.
  arXiv  Detail & Related papers  (2025-11-26T01:28:22Z)
• Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation [11.445615378917578]
  PACT is a program assessment and contract-adherence evaluation framework.<n>It provides a comprehensive test-suite corpus focused on contract violations.<n>It enables a systematic analysis of code generation under varied prompting conditions.
  arXiv  Detail & Related papers  (2025-10-14T01:12:37Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  We introduce SolBench, a benchmark for evaluating the functional correctness of Solidity smart contracts generated by code completion models.<n>We propose a Retrieval-Augmented Code Repair framework to verify functional correctness of smart contracts.<n>Results show that code repair and retrieval techniques effectively enhance the correctness of smart contract completion while reducing computational costs.
  arXiv  Detail & Related papers  (2025-03-03T01:55:20Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.