Assurance envelopes identify minimal evidence for software changes
Assurance Envelopes for Autonomous Coding Agents: Minimum-Cost Evidence for Software Change
Software EngineeringArtificial IntelligenceProgramming Languages
Summary
When software is changed by automated coding tools, many tests and checks from before still apply but not all are needed each time. The authors study how to find the smallest set of previous evidence like tests and proofs required to verify new changes. They model the relationships between evidence and properties as a graph and use optimization to pick minimal supporting evidence sets. Their method evaluates on small and synthetic examples, showing that different tasks need different evidence, and sometimes no sufficient evidence exists. The work helps reduce wasted effort when verifying software updates.
What this means in practice
- •For software development teams: Reduce repeated verification effort by restoring only necessary prior test and proof evidence during incremental software updates.
- •For automated code generation teams: Choose minimal supporting evidence to assure correctness properties when AI coding agents modify existing software.
Authors
Anjan Goswami
Abstract
When a coding agent returns to existing software, it inherits evidence from earlier engineering work: tests, type checks, proofs, static analyses, and traces. Reloading all of it is wasteful, but dropping a piece the change depends on can leave a required property unsupported. Given the properties a change must preserve, its obligations, we ask which least-cost subset of the available evidence re-establishes them, and we call such a subset a task-conditioned assurance envelope. Evidence and the rules that combine it form a typed inference graph; an obligation is met when forward chaining from the selected evidence reaches it, and we validate every selection by that closure rather than by trusting the optimizer. The software-derived graphs in our evaluation come from preserved outcomes of prior AI coding-agent runs; we freeze those artifacts and ask which accumulated evidence should be restored for a later task. Small graphs from Rust, IronBlocks, and Pong outcomes show that the minimum envelope depends on the task, that none may exist when current evidence cannot re-establish a required property, that some properties need several pieces of evidence together, and that expanding the requirements adds evidence rather than replacing it. A prespecified synthetic benchmark of 249 instances characterizes computation: a baseline that discards the 'several pieces together' structure necessarily fails to re-derive them; every completed exact cross-check agreed with the CP-SAT optimizer; and median solve time stayed below 20 ms at 500-evidence graphs, except that graphs with many alternative derivations per target timed out at far smaller sizes, so structure, not raw size, drives difficulty. The contribution is a bounded application of established optimization to selecting assurance context for a software change; discovering the obligations and downstream agent benefit remain open.