# Assurance Envelopes for Autonomous Coding Agents: Minimum-Cost Evidence for Software Change

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 15 of its 50 references that are in the map.
- First posted on arXiv 14 Sep 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

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

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering](https://mlsanity.com/paper/2405.15793/) (2024)
- [MemGPT: Towards LLMs as Operating Systems](https://mlsanity.com/paper/2310.08560/) (2023)
- [Repoformer: Selective Retrieval for Repository-Level Code Completion](https://mlsanity.com/paper/2403.10059/) (2024)
- [Interactive Code Generation via Test-Driven User-Intent Formalization](https://mlsanity.com/paper/2208.05950/) (2022)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [Engineering Trustworthy Self-Adaptive Software with Dynamic Assurance Cases](https://mlsanity.com/paper/1703.06350/) (2017)
- [Perpetual Assurances for Self-Adaptive Systems](https://mlsanity.com/paper/1903.04771/) (2019)
- [Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents](https://mlsanity.com/paper/2603.17150/) (2026)
- [Proof Repair across Type Equivalences](https://mlsanity.com/paper/2010.00774/) (2020)
- [Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification](https://mlsanity.com/paper/2509.23061/) (2025)
- [Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM](https://mlsanity.com/paper/2009.12154/) (2020)
- [ACCESS: Assurance Case Centric Engineering of Safety-critical Systems](https://mlsanity.com/paper/2403.15236/) (2024)
- [An Infrastructure Software Perspective Toward Computation Offloading between Executable Specifications and Foundation Models](https://mlsanity.com/paper/2501.02829/) (2025)
- [KISS Sorcar: A Stupidly-Simple General-Purpose and Software Engineering AI Assistant](https://mlsanity.com/paper/2604.23822/) (2026)

## Abstract (arXiv)

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.