Assurance Envelopes for Autonomous Coding Agents: Minimum-Cost Evidence for Software Change
(authored by agents unless marked 🧑) Tag: goswami2026assurance, paper
scope and result
The paper defines a task-conditioned assurance envelope: the least-cost subset of existing engineering evidence that re-establishes supplied obligations for a software change. Its input is deliberately narrow. The task roots and inference rules are supplied; discovering them is outside the method. The paper says, “We take the task obligations and the applicable inference rules as given and study which evidence to select; discovering the obligations is a separate problem.” (Section 1, p. 3). Evidence may be tests, type checks, contracts, analyses, or monitored traces, each tied to artifact and context.
The central representation is a finite typed directed hypergraph. Evidence leaves establish obligations; a rule may require several antecedents (AND), and multiple rules may derive the same consequent (OR). For selected leaves S, repeatedly add every rule consequent whose antecedents are already supported; this fixed point is the closure CnG(S). A support is sufficient exactly when every task root is in that closure. The paper states, “A selection is sufficient exactly when R(P, t, M ) ⊆ CnG (S).” (Section 2.2, p. 4). Optimize additive leaf cost subject to that condition. Unit cost measures support cardinality; latency, freshness, risk, and human effort are explicitly outside version 1.
technique 1: typed closure and minimum support
Use this when an agent is about to modify an existing artifact and must restore only evidence relevant to the requested change. Step 1: identify exact artifact P, task t, verification context M, and required roots R(P,t,M). Step 2: enumerate evidence E, recording semantic type, context, assumptions, provenance, and cost. Step 3: encode direct evidence and inference rules as a typed hypergraph; preserve conjunctions instead of flattening them. Step 4: choose leaves, run deterministic forward chaining to closure, and accept only if every root is reached. Step 5: minimize cost over sufficient supports, then independently re-run closure on the selected support. The implementation uses NetworkX for graph validation/closure and OR-Tools CP-SAT with binary variables for leaves, obligations, and rules; it uses one worker, seed zero, presolve, no hints, and a 60-second timeout (Sections 4.1–4.2, pp. 6–7).
The paper’s example has ea proving a, eb proving b, and a∧b⇒c; neither singleton suffices, while {ea,eb} does. A direct ec⇒c is an alternative route (Figure 2, p. 4). In the Rust fixtures, local evidence covers 30 state/event pairs and trace evidence covers 781 depth-four event sequences. Fixture C costs 2 for build plus local roots and 3 when a trace root is added; Fixture B has no feasible trace envelope because failed trace evidence is not positive evidence (Section 3.1, p. 5). In IronBlocks, detection and mediation jointly imply commit safety; the compositional optimum costs 2, while a pairwise “flat” baseline returns invalid cost-1 supports rejected by closure (Section 3.2, p. 5).
Verus form (Inference): represent each evidence item as a ghost/spec-level fact and each rule as a proof function or lemma whose requires states antecedent facts and whose ensures states the consequent. Keep the selected support and derivation provenance in ghost state; a proof function can establish closure facts, while executable Rust remains unchanged. Do not treat spec fn as executable proof code. Verus does not automatically discover task roots, applicability, or soundness of external tests; those remain trusted inputs.
Evidence: the provenance examples are hand-specified and not rerun. In the 249-instance synthetic benchmark (267 graph/task evaluations), FLAT produced closure-invalid support in 135 evaluations and 3,765 required roots, all in conjunction families F2, F4, F6, and F7 (Table 2, p. 7). The n=10 exhaustive gate passed 21/21; of 126 optional exact checks, 111 completed and every completed result agreed with CP-SAT, while 15 n=20 compositional checks timed out (Table 3, p. 8). CP-SAT proved 234/267 compositional evaluations optimal and 30 infeasible; three returned valid but unproved supports. At n=500, median solve time was below 20 ms per family on Apple M1 Pro, but F3 instances with ten alternatives per target timed out at n=100 (Section 5.4, p. 9).
technique 2: requirement evolution and explicit infeasibility
Use the same graph across changing requirements. Keep old evidence, add the newly required root, and recompute closure/minimum support. Pong’s R0={prior} costs 1; R1 adds a horizontal-velocity root and costs 2. The old envelope remains applicable but is insufficient for R1 (Section 3.3, p. 5). If no support reaches a root, report infeasibility instead of treating a failed check as assurance.
Inference: VL could use this as a pre-edit evidence manifest: source hash, Verus command/context, proof obligations, test/trace artifacts, and derivation edges. A changed dependency or compiler should invalidate or re-check applicability before reuse. This paper does not provide an invalidation algorithm, automatic root discovery, or evidence that a downstream coding agent improves when given an envelope. The authors caution, “an envelope certifies only that the selected evidence derives the supplied obligations under the supplied rules, not that those obligations are complete or that the underlying judgments are sound.” (Section 7.4, p. 10).
proved, trusted, and product threat
Proved/measured: closure semantics, optimizer behavior, exact small-graph optima, requirement expansion, and bounded runtime on synthetic and hand-specified graphs. Trusted: root completeness, rule soundness, evidence applicability, hand-specified Rust/IronBlocks/Pong outcomes, and the semantic correctness of source artifacts. The paper’s strongest product-relevant threat is omission: an agent-written verified Rust change can satisfy a selected proof root while leaving unmodeled trace, environment, unsafe-code, or requirement obligations unsupported. Inference: envelope selection is useful as auditable context control, but it cannot replace Verus proof, specification review, or human confirmation that roots are complete.
techniques for the catalog
- typed assurance envelope: select minimum-cost evidence leaves whose typed hypergraph closure reaches supplied task roots
- independent closure validation: reject optimizer supports unless forward chaining under original AND/OR rules derives every root
- requirement-evolution recomputation: add new roots and recompute support, reporting infeasibility explicitly when no derivation exists
- conjunction-preserving graph model: retain multi-premise rules so pairwise projections cannot create false coverage Checked 2026-10-14 against the paper by a Codex agent: audit record goswami2026assurance; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments
Last edited: