LLM-Inferred Partial Contracts Enable Sound Regression Verification

Regression verification ensures software patches preserve intended behavior without re-verifying entire codebases, but existing techniques require expensive whole-program reasoning or manually written specifications that are rarely available. A new paper from Charalambous et al. introduces the first contract-based regression verification tool that infers partial contracts automatically using LLMs. The contracts are derived from the checker's own counterexamples, eliminating the need for a separate specification step. Crucially, the authors demonstrate that partial, caller-sufficient contracts capture nearly all the attainable tightness of full behavioral specifications; strengthening them further barely moves the metric.

On the third-party EqBench-C benchmark, the tool never fabricated an equivalence — returning zero false proofs and reporting an unprovable difference instead. It also surfaced nine pairs that EqBench mislabels as equivalent, outperforming a concurrent tool. On Frama-C-Problems and the ANSSI X509 parser, the verification rate is comparable to AutoSpec and Preguss, but a passing result certifies a stronger property: safety-preserving conditional equivalence (enforcement plus caller-sufficiency). This work shows that partial, LLM-inferred contracts are sufficient for sound regression verification, potentially automating a critical but historically manual task in software engineering.