PaperlayerView exact revision on arXiv

Source-linked AI summary

Fault-Tolerant Budget Conservation in Distributed Multi-Agent Delegation

Genliang Zhu, Chu Wang

arXiv:2610.00349v1cs.AIcs.CRcs.DC

TL;DR

Distributed delegation makes a remaining budget an authorization resource, while allocation alone does not address lost replies and late effects. The paper couples exclusive escrow credits with bound operation reservations and evidence-based settlement. Its central result is that partition-local availability comes from preallocated rights, while uncertain effects remain charged until resolved by evidence.

  • Problem

    A distributed delegation graph can overspend when a timed-out effect later completes, because allocation constraints alone do not account for uncertain external execution.

    Source: §1 · p. 1, §4.4 · p. 10

  • Method

    The protocol moves exclusive credits through a delegation DAG and reserves bound operations before dispatch, keeping uncertain effects charged until authenticated settlement, authoritative no-effect proof, or retirement.

    Source: §16 · p. 56

  • Results

    Local availability comes from rights allocated before a partition, while uncertainty remains charged until evidence resolves it.

    Source: §16 · p. 56

  • Takeaways & Limitations

    Timeout refunds do not conserve authority, and reallocation may require coordination rather than remain available through every partition.

    Source: §7.9 · p. 38, §16 · p. 56

    External-effect conservation depends on sound normalization, complete mediation, enforceable maximum charges, gateway fencing and idempotency, and complete non-equivocating terminal evidence.

    Source: §14.1 · p. 54

Abstract

from arXiv · show

Resource limits are becoming an authorization boundary for AI agents that delegate work across concurrent and failure-prone workers. Parent-child allocation constraints, affine objects, and distributed escrow do not by themselves prevent overspend when replies are lost, effects complete after timeout, messages repeat, branches partition, or DAG joins alias one lineage. We formalize fault-tolerant budget conservation for distributed multi-agent delegation. Budgets are quantized resource vectors represented by exclusive escrow credits that move through a delegation DAG. Before dispatch, a branch converts credit into an operation reservation bound to lineage, epoch, normalized effect, maximum charge, receiver, and idempotency key. It persists a signed dispatch permit with quarantine; the gateway verifies that permit before first acceptance. Uncertain effects remain charged until authenticated settlement, a fenced authoritative no-effect proof, or permanent retirement. We prove ownership partition, ledger and effect conservation, descendant non-amplification, at-most-once settlement, late-completion safety, and partition confinement under explicit mediation, durability, authentication, normalization, and gateway assumptions. An indistinguishability result shows that partition-local availability requires exclusive preallocation. Bounded TLA+ checking, an independent JavaScript explorer, and crash-injected two-process SQLite experiments exercise the declared scope and detect timeout-refund and historical-certificate-validation mutants. The mechanism preserves the issued budget bound across the evaluated crash, retry, duplicate, partition, join, and late-completion schedules.

1 Introduction

Delegating agents turn a remaining budget into a distributed authorization resource, but allocation rules alone cannot prevent overspend when a timed-out external effect later completes. This paper couples exclusive credit lineage with effect obligations, building on prior allocation, authorization, transaction, and escrow mechanisms.

1 Introduction

  • A lost reply followed by a timeout refund can let three effects consume a two-effect authorization, so possible external effects must remain reserved through uncertainty.The protocol settles, returns, or permanently retires an obligation using evidence; elapsed time alone does not restore spendable authority.Source: §1 · p. 2
  • DAG joins cannot add authority when incoming references alias one credit generation; ownership must preserve disjoint lineage, while ledger and effect conservation require separate assumptions.The paper also limits its claims: fault tolerance preserves safety across declared faults, not universal availability or resolution of every uncertain operation.Source: §1 · pp. 1–3
  • The protocol moves exclusive quantized resource credits through a delegation DAG and reserves each operation before dispatch, binding it to lineage, epoch, effect, charge limit, receiver, and key.Its contributions include conservation and effect-coverage results, recovery and join protocols, and a coordination boundary: local availability during partitions requires exclusive preallocation.Source: §1 · p. 3

2.1 Resource-Bounded Agent Execution

  • Agent Contracts and Token Budgets address resource constraints and affine ownership, while this paper focuses on uncertain external effects across crashes, partitions, retries, and joins.The paper treats Agent Contracts as allocation-level prior work and adopts Token Budgets’ move-not-copy intuition while extending it across processes and recovery.Source: §1 · p. 2, §2.1 · pp. 3–4

2.2 Delegation Identity and Scope Attenuation

  • Identity and scope-attenuation systems constrain what agents may do, but do not by themselves establish exclusive ownership of a consumable budget unit.AIP treats its budget ceiling as per-token authorization, while the runtime remains responsible for aggregate spend enforcement.Source: §2.2 · p. 4

2.3 Transactional Effects and Commit-Time Authority

  • Transactional-effect and commit-time-authorization work establishes the need for an endpoint boundary; this paper adds conserved consumable rights and coverage for uncertain effects during recovery.Its claims are at-most-once settlement and continuous coverage at a mediated gateway, not exactly-once delivery.Source: §2.3 · pp. 4–5

2.4 Escrow, Numeric Invariants, and Coordination

  • Escrow and bounded-counter systems distribute decrement rights so disconnected replicas can act within numeric bounds; this paper applies exclusive preallocation to delegated agent credits and effect settlement.It identifies a consumable shared unit as nonmonotone: spending it in one partition removes an option from another.Source: §2.4 · p. 5

2.5 Leases, Fencing, and Durable Workflow

  • Leases and fencing order authority across generations, but expiry does not prove that a dispatched effect did not occur; reclaim also needs exclusive ownership and terminal evidence.Stable request identifiers, reconciliation, and linearizable local transitions provide related mechanisms; the paper positions its combined gap in Table 1.Source: §2.5 · p. 5, Table 1 · p. 6

3 System, Failure, and Threat Model

The system protects delegated resource budgets across asynchronous failures by separating untrusted agent proposals from trusted budget movement and mediated external effects. Its scope depends on explicit trust, durability, authentication, normalization, and gateway assumptions; the accompanying problem analysis explains why allocation, retries, and compensation alone do not ensure conservation.

3.1 Entities and Trust Boundaries; 3.2 Budget and Effect Surfaces

  • Trusted branch stores move budget state, while gateways mediate protected effects and provide authenticated outcomes; budgets are finite resource vectors, and effects are normalized to canonical descriptors.Cross-dimension exchange requires a separately authorized conversion contract.Source: §3.1 · p. 6, Figure 2 · p. 7, §3.2 · p. 7

3.3 Failure Model; 3.4 Adversary

  • The model allows lost, duplicated, delayed, reordered, and late messages, crashes, partitions, retries, and malicious or confused agents, but excludes Byzantine infrastructure and arbitrary corruption of trusted stores.Wall-clock order does not determine whether an effect occurred.Source: §3.3 · pp. 7–8, §3.4 · p. 8

3.6 Goals and Explicit Non-Goals

  • The safety goals cover ledger and effect conservation, non-amplification, settlement, late completion, and partition confinement, while availability and scope remain bounded: exhausted isolated branches may refuse, and production SLOs are not established.Concrete runtime trace lifting remains a separate proof obligation.Source: §3.6 · p. 9

4.1 Allocation Conservation Is Not Prefix Conservation; 4.2 Read–Check–Decrement Replicas Double Spend

  • Snapshot allocation checks do not ensure prefix conservation, and partitioned replicas can each spend the same apparent remainder; exclusive rights make local decrements ownership-preserving.Last-writer-wins convergence can yield a valid-looking zero after two effects.Source: §4.1 · p. 10, §4.2 · p. 10

4.3 Static Splitting Is Safe but Can Strand Utility; 4.6 Scope Attenuation Does Not Consume; 4.7 Compensation Is Not Conservation

  • Static splitting can strand idle capacity, scope attenuation does not consume budget, and Saga compensation does not erase a duplicated effect or its authorization cost.The protocol treats compensation as a further effect requiring its own authority and accounting.Source: §4.3 · p. 10, §4.6 · p. 10, §4.7 · p. 11

4.4 Timeout Refund Creates a Late-Completion Race; 4.5 Idempotency Keys Do Not Allocate Authority

  • A timeout cannot distinguish an unexecuted request from one that completed with a delayed response, so its reservation must remain charged absent fenced no-effect proof; idempotency keys must also bind authority, not merely deduplicate requests.The binding covers credit generation, effect digest, receiver, epoch, and maximum charge.Source: §4.4 · p. 10, §4.5 · p. 10

4.8 Independent Correct Components Can Compose Incorrectly

  • Locally correct allocation, gateway, lease, and receipt components can still disagree on operation identity or epoch, so the protocol requires a joint canonical binding and a concrete-to-abstract refinement contract.The enforcement verifier recomputes the canonical operation binding and rejects field mismatches.Source: §4.8 · p. 11

4.9 The Joint Conditions Are Individually Necessary

  • Without all four joint conditions, one-unit counterexamples violate external effect conservation; together with persist-before-exposure and complete mediation, they connect exact ownership partition to the external exposure bound.The conditions are exclusive ownership, instance injectivity, complete charge, and fence ordering.Source: §4.9 · p. 11

5 Formal Budget and Delegation Model

The model formalizes budgets as exclusive resource rights moving through a delegation DAG, with dispatched operations bound to reserved maximum charges and authenticated effect evidence. It specifies transitions and safety invariants for ownership and charge conservation, including rollover, reissue, joins, and bounds that depend on exact operation coverage and authenticated ownership transfers.

5.1 Resource Vectors and Labels

  • Budgets are quantized vectors, and delegation attenuates both resource amounts and semantic labels; expiry and policy-version checks remain external commit-time predicates.Without an authenticated conversion contract, resource conservation is componentwise and no cross-dimension conversion is defined.Source: §5.1 · pp. 11–12

5.2 Root Rights and Compressed Footprints

  • Root rights are represented as footprints whose splits partition atoms and whose joins union only disjoint footprints, making ownership aliasing explicit.Numeric balances are a compressed implementation of this set-based ownership semantics.Source: §5.2 · p. 12

5.3 Credits and the Delegation DAG

  • Credit lineages form an acyclic resource graph: splits partition rights, while joins atomically consume pairwise-disjoint inputs and cannot add aliased ancestor rights.A task’s dependency on multiple branches does not itself grant ownership of their budgets; joined labels must be an authenticated common lower bound.Source: §5.3 · pp. 12–13, §5.2 · p. 12

5.4 Transfers

  • Cross-store transfers seal rights in transit until an accept-or-cancel decision, and cancellation requires destination exclusion plus a competing compare-and-set; timeout is never a decision.Without shared decision authority or an exclusion protocol, cancellation is disabled and the rights remain in transit.Source: §5.4 · p. 13

5.5 Operations, Effects, and Terminal Evidence

  • Before dispatch, an operation reserves an exclusive footprint and binds its lineage, epoch, normalized effect, receiver, maximum charge, and canonical idempotency key.The gateway verifies a single authenticated acceptance binding; effect-equivalent protocol paths share a digest under the deployment’s effect contract.Source: §5.5 · pp. 13–14
  • Uncertain operations remain quarantined until authenticated settlement, a fenced authoritative no-effect proof, or permanent retirement; timeout alone never refunds rights.The model distinguishes externally signed terminal evidence from a fused local non-dispatch witness, which requires authenticated durable outbox history and an absorbing post-state.Source: §5.5 · pp. 14–15

5.6 Ownership State

  • Ownership is partitioned across available, in-transit, reserved, quarantined, committed, and forfeited buckets, with retirement keeping stranded capacity visible in the conservation equation.Forfeiture is absorbing: later evidence may annotate outcome and charge but cannot restore ownership; this makes the safety–utility tradeoff auditable.Source: §5.6 · p. 16, §5.7 · p. 18

5.7 Transition System

  • Every ownership-moving action requires a uniquely tagged source and atomically replaces it with one destination; replay stutters, while dispatch quarantines rights before possible gateway acceptance.A repeated accepted idempotency key returns the prior decision; unresolved quarantined rights can be retired but never become available again.Source: §5.7 · pp. 17–18
  • Terminal rollover moves only the uniquely available reusable footprint into a fresh generation of the same logical slot, atomically persisting the write-once decision and closing the predecessor.Exact replay stutters, changed targets are rejected, and committed, forfeited, transferred, or otherwise obligated atoms do not move.Source: §5.7 · p. 18
  • A fused terminal transition applies only to the fenced predecessor’s final nonterminal operation, combining its terminal remainder and safe available footprint into one normalized reissue target.The transition is one commit and does not relax Settle or Reissue.Source: §5.7 · p. 18
  • A join consumes disjoint inputs and creates one output over their union in a single atomic-authority commit, closing fully consumed inputs and installing the output as active.The inputs must have no active operations; the output receives a fresh logical slot and matching authoritative-epoch and active-generation registers.Source: §5.7 · p. 18

5.8 Safety Invariants

  • Reachable states require unique atom ownership, nonnegative buckets, lineage attenuation, current generations and epochs, operation binding, unique settlement, and injective effect instances.Accepted operation keys bind the operation and its lineage, epoch, effect, receiver, maximum vector, labels, and witness.Source: §5.8 · p. 19
  • Every protected dispatch must have durable reserved or forfeited atoms, or a committed receipt accounting for actual charge; epoch advance cannot revive an old generation.No-effect returns require durable never-dispatchable evidence or authoritative proof that past and future occurrence is impossible; partial success requires a complete receipt disabling further instances or charges.Source: §5.8 · p. 19

5.9 Effect Instances, Coverage, and External Exposure

  • Effect instances are distinct gateway-log entries, and an operation covers an instance only when its key, binding, effect digest, gateway, receiver, and acceptance-time authorization match.Coverage additionally requires the operation footprint to remain in reservation or forfeiture, or a complete committed receipt to identify the actual-charge footprint.Source: §5.9 · p. 19
  • A success receipt arriving after forfeiture is audit-only: the atoms remain forfeited and charged at the conservative maximum, within the stated external exposure bound.The bound depends on the ownership assumptions and Assumptions 4, 5, 6, 7, and 9, and does not claim unmediated physical reality.Source: §5.9 · pp. 19–20

5.10 Descendant Capacity

  • Descendant capacity is bounded by exact atom footprints transferred into the sub-DAG; task-dependency edges without credit transfer add no capacity.Incoming ownership events are deduplicated by atom identity on re-entry, and transfers out of the sub-DAG leave its capacity measure.Source: §5.10 · p. 20

6 Fault-Tolerant Delegation and Settlement Protocol

The protocol moves exclusive, attenuated credits through delegation while binding each protected effect to durable reservations and authenticated evidence. It keeps uncertain capacity charged and permits reuse only through fenced, evidence-backed transitions.

6.1 Design Principles

  • Six rules require exclusive footprints, attenuated labels, durable state before dispatch, effect-bound reservations, charged ambiguity, fenced reclaim, and idempotent replay.A fence alone does not release quarantined rights; reclaim also requires authoritative evidence that the exact binding was never accepted and did not occur.Source: §6.1 · p. 20

6.2 Joint Authorization and Budget Witness

  • The joint witness combines existing action, intent, execution, and dependency-closure predicates with this paper’s interface assumptions; conservation properties are established here.The cited related-work passages identify OpenPort [53], intent and execution predicates [50] [51], and dependency-closure binding [52].Source: §6.2 · pp. 20–21

6.3 Credit Certificates

  • Transfer certificates bind a vector and authorization label to a unique transfer; destination acceptance cannot enlarge them, and duplicate acceptance is keyed by root and transfer ID.The source durably seals removal of spendability before sending; unreachable transfers remain in transit unless destination fencing or a durable non-acceptance decision permits cancellation.Source: §6.3 · p. 21, §6.4 · p. 21

6.6 Terminal-Evidence Settlement

  • Settlement consumes authenticated actual charges and returns only verified remainder; pending or unknown outcomes remain quarantined, while verified no-effect evidence returns the full footprint.Recovery reconciles by the exact operation binding; unresolved uncertainty can remain charged permanently as forfeiture, with later evidence annotating the outcome without changing ownership.Source: §6.6 · p. 21, §6.7 · pp. 21–22

6.4 Idempotent Delegation

  • Delegation retries use the same stable transfer ID, while accepted transfers are never restored by the source and cancelled transfers can restore their footprint exactly once.Algorithm 1 persists the sealed transfer, outbox, and audit before sending; acceptance creates or recovers the uniquely named child.Source: §6.4 · p. 21, §6.7 · p. 22

6.5 Reserve Before Dispatch

  • Before dispatch, the branch durably moves the maximum charge into an obligation and quarantine; moving it before network exposure avoids an uncovered effect window.If the provider cannot reject charges above the declared maximum, it cannot support the hard-bound profile; a pre-send crash may strand budget pending proof of non-execution.Source: §6.5 · p. 21, §6.8 · p. 23

6.8 Epoch Fencing and Safe Reclaim

  • Safe reclaim closes the old generation, requires proven available ownership and an authoritative higher-epoch fence, and never reuses committed or forfeited atoms.The gateway rejects new old-epoch acceptance after fencing while revealing outcomes that crossed beforehand; a budget-store epoch check alone is insufficient when stale workers retain direct receiver credentials.Source: §6.8 · pp. 22, 24, 25, 27

6.9 Fan-In and Return

  • At joins, branches retain separate credits, join disjoint operation-free footprints under one authority, or transfer remainders through acknowledged sealed handoffs; reported balances cannot simply be added.Stable return IDs make duplicate completion or return messages stutter, and an indeterminate operation remains charged to the root.Source: §6.9 · p. 27

7 Safety Results: Conservation and Recovery

The section establishes prefix invariants for budget-right conservation through delegation, settlement, recovery, and epoch changes, including under crashes, partitions, lost responses, and permanently indeterminate effects without assuming eventual delivery. It gives conditional criteria for applying these guarantees to concrete runtimes, explains why partition-local spending of unallocated units requires exclusive preallocation, and identifies the assumptions and conservative outcomes that bound the guarantees.

7.2 Unique Ownership and Exact Conservation

  • Under Assumptions 1–3, every reachable state and root grant satisfy componentwise exact per-root conservation: A_g(s) + T_g(s) + R_g(s) + Q_g(s) + C_g(s) + F_g(s) = B_g.Under Assumptions 1–3, no finite sequence of duplicate messages, process restarts, reconciliations, or lineage-disjoint joins can increase a root’s spendable and obligated capacity beyond B_g.Source: §7.2 · p. 30

7.3 Lineage and Descendant Non-Amplification

  • Descendant credits cannot amplify their inherited rights: a credit-cut-closed lineage sub-DAG is bounded by its initial rights plus exact authenticated ingress, while task-DAG edges grant no capacity.Each atom moves along one lineage path, never copied; joins require disjoint footprints.Source: §7.3 · pp. 30–31

7.4 Stable Settlement and Continuous Effect Coverage

  • A canonical operation key permits at most one authoritative settlement, and dispatched atoms remain reserved or forfeited—not available—until authenticated terminal evidence.Timeouts, process death, lease expiry, partitions, missing responses, and epoch increments alone cannot refund the reservation.Source: §7.4 · p. 32
  • Every mediated effect instance remains continuously covered by its operation, with no one-effect-profile operation covering two distinct instances; settled charges plus maximum at-risk footprints remain bounded by the root budget.Risk operations retain their full maximum footprint in the indeterminate or forfeited bucket, including late success after retirement.Source: §7.4 · pp. 32–33

7.5 Epoch Fencing, Late Completion, and Safe Reclaim

  • After a gateway acceptance precedes an epoch fence, the reservation stays charged until terminal evidence; late success cannot let one atom fund both an old-epoch effect and a new-generation effect.If acceptance did not precede the fence, the gateway cannot newly accept the old epoch; timeout or failure suspicion is not a refund proof.Source: §7.5 · pp. 33–34

7.6 Partition Confinement and the Coordination Boundary

  • During a partition with no accepted cross-cut transfer, each component can spend only its own available escrow and cannot spend rights assigned to another component.Source: §7.6 · pp. 34–35
  • No protocol can guarantee both partition-local approval of a shared unallocated unit and global conservation; exclusive preallocation preserves availability only for escrowed units.A component that exhausts its local allocation must wait, reconcile, or refuse.Source: §7.6 · p. 35

7.7 Concrete Refinement Obligations

  • Theorem 8 requires initial-state, stepwise, and prefix-faithfulness obligations for concrete runtimes to inherit abstract safety results.The SQLite research profile tests the online first-acceptance guard, but finite trace agreement does not replace a universal handler-level refinement proof.Source: §7.7 · pp. 36–37
  • Under Assumptions 1–9 and trace-lifting, concrete prefixes inherit per-root conservation, descendant non-amplification, at-most-once settlement, effect coverage, exposure bounds, safe epoch reclaim, and partition escrow bounds.These conclusions retain their stated premises, including credit-cut-closed sub-DAGs, dispatched operations, and partition intervals without accepted cross-cut transfers.Source: §7.7 · p. 37

7.8 Assumption–Conclusion Boundary

  • External-effect conservation requires normalization, complete mediation, and a terminal-evidence-producing fenced gateway; ledger integrity alone is insufficient.The results use stated assumptions; they do not require every deployment to implement each assumption in the same way.Source: §7.8 · p. 37, Table 4 · p. 38

7.9 What the Theorems Permit

  • Unresolved rights may remain quarantined, reserved, or retired, reducing utilization while preserving conservation and coverage; the guarantees do not establish true provider costs or adapter conformance.A conserved internal ledger also does not prove equivalent effect normalization or absence of bypass credentials; tested invariant and evidence layers do not establish the handler-level trace-lifting obligation.Source: §7.9 · p. 38

8 Reference Architecture and Implementation Boundary

The reference architecture maps the abstract machine to durable branch, gateway, and checking roles while preserving its proof obligations. Its compact SQLite profile exercises a narrower single-chain subset, not the full DAG schema or universal refinement.

8 Reference Architecture and Implementation Boundary

  • The abstract machine is independent of any database, transport, agent framework, or model provider; the reference profile is implementable without weakening its proof obligations.The profile does not imply that an ordinary queue or API satisfies those obligations.Source: §8 · p. 39

8.1 Lifecycle Realization

  • The lifecycle has no timeout path from quarantine to available, and forfeited authority remains absorbing even when later evidence annotates its outcome.Authenticated success receipts support ordinary ownership progress; exclusion, no-effect, or reversal evidence follows separate paths.Source: §8.1 · p. 39

8.2 Durable Records

  • The SQLite prototype represents one serial reissue chain per root, not the full DAG schema with pairwise-disjoint split siblings or a universal refinement proof.Its complete executable-beta claim is limited to the concrete prototype schema and exercised rows.Source: §8.2 · p. 40

8.3 Write Ordering and Crash Cuts

  • After dispatch becomes possible, a crash leaves the obligation quarantined; after a send, recovery uses the canonical operation key rather than issuing a semantically new request.The ordering can sacrifice availability to prevent an effect from existing without a charged right; duplicate sends are handled through gateway idempotency and receipt queries.Source: §8.3 · p. 41

8.4 Reference Components

  • Issuance, credit transitions, branch-ledger actions, gateway acceptance, reconciliation, and independent checking are assigned to six logical components.The compact artifact implements only the exercised subset of these roles.Source: §8.4 · p. 41
  • Agreement between runtime assertions and the independent checker is stronger evidence than either alone, but does not establish complete transition replay or production handler-by-handler refinement.The stated boundary includes production database and cryptography behavior.Source: §8.4 · p. 42

8.5 Concurrency and Placement

  • Spending preallocated rights is local, while moving unused rights between partitions, joining credits, changing resource semantics, or reclaiming a lost generation requires coordination.Operations on disjoint credits can proceed concurrently without a shared counter.Source: §8.5 · p. 42

8.6 Complexity and Metadata

  • With range-compressed rights, ordinary vector operations are O(d), and operations store identifiers, digests, and O(d) quantities rather than materializing logical atoms.A transfer also stores a lineage/rights commitment; checkpointed Merkle or accumulator proofs can avoid carrying full ancestry on each request.Source: §8.6 · p. 42

9 Evaluation Methodology

The evaluation tests whether the protocol’s stated invariants hold in declared finite models and crash-fault runtime schedules, while separating bounded evidence from claims about arbitrary deployments.

9.1 Research Questions

  • The research questions test invariant preservation, timeout-refund and historical-certificate mutants, safe-profile crash schedules, and recovery and local timing as a health check.The timing observations are explicitly not a comparative performance claim.Source: §9.1 · p. 43

9.2 Evidence Strata

  • The evaluation separates bounded TLA+ and JavaScript exploration, two-process SQLite crash injection with an independent trace checker, and descriptive local timing.The checker recomputes properties from durable snapshots, reducing but not eliminating common-specification error; no stratum proves arbitrary deployment refinement.Source: §9.2 · pp. 43–44

9.3 Analytical Comparison Points

  • The comparison mechanisms are analytical reference points, not measured reimplementations; their contrasts include centralized availability, static escrow, local affine credits, allocation monitors, and replay registries.The proposed profile combines exclusive credit lineage with reservation, quarantine, and terminal-evidence settlement.Source: §9.3 · p. 44

9.4 Finite Scopes and Concrete Schedules

  • The finite scopes distinguish settlement and generation recovery from lineage and fan-in; the SQLite profile exercises ten safe cases and a timeout-refund mutant.The lineage mutant combines historical-input substitution with omitted disjointness validation, while model-level coverage is not a runtime implementation of transfer or DAG join.Source: §9.4 · pp. 44–46

9.5 Metrics

  • All safe profiles must have zero conservation, coverage, and exposure-bound violations; weakened rules count as detected only when an exercised schedule yields an independently validated counterexample.The evaluation uses deterministic pass/fail cases and treats bounded completion as evidence only within declared constants and assumptions.Source: §9.5 · p. 46
  • Timing is descriptive: restart time runs from process death to service readiness against the same database, and samples do not establish throughput, tail SLOs, capacity, or comparative overhead.Safety results are not combined with timing into one score.Source: §9.5 · p. 46

9.6 Decision Rules and Statistical Treatment

  • Local timing has no warm-up, random-sampling model, confidence interval, or hypothesis test; recorded runtime and startup details contextualize those observations.A zero bounded-model counterexample count applies only to the declared finite scope, not an unbounded proof.Source: §9.6 · p. 46

9.7 Predeclared Interpretation Boundaries

  • A timeout-only reclaim that appears safe signals a missing delayed-effect twin, while bounded model completion cannot establish correctness beyond its constants or assumptions.Provider-reported usage cannot validate actual invoice bounds, and fault-free speed cannot establish fault tolerance.Source: §9.7 · p. 46

10 Evaluation Results

Across the declared finite models and retained SQLite traces, the safe profile had no invariant violations, and both targeted weakenings were detected; the results remain bounded by the tested scopes and assumptions.

10.1 Bounded Model-Checking Results

  • All safe finite graphs completed with no invariant violations; the settlement TLC model explored 16,592 distinct states, matching the JavaScript encoding’s count.Matching counts are only a coarse consistency check, not proof of equal state sets, bisimulation, or independent specifications.Source: §10.1 · p. 47
  • All 18 safe named schedules passed with zero final invariant violations, including acceptance before a fence followed by late completion.The schedules test particular executions and do not enlarge the exhaustive finite scope.Source: §10.1 · p. 47

10.2 Targeted Necessity Checks

  • Both weakened mechanisms produced counterexamples, but the historical-certificate lineage mutant jointly substituted stale inputs and omitted disjointness validation.It therefore does not isolate an overlap-only ablation.Source: §10.2 · p. 47

10.3 Multi-Process Crash-Fault Results

  • 10/10 safe SQLite cases ran without a prefix violation, and the independent checker detected the timeout-refund mutant.The artifact included nine actual SIGKILL deaths and checked signed receipts, terminal return decisions, and negative handler assertions.Source: §10.3 · p. 48

10.4 Interpretation and Residual Limits

  • The SQLite profile validates its finite reference schedules, not universal runtime refinement, production cryptographic assurance, cross-store transfer, or DAG join.External-effect claims remain conditional on a cooperating, idempotent, fenced, queryable gateway with complete mediation.Source: §10.4 · pp. 48–49

11 Security Analysis

The security analysis confines budget authority to mediated, authenticated transitions and keeps uncertain effects charged, while identifying operational and infrastructure assumptions that bound the guarantees.

11.1 Safety Against a Malicious or Confused Agent

  • A worker may propose arbitrary actions, but the branch store accepts them only when current exclusive credit and immutable operation binding authorize the normalized effect.A compromised worker can still waste its own escrow by reserving unproductive work or withholding completion; conservation does not prevent budget denial.Source: §11.1 · p. 49

11.2 Replay, Equivocation, and Identifier Substitution

  • Stable identifiers alone do not prevent substitution: the verifier recomputes a canonical operation binding, rejects mismatched tuples, and treats exact replay as a stutter.Unused rights may return only to a same-root successor on the source lineage with a no-broader label.Source: §11.2 · p. 49

11.3 Stale Generations and Split Brain

  • Epoch fencing must be enforced at the trusted boundary before effects; ownership still requires consensus, single-writer placement, or another correct ownership service.The protocol does not solve consensus or claim Byzantine split-brain tolerance.Source: §11.3 · pp. 49–50

11.4 External-Effect Ambiguity

  • When a receiver drops or falsifies a response, reconciliation uses a fenced query or leaves the right quarantined or forfeited rather than guessing.A client-side retry library cannot create durable coupling between a completion record and an arbitrary third-party mutation.Source: §11.4 · p. 50

11.5 Underreporting and Variable Charges

  • A maximum reservation is sound only if the gateway can prevent actual charges from exceeding it; otherwise the hard-bound profile must refuse, reserve a conservative worst case, or soften its claim.Partial settlement requires an authenticated receipt for the charge, and stream cancellation alone is not a zero-charge receipt.Source: §11.5 · p. 50

11.6 Normalization and Path Aliasing

  • Normalization belongs to the trusted policy boundary, and the theorem covers only credentials and routes the deployment actually interposes.Unknown semantics fail closed; direct credentials, UI paths, or internal tool calls can bypass a proxy unless deployment controls mediate them.Source: §11.6 · p. 50

11.7 Audit Integrity and Rollback

  • A hash-linked log detects deletion or reordering relative to a trusted checkpoint, but rollback of both state and local log requires an external monotonic witness for stronger forensic detection.Audit records also contain sensitive metadata, so detailed receipts should be encrypted and access and retention controlled.Source: §11.7 · p. 50

12 Related Work Beyond the Closest Mechanisms

The paper positions its contribution at the intersection of delegated resource ownership and uncertain external effects, distinguishing consumable credits from authorization and workflow mechanisms.

12.1 Agent Economies and Governance Receipts

  • Agent Contracts and Token Budgets motivate allocation and affine ownership, while this work addresses ownership across durable crashes, joins, and uncertain effects.The paper distinguishes its effect receipts, which attest to receiver outcome and actual charge, from governance receipts that attest to policy decisions.Source: §12.1 · p. 51

12.2 Authorization Delegation

  • Authorization-delegation systems constrain permitted actions, whereas consumable credits prevent equally attenuated children from both owning the same final unit.The paper frames its operational question as how authenticated rights move and settle through crashes and partitions.Source: §12.2 · pp. 51–52

12.3 Escrow, CRDTs, and Mobile Rights

  • The paper extends escrow lineage with authorization labels, dynamic delegation, safe joins of non-aliased rights, and external-effect obligations that persist through uncertainty.A numerically valid convergent counter can still miss a duplicated payment or disclosure.Source: §12.3 · p. 52

12.4 Transactions, Workflows, and Exactly-Once Semantics

  • Unlike a universal exactly-once workflow claim, the theorem establishes at-most-once settlement and continuous charged coverage, including safe unavailability when an effect cannot be resolved authoritatively.The scope is consumable delegated authority rather than universal workflow execution.Source: §12.4 · p. 52

12.5 Coordination and Impossibility

  • Exclusive preallocation permits partition-local work, while creating or reallocating a shared spendable unit requires coordination or blocking.The paper presents this as an application-specific consequence of the coordination boundary.Source: §12.5 · p. 52

13 Discussion

The discussion clarifies that the conserved quantity is authenticated authorization capacity, while safety, availability, and utility depend on explicit allocation and endpoint conditions. It also outlines standards and a staged deployment path.

13.1 What Is Actually Conserved?

  • Equation (8)’s exact equality distinguishes available capacity from moving, reserved, uncertain, consumed, and forfeited rights.This makes apparent under-spending diagnosable as either availability or stranded capacity.Source: §13.1 · p. 52

13.2 Why Keep Both R and Q?

  • Reserved R rights may be locally returned only when the outbox provably never became dispatchable; uncertain Q rights require external evidence.Keeping these states separate prevents generic release of pending reservations from creating authority.Source: §13.2 · p. 53

13.3 Safety, Liveness, and Economic Utility

  • Partitioned branches progress only with suitable local rights and a reachable gateway; exhausted branches can block despite idle capacity elsewhere.Quarantined rights may remain unavailable indefinitely; allocation policy can reduce this cost, but prediction is outside the safety theorem.Source: §13.3 · p. 53

13.4 Vectors and Conversion

  • Cross-resource conversion is a new protected effect requiring a signed rate-and-rounding contract, source-right consumption, one-time target creation, and a value invariant.Without that contract, conversion is undefined rather than inferred.Source: §13.4 · p. 53

13.5 DAG Tasks, Forest-Owned Rights

  • Task dependencies do not confer budget ownership: joins require disjoint transferred credits or an atomic join, not sums of incoming task balances.Compressed proofs still need a disjointness witness and one-time consumption of each input generation.Source: §13.5 · p. 53

13.6 Standards Integration

  • Standards integration can reuse existing identity, authorization, and transport protocols, but interoperability must test semantic refinement, not only JSON shape.The proposed common profile specifies resource semantics, stable identifiers, binding digests, epochs, endpoint capabilities, terminal outcomes, and refusal codes.Source: §13.6 · pp. 53–54

13.7 Deployment Migration

  • Deployment migration proceeds from instrumentation without hard-bound claims to durable reservations, cooperative gateways, exclusive credits, fencing, reconciliation, and claim verification.Legacy direct paths remain outside complete mediation until credentials and egress controls prevent bypass.Source: §13.7 · p. 54

14 Limitations and Validity

The guarantees are conditional on a declared crash-fault model, correct authoritative services, and runtime mappings that satisfy the stated obligations. Formal and experimental evidence is bounded, and external validity depends on endpoint cooperation and defined resource semantics.

14.1 Model Limitations

  • The base model excludes Byzantine stores, compromised signatures, cross-root netting, and other listed behaviors; aggregate caps require issuer-level escrow.Per-root equations cannot prevent overspend if the issuer signs overlapping grants, and faulty atom compression can break the implementation mapping.Source: §14.1 · p. 54
  • The end-to-end effect theorem requires sound normalization, complete mediation, enforceable maximum charges, gateway fencing or idempotency, and complete non-equivocating evidence.The ledger theorem remains useful if these assumptions fail, but it is not then conservation of actual external cost; the base theorem also assumes correct authoritative stores and evidence services.Source: §14.1 · p. 54

14.2 Formal-Method Limitations

  • Model checking covers declared finite constants, schedules, and transitions; state-space completion does not prove database durability, authentication, cryptographic libraries, or unmodeled adapters.The encodings also omit duplicate-tag raw states in one invariant check and remain bounded rather than mechanized proofs of full raw-relation semantics.Source: §14.2 · p. 54
  • The trace-lifting criterion must be discharged handler by handler; unmodeled redirects or background retries prevent a deployment from inheriting the theorem.The SQLite profile covers exercised first-acceptance permit and crash-cut obligations, not every production handler.Source: §14.2 · p. 55

14.3 Experimental Limitations

  • The provider-free artifact measures formal scopes, named crash windows, and one local implementation and host, not production quality or scale.Model quality, real-provider accounting, Internet-scale latency, multi-region failover, operator response, failure frequency, and capacity planning remain separate targets.Source: §14.3 · p. 55
  • Without endpoint cooperation, a lost response cannot distinguish non-execution from completed execution, so experiments can demonstrate but not remove this ambiguity.Budget dimensions transfer only when deployments define a conservative maximum and authoritative settlement relation; quantization can over-reserve.Source: §14.3 · p. 55, §14.4 · p. 55

14.5 Internal Validity

  • Independent implementations, mutation tests, prefix checks, stable manifests, and explicit claim-evidence mapping reduce correlated specification risk.The cited related-work boundary uses recent papers conservatively and does not treat them as evidence of deployment prevalence.Source: §14.5 · p. 55, §14.4 · p. 55

15 Ethics and Responsible Deployment

Responsible deployment requires treating budget enforcement as an authorization control, not a guarantee of beneficial decisions. It also requires safeguards for sensitive delegation records and against misuse of quarantined capacity.

Ethics and Responsible Deployment

  • Budget enforcement can reduce financial loss, excessive API use, unauthorized disclosure, and repeated high-impact effects, but a green ledger does not establish that decisions are beneficial or mediation complete.Interfaces should show endpoint profile, quarantined capacity, unresolved effects, and assumption failures alongside remaining balance.Source: §15 · p. 55
  • Receipts and delegation graphs can expose organizational structure, purposes, recipients, spending patterns, and sensitive content, requiring minimization and access safeguards.Cryptographic commitments may reduce disclosure but do not make metadata harmless.Source: §15 · p. 55
  • Quarantine can be abused to deny service or trap shared capacity, so issuers should cap reservations and define escalation and forfeiture authority.Human overrides should be new authorizations, not automatic punitive decisions based on ambiguous outcomes or unverified assertions.Source: §15 · p. 55

16 Conclusion

The paper frames distributed delegation budgets as authorization objects and combines exclusive credit lineage with explicit obligations for external effects. Under stated assumptions, the protocol preserves conservation across uncertainty and partition-related schedules.

Conclusion

  • Allocation inequalities, affine types, attenuated scopes, idempotency keys, and convergent counters each address only part of delegation-budget safety.They do not individually prevent timeout refunds colliding with late effects, aliased fan-in reminting capacity, or stale workers spending reclaimed generations.Source: §16 · p. 56
  • The protocol moves exclusive labeled credit through lineage, reserves before exposure, quarantines ambiguity, and applies authenticated terminal evidence at most once.Under stated assumptions, settled charge plus conservative outstanding exposure stays within the issued root vector, with ledger conservation and late-completion safety.Source: §16 · p. 56
  • Local availability comes from rights allocated before partition, while uncertain effects remain charged until evidence resolves them.Refunding on timeout hides rather than conserves authority and delays discovery of overspend.Source: §16 · p. 56

Data, Code, and Materials Availability

The paper supplies a manuscript and bibliography alongside a formal resource model and concrete-to-abstract refinement obligations. Its claims remain limited to stated assumptions and the accompanying artifact, which is not distributed with the preprint.

Data, Code, and Materials Availability

  • The public preprint includes manuscript source and bibliography, but not the executable artifact or a claimed public archival URL.The artifact's scope and expected outputs are documented for auditing against a frozen internal release.Source: Data, Code, and Materials Availability · p. 56

Competing Interests

  • The authors develop agent-governance technology, and make no production-deployment claim beyond the stated assumptions and accompanying artifact.Source: Competing Interests · p. 56

A Notation and Semantic Domains

B Complete Abstract Transition Contract

  • The abstract transition contracts make preconditions and postconditions explicit; “same atoms” requires identity-preserving movement, not unrelated issuance after numeric subtraction.Source: B Complete Abstract Transition Contract · p. 56

C Concrete-to-Abstract Refinement Obligations

  • Concrete traces comprise committed transactions, gateway observations, and authenticated terminal evidence, while volatile steps without exposed effects or durable changes map to stutter.Tables 15–16 state the minimum simulation obligations.Source: C Concrete-to-Abstract Refinement… · p. 57

D.1 Timeout Refund and Late Completion

The section addresses how delegation preserves budget ownership through timeouts, retries, joins, stale workers, and partial settlement. It also describes the artifact and deployment conditions that bound the evidence and its claims.

D.1 Timeout Refund and Late Completion

  • Timeout refunds and replayed transfer certificates can duplicate one issued atom; uncertain effects remain charged, and imports require a unique destination decision.The machine waits for a query that distinguishes no effect from delayed completion, or retires the atom; source cancellation also requires a durable destination fence.Source: §D.1 · p. 58, §D.2 · p. 58

D.3 Aliased Diamond Join

  • A join rejects aliased descendant credit because task multiplicity does not create credit multiplicity.The set-based check finds the same nonempty atom set on both inputs rather than summing the referenced credit twice.Source: §D.3 · p. 58, Table 14 · p. 59

D.4 Stale Epoch After Reclaim

  • Reclaim advances a gateway-enforced epoch but does not itself rewrite old credit or authorize reallocation.Reallocation follows closure and exact reusable-hold evidence; the gateway rejects new stale-epoch keys and returns recorded outcomes for settlement.Source: §D.4 · p. 59, Table 15 · p. 60, Table 16 · p. 61

D.5 Partial Charge and Duplicate Receipt

  • A matching partial receipt commits its charged subset and remainder atomically; replay returns the same decision, while a conflicting receipt is quarantined.For a reservation of (1000 cents, 3 calls), a receipt for (730, 1) returns (270, 2).Source: §D.5 · p. 60

F.1 Directory Contract

  • The artifact combines complementary TLA+ models, a JavaScript encoding, and SQLite traces whose checker independently validates durable snapshots and dispatch-permit bindings.The JavaScript model is not an independent conceptual specification, and finite traces do not establish universal adapter or end-to-end refinement.Source: §F.1 · p. 62

F.2 Canonical Commands

  • Verification checks retained evidence, reruns finite and schedule checks, and fails on stale digests, missing cases, invariant violations, changed outputs, or database-integrity failures.The artifact records its environment and deterministic schedule settings; reported timings are health checks, not throughput results or production SLOs.Source: §F.2 · p. 63, §F.3 · p. 63, §F.4 · p. 63

G Deployment Assurance Checklist

  • Deployment requires complete mediation, durable reservation-to-dispatch transitions, signed first-acceptance permits, bound terminal evidence, fenced recovery, and pairwise-disjoint ownership at joins.The checklist also calls for bounded child reservations, separate monitoring of T, Q, and F, adapter conformance, and published endpoint capabilities.Source: G Deployment Assurance Checklist · p. 64

H Proof and Evidence Dependency Map

  • The evidence chain runs from authenticated exclusive issuance through settlement uniqueness and injective effect coverage; formal exploration and concrete trace checking cover different links.Neither evidence layer replaces verification of the stated environmental assumptions.Source: H Proof and Evidence Dependency Map · p. 64

Related papers

Loading 2610.00349v1…