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

1 Introduction

• A coding agent inherits distributed engineering conclusions, but restoring every prior artifact is unnecessary and may not help the next change.The evaluation uses preserved outcomes from prior AI coding-agent runs and studies evidence restoration, not how the original code was generated.Source: §1 · pp. 1–2
• The task is to select the least-cost existing evidence that re-establishes supplied obligations for a particular program, change, and context.The paper takes obligations and applicable inference rules as inputs rather than inferring them from natural language or code.Source: §1 · p. 2
• The formulation specializes established cover and proof-support problems to selecting evidence for a future coding task’s supplied obligations.The introduction relates independent coverage to weighted set cover and conjunctive or alternative support to minimum-support problems over directed hypergraphs or AND/OR graphs.Source: §1 · p. 2
• The paper formulates task-specific evidence support over typed evidence and explicit inference rules, relating it to known cover and proof-support problems.The evaluation also uses a prespecified 249-instance synthetic benchmark to cross-check optimization and characterize bounded computation.Source: §1 · p. 2
• Rust and IronBlocks graphs show task-dependent minimum support, infeasibility when evidence cannot derive a required root, and conjunctive dependencies lost by a pairwise baseline.The Pong graph shows that requirement expansion retains prior support and adds one evidence leaf.Source: §1 · p. 2
• The work is a bounded evaluation over small software-derived graphs and a synthetic scale study, with task roots and inference rules supplied.The introduction presents four contributions, including implementation and scalability evaluation.Source: §1 · p. 2

2 Task-Conditioned Assurance Envelopes

• Obligations are heterogeneous and context-dependent, so evidence for one property cannot substitute for another unless an explicit rule connects them.Source: §2 · p. 3

2.2 Derivation and sufficiency

• Selected evidence seeds forward chaining: conjunctive rules add consequents only when all premises hold, while alternative rules can derive a root by another route.Source: §2 · p. 3, §2.1 · p. 3, §2.2 · p. 4

2.1 Problem objects

• The task supplies its required roots from known obligations; complete root discovery remains an external requirements and change-impact problem.Source: §2.1 · p. 3

2.3 Minimum support, ties, and infeasibility

• A sufficient selection reaches every supplied root; the envelope minimizes scalar evidence cost, but none exists when current evidence cannot derive all roots.Source: §2.3 · p. 4, §2.2 · p. 4
• V1 treats support cost as scalar; optimizing latency, freshness, human effort, or risk needs a policy and may require a Pareto frontier.Source: §2.3 · p. 4
• Independent fixed coverage is weighted set cover; conjunctions, alternatives, intermediate obligations, and shared leaves yield known hypergraph support problems.Source: §2.3 · p. 4

3 Provenance-Derived Software Graphs

• These are hand-specified graphs from frozen prior-agent outcomes; obligations, rules, and unit costs were prespecified, and an independent closure validator checked selected supports.The experiment studies evidence support, not the quality of the runs that produced the software.Source: §3 · p. 5

3.1 Rust: task conditioning and infeasibility

• For Rust Fixture C, adding the trace root raises the exact optimum from cost 2 to 3; Fixture B’s failed trace evidence leaves its trace task infeasible.The graph fixes preserved, depth-bounded outcomes; it does not establish an unbounded temporal property.Source: §3.1 · p. 5

3.2 IronBlocks: compositional support

• IronBlocks commitment safety needs both detection and mediation (cost 2); FLAT’s individual cost-1 choices fail original-graph closure.The graph’s composition relation was supplied by construction.Source: §3.2 · p. 5

3.3 Pong: requirement evolution

• Pong’s expanded requirement retains the prior leaf and adds a horizontal leaf, raising envelope cost from 1 to 2.The graph fixes the repaired artifact and evaluates requirement expansion, not artifact-change invalidation; the reported values are documented or reconstructed rather than freshly reproduced.Source: §3.3 · p. 6

4.1 Prespecified design

• The prespecified benchmark contains 249 graph/cost instances, 267 graph/task evaluations, and 801 method rows; primary evidence sizes range from 10 to 500.Feasible graphs start from a known support skeleton before alternatives or distractors are added.Source: §4.1 · p. 6

COMPOSITIONAL

• FLAT projects each AND rule into independent pairwise links and solves weighted set cover, intentionally omitting the need to combine premises.The original-graph method instead solves for minimum-cost support while preserving the composition structure.Source: COMPOSITIONAL · p. 7, §4.1 · p. 7

4.2 Optimization and validation

• CP-SAT encodes conjunction and justification; exhaustive solvers cross-checked graphs up to 20 leaves, with all 21 n=10 F1–F7 gate cases agreeing and closure validating supports.Runs used one worker, seed zero, presolve, no hints, and a 60-second per-method timeout.Source: §4.2 · p. 7

5.1 Loss from erasing conjunction

• 135 of 267 task evaluations had flat-reported coverage rejected by closure under the original graph, and every case belonged to a family with required conjunctions.The pairwise projection is unsound relative to the original semantics when it converts required conjunctions into alternatives; this finding concerns that prespecified projection, not graph-versus-metadata comparisons generally.Source: §5.1 · p. 7

5.2 Support reduction

• Family-level median support reduction ranged from 0.50 to 0.80 in F1, F3, F5, F6, and F8, while F2 and F4 had zero reduction.The metric is 1 −|S|/|E| and covers valid proven compositional optima; these generated support-cardinality reductions do not measure token use, verification runtime, money, or human effort.Source: §5.2 · p. 8, Figure 3 · p. 8

5.3 Exact agreement and exhaustive-search limit

• Every completed exact check agreed with CP-SAT: the mandatory n=10 gate passed all 21 instances, and 111 of 126 optional oracle checks completed.Fifteen n=20 compositional checks timed out, while the exact flat oracle completed every n=20 instance; no CP-SAT-selected support failed independent closure validation. Table 3 reports that n=20 compositional enumeration completed only for F1 and F5.Source: §5.3 · p. 8, Table 3 · p. 8

5.4 Runtime behavior

• Below 20 ms was the median CP-SAT solve time at n=500 for every family, but all three n=100 F3 instances with ten alternatives per target timed out at 60 seconds.The three n=100 instances returned valid cost-10 supports without proving optimality; prespecified n=500 F3 instances with five alternatives per target were proven optimal. CP-SAT also proved 234 of 267 compositional evaluations optimal and 30 infeasible, all from F7; three more returned closure-valid supports without proving optimality within 60 seconds.Source: §5.4 · pp. 8–9, Figure 4 · p. 9

• Immutable Python dataclasses represent evidence, obligations, rules, and task requirements, with evidence carrying semantic type, context, assumptions, and integer cost.An existing assurance record can serialize leaves and bind them to artifact, checker, scope, and provenance; it serves as supporting infrastructure rather than the central result.Source: §6 · p. 9
• NetworkX checks graph structure and typing, while deterministic forward chaining records derivation provenance and an independent closure validator checks every CP-SAT support.The exhaustive optimizer returns feasibility, all equal-cost optima, and inclusion-minimal supports for bounded instances.Source: §6 · p. 9
• All 249 canonical manifests regenerated byte for byte, and a second selected-support run reproduced the timing-free results under Python 3.12.14, NetworkX 3.6.1, and OR-Tools 9.15.6755.The scale generator uses a SHA-256 counter construction rather than platform pseudorandomness. Canonical manifests bind family, parameters, seed, costs, nodes, edges, roots, and graph hashes.Source: §6 · p. 9

7.1 Long-horizon use

• A long-horizon agent could request an envelope before modifying a component, restoring evidence and derivations for supplied task roots rather than all prior context.A missing root would yield an explicit infeasible result; possible reductions in irrelevant context or repeated checking have not been measured.Source: §7.1 · p. 10

7.2 Residual obligations and evolution

• Verification context changes which obligations remain, requirement changes can alter roots, and artifact changes raise a separate evidence-applicability problem.Source, dependencies, compiler, runtime, or assumptions may leave evidence applicable, require transport, make applicability uncertain, or invalidate it; integrating existing dependency analyses is future work rather than a new invalidation algorithm.Source: §7.2 · p. 10

7.3 The unsolved input problem

• Envelope validity depends on suitable roots and sound rules, but this study supplies roots manually.Future evaluations should test automatic root construction and agent decisions made with selected support.Source: §7.3 · p. 10

7.4 Broader impact

• An envelope only establishes that selected evidence derives supplied obligations under supplied rules; it does not establish that those obligations are complete or the judgments sound.Treating a sufficient envelope as a correctness guarantee would overstate what it establishes; the formulation adds no generative capability and uses evidence from prior engineering work.Source: §7.4 · p. 10

• Hand-specified obligations and rules may omit real requirements or encode a bridge too strongly, and unit or small integer costs do not represent real acquisition, context, or risk.Source: §8 · p. 10
• Hand-designed graph families improve control but may favor the phenomena studied, and F7 infeasibility is constructed.Implementation checks reduce implementation risk but do not establish the semantic truth of supplied rules.Source: §8 · p. 11
• Rust, IronBlocks, and Pong provide small provenance-derived graphs, while the 249 synthetic instances stop at 500 evidence leaves and do not test downstream-agent benefit.Pong numerical evidence was documented and reconstructed rather than freshly reproduced.Source: §8 · p. 11
• Timing comes from one run per graph and method on an Apple M1 Pro; three feasible CP-SAT runs did not prove optimality, and selected n=20 exact searches timed out.Optimum and reduction claims exclude supports whose optimality was not proved.Source: §8 · p. 11

9.1 Assurance structures and evolution

• Assurance cases and lifecycle systems structure and maintain evidence; this graph is a narrow assurance/proof slice focused on cost-aware support for future-task roots.It is not proposed as a competing assurance metamodel.Source: §9.1 · p. 11

9.2 Selection, reuse, and minimum support

• Weighted set cover, directed hypergraphs, and AND/OR proof graphs capture related support problems; this work applies known optimization to typed software evidence and validates selected supports independently.Test-impact analysis, proof reuse, and program slicing can help construct roots or determine applicability, which this study treats as inputs.Source: §9.2 · p. 11

9.3 Program logics and enforcement

• Established logics and enforcement methods supply typed judgments and bridges; the envelope records them without unifying their semantics or introducing a verification method.IronBlocks uses a supplied conjunction of detection and commitment mediation to instantiate the distinction between runtime observation and intervention.Source: §9.3 · pp. 11–12

9.4 Provenance, intent, and coding agents

• Supply-chain provenance, intent formalization, and agent-context research address adjacent problems, while this study selects machine-produced evidence for supplied obligations and leaves downstream agent benefit unmeasured.The envelope concerns explicit derivations covering software obligations, rather than selectively retrieved repository context.Source: §9.4 · p. 12

10 Conclusion

• An assurance envelope is sufficient when closure derives every required root, and minimum-cost selection avoids unnecessary evidence leaves under the chosen cost model.The support problem uses typed evidence and explicit composition rules.Source: §10 · p. 12
• Preserved-evidence graphs show task-dependent support, infeasibility, conjunction, and requirement expansion; synthetic checks expose pairwise-baseline loss and agreement with CP-SAT in completed exact checks.The 249-instance benchmark also found support reduction ranging from null to substantial, under bounded conditions.Source: §10 · p. 12
• Open problems are constructing and maintaining task obligations and evidence applicability as code, context, and intent evolve, then evaluating downstream coding-agent benefit.The evaluation starts from supplied obligations rather than inferring them.Source: §10 · p. 12