Skip to content

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

Sep 2026 · 0 citations · 50 references
Computer Science

TL;DR

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.

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.

View source

Similar papers

#artificial intelligence Review Sep 2026

From Verification Failures to Reusable Guidance for Coding Agents

Coding agents need to establish that a program satisfies a specification and that the specification captures the requested behavior. We study how expert diagnosis of verification failures can become reusable guidance for this work. Our approach combines executable language definitions in the K framework with a kit of p...

Yu-Qing Zhai, Xiao-Hong Chen, Ling-Ming Zhang et al. · 0 citations
#artificial intelligence Preprint Oct 2026

Verify Claims, Not Scores: Evidence-Based Verification of Modular Agents

When developers change one component of an agent, such as its controller, a learned model or its verifier, they usually judge the change by an aggregate task score. That score cannot tell whether improvement was attainable, which component lost value, or what the agent's own checks certify. We introduce a claim-specifi...

A. Alzahrani · 0 citations
Preprint Aug 2026

A Policy Algebra for Trust-Preserving Agentic AI Execution

A policy algebra is proposed that defines the reliability envelope within which agent capability may be exercised and provides researchers and practitioners with formal correctness conditions, executable decision semantics, and trace evidence for building agents that are not only capable, but reliably capable.

Bhaskar Tripathi, Anurag Kumar, R. Kumar et al. · 0 citations
#software testing Review Sep 2026

From Agent Output to Authorized Transition

This paper presents the Agile-V Assurance Spine, a cross-domain transition contract for software, firmware, and PCB engineering, and contributes a precise vocabulary, compositional architecture, domain profiles, mapping to open-source implementations, and an adversarial evaluation agenda.

Christopher Koch · 0 citations
#software testing Review Aug 2026

Model-Based Agentic Software Engineering

MAGE explains how externalized knowledge, bounded action, independent evaluation, and retained human authority can compose into a governed engineering environment, and proposes tests of when that environment turns commodity intelligence into durable engineering progress.

James C. Davis, Kelechi G. Kalu, Hui-Yun Peng et al. · 2 citations

Related blog posts

Microsoft Research Blog Nov 5, 2026

Formally verifying agent-written full-stack web apps with PDD Kit

AI agents can generate code at a scale that’s hard for humans to review line-by-line. PDD Kit helps ensure the code is doing what the developer intended by creating formal specifications and testing against them. It converts developer intent into a Verus specification, proves AI-generated code meets it for every input, and uses tests where proofs aren't practical. Developers review intent, not every line. The post Formally verifying agent-written full-stack web apps with PDD Kit appeared first o…

GPT-Lab Nov 3, 2026

Sovereignty Is the Option to Leave

Is your company’s AI sovereign? A practical guide for CIOs on AI vendor lock-in, EU Data Act switching, cloud sovereignty, and testing your exit plan before you need it. The post Sovereignty Is the Option to Leave appeared first on GPT-Lab.

Microsoft Research Blog Oct 30, 2026

From synthetic enterprise data evaluations to real Microsoft Copilot AI confidence

Evaluating Microsoft Copilot at enterprise scale requires test data that captures the full complexity of real organizations, yet real enterprise data contains sensitive information that cannot be used for evaluation under any circumstances. The post From synthetic enterprise data evaluations to real Microsoft Copilot AI confidence appeared first on Microsoft Research.

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.