Assurance envelopes compute the least-cost subset of prior test, proof and trace evidence a coding agent must reload for a given change

arXiv·medium signalXBlueskyLinkedInCopy link

When a coding agent returns to existing software it inherits tests, type checks, proofs, static analyses and traces from earlier runs; reloading everything wastes context, and dropping the wrong piece leaves a required property unsupported. This work models evidence and combination rules as a typed inference graph and asks for the minimum-cost evidence subset whose forward closure reaches the change's obligations, validating every selection by that closure rather than trusting the optimizer. On graphs built from preserved outcomes of real prior AI coding-agent runs (Rust, IronBlocks, Pong) the minimum envelope is task-dependent, sometimes does not exist, and some properties need several evidence pieces jointly; across a 249-instance prespecified synthetic benchmark median CP-SAT solve time stayed under 20 ms at 500-evidence graphs, with timeouts driven by many alternative derivations per target rather than raw graph size.