Fault-Tolerant Budget Conservation in Distributed Multi-Agent Delegation

Fault-Tolerant Budget Conservation in Distributed Multi-Agent Delegation

arXiv:2610.00349v1 [cs.AI] 29 Sep 2026

GENLIANG ZHU, Accentrust, Canada and Georgia Institute of Technology, USA CHU WANG, Accentrust, Canada and University of Illinois Urbana-Champaign, USA 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. CCS Concepts: • Security and privacy → Access control; Formal security models; • Software and its engineering → Formal methods. Additional Key Words and Phrases: AI agents, multi-agent systems, distributed systems, resource governance, budget enforcement, delegation, fault tolerance, network partitions, escrow, double spending, external effects

1 Introduction AI agents increasingly act as spenders, callers, schedulers, and delegators. A user may authorize a procurement agent to spend at most $500, an incident agent to issue at most 20 production writes, or a research coordinator to make at most 100 paid API calls. The coordinator can then create workers, workers can create specialists, and multiple branches can converge at a final reviewer. A scalar “remaining budget” is no longer a local counter. It is a consumable authorization resource moving through a distributed, asynchronous delegation graph. Here fault-tolerant means that the safety bound is preserved across declared crash and communication faults. It does not mean every isolated branch remains available or every uncertain operation eventually resolves. Recent work makes important parts of this problem explicit. Agent Contracts defines multidimensional resource constraints and a conservation law requiring child allocations to remain within the parent contract [48]. Token Budgets documents 63 production budget overruns and uses affine ownership to reject in-process aliasing, double-spending, and use-after-delegation [22]. AIP binds identity, attenuated authorization, provenance, and completion records across the Model Context Protocol (MCP), Agent2Agent (A2A), and HTTP [36]. Attenuating Authorization Tokens specify offline holder-derived restriction of tool and argument authority, depth, and lifetime while Authors’ Contact Information: Genliang Zhu, Accentrust, Vancouver, Canada and Georgia Institute of Technology, Atlanta, Georgia, USA, research@accentrust.com; Chu Wang, Accentrust, Vancouver, Canada and University of Illinois UrbanaChampaign, Urbana, Illinois, USA, wally@accentrust.com.

2

Zhu and Wang Allocation-safe appearance, unsafe settlement Root budget 𝐵 = 2

Worker B spend own 1

Timeout Worker A lost reply refund 1; B spends reserve 1; dispatch

Late A effect total = 3 > 2

Fault-tolerant response: uncertainty retains the right Root budget 𝐵 = 2

Worker A lost reply Indeterminate reserve 1; dispatch keep reserved

Reconcile receipt / no-effect proof

One transition commit or return

Fig. 1. Parent/child allocation conservation does not prevent a timeout-refund/late-completion double spend. The safe trace keeps the reservation charged while the external outcome is indeterminate. Color is redundant with labels and arrow meaning.

leaving transport binding deployment-specific [32]. Together, these systems establish the allocation, affine-ownership, identity, and attenuation foundations on which this paper builds. Our contribution is the coupling of exclusive vector credit lineage with accepted and uncertain externaleffect coverage across crashes, partitions, retries, and multi-parent joins. The settlement gap. Allocation safety is not execution safety. Consider a root grant of two paid effects. The coordinator allocates one unit to each of workers 𝐴 and 𝐵, so the allocation law is satisfied. Worker 𝐵 first spends its own unit. Worker 𝐴 then reserves its unit and sends a payment request. The response is lost. Its controller times out, declares the worker dead, and refunds the unit to the parent. Worker 𝐵 spends that refunded unit, after which the original 𝐴 payment completes. Every allocation calculation was locally plausible; three effects have nevertheless consumed a twoeffect authorization. Figure 1 separates the unsafe trace from the required response. The missing object in this allocation-only trace is an explicit effect obligation: once an external effect may have crossed the durability boundary, its budget remains reserved through uncertainty. Recovery may query, settle, or permanently retire the obligation; elapsed time alone cannot make the right spendable again. Why a delegation DAG is harder than a tree. Agent delegation is not necessarily hierarchical. Two branches may ask a shared specialist to synthesize results; a reviewer may join multiple principalapproved inputs; retries may reconstruct a worker under a new process identity. A child with two incoming references does not thereby own the sum of both ancestors. If those references alias one credit generation, adding them creates authority. The budget-ownership relation must therefore preserve disjoint lineage even when the task graph has joins. Dual conservation. The paper distinguishes two properties: ledger conservation: effect conservation:

Avail + Transit + Reserved + Quarantined + Committed + Forfeited = Issued,

(1)

∀𝜄 ∈ Obs, ∃! 𝑜 ∶ Covered(𝜄, 𝑜),

(2)

Exposure𝑔 ⪯ B𝑔 .

Equation (1) prevents rights from being created and keeps ambiguous dispatched work visible in the quarantined bucket. Equation (2) prevents a real effect instance from becoming unaccounted while messages, controllers, and receipts disagree, and bounds settled actual charge plus the maximum charge of uncertain operations. The unique operation 𝑜 is quarantined, committed, or conservatively forfeited; injectivity prevents one reservation from covering two distinct instances.

Fault-Tolerant Budget Conservation in Agent Delegation

3

Neither equation implies the other without the binding and maximum-charge assumptions stated in Section 3. Approach. We model each root grant as a vector of quantized resources. The issuer creates exclusive escrow credits. Delegation moves a subvector into a fresh child generation and atomically removes it from the parent generation. A branch can spend locally during a partition only from its exclusive escrow. Before dispatch, the branch durably creates a reservation bound to the root, credit lineage, current epoch, normalized effect, maximum charge, receiver, and stable operation key. Dispatch changes the obligation state but does not refund. Authenticated, effect-bound success receipts are applied at most once; verified no-effect certificates return the reservation; irrecoverable uncertainty can be permanently forfeited but not silently reused. Contributions. This paper makes five contributions: (1) A fault-aware authorization semantics. We define resource vectors, exclusive credits, a delegation DAG, operation obligations, authenticated terminal evidence, and a transition system that separates allocation, execution, settlement, and effect coverage. (2) A fault-tolerant protocol. We give algorithms for idempotent split/delegation, local reservation, dispatch, terminal-evidence settlement, multi-parent join, recovery, epoch fencing, and safe reclaim, together with refinement obligations for MCP/A2A/HTTP adapters. (3) Conditional safety results. We prove ownership partition, global conservation, descendant non-amplification, at-most-once settlement, effect-instance coverage, an external exposure bound, late-completion safety, and partition confinement. We state an explicit trace-lifting criterion that a concrete runtime must discharge before inheriting those abstract results. (4) A coordination boundary. An indistinguishability argument shows why a shared, unallocated unit cannot remain spendable in every partition without risking amplification. Exclusive preallocation buys local availability; reallocation and reclaim may require coordination. (5) An evidence-disciplined reference profile. We specify a provider-free artifact that connects finite model checking, transition-level invariant checks, mutation, fault injection, and descriptive local timing to explicit claims. Hosted-model quality and production deployment remain outside the evidence. Non-goals. We do not invent escrow, bounded counters, leases, Sagas, idempotency, transactional tool use, commit-time authorization, or delegation tokens. We do not guarantee exactly-once network delivery, roll back irreversible effects, infer prices, optimize allocation, tolerate Byzantine infrastructure, or remain globally available through arbitrary partitions. 2 Background and Closest Work 2.1

Resource-Bounded Agent Execution

Agent Contracts unifies input/output specifications, skill sets, multi-dimensional resources, temporal bounds, success criteria, and termination in one lifecycle [48]. For delegation it requires ∑𝑖 𝑅𝑖 ≤ 𝑅parent , supports recursive subcontracts and returned capacity, and reports zero conservation violations in a 50-topic three-agent pipeline. Its hard monitor checks between actions, and the paper explicitly notes that a single call can exceed a budget before usage is known. Our work treats Agent Contracts as the closest allocation-level neighbor. Our question is what happens after allocation when messages duplicate, branches partition, a process crashes, or an external effect is uncertain. Token Budgets establishes that an ordinary copyable number is the wrong abstraction [22]. Its affine Rust object prevents a cost-bearing value from being cloned, double-spent, or used after delegation within the type-system envelope. The paper also quantifies static over-reservation,

4

Zhu and Wang

sketches distributed reservation using mechanisms such as Sagas, consensus, and leases, and identifies distributed partial failure as a substantial open extension. Our protocol adopts the same move-not-copy intuition but makes that extension explicit across processes, languages, protocols, crash recovery, and DAG joins. CapLease is the closest durable-authorization neighbor: it records consumable authorization state across retries, concurrent use, delegation, and crash recovery, with an idempotent receiver contract [47]. It therefore establishes durable agent authorization as direct prior art. The distinct contribution here is partition-aware transfer of exclusive multi-dimensional credit through a delegation DAG, including atomic multi-parent joins, together with one conservation argument spanning both credit lineage and accepted or uncertain external effects. Among the systems compared here, EpochX is the closest credits-native infrastructure: it locks task bounties, delegates budgets recursively, and settles rewards on acceptance [46]. Its focus is a production marketplace and reusable asset economy. Our focus is the prefix invariant and effectcoverage semantics when transfer, settlement, retry, and recovery traces are duplicated, reordered, lost, partitioned, or crash-interrupted. 2.2

Delegation Identity and Scope Attenuation

AIP supplies verifiable identity, attenuated authorization, provenance, and completion records across MCP, A2A, and HTTP [36]. It carries a budget_usd ceiling that attenuates along a token chain, but treats that value as a per-token authorization ceiling rather than a running balance; the runtime remains responsible for aggregate spend enforcement. AATs let a holder derive a signed chain with equal-or-narrower tools, arguments, depth, and lifetime without contacting the root issuer, while leaving transport binding deployment-specific [32]. Overlaying Governance formalizes recursive delegation and scope composition over existing policy [18]. These mechanisms prevent scope amplification. A consumable right adds a different obligation: two children can each hold the same narrow scope while only one may consume the remaining unit. Offline attenuation alone cannot decide exclusive ownership. PAuth derives service-side slices for task-implied concrete operations and binds operand values to provenance-aware authorization envelopes [44]. It strengthens operation-specific authorization, but does not define exclusive ownership of consumable budgets, crash/partition credit transfer, or settlement of an uncertain external effect. Stateful least privilege makes authorization decisions depend on execution history and represents policy state as replicated state machines [9]. This establishes stateful cloud authorization as a deployed security direction. Our state is narrower but structurally different: it tracks exclusive consumable-credit generations and their effect obligations across an agent delegation DAG. MCP standardizes model-to-tool connectivity and profiles OAuth authorization; A2A standardizes agent discovery and task exchange [1, 30]. MPAC adds multi-principal sessions, intent, operations, conflicts, Lamport-clock watermarks, optimistic concurrency, and governance [37]. We use protocol adapters and causal metadata but do not claim a general coordination protocol. The active individual Internet-Draft on Transaction Tokens for Agents propagates subject, actor, and agentic context through multi-agent call chains [38]; it specifies neither a running consumable balance nor exclusive escrow ownership or effect coverage. 2.3 Transactional Effects and Commit-Time Authority Atomix gives agent tool calls progress-aware transactional semantics. It uses epochs, per-resource frontiers, delayed commit for bufferable effects, and compensation for externalized effects [31]. Commit-time authorization separately requires fresh, causally prior, effect-bound, eligible authority at the durability boundary [41]. Context-to-Execution Integrity binds protected fields, exact

Fault-Tolerant Budget Conservation in Agent Delegation

5

effects, and invocation authority [40]. These works establish that endpoint success is not enough and that external effects need a boundary protocol. We add conserved consumable rights across distributed delegation and keep uncertain effects charged across recovery. Compensation is useful but weaker than prevention for irreversible payments, messages, disclosures, or physical actions. Sagas explicitly accept application-specific compensation rather than atomic rollback [12]. Likewise, “exactly once” can conflate delivery, state consistency, and deterministic replay [45]. Our claims are at-most-once settlement and continuous coverage at a mediated gateway, not exactly-once delivery. Two recent results sharpen this boundary. Machine-checked dual-write recovery shows that source-side state alone cannot safely distinguish a missing sink write from a completed one and formalizes recovery around sink acceptance records and fencing [3]. A cross-runtime study of agent tool calls similarly finds that exactly-once behavior depends on the model, harness, and tool contract, and that verification alone does not close late-commit races [28]. Our protocol adopts that receiver-visible boundary and adds the invariant that every accepted or still uncertain effect remains covered by exclusive credit. 2.4

Escrow, Numeric Invariants, and Coordination

The Escrow Transactional Method permits concurrent changes while reserving enough rights to preserve numeric bounds [33]. Bounded Counter conflict-free replicated data types (CRDTs) build on convergent replicated-data-type semantics and distribute decrement rights so disconnected replicas can act without violating a lower bound [5, 43]. Just-Right Consistency combines CRDTs, transactional causal consistency, bounded counters, and static analysis to synchronize only where application correctness requires it [42]. These are foundational prior art, not our inventions. Invariant confluence characterizes when valid divergent states can merge without coordination [4]. The recent Complete CALM criterion states a broader history-based boundary between monotone specifications and those requiring coordination [16]. A consumable shared unit is nonmonotone: spending in one partition removes an option from another. Our protocol applies the classical answer–exclusive preallocation–and then adds agent-specific delegation lineage, authority bindings, normalized effects, and settlement obligations. 2.5

Leases, Fencing, and Durable Workflow

Leases provide time-bounded authority under clock and failure assumptions [14]; lock services use monotonically ordered ownership and durable consensus to coordinate clients [8, 34]. Expiry does not undo an already dispatched effect. We use an epoch as a fencing generation, never as evidence that the previous effect did not happen. Recent capability-coherence work maps authorization revocation to memory consistency and reports an execution-count bound on post-revocation operations [35]. That revocation bound is complementary: our epoch fence controls acceptance across ownership generations, while reclaim also requires exclusive credit ownership and terminal effect evidence. Durable distributed applications commonly decompose work into idempotent steps, stable request identifiers, and reconciliation rather than assuming a cross-organization transaction [15]. Stable call identifiers and duplicate suppression trace back to classic RPC semantics [7]; durable systems additionally need the completion record and protected mutation to share the relevant atomicity boundary. Linearizability remains the abstraction for an authoritative local transition [17]; Lamport order supplies causal structure without pretending synchronized clocks determine truth [24]. Table 1 positions the resulting gap.

6

Zhu and Wang

Work

Consumable vector

Recursive / DAG delegation

Crash + partition

External-effect settlement

Agent Contracts

Yes

Recursive hierarchy

No fault semantics evaluated

Between-action monitor

Token Budgets

Cost scalar/object

Fan-out ownership

In-process focus

CapLease

Consumable authorization state

Delegation

Crash/retry recovery

EpochX

Task credits / bounties

Recursive delegation

No reported crash/partition proof

Lock + acceptance settlement

Agent marketplace and asset economy

AIP / AAT

Reusable scopes

Signed chains

Offline verification

MPAC

Not central

Atomix

Resource frontiers

Multi-principal graph Workflow branches

Optimistic conflicts Fault injection

Invocation + completion binding Operation state

Identity and monotone scope attenuation General agent coordination Transactional tool semantics

RIFL / Beldi / ExoFlow

No budget vector remote procedure call (RPC)/workflow graph Numeric rights Replica rights graph

Crash recovery

Commit-time authorization

Not central

Multi-agent workflow

Controlled invalidation

This paper

Quantized vector

Disjoint lineage in a task DAG

Crash, retry, partition, late completion

Escrow / Bounded Counter

Partition-aware

Primary contribution

Resourcebounded contract + allocation law Estimator-based Incident catalog cap + affine Rust case study Idempotent Durable receiver contract authorizationstate protocol

Commit + compensation Durable completion / exactly-once workflow Database update Fresh effect-bound witness Reservation + authenticated terminal evidence

Replay-safe execution substrates Numeric invariant preservation No resource transfer/settlement law Dual ledger/effect conservation

Boundary relative to this paper No duplicate/lateeffect/fencing model No durable cross-protocol recovery No partitioned vector-credit DAG join/effectcoverage theorem No prefix ownership/effectuncertainty invariant No exclusive consumable ownership No resource invariant No delegated budget conservation No delegated-right or charge-bound theorem No agent authority/effect witness

Conditional on mediated gateway and terminalevidence soundness

Table 1. Closest work is complementary. The contribution is not any individual primitive, but a fault-aware composition that keeps exclusive delegated rights and external-effect obligations coupled.

3 System, Failure, and Threat Model 3.1

Entities and Trust Boundaries

The system contains a root issuer, delegation controllers, agent runtimes, durable branch stores, effect gateways, a terminal-evidence authority, a reconciler, and an auditor. The issuer authenticates a task grant and creates the initial budget vector. Controllers split and move rights. Agent models propose work but cannot mint, settle, or refund credit. Each branch store atomically records local ownership, reservations, outbox state, and terminal evidence. The effect gateway is the completemediation point for a protected effect. It enforces the canonical operation key and epoch, and returns or exposes an authoritative outcome. In the reference profile, the issuer, controller, branch store, gateway, terminal-evidence authority, and reconciler form the declared enforcement trusted computing base (TCB); the controller and reconciler are trusted orchestration but still cannot bypass store/gateway validation. A deployment may remove those two orchestrators from the TCB only if every request is independently

Fault-Tolerant Budget Conservation in Agent Delegation

7

declared trusted enforcement envelope

Root issuer grant + budget vector

Delegation controller exclusive split / transfer

Branch store credit + reservation + outbox

proposal decision

Untrusted agent plan / delegate / retry

reserved dispatch

Reconciler query / settle / retire

Evidence authority signed success / no-effect

Effect gateway idempotency + fence + effect

External receiver durable domain state

read-only evidence export

Independent audit verifier trace + conservation totals

Fig. 2. Reference architecture and declared trust boundary. The untrusted agent may propose and retry; only the trusted branch store can move budget state. Protected external effects pass through a gateway whose authenticated outcome drives idempotent settlement. The independent verifier is a read-only evidence consumer outside the safety TCB.

revalidated at the authoritative store or gateway. The gateway’s enforcement verifier is therefore distinct from the read-only independent audit verifier shown outside the boundary. Figure 2 shows the reference boundary. The network and agent data plane are untrusted. The issuer need not be online for every local spend: partition-local availability derives from credit already escrowed to that branch. Cross-zone transfer, reclaim, or expansion can require an online coordinator. 3.2

Budget and Effect Surfaces

The protected budget is a finite vector over dimensions 𝒦: currency quanta, paid API calls, risk units, recipient-specific disclosures, or effect counts. Each dimension has an authenticated unit, quantization, and maximum-charge rule. Cross-dimension exchange is disallowed unless a separately authorized conversion contract is present; otherwise a dollar cannot silently substitute for a risk unit. Protected effects include any mediated external state change whose authority is consumable: a payment, message, credential issuance, infrastructure write, record mutation, disclosure, or paid call. Pure reads may still consume an API or disclosure budget. The normalizer maps protocolspecific requests to a canonical effect descriptor. Effects outside the declared gateway envelope, including covert channels and direct credentials, are outside the theorem. 3.3

Failure Model

The network is asynchronous. Messages can be lost, duplicated, delayed, reordered, or delivered after an arbitrary partition. Processes can crash and restart, losing volatile state while preserving completed durable commits. We do not use wall-clock order to infer whether an effect happened. Clocks are used only for policy expiry under a stated deployment profile; epochs and authoritative terminal evidence determine settlement. The model includes concurrent fan-out and fan-in, duplicate delegation and dispatch, retries, crash before or after each durable write, response loss, timeout followed by late completion, branch

8

Zhu and Wang

partition and healing, stale epoch messages, repeated terminal evidence, and recovery scans. It excludes Byzantine consensus and arbitrary corruption inside a trusted durable store. 3.4

Adversary

The planner, model, tool description, retrieved content, and downstream agent may be malicious or confused. They can request overlapping child budgets, replay messages, alias a reservation across effects, relabel effects, trigger retry storms, construct joins with shared ancestry, withhold completion, and present stale epochs. They cannot forge issuer or terminal-evidence signatures, break collision-resistant digests, bypass the protected gateway, or directly mutate the trusted store under the main theorem. 3.5

Assumptions

Assumption 1 (Authenticated Roots and cRedits). Root grants, credit generations, controller identities, and protocol bindings are unforgeable and domain-separated. Assumption 2 (DuRable local lineaRization). Each branch transition atomically updates credit, operation, outbox, and audit records in one durable local transaction. Assumption 3 (Unie Root issuance and stable decisions). Each root generation is issued once. Local split, join, reservation, settlement, and successor-generation decision keys are linearized by their authoritative store. In particular, one write-once (𝑔, 𝜒𝑐 , 𝑐𝑖𝑑, 𝜂𝑐 , reissue) decision, whose predecessor epoch comes from the authenticated credit record rather than a caller parameter, selects at most one successor pair (𝜂+ , 𝑐 + ). Each cross-store transfer ID has one monotone decision register whose value can change from pending to exactly one of accepted or cancelled. Exclusive ownership is a protocol invariant to be proved, not part of this assumption. Assumption 4 (Sound effect boundaRy). All protected paths are normalized to the correct resource dimensions and effect identity before dispatch. Assumption 5 (Fenced idempotent gateway). For each receiver-scoped key, gateway acceptance, fence installation, effect record creation, and terminal outcome have one linearization order. The gateway selects the authoritative epoch and fence by the authenticated (𝑔, 𝜒𝑐 ) committed inside the operation key and 𝛽𝑜 . The gateway rejects a not-yet-accepted stale generation, treats a canonical operation key as unique within the receiver namespace, rejects any changed binding under that key, and treats exact replay idempotently. A request accepted before a fence may complete afterward and remains queryable; the fence prevents only a new old-generation acceptance. The gateway revalidates the bound domain precondition and commit-time witness immediately before acceptance. Assumption 6 (Maximum-chaRge contRact). For endpoint profile 𝜒 , a trusted function RequiredCap(𝑒, 𝜒 ) returns a conservative vector. Reservation requires RequiredCap(𝑒, 𝜒 ) ⪯ u𝑜 , and the gateway prevents the complete actual charge of the accepted effect instance from exceeding u𝑜 . If no such cap can be enforced, the hard-bound profile is unsupported. Assumption 7 (TeRminal-evidence completeness and non-eivocation). Authenticated terminal evidence is a tagged success receipt or no-effect certificate. Both bind the operation ID and key, complete acceptance digest 𝛽𝑜 , root, logical slot and credit lineage, epoch, effect digest, receiver, outcome, issuer, and signature. A success receipt additionally binds the unique instance ID, gateway acceptance sequence, and complete actual charge no greater than the reservation. A no-effect certificate instead binds a receiver-installed fenceEpoch > 𝜂𝑜 . The authority does not sign conflicting terminal variants. A success receipt exists only for the unique effect instance accepted under that exact 𝛽𝑜 . A no-effect certificate may be issued only when the exact (𝑔𝑜 , 𝜒𝑜 , 𝜅𝑜 , 𝛽𝑜 , 𝜂𝑜 ) binding never linearized

Fault-Tolerant Budget Conservation in Agent Delegation

9

Fault or attack

Naive failure

Required mechanism

Safe consequence

Concurrent fan-out Multi-parent join

Two children copy one remainder Shared ancestor counted twice Effect executes twice Timeout interpreted as failure Ledger misses consumption Old owner spends reclaimed credit Both sides spend cached total Fabricated “no effect” proof

Exclusive atomic split with stable operation ID Disjoint lineage test and atomic input consumption Canonical effect key at fenced gateway Durable obligation and indeterminate state Authenticated receipt query and idempotent settlement Monotone epoch and gateway fence Preallocated exclusive escrow Evidence authority or permanent retirement

Inputs consumed once; duplicate is a stutter Alias rejected; distinct inputs may merge Replay returns same outcome Credit stays reserved

Duplicate dispatch Response loss Crash after effect Stale worker Network partition Unknown receiver

Recovery moves reservation once Old generation rejected Each component spends only its rights No unsafe automatic refund

Table 2. Failure semantics. Safety may reduce availability or strand budget; the protocol reports that cost rather than hiding it as successful execution.

GatewayAccept; it proves both non-acceptance/non-occurrence and that its installed fence makes every future occurrence under that binding impossible. A fence does not cancel an already accepted request. Assumption 8 (AdapteR Refinement). MCP, A2A, HTTP, and runtime adapters preserve canonical operation and transfer identifiers, root, logical slot, credit lineage and footprint commitments, source and operation labels, resource and maximum-charge vectors, selector schema version, epoch, 𝜅 , 𝛽𝑜 , normalized effect and receiver, joint witness, and every terminal-evidence binding and committed/remainder footprint commitment used by the abstract transition. Assumption 9 (Complete mediation). An agent cannot reach a protected effect with credentials or a path outside the branch store and effect gateway. 3.6

Goals and Explicit Non-Goals

The safety goals are global ledger conservation, descendant non-amplification, at-most-once settlement, continuous injective effect coverage, a root-bounded external exposure vector, stale-epoch rejection, late-completion safety, and partition confinement. Concrete trace lifting is a separate implementation proof obligation. Liveness is conditional: an online branch with sufficient local escrow and a responsive gateway can progress without contacting the root issuer. A permanently partitioned, escrow-exhausted branch can safely refuse forever. The paper does not optimize allocation, predict token or price use, guarantee receiver honesty beyond Assumption 7, reverse completed effects, provide exactly-once network delivery, tolerate Byzantine infrastructure, conceal accounting data from the evidence plane, or establish production service-level objectives (SLOs).

10

Zhu and Wang

4 Why Simpler Mechanisms Fail 4.1

Allocation Conservation Is Not Prefix Conservation

The static condition

∑

𝑏𝑖 ≤ 𝑏𝑝

𝑖∈children(𝑝)

checks one allocation snapshot. It says nothing about whether an old child still owns 𝑏𝑖 after a refund, whether the same request was applied twice, or whether an external effect already consumed the allocation. The property we require holds for every execution prefix and accounts for in-flight and uncertain obligations. 4.2

Read–Check–Decrement Replicas Double Spend

If two partitioned branches read a global remaining value 1, both can locally verify 1 ≥ 1 and decrement. Last-writer-wins convergence can produce the valid-looking final value 0 after two effects. CRDT convergence is not invariant preservation; unrestricted decrement is not invariantconfluent [4]. Exclusive rights make each local decrement monotone with respect to ownership. 4.3

Static Splitting Is Safe but Can Strand Utility

Giving each of 𝑛 possible workers 𝐵/𝑛 before execution prevents double-spend, but idle branches strand capacity and dynamic fan-out requires worst-case over-reservation. Token Budgets measures this cost in its setting [22]. Our protocol retains the safety of static escrow while allowing coordinated, idempotent transfer and return. It does not pretend that reallocation remains available through every partition. 4.4

Timeout Refund Creates a Late-Completion Race

Let an operation be dispatched before time 𝑡 , let no response arrive by 𝑡 + Δ, and let the controller refund. There are two executions indistinguishable to the controller at 𝑡 + Δ: one in which the gateway never executed and one in which it executed but the response is delayed. A refund is safe in the first and unsafe in the second. No timeout value resolves the information gap. The system needs a fenced, authoritative no-effect proof or must retain/retire the reservation. 4.5

Idempotency Keys Do Not Allocate Authority

A stable request key can stop the same receiver from applying one effect twice. It does not stop two different operation keys from spending the same credit, a relabeled path from creating the same normalized effect, or two receivers from interpreting keys in different namespaces. The key must be bound to one credit generation, effect digest, receiver, epoch, and maximum charge, and the gateway must enforce that binding. 4.6

Scope Attenuation Does Not Consume

A scope token answers which operations a child may invoke. It can be copied to two children without widening the scope set, yet both children may spend the last dollar. Scope non-amplification and resource conservation are orthogonal. We compose with AIP/AAT-style identity and attenuation rather than replacing them.

Fault-Tolerant Budget Conservation in Agent Delegation

4.7

11

Compensation Is Not Conservation

A Saga can schedule a refund after a duplicated purchase, but the duplicate effect occurred and compensation can fail, cost money, or be semantically incomplete. Compensation is a valid recovery policy for designated effects; it is not evidence that the authorization budget was never exceeded. We record compensation as a further effect with its own authority and accounting. 4.8

Independent Correct Components Can Compose Incorrectly

An allocation service, idempotent gateway, lease manager, and receipt verifier can each be locally correct while disagreeing on operation identity or epoch. For example, a gateway may deduplicate on an HTTP key while the ledger retries under a new operation ID; or a lease manager may fence the branch while the receiver accepts the old generation. The protocol therefore requires one joint canonical binding and a concrete-to-abstract refinement contract. 4.9

The Joint Conditions Are Individually Necessary

The external bound is not obtained by merely placing familiar components next to one another. It uses four cross-component conditions on the same canonical operation: 𝒥 = ExclusiveOwnership ∧ InstanceInjectivity ∧ CompleteCharge ∧ FenceOrdering. Each conjunct has a one-unit counterexample if omitted while the others are retained: (1) without exclusive ownership, two branches reserve the same atom under distinct valid keys and each produces one correctly receipted effect; (2) without instance injectivity, one valid reservation and key produces two distinct receiver instances while only one operation remains in the ledger; (3) without complete charge, the gateway enforces a cap of one but a receipt reports zero for a one-unit effect, so internal settlement is conserved while actual cost is not; and (4) without fence ordering, an old request can be accepted after its atom is reissued, then both the old and successor operations complete. Consequently, bounded counters alone do not imply effect conservation, and durable completion records alone do not imply delegated-right conservation. The contribution proved below is the composition: 𝒥, together with persist-before-exposure and complete mediation, turns exact ownership partition into the external exposure bound in Equation (11). 5 Formal Budget and Delegation Model 5.1

Resource Vectors and Labels

Let 𝒦 be a finite set of authenticated resource dimensions. A budget is a vector b ∈ ℕ|𝒦| . We use componentwise order, addition, and partial subtraction: x ⪯ y ⟺ ∀𝑘 ∈ 𝒦 ∶ 𝑥𝑘 ≤ 𝑦𝑘 ,

y −̇ x is defined iff x ⪯ y.

Quantization is explicit. A currency dimension may use cents; an effect count uses integer events. The abstract results extend to cancellative commutative resource monoids with decidable subresource, but the executable profile uses finite natural vectors. A resource label 𝜆 = (𝑔, 𝜏 , 𝑝, purpose, audience, effectClass, 𝑡exp , 𝑣) binds root grant 𝑔 , task atom 𝜏 , principal 𝑝 , purpose, recipient/audience, effect class, expiry, and policy version. The relation 𝜆′ ⊑ 𝜆 means that every behavior denoted by 𝜆′ is permitted by 𝜆. It is a partial order. Delegation requires both quantitative and semantic attenuation:

12

Zhu and Wang

bchild ⪯ bparent ,

𝜆child ⊑ 𝜆parent .

(3)

An authenticated conversion contract is required to exchange dimensions. In its absence all conservation equations are componentwise and no conversion is defined. Expiry and policy-version currency are evaluated as external predicates in the commit-time witness. The budget-ownership machine does not infer trusted time or independently prove policy freshness. 5.2

Root Rights and Compressed Footprints

Definition 1 (Root Right univeRse). For root grant 𝑔 with issued vector B𝑔 , define

𝑈𝑔 = ⨄ {(𝑔, 𝑘, 𝑗) ∣ 1 ≤ 𝑗 ≤ 𝐵𝑔,𝑘 }. 𝑘∈𝒦

Each element is a logical consumable right in one dimension. It need not be materialized; an implementation may represent contiguous ranges, rights matrices, or balance certificates. For 𝑋 ⊆ 𝑈𝑔 , let vec(𝑋 )𝑘 = |{(𝑔, 𝑘, 𝑗) ∈ 𝑋 }|. Sets make aliasing explicit. A split partitions one footprint; a join unions only pairwise-disjoint footprints. Numeric balances are a compressed implementation of this ownership semantics. 5.3

Credits and the Delegation DAG

Definition 2 (CRedit geneRation). A credit generation is

𝑐 = ⟨𝑐𝑖𝑑, 𝑔, 𝜒𝑐 , owner, 𝑃𝑐 , 𝑋𝑐 , 𝜆𝑐 , 𝜂𝑐 , 𝜎𝑐 ⟩ where 𝑐𝑖𝑑 is the generation identifier, 𝜒𝑐 is the stable logical slot (reissue-chain) identifier, 𝑃𝑐 is a finite set of parent generations, 𝑋𝑐 ⊆ 𝑈𝑔 is its currently available footprint, 𝜆𝑐 ⊑ 𝜆𝑔 , 𝜂𝑐 is a monotonically ordered epoch, and 𝜎𝑐 ∈ {active, closing, closed} is its lifecycle status. Its available vector is a𝑐 = vec(𝑋𝑐 ). A reissue preserves 𝜒𝑐 while creating a fresh 𝑐𝑖𝑑 and higher epoch; a split or join creates fresh logical slots for its output credits. Consequently, disjoint split siblings may be current concurrently. For state 𝑠 , let ActiveGeneration𝑠 (𝑔, 𝜒 ) denote the credit authority’s current-generation register for logical slot (𝑔, 𝜒 ). The current-generation predicate is Current𝑠 (𝑐, 𝜂) ⟺ 𝜎𝑐 = active ∧ 𝜂 = 𝜂𝑐

∧ 𝜂 = AuthoritativeEpoch𝑠 (𝑔, 𝜒𝑐 )

(4)

∧ ActiveGeneration𝑠 (𝑔, 𝜒𝑐 ) = 𝑐𝑖𝑑. Uniqueness is therefore per logical reissue chain, not per root, owner, or authority. It prevents two generations of the same slot from being spendable without forbidding independently owned, pairwise-disjoint sibling slots. This predicate never substitutes for ownership: every ownershipmoving action also requires its referenced input footprint to have exactly the stated singleton raw source tag. For dispatch that source is R(𝑜), not the credit’s remaining available footprint. The task graph 𝒢𝑇 = (𝑉𝑇 , 𝐸𝑇 ) may be a DAG. The credit-lineage graph 𝒢𝐶 is also acyclic, but its edges have resource semantics. A multi-parent credit can be created only by Join, which consumes pairwise-disjoint inputs atomically. Thus a task node may depend on two branches without owning both branches’ budgets; dependency is not ownership.

Fault-Tolerant Budget Conservation in Agent Delegation

13

Definition 3 (Lineage-disjoint join). For current inputs 𝑐1 , … , 𝑐𝑚 , a join is admissible only if 𝑚

∀𝑖 ≠ 𝑗 ∶ 𝑋𝑐𝑖 ∩ 𝑋𝑐𝑗 = ∅

∧

⋀ Current𝑠 (𝑐𝑖 , 𝜂𝑐𝑖 )

∧

𝑖=1

∃𝑔 ⋆ ∀𝑖 ∶ 𝑔𝑐𝑖 = 𝑔 ⋆ ,

and the branch store can consume all inputs in one authoritative transition. The output is a same-root credit 𝑐 ′ with 𝑔𝑐 ′ = 𝑔 ⋆ and footprint ⋃𝑖 𝑋𝑐𝑖 ; its label must be an authenticated common lower bound, ∀𝑖 ∶ 𝜆′ ⊑ 𝜆𝑐𝑖 . We do not assume that the label partial order has a greatest lower bound. The set representation prevents two aliases of one ancestor from being added. In a compressed implementation, each transfer certificate carries a lineage commitment and a disjointness witness checked against durable spent/transfer records. 5.4

Transfers

A cross-store delegation cannot atomically debit one database and credit another without a distributed transaction. We represent a durable handoff

𝑥 = ⟨𝑥𝑖𝑑, 𝑐𝑠 , src, dst, 𝑋𝑥 , 𝜆𝑥 , 𝜂𝑠 , 𝜎𝑥 ⟩. The source atomically removes 𝑋𝑥 from 𝑋𝑐𝑠 and records 𝜎𝑥 = sealed. Those atoms are in transit: neither source nor destination may spend them. Every 𝑥𝑖𝑑 has one monotone decision register

𝛿[𝑥𝑖𝑑] ∈ {pending, accepted(𝑑𝑠𝑡, 𝑐𝑖𝑑), cancelled(𝑠𝑟𝑐)}.

(5)

The compare-and-set from pending to accepted is the logical ownership switch to the uniquely named destination child; a crash after that decision is recovered by materializing the same child row, which is an abstract stutter. Source cancellation requires a destination-exclusion proof and a compare-and-set from pending to cancelled; that decision logically restores the source, and later row finalization only materializes it. Thus accept and cancel cannot both become terminal, and stale source or destination rows never override the decision register. If no shared decision authority or exclusion protocol is available, cancellation is disabled and the rights remain in T. Timeout is never a decision. 5.5

Operations, Effects, and Terminal Evidence

Throughout, 𝐻 (tag ∥ ⋯) denotes a collision-resistant, domain-separated hash over one lengthprefixed canonical encoding. Maps and sets have deterministic key/element order, integers have a single representation, and strings have a fixed Unicode normalization. 𝐻 (𝑃𝑐 ) and 𝐻 (𝑋𝑜 ) may be verified lineage and rights commitments rather than materialized sets, but their opening/verification contract must bind exactly the modeled values. Definition 4 (NoRmalized effect). A normalized effect is

𝑒 = ⟨class, resource, subject, receiver, payloadDigest, domainPrecondition⟩. The function Normalize maps a protocol-specific proposal and current domain state to 𝑒 . Effectequivalent MCP, A2A, HTTP, shell, or browser paths share the same digest under the deployment’s effect contract. Definition 5 (Effect instance). An effect descriptor is a template; an occurrence is a distinct instance 𝜄 = ⟨𝑖𝑖𝑑, gateway, receiver, 𝜅, 𝛽, ℎ𝑒 , acceptSeq⟩. The acceptance sequence is assigned by the gateway’s per-key linearization domain, and 𝛽 is the complete accepted-operation binding defined below. The one-effect profile permits at most one 𝑖𝑖𝑑 for a

14

Zhu and Wang

canonical key. If an endpoint commits a bundle atomically, the entire bundle is one normalized instance and its receipt reports the bundle’s complete charge. For a terminal instance, ActualCharge(𝜄) is the unique resource vector assigned to that complete instance by the trusted charge contract; Assumption 7 requires the committed receipt to report exactly this vector. It is not inferred from an agent’s estimate or a partial stream observation. Definition 6 (OpeRation ReseRvation). An operation is

𝑜 = ⟨𝑜𝑖𝑑, 𝑔, 𝜒𝑐 , 𝑐𝑖𝑑, 𝜂𝑐 , 𝜅, 𝑒, ℎ𝑒 , 𝑋𝑜 , u, 𝜆𝑜 , Φ𝑜 , 𝜈sel , 𝜎𝑜 ⟩, where 𝑜𝑖𝑑 is a stable operation ID. The source credit is 𝑐𝑜 ; we write 𝑔𝑜 = 𝑔𝑐𝑜 , 𝜒𝑜 = 𝜒𝑐𝑜 , 𝑐𝑖𝑑𝑜 = 𝑐𝑖𝑑𝑐𝑜 , and 𝜂𝑜 = 𝜂𝑐𝑜 , while the unsubscripted source fields displayed in the tuple denote those same immutable values. Moreover, 𝜅 = 𝐻 (op ∥ 𝑖𝑠𝑠𝑢𝑒𝑟 ∥ 𝑔 ∥ 𝑐𝑖𝑑 ∥ 𝑜𝑖𝑑 ∥ 𝑟𝑒𝑐𝑒𝑖𝑣𝑒𝑟 ∥ ℎ𝑒 ) is its receiver-scoped canonical idempotency/query key. The collision- resistant, domain-separated derivation makes a key name one operation binding within the threat model; 𝜅 is not an agent-chosen alias. Here 𝑒 and ℎ𝑒 are the normalized effect and digest, 𝑋𝑜 is an exclusively reserved footprint, u = vec(𝑋𝑜 ) is the maximum charge, 𝜆𝑜 ⊑ 𝜆𝑐 , Φ𝑜 is the joint authorization witness, and 𝜎𝑜 is the operation phase. 𝜈sel names the immutable deterministic footprint-selector schema used if a successful receipt reports a partial charge. The gateway does not accept a loose collection of fields. It linearizes the domain-separated digest

𝛽𝑜 = 𝐻 (accept ∥ 𝑜𝑖𝑑 ∥ 𝑔 ∥ 𝜒𝑐 ∥ 𝑐𝑖𝑑 ∥ 𝜂𝑐 ∥ 𝜅 ∥ 𝐻 (𝑃𝑐 ) ∥ 𝐻 (𝑋𝑜 ) ∥ ℎ𝑒 ∥ 𝑟𝑒𝑐𝑒𝑖𝑣𝑒𝑟 ∥ u ∥ 𝐻 (𝜆𝑐 ) ∥ 𝐻 (𝜆𝑜 ) ∥ 𝐻 (Φ𝑜 ) ∥ 𝜈sel ).

(6)

Thus the root, logical slot, source lineage, generation, reserved rights, semantic ceiling, effect, receiver, maximum charge, selector schema, and commit witness compared by Covered are fields of one authenticated acceptance binding rather than implicit attributes of 𝜄 . The operation phases are: reserved ∶ indeterminate ∶ committed ∶ verified-aborted ∶ forfeited ∶

durable obligation and outbox exist; dispatch not known to begin, dispatch may have crossed the effect boundary, authoritative success receipt applied by one terminal decision, durable local non-dispatch proof or authoritative no-effect certificate, rights permanently unavailable; uncertainty is not refunded.

Dispatch moves reserved to indeterminate before or atomically with exposing work to the gateway. A synchronous success can proceed directly to settlement, but a crash at any cut leaves a durable reservation or indeterminate obligation. Definition 7 (Authenticated teRminal evidence). Externally authenticated terminal evidence is the tagged sum 𝜖 ∶∶= 𝑟 + ∣ 𝜋¬𝑒 , where

𝑟 + = ⟨𝑟𝑖𝑑, 𝑜𝑖𝑑, 𝑖𝑖𝑑, acceptSeq, 𝜅, 𝛽𝑜 , 𝑔, 𝜒𝑐 , 𝑐𝑖𝑑, 𝜂𝑐 , ℎ𝑒 , receiver, d, committed, 𝑡, issuer, signature⟩, 𝜋¬𝑒 = ⟨𝑝𝑖𝑑, 𝑜𝑖𝑑, 𝜅, 𝛽𝑜 , 𝑔, 𝜒𝑐 , 𝑐𝑖𝑑, 𝜂𝑐 , ℎ𝑒 , receiver, fenceEpoch, verified-no-effect, 𝑡, issuer, signature⟩. Verify+ (𝑟 + , 𝑜) holds only when every binding agrees, the issuer is trusted for the receiver, the signature is valid, 0 ⪯ d ⪯ u𝑜 , and d = ActualCharge(𝜄) for the identified gateway instance. Verify¬𝑒 (𝜋¬𝑒 , 𝑜)

Fault-Tolerant Budget Conservation in Agent Delegation

15

additionally requires exact (𝑔𝑜 , 𝜒𝑜 , 𝜅𝑜 , 𝛽𝑜 , 𝜂𝑜 ) agreement, a trusted proof authority, and fenceEpoch > 𝜂𝑜 installed for the same (𝑔𝑜 , 𝜒𝑜 ) at the receiver, and establishes the permanent non-acceptance/nonoccurrence condition in Assumption 7. Let Verifyterm (𝜖, 𝑜) select the appropriate variant verifier. Neither variant may substitute for the other. A fused local recovery transaction additionally admits a distinct durable non-dispatch witness

𝜋local = ⟨𝑙𝑖𝑑, 𝑜𝑖𝑑, 𝜅, 𝛽𝑜 , 𝑔, 𝜒𝑐 , 𝑐𝑖𝑑, 𝜂𝑐 , ℎ𝑒 , outboxSeq, 𝐻 (outboxRow), never-dispatchable, 𝑡, issuer, authenticator⟩. LocalNoDispatchPre𝑠 (𝜋local , 𝑜) holds only when all immutable operation and acceptance-binding fields agree; the issuer and authenticator identify the authoritative durable operation store; and the named outbox row’s authenticated monotone history has never reached dispatchable. The protected send path accepts only rows carrying an earlier durable dispatchable marker. Define Verifylocal (𝜋local , 𝑜, 𝑠, 𝑠 ′ ) ⟺ LocalNoDispatchPre𝑠 (𝜋local , 𝑜)

∧ Outbox𝑠 ′ [𝑜𝑖𝑑] = local-abort ∧ PersistedLocal𝑠 ′ (𝜋local , 𝑜). PersistedLocal𝑠 ′ means that the authoritative store persisted and authenticated the witness in that same serialized commit. The absorbing post-state permanently prevents later dispatch; this witness is therefore not a textual worker assertion. Define the full terminal-outcome witness type and the return-only subtype 𝜔 ∶∶= 𝑟 + ∣ 𝜋¬𝑒 ∣ 𝜋local , 𝜁 ∶∶= 𝜋¬𝑒 ∣ 𝜋local . Thus 𝜖 remains external signed evidence, whereas 𝜔 is the closed tagged sum used by a fused terminaland-successor transaction. For every supported selector schema 𝜈sel , fix a public total order ≺𝑔,𝜈sel on the atoms of each root and dimension. For fixed 𝑔 , 𝑋 ⊆ 𝑈𝑔 , and d ⪯ vec(𝑋 ), define Take𝜈sel (𝑋 , d) = ⋃ First𝑑𝑘 (𝑋 ∩ {(𝑔, 𝑘, 𝑗) ∣ 𝑗 ≥ 1}, ≺𝑔,𝜈sel ). 𝑘∈𝒦

Here First𝑛 (𝑌 , ≺) is the set of the 𝑛 least elements of finite 𝑌 ; its existence in every dimension follows from d ⪯ vec(𝑋 ). Thus 𝐷𝑜 = Take𝜈sel (𝑋𝑜 , d𝑟 + ) is not re-chosen after a crash or software upgrade. The terminal decision atomically persists commitments to both 𝐷𝑜 and 𝑋𝑜 ∖ 𝐷𝑜 . A conforming implementation uses this version-bound partition; persisting the charge vector alone is insufficient for atom-level lineage refinement. Write 𝑐 ⪯lin 𝑐 ′ when 𝑐 = 𝑐 ′ or an authenticated directed path in 𝒢𝐶 leads from 𝑐 to 𝑐 ′ . For a source credit 𝑐𝑜 and candidate terminal ownership transition 𝑠 → 𝑠 ′ , let Succ𝑠→𝑠 ′ (𝑐𝑜 ) contain (i) 𝑐𝑜 , or its authenticated same-lineage successor, only when that target is current in both states, and (ii) a fresh same-authority child that is absent in 𝑠 and created with 𝑃𝑐𝑟 = {𝑐𝑜 }, a fresh logical slot 𝜒𝑐𝑟 , and the unique current generation for that slot in 𝑠 ′ by this same transition. It may also contain (iii) the fresh same-slot successor 𝑐𝑟 = 𝑐 + created by TerminalRollover, but only when that same atomic action satisfies Equations (17)–(18), closes 𝑐𝑜 , and installs 𝑐 + as current for (𝑔, 𝜒𝑐𝑜 ). Every member satisfies 𝑐𝑜 ⪯lin 𝑐𝑟 ; the set never contains an ancestor, unrelated credit, or acceptedtransfer destination. Define the transition predicate ReturnTarget(𝑜, 𝑐𝑟 , 𝑠, 𝑠 ′ ) ⟺ 𝑔𝑐𝑟 = 𝑔𝑜 ∧ 𝑐𝑟 ∈ Succ𝑠→𝑠 ′ (𝑐𝑜 ) ∧ 𝑐𝑜 ⪯lin 𝑐𝑟

∧ Current𝑠 ′ (𝑐𝑟 , 𝜂𝑐𝑟 ) ∧ Authority(𝑐𝑟 ) = SettlementAuthority(𝑜) ∧ 𝜆𝑐𝑟 ⊑ 𝜆𝑐𝑜 .

(7)

16

Zhu and Wang

The terminal decision row binds 𝑐𝑟 before the concrete ownership update; both become visible in one atomic commit, so the abstract machine exposes no intermediate state. Returning capacity to a broader ancestor or another store is a subsequent sealed Delegate transition, not an implicit side effect of settlement. A governance receipt saying “policy allowed” is not an effect receipt. A model- or agent-reported token count is not authoritative unless the resource contract designates that reporter. The guarantee tiers are: (1) fenced, idempotent, queryable receiver: ledger and mediated effect coverage; (2) receipt-producing but non-idempotent receiver: no unsafe refund after ambiguity, possibly permanent forfeiture; and (3) agent self-report only: internal ledger integrity, not actual cost/effect conservation. 5.6

Ownership State

The ownership state is not typed as a total location function. It contains six raw relations that could, in an invalid state, overlap or omit a right: 𝒜𝑠 ⊆ 𝑈𝑔 × 𝒞, 𝒬𝑠 ⊆ 𝑈𝑔 × 𝒪,

𝒯𝑠 ⊆ 𝑈𝑔 × Transfers, ℛ𝑠 ⊆ 𝑈𝑔 × 𝒪, 𝒞𝑠 ⊆ 𝑈𝑔 × 𝒪, ℱ 𝑠 ⊆ 𝑈 𝑔 × 𝒪.

The letters denote available credit, sealed transfer, reserved operation, indeterminate/quarantined operation, committed consumption, and forfeited capacity created by the Retire action. For a tagged relation, let supp(𝑍𝑠 ) = {𝑢 ∣ ∃𝑧 ∶ (𝑢, 𝑧) ∈ 𝑍𝑠 } and define the candidate-location multiset Own𝑠 (𝑢) = {A(𝑐) ∶ (𝑢, 𝑐) ∈ 𝒜𝑠 } ⊎ {T(𝑥) ∶ (𝑢, 𝑥) ∈ 𝒯𝑠 }

⊎ {R(𝑜) ∶ (𝑢, 𝑜) ∈ ℛ𝑠 } ⊎ {Q(𝑜) ∶ (𝑢, 𝑜) ∈ 𝒬𝑠 } ⊎ {C(𝑜) ∶ (𝑢, 𝑜) ∈ 𝒞𝑠 } ⊎ {F(𝑜) ∶ (𝑢, 𝑜) ∈ ℱ𝑠 }. A conflicting distinct tag or cross-relation overlap therefore produces two candidates rather than being hidden by a function type. Byte-identical physical replicas of one logical row abstract to one relation member and are governed by the store’s uniqueness key. Only after ownership partition is proved do we write loc𝑠 (𝑢) for the unique element of Own𝑠 (𝑢). Bucket vectors are computed from the raw supports: A𝑔 (𝑠) = vec(supp(𝒜𝑠 )),

…,

F𝑔 (𝑠) = vec(supp(ℱ𝑠 )).

Within one relation, the protocol invariant also requires a right to have at most one tag. The support deliberately measures resource mass rather than tag multiplicity; all conservation equalities use it only after Own𝑠 (𝑢) has established the ownership partition. Competing tags are detected by Own, not by supp. The target invariant is: A𝑔 + T𝑔 + R𝑔 + Q𝑔 + C𝑔 + F𝑔 = B𝑔 .

(8)

Tracking F𝑔 matters. If crash or distrust permanently strands a right, writing only “consumed ≤ 𝐵” hides the availability loss. Retirement keeps the equation exact and makes the safety–utility tradeoff auditable.

Fault-Tolerant Budget Conservation in Agent Delegation

5.7

17

Transition System

The abstract machine starts at 𝒜𝑠0 = 𝑈𝑔 × {𝑐𝑔 },

A𝑔 = B𝑔 ,

T𝑔 = R𝑔 = Q𝑔 = C𝑔 = F𝑔 = 0.

For every ownership-moving action, the guard requires Own𝑠 (𝑢) = {ℓsrc } for every input atom. Its authoritative commit removes each source pair and inserts exactly one destination pair in the same transition. A replay can return the prior decision but cannot execute the relation update twice. Each transition is atomic at its stated local authority: Issue(𝑔, B𝑔 , 𝜆𝑔 ). Create the root credit with a fresh logical slot, status active, and initial epoch 𝜂𝑐 ; atomically set AuthoritativeEpoch(𝑔, 𝜒𝑐 ) = 𝜂𝑐 and ActiveGeneration(𝑔, 𝜒𝑐 ) = 𝑐𝑖𝑑 , and assign every atom in 𝑈𝑔 to it. Split(𝑐, 𝑋1 , … , 𝑋𝑚 ). Require that 𝑐 is the current owner generation at its authoritative epoch, pairwise-disjoint 𝑋𝑖 ⊆ 𝑋𝑐 , and label attenuation. Remove ⋃𝑖 𝑋𝑖 from the parent and create children with pairwise-distinct fresh logical slots and generation identifiers. In the same commit, install each child as active with matching authoritative-epoch and active-generation registers. If the parent retains a nonempty available footprint or any outstanding operation/transfer it remains current; only if the action consumes its complete responsibility does it close the parent and clear that slot’s active-generation register. A stable request ID makes replay a stutter. Delegate(𝑐, dst, 𝑋 , 𝜆′ , 𝑥𝑖𝑑). Atomically move 𝑋 ⊆ 𝑋𝑐 from A(𝑐) to T(𝑥) and initialize 𝛿[𝑥𝑖𝑑] = pending. AcceptTransfer wins the decision compare-and-swap (CAS) and logically moves the same atoms to a uniquely named child credit with a fresh logical slot; CancelTransfer needs an exclusion proof and the competing CAS to logically restore them to the source. Acceptance atomically installs the child as active with matching authoritative-epoch and active-generation registers. Later database-row materialization stutters. The source cannot spend sealed atoms. Reserve(𝑐, 𝑜, 𝑋 , 𝑒). Require 𝑋 ⊆ 𝑋𝑐 , current epoch, joint witness, and effect/label compatibility. Atomically move 𝑋 from A(𝑐) to R(𝑜) while persisting operation, obligation, outbox, and audit. Dispatch(𝑜). Revalidate epoch and witness. Before possible gateway acceptance, move 𝑋𝑜 from R(𝑜) to Q(𝑜). A stale, provably unexposed reservation is returned only through Return(𝑜, 𝜋local ), which installs the absorbing local outbox marker. GatewayAccept(𝑜). If the per-key register already contains Accepted[𝜅𝑜 ] = 𝛽𝑜 , return that decision and stutter regardless of the operation’s later terminal bucket. A different stored binding is rejected. Only when the key is unseen may first acceptance linearize: require the matching durable dispatchable marker and 𝑋𝑜 wholly in Q(𝑜) or absorbing F(𝑜), then recompute and atomically accept the complete immutable digest 𝛽𝑜 against the receiver’s key, current witness, and the fence selected by the authenticated slot (𝑔, 𝜒𝑐 ). An unexposed reservation or a new old-epoch key is rejected. EffectOccurs(𝑜, 𝜄). Require a prior accepted (𝜅𝑜 , 𝛽𝑜 ) binding and 𝜄.𝛽 = 𝛽𝑜 ; append the fresh instance 𝜄 to the gateway’s monotone observation log. Under the one-effect profile, a second instance for the same 𝜅𝑜 is disabled; transport attempts may duplicate without appending another instance.

18

Zhu and Wang

Settle(𝑜, 𝑟 + ). Require 𝑋𝑜 wholly in Q(𝑜), a verified success receipt, and 𝜄𝑟 + ∈ Obs(𝑠). Derive 𝐷𝑜 = Take𝜈sel (𝑋𝑜 , d𝑟 + ) and persist the exact committed and remainder commitments. Move 𝐷𝑜 to C(𝑜). If 𝑋𝑜 ∖ 𝐷𝑜 ≠ ∅, require a decision-bound 𝑐𝑟 satisfying Equation (7) and move the remainder there. Settlement never widens the source label, changes the root, jumps to an ancestor, or resurrects a stale generation. If an identical receipt was already applied, stutter; any conflicting receipt is rejected. Return(𝑜, 𝜁 ). Require exactly one type-matched branch. The local branch has

𝜁 = 𝜋local ,

𝑋𝑜 wholly in R(𝑜),

Verifylocal (𝜋local , 𝑜, 𝑠, 𝑠 ′ ).

The external branch has 𝜁 = 𝜋¬𝑒 , 𝑋𝑜 wholly in Q(𝑜), and an authoritative fenced Verify¬𝑒 (𝜋¬𝑒 , 𝑜) proof that the exact binding was never gateway-accepted and did not and cannot execute. Also require a decision-bound 𝑐𝑟 satisfying Equation (7). Move all 𝑋𝑜 from the branch-specific source to 𝑐𝑟 and mark the operation verified-aborted; the local branch atomically installs the absorbing outbox marker. Retire(𝑜). Move an unresolved 𝑋𝑜 from Q(𝑜) to F(𝑜). The bucket is absorbing: atoms never become available or committed. Later evidence annotates the operation’s outcome and actual charge without moving ownership, so forfeiture remains a conservative maximum charge. Fence(𝑐, 𝜂′ ). For a first installation, require Current𝑠 (𝑐, 𝜂𝑐 ) and 𝜂′ > AuthoritativeEpoch𝑠 (𝑔, 𝜒𝑐 ) = 𝜂𝑐 . Atomically advance the slot’s authoritative epoch, mark 𝑐 closing, clear 𝑐𝑖𝑑 as its active generation, and install the same monotone fence at all protected gateways before permitting new-generation use. An exact already-installed retry stutters. A not-yet-accepted old request is rejected; a request accepted before the fence may complete later and remains charged/queryable. Reissue(𝑐, 𝜂, 𝜂+ , 𝑐 + ). Require Equations (14), (15), and (16), require SafeA𝑠 (𝑐, 𝜂) = Avail𝑠 (𝑐, 𝜂), and require the writeonce reissue decision for the normalized predecessor key (𝑔, 𝜒𝑐 , 𝑐𝑖𝑑, 𝜂𝑐 , reissue) to select (𝜂+ , 𝑐 + ), with 𝜂 = 𝜂𝑐 . In one transaction, persist that decision, mark 𝑐 closed, update currentgeneration metadata, and move exactly the uniquely available reusable footprint into fresh generation (𝑐 + , 𝜂+ ) of the same logical slot. Exact replay stutters and a changed target is rejected. Old committed, forfeited, transferred, or otherwise obligated atoms do not move. TerminalRollover(𝑜, 𝜔, 𝑐, 𝜂, 𝜂+ , 𝑐 + ). Apply the fused transition in Equations (17)–(18) only when 𝑜 is the final nonterminal operation of the fenced predecessor. In one commit, apply its type-matched terminal-outcome witness, move the terminal remainder together with the predecessor’s already safe available footprint into the one normalized reissue target, close the predecessor, and install the sameslot successor. This is one abstract action, not an implicit relaxation of Settle or Reissue. Join(𝑐1 , … , 𝑐𝑚 ). Require Definition 3, no active operations on the input portions, and one atomic authority. Consume inputs and create one output over their disjoint union with a fresh logical slot. The same commit closes every fully consumed input and clears its active-generation register, then installs the output as active with matching authoritative-epoch and active-generation registers.

Fault-Tolerant Budget Conservation in Agent Delegation

5.8

19

Safety Invariants

For all reachable states, we require: I1. Ownership partition. |Own𝑠 (𝑢)| = 1 for every 𝑢 ∈ 𝑈𝑔 , including uniqueness of the tag inside its raw relation. I2. Non-negative vectors. All bucket vectors are in ℕ|𝒦| . I3. Semantic attenuation. Every descendant label restricts every lineage ancestor label applicable to its footprint. I4. Current generation. A split, delegate, reserve, join, or dispatch uses the current owner generation and epoch. I5. Operation binding. Each 𝑜𝑖𝑑 derives exactly one canonical 𝜅 . Within its receiver namespace, an accepted 𝜅 maps to exactly one 𝛽𝑜 , which immutably binds 𝑜𝑖𝑑 , root, logical slot, footprint and lineage commitments, epoch, effect digest, receiver, maximum vector, selector schema version, source and operation labels, and the joint witness. I6. Settlement uniqueness. At most one non-conflicting authoritative terminal-evidence variant is applied to an operation. I7. Instance injectivity. The monotone gateway log contains at most one effect instance per canonical key, and one operation covers at most one instance in the one-effect profile. I8. Dispatch coverage. Every protected dispatch without a terminal verified-no-effect decision has a durable operation whose atoms are wholly in Q or F, or whose complete committed receipt accounts for its actual-charge subset in C. A full no-effect return is backed either by durable never-dispatchable evidence or by authoritative proof that past and future occurrence is impossible. A partial-success remainder is backed by one complete terminal receipt that proves the exact actual charge and disables any further instance or charge under (𝜅𝑜 , 𝛽𝑜 ). I9. No stale resurrection. Advancing an epoch does not make a prior generation current again. 5.9

Effect Instances, Coverage, and External Exposure

The state variable Obs(𝑠) is the gateway’s monotone log of instances appended only by EffectOccurs. It is a set of 𝜄 from Definition 5, not a set of effect descriptors. Thus two separate payments with identical payloads remain two instances. The relation Covered(𝜄, 𝑜, 𝑠) is non-recursive. It holds exactly when: (1) 𝜄.𝜅 = 𝜅𝑜 , 𝜄.𝛽 = 𝛽𝑜 , 𝜄.ℎ𝑒 = ℎ𝑒𝑜 , and the gateway and receiver agree; by Equation (6), equality of 𝛽 also binds root, logical slot, lineage, epoch, footprint, labels, maximum vector, and witness; (2) 𝑜 ’s label and commit-time witness were valid at gateway acceptance; and (3) either 𝑋𝑜 remains wholly in Q(𝑜) or F(𝑜), or a complete committed receipt for 𝜄 identifies 𝐷𝑜 = Take𝜈sel (𝑋𝑜 , ActualCharge(𝜄)) in C(𝑜). Coverage and instance injectivity are:

∀𝜄 ∈ Obs(𝑠),

∃! 𝑜 ∈ 𝒪 ∶ Covered(𝜄, 𝑜, 𝑠),

Covered(𝜄1 , 𝑜, 𝑠) ∧ Covered(𝜄2 , 𝑜, 𝑠) ⟹ 𝜄1 = 𝜄2 .

(9) (10)

Let Settled𝑔 (𝑠) contain exactly the instances whose unique covering operation satisfies 𝑔𝑜 = 𝑔 and whose complete receipt has placed its actual-charge footprint in C. Let Risk𝑔 (𝑠) = {𝑜 ∣ 𝑔𝑜 = 𝑔∧ 𝑋𝑜 is wholly in Q(𝑜) or F(𝑜)}, irrespective of any later evidence annotation. The charged footprints associated with Settled𝑔 and the full footprints associated with Risk𝑔 are pairwise disjoint by ownership location. In particular, a success receipt arriving after forfeiture is recorded for audit but does not move F, does not enter Settled, and remains charged at the conservative maximum. The external exposure bound is:

20

Zhu and Wang

∑

ActualCharge(𝜄) +

𝜄∈Settled𝑔 (𝑠)

∑

u𝑜 ⪯ C𝑔 (𝑠) + Q𝑔 (𝑠) + F𝑔 (𝑠) ⪯ B𝑔 .

(11)

𝑜∈Risk𝑔 (𝑠)

This is stronger than an internally consistent counter and weaker than a claim about unmediated physical reality. It additionally depends on the ownership assumptions used by Theorem 1 and on Assumptions 4, 5, 6, 7, and 9. 5.10

Descendant Capacity

For an execution prefix 𝜌 ending in 𝑠 , a single-root sub-DAG 𝑊 , and a cut separating it from its ancestors, let In𝜌 (𝑊 ) ⊆ 𝑈𝑔 be the union of exact atom footprints in authenticated ownership events that crossed from a responsible lineage outside 𝑊 to one inside 𝑊 along 𝜌 . This includes cross-cut split, accepted transfer, return, successor reissue, and join inputs, and is deduplicated by atom identity on re-entry. Let Held𝑠 (𝑊 ) include atoms currently available, reserved, indeterminate, committed, or forfeited in descendants of 𝑊 . Descendant non-amplification is: Held𝑠 (𝑊 ) ⊆ In𝜌 (𝑊 ),

vec(Held𝑠 (𝑊 )) ⪯ vec(In𝜌 (𝑊 )).

(12)

Transfers out of 𝑊 leave the left-hand side. A task dependency edge without a credit transfer contributes no capacity. 6 Fault-Tolerant Delegation and Settlement Protocol 6.1

Design Principles

The protocol follows six rules: (1) Move quantities and attenuate labels. A child receives both an exclusive footprint and a narrower-or-equal authorization label. (2) Persist before exposure. Reservation, obligation, outbox, and audit state commit before a protected dispatch can escape. (3) Bind the real effect. The reservation uses a normalized effect digest and current dependency/authority witness, not a tool name alone. (4) Treat ambiguity as charged. Response loss produces indeterminate, never automatic refund. (5) Fence before reuse. Reclaim from an exposed obligation requires a gateway-visible fence and authoritative evidence that the exact binding was never accepted and did not occur; a fence alone never releases quarantined rights. (6) Make replay a stutter. Stable transfer, operation, and terminal-evidence IDs return the prior decision without repeating state movement. 6.2

Joint Authorization and Budget Witness

The prior research stack supplies complementary predicates over one canonical operation: ValidWitness(𝑜) ⟺ StaticPolicy(𝑜) ∧ TaskIntent(𝑜) ∧ ProvenanceCeiling(𝑜)

∧ SessionLease(𝑜) ∧ SafeRoute(𝑜) ∧ CurrentClosure(𝑜)

(13)

∧ NormalizedEffect(𝑜) ∧ CurrentCredit(𝑜). OpenPort supplies the server-side action boundary [53]. Public work on intent-governed authorization and server-verified action claims supplies concrete examples of the intent and execution predicates [50, 51]; versioned dependency-closure binding supplies the current recursive skill closure and normalized effect [52]. The remaining predicates in Equation (13) are explicit interface

Fault-Tolerant Budget Conservation in Agent Delegation

21

assumptions defined by this paper. They are inputs at the witness boundary, not imported conservation results: the exclusive distributed-credit and settlement properties are established here. 6.3

Credit Certificates

A transfer certificate contains: { "transfer_id": "...", "root_grant_id": "...", "source_credit_id": "...", "source_epoch": 17, "destination": "agent://worker-b", "resource_vector": {"usd_cents": 4000, "api_calls": 6}, "lineage_commitment": "...", "rights_commitment": "...", "authorization_label_digest": "...", "expires_at": "...", "issuer": "...", "signature": "..." }

The destination cannot enlarge the vector or label. The certificate identifies a transfer operation, not a bearer balance that may be imported repeatedly. Acceptance writes a uniqueness key over (root, transfer_id). 6.4

Idempotent Delegation

Algorithm 1 performs a sealed cross-store transfer. A local split is its single-authority, no-transit specialization. The source transition is authoritative for removing spendability. Message send occurs after the durable seal. If the destination is unreachable, 𝑋 remains in T𝑔 . Safe cancel is a protocol transition requiring destination fencing or a durable decision that the transfer cannot later be accepted. The implementation may instead leave it in transit until reconciliation. 6.5

Reserve Before Dispatch

Algorithm 2 converts available credit to a durable obligation. The maximum vector u must be known conservatively. If a provider can exceed u without rejection, that provider cannot support the hard-bound profile. The explicit R → Q cut is conservative. A crash after the move but before network send can strand budget until the gateway proves non-execution. Moving after send would create an uncovered effect window. Safety chooses possible stranding. 6.6

Terminal-Evidence Settlement

Algorithm 3 is idempotent and never re-executes the effect. Success consumes the actual vector and returns only the authenticated remainder. A no-effect certificate returns the full footprint. Pending or unknown status is not terminal evidence and leaves it in Q. 6.7

Recovery, Reconciliation, and Forfeiture

Algorithm 4 scans operations in reserved or indeterminate. Reserved operations whose outbox was never made dispatchable can be aborted inside the branch transaction. Once dispatchability

22

Zhu and Wang

Algorithm 1 DelegateEscRow(𝑐, dst, q, 𝜆′ , 𝑥𝑖𝑑) Require: current credit 𝑐 , destination, vector, attenuated label, stable transfer ID 1: begin durable source transaction 2: if a decision for 𝑥𝑖𝑑 exists then 3: return the recorded certificate or rejection 4: end if 5: require Current𝑠txn (𝑐, 𝜂𝑐 ), q ⪯ a𝑐 , and 𝜆 ′ ⊑ 𝜆𝑐 6: choose footprint 𝑋 ⊆ 𝑋𝑐 with vec(𝑋 ) = q 7: 𝑋𝑐 ← 𝑋𝑐 ∖ 𝑋 8: persist sealed transfer 𝑥 = (𝑥𝑖𝑑, 𝑐, dst, 𝑋 , 𝜆 ′ , 𝜂𝑐 ) 9: initialize 𝛿[𝑥𝑖𝑑] = pending; persist outbox and audit; commit 10: send certificate from outbox, retrying with the same 𝑥𝑖𝑑 11: destination verifies signature, epoch, label, and uniqueness 12: destination CASes 𝛿[𝑥𝑖𝑑] ∶ pending → accepted(𝑑𝑠𝑡, 𝑐𝑖𝑑 ′ ) 13: if the decision is accepted then 14: atomically create or recover the uniquely named child 𝑐𝑖𝑑 ′ over 𝑋 15: source records the terminal decision; it never restores an accepted 𝑋 16: return accepted child certificate 17: else if the decision is cancelled then 18: reject import; source may restore 𝑋 exactly once 19: source records the terminal decision 20: return durable cancellation or rejection status 21: end if

was committed, the reconciler queries the gateway by 𝜅 . It applies an authenticated success receipt, installs a fence and obtains a no-effect proof, or retains uncertainty. Forfeiture is not a cleanup trick. It records that the system cannot safely reuse the capacity. Later evidence may annotate a committed outcome and actual charge, but F remains the conservative maximum and no ownership bucket changes. 6.8

Epoch Fencing and Safe Reclaim

A controller may advance a credit epoch after a worker is lost. The new epoch does not itself reclaim outstanding rights. We first close the old generation: For the remainder of this section, Ops(𝑐, 𝜂) and Transfers(𝑐, 𝜂) are monotone historical index sets: they contain every durably created operation or transfer whose immutable source binding names credit 𝑐 and authenticated epoch 𝜂, including terminal records. They are not filtered “live” views. SettlementAuthority(𝑜) is the immutable branch authority bound at Reserve that may apply 𝑜 ’s terminal ownership decision. FenceInstalled𝑠 (𝑔, 𝜒 , 𝜂+ ) means every gateway protecting that root/slot durably enforces a rejection floor of at least 𝜂+ . Finally, let

𝐾𝑐 = (𝑔, 𝜒𝑐 , 𝑐𝑖𝑑, 𝜂𝑐 , reissue) and let Decision𝑠 [𝐾𝑐 ] and TermDecision𝑠 [𝑜𝑖𝑑] be partial write-once registers, with ⊥ denoting an unassigned value.

Fault-Tolerant Budget Conservation in Agent Delegation

23

Algorithm 2 ReseRveAndDispatch(𝑐, proposal, u, 𝑜𝑖𝑑) Require: current credit, proposed protected effect, maximum vector, stable operation ID, supported selector schema 𝜈sel 1: 𝑒 ← Normalize(proposal, currentDomainState) 2: ℎ𝑒 ← 𝐻 (effect ∥ 𝑒) 3: compile current joint witness Φ𝑜 satisfying Equation (13) 4: require RequiredCap(𝑒, 𝜒 ) ⪯ u 5: derive key 𝜅 ← 𝐻 (op ∥ 𝑖𝑠𝑠𝑢𝑒𝑟 ∥ 𝑔 ∥ 𝑐𝑖𝑑 ∥ 𝑜𝑖𝑑 ∥ 𝑟𝑒𝑐𝑒𝑖𝑣𝑒𝑟 ∥ ℎ𝑒 ) 6: begin durable branch transaction 7: if operation 𝑜𝑖𝑑 exists then 8: require all immutable bindings equal; return recorded state 9: end if 10: require Current𝑠txn (𝑐, 𝜂𝑐 ), u ⪯ a𝑐 , Φ𝑜 valid, and 𝑒 compatible with 𝜆𝑐 11: choose 𝑋𝑜 ⊆ 𝑋𝑐 with vec(𝑋𝑜 ) = u 12: derive 𝛽𝑜 from the selected 𝑋𝑜 and every field in Equation (6) 13: construct the canonical signed operation envelope containing every preimage field of 𝜅 and 𝛽𝑜 , plus both digests 14: move 𝑋𝑜 ∶ A(𝑐) → R(𝑜) 15: atomically persist operation/obligation with 𝛽𝑜 , the exact non-dispatchable envelope in the outbox, and audit; commit 16: begin dispatch transaction; reload the persisted envelope 17: recompute and require its 𝜅 , 𝛽𝑜 , signature, and immutable operation binding; recheck Current𝑠txn (𝑐, 𝜂𝑐 ) and the persisted Φ𝑜 18: if either check is stale while outbox is provably unexposed then 19: construct the type-tagged candidate 𝜋local from the persisted operation and outbox row 20: bind a decision-fixed target descriptor 𝑐return ; require this transaction’s before/after states satisfy Equation (7) ′ ), return 𝑋 to 𝑐 21: atomically require Verifylocal (𝜋local , 𝑜, 𝑠txn , 𝑠txn 𝑜 return , write the canonical terminal-decision/audit records, and mark verified-aborted 22: commit; return the recorded stale-generation rejection 23: end if 24: construct a branch-signed dispatch permit over 𝛽𝑜 25: atomically move 𝑋𝑜 ∶ R(𝑜) → Q(𝑜), persist the permit, and mark the outbox dispatchable; commit before gateway exposure 26: send only the persisted envelope and permit through the fenced gateway 27: before first acceptance, gateway recomputes 𝜅 and 𝛽𝑜 , verifies the permit, and revalidates the bound precondition and current commit witness; an exact accepted replay returns the stored decision 28: return synchronous success receipt if present; otherwise indeterminate

Closed𝑠 (𝑐, 𝜂, 𝜂+ ) ⟺ 𝜂 = 𝜂𝑐 ∧ 𝜂+ = AuthoritativeEpoch𝑠 (𝑔, 𝜒𝑐 ) ∧ 𝜂+ > 𝜂

∧ 𝜎𝑐 ∈ {closing, closed} ∧ FenceInstalled𝑠 (𝑔, 𝜒𝑐 , 𝜂+ ) ∧ ∀𝑥 ∈ Transfers(𝑐, 𝜂) ∶ 𝛿[𝑥] ∈ {accepted, cancelled} ∧ ∀𝑜 ∈ Ops(𝑐, 𝜂) ∶ 𝜎𝑜 ∈ {committed, verified-aborted, forfeited}. (14)

24

Zhu and Wang

Algorithm 3 SettleOutcome(𝑜, 𝜖) Require: durable operation 𝑜 , candidate terminal evidence 𝜖 ∈ {𝑟 + , 𝜋¬𝑒 } 1: begin durable branch transaction 2: if 𝑋𝑜 is wholly in absorbing F(𝑜) then 3: require Verifyterm (𝜖, 𝑜) 4: append or return the idempotent late-evidence annotation 5: commit; return the unchanged forfeited ownership decision 6: end if 7: if evidence ID or terminal decision for 𝑜𝑖𝑑𝑜 was applied then 8: require byte-equivalent binding; return the prior decision 9: end if 10: require 𝑋𝑜 is wholly in Q(𝑜) 11: if 𝜖 = 𝑟 + then 12: require Verify+ (𝑟 + , 𝑜) and 𝜄𝑟 + ∈ Obs(𝑠) 13: derive 𝐷𝑜 ← Take𝜈sel (𝑋𝑜 , d𝑟 + ) and bind 𝐻 (𝐷𝑜 ), 𝐻 (𝑋𝑜 ∖ 𝐷𝑜 ) 14: if 𝑋𝑜 ∖ 𝐷𝑜 ≠ ∅ then 15: bind a decision-fixed target descriptor 𝑐return ; require this transaction’s successor state satisfy Equation (7) 16: end if 17: move 𝐷𝑜 ∶ Q(𝑜) → C(𝑜) 18: if 𝑋𝑜 ∖ 𝐷𝑜 ≠ ∅ then 19: move 𝑋𝑜 ∖ 𝐷𝑜 ∶ Q(𝑜) → A(𝑐return ) 20: end if 21: mark 𝑜 committed and persist 𝑟 + /audit atomically 22: else 23: require 𝜖 = 𝜋¬𝑒 and Verify¬𝑒 (𝜋¬𝑒 , 𝑜) 24: bind a decision-fixed target descriptor 𝑐return ; require this transaction’s successor state satisfy Equation (7) 25: move 𝑋𝑜 ∶ Q(𝑜) → A(𝑐return ) 26: mark 𝑜 verified-aborted and persist 𝜋¬𝑒 /audit atomically 27: end if 28: commit; return durable decision Let SafeA𝑠 (𝑐, 𝜂) be the atoms for which the reclaim authority holds a durable proof that Own𝑠 (𝑢) = {A(𝑐)}, together with retained provenance: the atom was idle, returned by a verified abort or authenticated remainder, or restored after a cancelled transfer. This raw-ownership condition does not require the fenced old generation itself to remain Current𝑠 . An accepted transfer, a committed atom, and a forfeited atom are excluded. Let Avail𝑠 (𝑐, 𝜂) = {𝑢 ∈ 𝑈𝑔 ∣ 𝜂 = 𝜂𝑐 ∧ Own𝑠 (𝑢) = {A(𝑐)}}. A successor-installing action is enabled only when SafeA𝑠 (𝑐, 𝜂) = Avail𝑠 (𝑐, 𝜂); otherwise the predecessor remains closing and the unproved capacity is stranded, not silently reclassified as reusable. The exact reusable footprint is therefore Reusable𝑠 (𝑐, 𝜂, 𝜂+ ) = {

SafeA𝑠 (𝑐, 𝜂), ∅,

Closed𝑠 (𝑐, 𝜂, 𝜂+ ) ∧ SafeA𝑠 (𝑐, 𝜂) = Avail𝑠 (𝑐, 𝜂), otherwise.

(15)

Fault-Tolerant Budget Conservation in Agent Delegation

25

Algorithm 4 RecoveRAndReconcile(𝑜) Require: durable nonterminal operation 𝑜 1: if 𝑜.𝑝ℎ𝑎𝑠𝑒 = reserved and durable outbox proves never dispatchable then 2: construct the type-tagged candidate 𝜋local 3: bind a decision-fixed target descriptor 𝑐return ; require the atomic transition’s before/after states satisfy Equation (7) 4: atomically require Verifylocal (𝜋local , 𝑜, 𝑠, 𝑠 ′ ), return 𝑋𝑜 to 𝑐return , and mark verified-aborted 5: return 6: end if 7: query gateway by the exact binding (𝑔𝑜 , 𝜒𝑜 , 𝜅𝑜 , 𝛽𝑜 , 𝜂𝑜 ) 8: if authenticated success receipt 𝑟 + is returned then 9: SettleOutcome(𝑜, 𝑟 + ) 10: else if gateway atomically fences the old binding/epoch and returns 𝜋¬𝑒 then 11: SettleOutcome(𝑜, 𝜋¬𝑒 ) 12: else if administrator chooses permanent safety over utilization then 13: move 𝑋𝑜 ∶ Q(𝑜) → F(𝑜); preserve obligation 14: else 15: retain indeterminate; schedule bounded-backoff reconciliation 16: end if Let FreshAuthenticated𝑠 (𝑐 + ) mean that no credit with the signed identity of 𝑐 + exists in 𝑠 and that its credit-authority authentication verifies. Then ReissueTarget(𝑐, 𝜂, 𝜂+ , 𝑐 + , 𝑠, 𝑠 ′ )

⟺ FreshAuthenticated𝑠 (𝑐 + ) ∧ 𝜂 = 𝜂𝑐 ∧ 𝜂+ = AuthoritativeEpoch𝑠 (𝑔, 𝜒𝑐 ) ∧ 𝑔𝑐 + = 𝑔𝑐 ∧ 𝜒𝑐 + = 𝜒𝑐 ∧ 𝑃𝑐 + = {𝑐}

(16)

∧ Authority(𝑐 + ) = Authority(𝑐) ∧ 𝜂𝑐 + = 𝜂+ ∧ 𝜆𝑐 + ⊑ 𝜆𝑐 ∧ Current𝑠 ′ (𝑐 + , 𝜂+ ) ∧ ¬Current𝑠 ′ (𝑐, 𝜂). The reference SQLite profile fuses a final terminal decision with successor installation. To give that concrete transaction one exact abstract image, define ValidTerminal𝑠 (𝑜, 𝜔) to mean exactly one of: (i) 𝜔 = 𝑟 + , 𝑜 is quarantined with all 𝑋𝑜 in Q(𝑜), Verify+ (𝑟 + , 𝑜), and the receipt’s 𝜄𝑟 + ∈ Obs(𝑠); (ii) 𝜔 = 𝜋¬𝑒 , 𝑜 is quarantined with all 𝑋𝑜 in Q(𝑜), Verify¬𝑒 (𝜋¬𝑒 , 𝑜), and the verified certificate binds the installed higher fence for (𝑔𝑜 , 𝜒𝑜 ) and proves that the exact binding was never accepted and cannot execute; or (iii) 𝜔 = 𝜋local , 𝑜 is reserved with all 𝑋𝑜 in R(𝑜), and LocalNoDispatchPre𝑠 (𝜋local , 𝑜). Let the terminal outcome determine two disjoint footprints:

𝜔 𝑟+ 𝜋¬𝑒 or 𝜋local

CommitFoot(𝑜, 𝜔) 𝐷𝑜 ∅

ReturnFoot(𝑜, 𝜔) 𝑋𝑜 ∖ 𝐷𝑜 𝑋𝑜 .

Define committed, 𝜔 = 𝑟 +, TermStatus(𝜔) = { verified-aborted, 𝜔 ∈ {𝜋¬𝑒 , 𝜋local }.

26

Zhu and Wang

The terminal record stores this tag, the evidence and acceptance-binding digests, and the exact committed and return footprint commitments: TermRecord(𝑜, 𝜔) = ⟨TermStatus(𝜔), 𝐻 (𝜔), 𝐻 (𝛽𝑜 ),

𝐻 (CommitFoot(𝑜, 𝜔)), 𝐻 (ReturnFoot(𝑜, 𝜔))⟩. Define RolloverReady𝑠 (𝑐, 𝜂, 𝜂+ , 𝑜, 𝜔)

⟺ 𝜂 = 𝜂𝑐 ∧ 𝜂+ > 𝜂 ∧ 𝜂+ = AuthoritativeEpoch𝑠 (𝑔, 𝜒𝑐 ) ∧ FenceInstalled𝑠 (𝑔, 𝜒𝑐 , 𝜂+ ) ∧ 𝜎𝑐 = closing ∧ ValidTerminal𝑠 (𝑜, 𝜔) ∧ 𝑜 ∈ Ops(𝑐, 𝜂) ∧ Authority(𝑐) = SettlementAuthority(𝑜)

(17)

∧ TermDecision𝑠 [𝑜𝑖𝑑] = ⊥ ∧ Decision𝑠 [𝐾𝑐 ] = ⊥ ∧ SafeA𝑠 (𝑐, 𝜂) = Avail𝑠 (𝑐, 𝜂) ∧ ∀𝑥 ∈ Transfers(𝑐, 𝜂) ∶ 𝛿[𝑥] ∈ {accepted, cancelled} ∧ ∀𝑜 ′ ∈ Ops(𝑐, 𝜂) ∖ {𝑜} ∶ 𝜎𝑜 ′ ∈ {committed, verified-aborted, forfeited}. Then the fused action is defined, not merely implemented by convention: TerminalRollover(𝑜, 𝜔, 𝑐, 𝜂, 𝜂+ , 𝑐 + , 𝑠, 𝑠 ′ ) ⟺ RolloverReady𝑠 (𝑐, 𝜂, 𝜂+ , 𝑜, 𝜔) ∧ ReissueTarget(𝑐, 𝜂, 𝜂+ , 𝑐 + , 𝑠, 𝑠 ′ )

∧ Decision𝑠 ′ [𝐾𝑐 ] = (𝜂+ , 𝑐 + ) ∧ TermDecision𝑠 ′ [𝑜𝑖𝑑] = TermRecord(𝑜, 𝜔) ∧ 𝜎𝑜′ = TermStatus(𝜔) ∧ 𝜎𝑐′ = closed ∧ (𝜔 = 𝜋local ⇒ Verifylocal (𝜋local , 𝑜, 𝑠, 𝑠 ′ ))

(18)

SafeA𝑠 (𝑐, 𝜂) ∶ A(𝑐) → A(𝑐 + ), ∧ {CommitFoot(𝑜, 𝜔) ∶ Q(𝑜) → C(𝑜), ReturnFoot(𝑜, 𝜔) ∶ R(𝑜) or Q(𝑜) → A(𝑐 + ),

∧ Closed𝑠 ′ (𝑐, 𝜂, 𝜂+ ), ∧ Frame𝑜,𝑐,𝑐 + (𝑠, 𝑠 ′ ). Frame𝑜,𝑐,𝑐 + (𝑠, 𝑠 ′ ) keeps every state component unchanged except the three displayed ownership moves, 𝑜 ’s terminal record/status, 𝑐 ’s closure, creation/current installation of 𝑐 + , and the two displayed write-once decisions. Every branch sets the named outbox’s outcome field exactly to the value fixed by TermRecord and appends exactly its content-addressed audit node. The 𝜋local branch, and no other branch, additionally replaces the outbox dispatch gate by its absorbing local-abort marker. The three moved sets are pairwise disjoint: SafeA𝑠 (𝑐, 𝜂) is available before the action, whereas CommitFoot ⊎ ReturnFoot = 𝑋𝑜 is reserved or quarantined. The commit also persists the canonical 𝐷𝑜 /remainder commitments when 𝜔 = 𝑟 + , marks 𝑜 terminal, closes 𝑐 , and installs 𝑐 + as the active generation for the same slot. Exact replay stutters; a changed witness, partition, epoch,

Fault-Tolerant Budget Conservation in Agent Delegation

27

or successor is rejected. The authority conjunct in Equation (17), together with ReissueTarget, supplies the settlement-authority clause of ReturnTarget for every returned atom without defining either predicate circularly. Reuse is a new ownership transition: under the state-transition predicate in Equation (16), it atomically moves exactly Reusable𝑠 (𝑐, 𝜂, 𝜂+ ) from its proved available records into a fresh sameroot, same-authority, non-widening lineage successor (𝑐 + , 𝜂+ ). It never changes an old C or F record and never reuses an accepted transfer. The gateway rejects a new old-epoch acceptance after the fence while idempotently revealing an outcome that crossed before it. An epoch check only at the budget store is insufficient if a stale worker holds direct receiver credentials. 6.9

Fan-In and Return

A task join has three safe choices: (1) retain separate branch credits and select one for each new effect; (2) atomically join disjoint, operation-free footprints under one authoritative store; or (3) transfer each branch’s remainder through sealed handoffs to a join store, then join after acknowledgment. It may not add reported numeric balances from branches. Each return uses a stable transfer ID and consumes the child footprint. Duplicate completion or return messages stutter. A canceled branch with an indeterminate operation can return only its unaffected available footprint; the obligation remains charged to the root. 6.10

Protocol Adapters

An adapter maps concrete events to abstract transitions:

𝛼 ∶ ConcreteEvent → {Issue, Split, Delegate, AcceptTransfer, CancelTransfer, Reserve, Dispatch, GatewayAccept, EffectOccurs, Settle, Return, Retire, Fence, Reissue, TerminalRollover, Join, stutter}. For MCP, the operation binding travels with the tool call or trusted proxy context. For A2A, a task delegation carries the child credit certificate and the completion record carries the stable operation/transfer IDs. For HTTP, the gateway maps 𝜅 to an idempotency or conditional-write primitive. Protocol authentication can use AIP/AAT or conventional workload identity; the budget protocol does not define a new bearer-token format. An adapter is conforming only if it preserves root, logical slot, credit generation, lineage and footprint commitments, vector and maximum charge, selector schema version, label digests, epoch, canonical operation key, complete acceptance digest 𝛽𝑜 , normalized effect digest, receiver, joint witness, terminal- evidence binding, and terminal committed/remainder footprint commitments. Unknown fields that affect effect semantics fail closed. A textual Agent message never substitutes for a trusted adapter event. 6.11

Stable Decisions and Reason Codes

Every rejection or uncertainty is explicit: 7 Safety Results: Conservation and Recovery This section proves safety for the abstract machine in Section 5 and states the additional obligations needed to lift the results to a concrete implementation. The proofs are prefix properties: they hold after every transition, including prefixes that end at a crash, partition, lost response, or permanently indeterminate effect. They do not assume eventual message delivery.

28

Zhu and Wang

Reason

Meaning

Required response

INSUFFICIENT_ LOCAL_ESCROW LINEAGE_ALIAS STALE_CREDIT_EPOCH

Branch lacks exclusive rights

OPERATION_ BINDING_MISMATCH TERMINAL_EVIDENCE_ BINDING_MISMATCH

Replay changed effect/vector/receiver Success receipt or no-effect certificate does not prove this operation Dispatch may have crossed boundary No authoritative non-acceptance/no-effect proof under the installed fence Concrete event lacks abstract binding

Coordinate transfer or refuse; never read a stale global total Reject and audit Return prior outcome or reject; do not execute Reject as conflicting replay

EFFECT_INDETERMINATE NO_SAFE_RECLAIM_PROOF

ADAPTER_ REFINEMENT_FAILURE

Join inputs overlap Message targets an old generation

Retain reservation and investigate

Keep quarantined; query or forfeit Retain Q or F; settle, or fence and query for proof Fail closed at boundary

Table 3. Stable decisions make conservative failure observable. None of the uncertain cases is silently converted into available budget.

7.1

Proof Setup 𝑎

Write 𝑠 − → 𝑠 ′ when abstract action 𝑎 takes state 𝑠 to 𝑠 ′ , and let Reach be the least set containing the initial state and closed under the transition relation. For a root 𝑔 , resource dimension 𝑘 , and atom 𝑢 ∈ 𝑈𝑔 , define

𝜒𝑔 (𝑢)𝑘 = {

1, 𝑢 = (𝑔, 𝑘, 𝑗) for some 𝑗, 0, otherwise.

For a location class 𝑍 ∈ {A, T, R, Q, C, F}, write 𝒵𝑠 for its raw tagged ownership relation and define Z𝑔 (𝑠) =

∑

𝜒𝑔 (𝑢).

𝑢∈supp(𝒵𝑠 )

This definition does not presume that the six relations are disjoint or total. Distinct competing tags within one relation or a cross-relation overlap remain visible in the candidate multiset Own𝑠 (𝑢) from Section 5; byte-identical storage replicas abstract to one logical relation member. The transition relation treats each stable operation identifier as a single-assignment decision key. Repeating an already accepted request with identical immutable fields is a stutter step; repeating it with different fields is rejected and is also a stutter at the abstract level. A crash before an atomic durable commit is a stutter. A crash after that commit observes the committed successor state. These conventions make crash cuts explicit without assuming that a process executes a multirecord update exactly once. 𝑎

Definition 8 (Atom-pReseRving tRansition). A transition 𝑠 − → 𝑠 ′ is atom preserving for root 𝑔 if there is a set 𝑌 ⊆ 𝑈𝑔 such that

∀𝑢 ∉ 𝑌 ∶ Own𝑠 ′ (𝑢) = Own𝑠 (𝑢),

Fault-Tolerant Budget Conservation in Agent Delegation

29

and, for each 𝑢 ∈ 𝑌 , the action guard requires Own𝑠 (𝑢) = {ℓsrc } and the authoritative commit atomically removes that source pair and inserts exactly one permitted destination pair. It neither duplicates nor deletes an input atom. Every non-issuance action in the abstract machine is atom preserving. Split, Join, ordinary successor-generation issuance, and TerminalRollover change the credit tag inside 𝒜; Delegate, acceptance, and cancellation move atoms A → T → A; Reserve, Dispatch, Settle, Return, and Retire move atoms among the six bucket classes. TerminalRollover additionally applies one terminal partition while installing the successor, but its moved footprints are disjoint. Fence changes an epoch but not an ownership relation. Later evidence for a forfeited operation annotates its outcome while F(𝑜) remains absorbing. 7.2

Unique Ownership and Exact Conservation

Lemma 1 (OwneRship-paRtition pReseRvation). Under Assumptions 1–3, every reachable state 𝑠 ∈ Reach has exactly one raw ownership tag for each 𝑢 ∈ 𝑈𝑔 :

∀𝑔 ∀𝑢 ∈ 𝑈𝑔 ,

|Own𝑠 (𝑢)| = 1.

PRoof. We induct on the length of the execution prefix. At issuance, authenticated root uniqueness gives one 𝑈𝑔 , and Issue assigns every atom in it to the root credit. Thus the property holds initially. 𝑎

Assume it holds in 𝑠 . Consider 𝑠 − → 𝑠 ′ . A rejected, duplicate, or pre-commit-crash action stutters, so the induction hypothesis applies directly. For a committed action, Assumption 2 excludes a visible state containing only a proper subset of its local moves, while the protocol guard checks that every input has a singleton source tag. Stable local decision keys and the transfer decision register in Assumption 3 prevent replay or competing terminal decisions from applying a second move. Each transition is atom preserving:

• Split removes pairwise-disjoint 𝑋𝑖 from one parent before assigning each 𝑋𝑖 to one child. No atom is in two 𝑋𝑖 . • A delegation seal removes each source pair and inserts one T(𝑥) pair. Acceptance and cancellation compete on the monotone register in Equation (5). An accepted decision completes the uniquely named destination import; a cancelled decision restores the source. Neither terminal value enables the other, and a pending transfer remains solely in T. • Reserve and Dispatch respectively relabel A(𝑐) as R(𝑜) and R(𝑜) as Q(𝑜). • Successful Settle partitions 𝑋𝑜 into the disjoint, version-determined footprints 𝐷𝑜 = Take𝜈sel (𝑋𝑜 , d𝑟 + ) and 𝑋𝑜 ∖ 𝐷𝑜 , assigning the former to C(𝑜) and the latter, when nonempty, to the one decision-bound available credit satisfying Equation (7). Verified abort and retirement each select exactly one successor for every input atom; outcome annotation after retirement changes no ownership relation. • TerminalRollover partitions the final operation into the disjoint CommitFoot(𝑜, 𝜔) and ReturnFoot(𝑜, 𝜔). These are disjoint from SafeA𝑠 (𝑐, 𝜂), whose atoms are available before the action. Equation (18) sends every atom in the three sets to exactly one of C(𝑜) or A(𝑐 + ) in the same authoritative commit. • An admissible Join consumes all pairwise-disjoint input footprints in one authoritative action, then assigns their union to one output credit. • Fence, gateway acceptance, effect occurrence, and evidence annotation do not change an ownership relation. Successor-generation issuance moves only the singleton available atoms in Reusable𝑠 (𝑐, 𝜂, 𝜂+ ) to one fresh available tag satisfying Equation (16).

30

Zhu and Wang

Hence each changed atom loses exactly one source tag and gains exactly one destination tag in the same abstract commit, while all other candidate multisets are unchanged. The property therefore holds in 𝑠 ′ . Only now is loc𝑠 (𝑢) well-defined as the unique element of Own𝑠 (𝑢); uniqueness was not supplied by a function type. □ TheoRem 1 (Exact peR-Root vectoR conseRvation). Under Assumptions 1–3, every reachable state and every root grant satisfy, componentwise, A𝑔 (𝑠) + T𝑔 (𝑠) + R𝑔 (𝑠) + Q𝑔 (𝑠) + C𝑔 (𝑠) + F𝑔 (𝑠) = B𝑔 . All six vectors remain in ℕ|𝒦| . PRoof. Fix 𝑔 and 𝑘 . By Lemma 1, every atom (𝑔, 𝑘, 𝑗) ∈ 𝑈𝑔 contributes exactly one to exactly one of the six bucket coordinates. There are 𝐵𝑔,𝑘 such atoms by Definition 1. Summing their indicators gives 𝐴𝑔,𝑘 + 𝑇𝑔,𝑘 + 𝑅𝑔,𝑘 + 𝑄𝑔,𝑘 + 𝐶𝑔,𝑘 + 𝐹𝑔,𝑘 = 𝐵𝑔,𝑘 . The argument holds independently for every 𝑘 . Each coordinate is a cardinality and is therefore a non-negative integer. Notice that the proof does not require a terminal response: an unresolved dispatch contributes to Q𝑔 , and permanently stranded authority contributes to F𝑔 . □ CoRollaRy 1 (No minting by RetRy, RecoveRy, oR join). Under Assumptions 1–3, no finite sequence of duplicate messages, process restarts, reconciliations, or lineage-disjoint joins can increase the sum of spendable and obligated capacity for a root beyond B𝑔 . PRoof. Retries and recovery actions are either stutters or atom-preserving moves. Joins union disjoint footprints after consuming their inputs. Theorem 1 therefore applies to every resulting prefix. □ 7.3

Lineage and Descendant Non-Amplification

For the next results, define the responsible lineage of an atom to be the credit lineage that currently holds it or the lineage embedded in its transfer or operation binding. Terminal locations retain that binding; a committed or forfeited atom does not lose provenance merely because it is no longer spendable. Lemma 2 (Lineage pRovenance). Under Assumptions 1–3, for every reachable state, the responsible lineage of each 𝑢 ∈ 𝑈𝑔 contains a path from the unique root credit to its current credit, transfer, or operation. Along that path the atom is moved, never copied, and every descendant label applicable to 𝑢 restricts its ancestor labels. PRoof. The root path is trivial after Issue. Induct on transitions. Split adds one parent edge for each moved atom; pairwise disjointness selects one child. Delegate records the source generation in its sealed certificate, and destination acceptance creates one child from that certificate. Reserve copies the credit identifier, epoch, and label binding into the operation while moving the atom out of availability. Dispatch, Retire, and reconciliation preserve that operation binding. Settle and Return can place a returned atom only in a same-root successor that is current at the atomic commit and satisfies Equation (7); cross-store or ancestor return must use a later sealed transfer. Ordinary Reissue creates only the authenticated same-root, same-authority successor in Equation (16), with 𝜆𝑐 + ⊑ 𝜆𝑐 . TerminalRollover records that same authenticated reissue edge atomically with the final terminal decision: committed atoms end at 𝑜 , while every returned atom and every atom in the predecessor’s disjoint SafeA footprint has the unique predecessor 𝑐 and ends at 𝑐 + . An admissible Join requires all inputs and its output to have the same root and records all input generations

Fault-Tolerant Budget Conservation in Agent Delegation

31

but, because their footprints are disjoint, each individual atom has exactly one input predecessor. Assumption 1 prevents a forged predecessor; Lemma 1 and the singleton source guard prevent a second owner. Equations (3) and (7) supply label restriction at every lineage-creating or return step. Transitivity of ⊑ gives restriction against all applicable ancestors. □ Fix a finite execution prefix 𝜌 ending in state 𝑠 and a single-root credit sub-DAG 𝑊 . Call 𝑊 credit-cut closed along 𝜌 when every authoritative ownership event that moves responsibility for an atom from a lineage outside 𝑊 to one inside 𝑊 appends the exact moved footprint to a monotone authenticated ingress history. Such events include cross-cut split outputs, accepted sealed transfers, returned remainders and verified aborts, successor reissues, and every outside input consumed by a join. A task-dependency edge or balance report alone is not an ingress. Let In𝜌 (𝑊 ) be the set union of those event footprints, deduplicated by atom identity if the same right later re-enters, and let Held𝑠 (𝑊 ) be the atoms whose current available, reserved, indeterminate, committed, or forfeited responsibility lies in 𝑊 ; atoms sealed for transfer out of 𝑊 are excluded. TheoRem 2 (Descendant non-amplification). Under Assumptions 1–3, for every finite execution prefix 𝜌 ending in reachable state 𝑠 and every sub-DAG 𝑊 that is credit-cut closed along 𝜌 , Held𝑠 (𝑊 ) ⊆ In𝜌 (𝑊 ),

vec(Held𝑠 (𝑊 )) ⪯ vec(In𝜌 (𝑊 )).

If 𝑊 contains the root credit, take In𝜌 (𝑊 ) = 𝑈𝑔 . PRoof. Induct on the transitions of 𝜌 , reasoning per atom. Initially a non-root 𝑊 holds no atom, whereas a root-containing 𝑊 holds a subset of 𝑈𝑔 . A transition whose source and destination responsible lineages are both inside 𝑊 merely relabels the atom. A transition to a lineage outside 𝑊 , including an egress seal, removes it from Held(𝑊 ). A transition from outside to inside can add only an atom in its exact authenticated footprint; credit-cut closure appends that footprint to the history defining In𝜌 (𝑊 ) in the same logical move. This case covers cross-cut split, transfer, return, ordinary reissue, TerminalRollover, and join rather than assuming any of them is internal. Transitions on the outside and stable decision replays do not change either side; the latter stutter because their decision keys are unique. Lemma 1 excludes a second simultaneous owner in every case. Hence the set inclusion is preserved. Applying vec, which is monotone under set inclusion, gives the componentwise inequality. □ The theorem is deliberately about the credit-lineage DAG, not the task DAG. Adding a dependency edge, reference, model message, or shared specialist does not change In𝜌 (𝑊 ) and therefore grants no capacity. 7.4

Stable Settlement and Continuous Effect Coverage

Lemma 3 (TeRminal-decision stability). Under Assumptions 2, 3, and 7, for any operation 𝑜 , at most one terminal settlement decision can change ownership of 𝑋𝑜 . After that decision, an identical evidence item is a stutter and conflicting terminal evidence is rejected. PRoof. The operation row and its terminal-decision key are updated in the same local transaction as the ownership move. By Assumption 2, two concurrent settlement attempts are serialized: the first committed attempt either records a terminal decision or leaves the old state unchanged. Every later attempt observes that decision. An identical witness returns the recorded result; any byte-distinct witness conflicts with the stored TermRecord digest and is rejected before an ownership move. Before a first decision can be created, an external variant must pass its typematched Verifyterm verifier and a local variant must pass Verifylocal (𝜋local , 𝑜, 𝑠, 𝑠 ′ ); the closed sum admits no unverified fourth case. TerminalRollover uses this same operation terminal-decision key

32

Zhu and Wang

while atomically adding the independent normalized reissue decision; it is not a second settlement namespace. A crash before the first commit leaves no ownership move; a crash after it leaves the terminal key and ownership move together. Consequently there is no reachable prefix in which two terminal settlement transitions both move 𝑋𝑜 . □ TheoRem 3 (At-most-once authoRitative settlement). Under Assumptions 1, 2, 3, 5, and 7, each canonical operation key 𝜅𝑜 has at most one non-conflicting authoritative outcome, and its charged footprint is applied to C𝑔 at most once. PRoof. Assumption 5 maps all gateway retries under 𝜅𝑜 to one logical receiver outcome. Assumption 7 binds either admissible evidence variant to 𝑜𝑖𝑑 , 𝜅𝑜 , the complete acceptance digest 𝛽𝑜 , root, logical slot, lineage, epoch, effect digest, and receiver. A success receipt additionally binds the instance and charge; a no-effect certificate instead binds the higher installed fence for the same logical slot and is mutually exclusive with success. Lemma 3 allows at most one variant to move ownership. Thus the canonical footprint 𝐷𝑜 = Take𝜈sel (𝑋𝑜 , d𝑟 + ) enters C(𝑜) at most once. Network messages and responses may be delivered more than once; the theorem concerns authoritative settlement, not exactly-once transport. □ Lemma 4 (Ambiguity Remains chaRged). Suppose Dispatch(𝑜) has committed. Every atom of 𝑋𝑜 remains in Q(𝑜) until Settle, Return, Retire, or the corresponding terminal branch of TerminalRollover. Before authenticated successful or verified-no-effect terminal evidence, it is either retained in Q(𝑜) or conservatively moved to absorbing F(𝑜). A timeout, process death, lease expiry, partition, missing response, or epoch increment alone cannot move any atom of 𝑋𝑜 to A. PRoof. After the durable dispatch cut, the abstract location is Q(𝑜). Inspecting the transition relation, only Settle, Return, Retire, and TerminalRollover can remove an atom from that location. Authenticated successful settlement partitions it into C and an authenticated remainder in A; a fenced verified-no-effect decision returns it to A; retirement moves it to F. The corresponding TerminalRollover branches apply exactly the same terminal partitions while atomically installing a successor. Nonterminal reconciliation observations stutter. Timeout, failure suspicion, and lease expiry are not ownership transitions. Fence changes only the accepted epoch. Therefore ambiguity cannot create available capacity. □ TheoRem 4 (Continuous injective coveRage of mediated effect instances). Under Assumptions 1, 2, 3, 4, 5, 6, 7, and 9, every reachable state satisfies

∀𝜄 ∈ Obs(𝑠),

∃! 𝑜 ∈ 𝒪 ∶ Covered(𝜄, 𝑜, 𝑠),

and no one-effect-profile operation covers two distinct instances. PRoof. Induct on abstract transitions, treating Obs as a monotone state variable. Initially it is empty. Only EffectOccurs(𝑜, 𝜄) can append an instance. Its guard requires a prior gateway acceptance of the immutable digest 𝛽𝑜 in Equation (6), together with 𝜅𝑜 . On first acceptance, the action guard requires a matching durable dispatchable marker and the full footprint in Q(𝑜), or conservatively in F(𝑜) after retirement. An exact replay after a later terminal move reads the existing accepted register and stutters; it cannot create a new acceptance. The accepted witness also establishes RequiredCap(𝑒, 𝜒 ) ⪯ u𝑜 , and the (𝑔, 𝜒𝑐 ) committed inside 𝛽𝑜 selects the corresponding current-generation register and gateway fence. Thus the three non-recursive clauses of Covered(𝜄, 𝑜, 𝑠) hold when 𝜄 is appended. Assumption 5 allocates a fresh 𝑖𝑖𝑑 and acceptance sequence to at most one instance for the receiver-scoped key. The canonical domain-separated derivation of 𝜅 , stable operation decision, and immutable binding prevent a different operation from acquiring that key within the stated

Fault-Tolerant Budget Conservation in Agent Delegation

33

collision-resistance assumption; the one-effect guard prevents the same operation from appending a second instance. This proves both directions of injectivity. Two separate operations may still request byte-identical descriptors; their keys and 𝑖𝑖𝑑 values make them distinct budgeted instances. Subsequent ownership actions preserve coverage. Before terminal evidence, Lemma 4 retains all of 𝑋𝑜 in Q, or Retire moves it wholly to absorbing F. A complete committed receipt identifies the unique 𝜄 , moves the version-determined footprint

𝐷𝑜 = Take𝜈sel (𝑋𝑜 , ActualCharge(𝜄)) to C, and returns only the complement to a target satisfying Equation (7). A verified-no-effect return is disabled after gateway acceptance linearizes by terminal-evidence non-equivocation and the non-acceptance premise of Assumption 7. If TerminalRollover is applied to an operation covering 𝜄 , its ValidTerminal evidence can therefore only be that same complete success receipt: the no-effect branch contradicts prior acceptance and the local-abort branch contradicts durable dispatch. Equation (18) moves the same 𝐷𝑜 to C, moves only its complement to the successor, and moves the predecessor’s disjoint SafeA footprint without changing 𝑜 ’s coverage. Evidence arriving after retirement annotates the record without moving F; the operation remains in Risk𝑔 at its maximum rather than entering Settled𝑔 . All other transitions preserve 𝛽𝑜 and Obs. Hence coverage and injectivity hold for every prefix. □ TheoRem 5 (Root-bounded mediated exteRnal exposuRe). Under the assumptions of Theorem 4, every reachable state satisfies Equation (11):

∑ 𝜄∈Settled𝑔 (𝑠)

ActualCharge(𝜄) +

∑

u𝑜 ⪯ C𝑔 (𝑠) + Q𝑔 (𝑠) + F𝑔 (𝑠) ⪯ B𝑔 .

𝑜∈Risk𝑔 (𝑠)

PRoof. For every settled instance, success-receipt completeness gives the distinct charged footprint 𝐷𝑜 = Take𝜈sel (𝑋𝑜 , ActualCharge(𝜄)) in 𝒞𝑠 . For every risk operation, irrespective of a later evidence annotation, its entire maximum footprint 𝑋𝑜 is present in 𝒬𝑠 or ℱ𝑠 , so u𝑜 = vec(𝑋𝑜 ). By definition an F-resident late success is counted only in this second, conservative term. The coverage injectivity theorem and ownership partition make all of these charged and at-risk footprints pairwise disjoint; no atom contributes to both sums. Their vector sum is therefore bounded by the raw supports of 𝒞𝑠 , 𝒬𝑠 , ℱ𝑠 . Exact conservation and non-negativity then give C𝑔 + Q𝑔 + F𝑔 ⪯ B𝑔 . The first sum reports actual settled charge; the second deliberately charges uncertainty and forfeiture at their enforced maxima. □ 7.5

Epoch Fencing, Late Completion, and Safe Reclaim

Lemma 5 (No stale ResuRRection). Under Assumptions 1, 2, and 5, if the authoritative epoch for credit 𝑐 advances from 𝜂 to 𝜂′ > 𝜂, no later transition can make 𝜂 current again, and no new protected effect under (𝑐, 𝜂) is accepted after the corresponding gateway fence is installed. PRoof. Epoch updates are strictly increasing by the Fence precondition, so the credit authority cannot restore 𝜂. Assumption 5 requires the protected gateway to compare an incoming generation against the installed fence. It either rejects a previously unseen stale request or returns the outcome already recorded for its stable key. Neither behavior creates a new old-epoch effect. Reordered or replayed messages do not alter the monotone fence. □ TheoRem 6 (Late-completion safety). Assume 1, 2, 3, 4, 5, 7, and 9. Let a mediated operation 𝑜 be dispatched under epoch 𝜂, let its caller time out, and let a controller later install an authoritative successor epoch 𝜂+ > 𝜂. If GatewayAccept(𝑜) linearized before the fence, all of 𝑋𝑜 remains charged in Q(𝑜) or F(𝑜) until complete terminal evidence. A pre-retirement success moves its exact actual-charge

34

Zhu and Wang

footprint 𝐷𝑜 to C(𝑜); only its authenticated complement may return to A, after the same terminal decision excludes any further instance or charge under the old binding. A post-retirement result leaves all of 𝑋𝑜 in absorbing F(𝑜). If no acceptance linearized before the fence, the gateway cannot newly accept the old epoch afterward. Consequently neither ordinary generation closure and successor issuance under Equations (14)–(16) nor fused terminal rollover under Equations (17)–(18) can make one atom simultaneously fund a late old-epoch effect and a new-generation effect. PRoof. There are two cases. Acceptance linearized before the fence. Its reservation was already in Q(𝑜) by the durablebefore-exposure order. Timeout and epoch advance do not refund it by Lemma 4. A complete pre-retirement success moves 𝐷𝑜 = Take𝜈sel (𝑋𝑜 , d𝑟 + ) permanently to C(𝑜) and may return 𝑋𝑜 ∖ 𝐷𝑜 only in the same write-once terminal decision. Receipt completeness and the one-effect gateway rule then prohibit a later instance or additional charge under (𝜅𝑜 , 𝛽𝑜 ), so no returned complement atom funds the old effect. If retirement commits first, F remains absorbing and late evidence only annotates it; otherwise the unresolved footprint stays in Q(𝑜). Assumption 7 disables a verified-no-effect return after acceptance has linearized, and a fence does not cancel that acceptance. No acceptance linearized before the fence. Lemma 5 disables a new old-epoch acceptance, so no protected effect can arise from that binding. If a retry instead observes a previously recorded acceptance or result, the premise of this case is false and the execution belongs to the first case. Equation (14) closes the old generation only after the fence is installed, every transfer decision is terminal, and every old operation is committed, verified-aborted, or forfeited. Equation (15) then selects only uniquely available, retained-provenance atoms. Committed and forfeited atoms, and atoms carried by accepted transfers, are excluded. For the dispatched operation in this theorem, a verified-aborted atom is selectable only with an authoritative no-effect certificate protected by the same fence; an authenticated success remainder is selectable only after its exact charged complement and complete single-instance terminal result are fixed. An ordinary successor-generation action moves, rather than copies, that exact set under the normalized write-once reissue decision. When the last terminal decision and successor installation are fused, Equations (17)– (18) establish the same facts atomically: the canonical committed and return footprints partition 𝑋𝑜 , both are disjoint from the predecessor’s SafeA footprint, and exactly the return and SafeA atoms move to the normalized same-slot successor. Therefore a reclaimed atom can neither be in 𝐷𝑜 nor later acquire charge under the old binding, and no atom can fund effects in both generations. □ CoRollaRy 2 (FailuRe suspicion is neveR a Refund pRoof). Replacing the terminal-evidence premises in Equations (14)–(15) or (17)–(18) with a timeout, worker lease expiry, or controller failure detector invalidates Theorem 6. PRoof. In an asynchronous system, an observer cannot distinguish an unexecuted request from an executed request whose response is delayed. Refund in the latter execution makes the same atoms available while the effect exists. The gateway fence and authoritative outcome are therefore proof obligations, not implementation conveniences. □ 7.6

Partition Confinement and the Coordination Boundary

TheoRem 7 (PaRtition confinement). Under Assumptions 1–3, consider a network partition that separates credit authorities into components 𝑃1 , … , 𝑃𝑚 at state 𝑠𝑐 . For each fixed root 𝑔 , define the component-held footprint 𝑔

Held𝑠 (𝑃𝑖 ) = {𝑢 ∈ 𝑈𝑔 ∣ 𝑢 ’s current A/R/Q/C/F responsible authority is in 𝑃𝑖 }.

Fault-Tolerant Budget Conservation in Agent Delegation

35

Pending T atoms are excluded from this set and assigned separately to their unique source component below. Define 𝑔

𝑔

𝐸𝑖 = Held𝑠𝑐 (𝑃𝑖 ) ∪

⋃

𝑋𝑥 ,

𝑥∶𝛿𝑠𝑐 [𝑥]=pending src(𝑥)∈𝑃𝑖 , 𝑋𝑥 ⊆𝑈𝑔

with set union by atom identity. An already accepted transfer is owned by its destination and a cancelled transfer by its source; only a pending transfer is charged to its source component for this cut accounting. If no cross-cut transfer is accepted during the partition, then for every prefix during that partition, 𝑔

𝑔

Held𝑠 (𝑃𝑖 ) ⊆ 𝐸𝑖

and

𝑔

∑ vec(Held𝑠 (𝑃𝑖 )) ⪯ B𝑔 . 𝑖

In particular, a component can progress locally from its own available escrow but cannot spend a right assigned to another component. 𝑔

PRoof. The 𝐸𝑖 are pairwise disjoint by ownership partition and the unique pending-transfer source. Induct over partition-time transitions. Local split, reserve, dispatch, settlement, retirement, return, ordinary reissue, TerminalRollover, or same-root join only relabels root-𝑔 atoms already in 𝑔 𝐸𝑖 . A pending local transfer can accept within the same component; a pending cross-cut transfer 𝑔 either stays in T or cancels back to its source 𝐸𝑖 , because cross-cut acceptance is excluded by premise. Stable replays stutter, and a message reporting a remote balance is not a credit transition. 𝑔 𝑔 𝑔 Thus Held𝑠 (𝑃𝑖 ) ⊆ 𝐸𝑖 throughout. Disjointness and ⋃𝑖 𝐸𝑖 ⊆ 𝑈𝑔 yield the aggregate inequality. A component that exhausts its local A must wait, reconcile, or refuse; safety does not imply continued availability. □ PRoposition 1 (Unallocated-unit impossibility). In an asynchronous system with a possible partition, no protocol can simultaneously guarantee both: (1) local availability: either of two isolated branches must approve a request to spend the same currently unallocated unit using only its local state; and (2) global conservation: across all executions, at most one protected effect may consume that unit. This holds even with crash-free branches and reliable local storage. PRoof. Let branches 𝑝 and 𝑞 have identical knowledge that one shared unit remains, then partition them before either receives another message. Consider execution 𝐸𝑝 , in which only 𝑝 receives a spend request. Local availability requires 𝑝 to approve. Symmetrically, in execution 𝐸𝑞 , in which only 𝑞 receives a request, 𝑞 must approve. Now construct 𝐸𝑝𝑞 , in which both receive their requests during the same partition. Up to its decision, 𝑝 ’s local history in 𝐸𝑝𝑞 is indistinguishable from its history in 𝐸𝑝 , so it approves. Likewise 𝑞 ’s history is indistinguishable from 𝐸𝑞 , so it approves. Two effects consume one unit, contradicting global conservation. Randomization cannot provide a universal safety guarantee: any coin outcomes that permit the respective one-sided approvals form an execution in which both approve. Exclusive preallocation avoids the contradiction by falsifying the first premise: at most one partition has the right to approve that unit. It provides availability for preallocated escrow, not for a shared unallocated remainder. □ 7.7

Concrete Refinement Obligations

Let Σ be the concrete state of branch databases, outboxes, gateway records, terminal-evidence stores, and epoch authorities. Let Rep(Σ, 𝑠) be a representation relation requiring:

36

Zhu and Wang

(1) each durable concrete credit, transfer, and operation maps to the corresponding abstract object with equal root, logical slot, lineage, label, epoch, vector, and immutable identifiers; (2) each sealed transfer has exactly one logical owner location; its monotone accept/cancel decision and crash finalization map to the same abstract transfer decision rather than a second import or restoration; (3) each committed database transaction maps to one abstract transition, including a fused terminal-decision-plus-successor transaction mapping to TerminalRollover, and each uncommitted or duplicate event maps to stutter; (4) each concrete operation phase and write-once terminal-decision key agree with its abstract R/Q/C/F ownership; its selector schema and exact committed/remainder footprint commitments agree with the abstract deterministic partition and disable every conflicting terminal move; (5) gateway observations and terminal evidence map to the normalized effect and operation named by their acceptance digest 𝛽𝑜 , and concrete acceptance/fence records preserve the bound logical slot and their authoritative linearization order; (6) every concrete remainder or no-effect return maps to a same-root, current-at-commit, sameauthority, label-non-widening target satisfying Equation (7); (7) every ordinary successor-generation issuance carries a concrete Closed proof and moves exactly the concrete image of Reusable, excluding committed, forfeited, accepted, and unresolved rights, into the sole target selected by its write-once reissue decision and satisfying Equation (16); the decision, current-generation metadata, and ownership move commit atomically; (8) every fused final terminal decision and successor installation maps to TerminalRollover: it satisfies Equations (17)–(18), persists the canonical terminal partition and normalized reissue decision, and moves only the disjoint terminal-return and SafeA footprints to the same-slot successor; and (9) compressed footprints map injectively to logical rights, preserve disjointness, and have concrete sums equal to the abstract vec of their atom sets. For paired finite prefixes 𝜌̂ = (Σ0 , … , Σ𝑛 ) and 𝜌 = (𝑠0 , … , 𝑠𝑛 ), define Rep∗ (𝜌,̂ 𝜌) to require: (i) Rep(Σ𝑖 , 𝑠𝑖 ) for every 𝑖; (ii) every concrete authenticated cross-cut ingress event maps one-for-one to the corresponding abstract event with the same exact footprint and atom-identity deduplication, while task edges and balance reports map to no ingress; and (iii), for any partition-confinement claim, the paired prefixes preserve the cut state and interval, authority-to-component assignment, pending-transfer source component, and the predicate that no cross-cut acceptance commits during the interval. Conditions (ii)–(iii) are the prefix-faithfulness obligation on 𝛼 . TheoRem 8 (Conditional tRace-lifting cRiteRion). Under Assumptions 2 and 8, a concrete runtime inherits the abstract safety results if it discharges the initial-state, stepwise, and prefix-faithfulness obligations: Rep(Σ0 , 𝑠0 ) and, for every concrete step Σ → Σ′ and every abstract state 𝑠 , 𝛼(Σ,Σ′ )

Rep(Σ, 𝑠) ⟹ ∃𝑠 ′ . ([𝑠 ′ = 𝑠 ∧ 𝛼(Σ, Σ′ ) = stutter] ∨ [𝑠 −−−−−−→ 𝑠 ′ ]) ∧ Rep(Σ′ , 𝑠 ′ ).

(19)

The disjunction denotes either one enabled abstract action with the same immutable binding or a stutter step. If these obligations hold, then for every finite concrete execution

Σ0 → Σ1 → ⋯ → Σ𝑛

Fault-Tolerant Budget Conservation in Agent Delegation

37

there exists an abstract execution 𝛼1

𝛼2

𝛼𝑛

𝑠0 −−→ 𝑠1 −−→ ⋯ −−→ 𝑠𝑛 stutter

such that Rep∗ ((Σ0 , … , Σ𝑛 ), (𝑠0 , … , 𝑠𝑛 )). Here 𝑠 −−−−−→ 𝑠 denotes the explicit abstract self-loop used for the first disjunct. PRoof. Induct on 𝑖. The initial obligation supplies the base case. Applying Equation (19) to each concrete successor supplies either a matching enabled abstract action or a stutter and preserves Rep. Concatenating those witnesses yields the abstract execution and pointwise clause (i) of Rep∗ ; prefix faithfulness supplies clauses (ii)–(iii). □ The theorem states the exact criterion a concrete runtime must satisfy. A production implementation establishes Equation (19) handler by handler, including transfer accept/cancel, 𝑊2 /𝑊3 /𝑊4 crash cuts, gateway acceptance versus fencing, effect occurrence, ordinary successor-generation issuance, and TerminalRollover. The artifact exercises bounded and concrete traces against these obligations; finite trace agreement does not replace a universal implementation refinement proof. The SQLite research profile implements and tests the online first-acceptance guard through a branch-signed 𝑊3 permit, including missing, forged, stale, crash-recovered, and proof-excluded cases. This supports the evaluated profile’s guard while leaving the universal adapter obligation and conditional end-to-end theorem subject to a complete handler-level refinement argument. TheoRem 9 (Conditional end-to-end dual conseRvation). If Assumptions 1–9 hold and the concrete runtime satisfies the trace-lifting obligations of Theorem 8, then every finite concrete execution prefix 𝜌̂ has a lifted abstract prefix 𝜌 for which the following properties hold and reflect back to 𝜌̂ under the stated theorem-specific premises: (1) exact per-root vector conservation as in Equation (8); (2) for every sub-DAG 𝑊 that is credit-cut closed along the lifted prefix 𝜌 , descendant nonamplification as in Equation (12); (3) at-most-once authoritative settlement per canonical operation; (4) unique continuous coverage for every gateway-observed protected effect as in Equation (9); (5) settled actual charge plus conservative outstanding exposure bounded by the issued vector as in Equation (11); (6) for every dispatched operation closed and reissued either ordinarily under Equations (14)–(15) or atomically under Equations (17)–(18), no old-epoch effect funded by capacity safely reclaimed into a new generation; and (7) during every partition interval with no accepted cross-cut transfer, partition-local spending bounded by the exclusive escrow assigned at the cut. PRoof. Theorem 8 maps the concrete prefix to a reachable abstract prefix. Apply Theorems 1, 2, 3, 4, 5, 6, and 7 to that abstract prefix whenever their explicit sub-DAG, dispatched-operation, and partition-interval premises hold. The representation relation preserves the identifiers, selector version, footprint vectors and terminal partition commitments, epochs, effects, and terminal-evidence bindings mentioned by those properties, so each property transfers back to the concrete state. □ 7.8

Assumption–Conclusion Boundary

Table 4 records the proof surface. “Required” means that the result as stated uses the assumption; it does not mean that every deployment must implement that assumption in the same way.

38 Result Ownership partition and exact conservation

Zhu and Wang Required assumptions / premises

Authenticated unique roots/credits (Assumption 1); atomic durable moves (2); singleton-source guards and stable decision keys (3) Semantic and Root/lineage authenticity; descendant exclusive transfer; label non-amplification attenuation and credit-cut accounting At-most-once Atomic terminal-decision key; settlement immutable operation binding; sound tagged terminal evidence; receiver-scoped gateway idempotency Effect coverage and Authenticated binding, atomic external exposure durable ownership, and stable bound decisions (1–3); persist-before-exposure; sound normalization (4); enforced maximum-charge contract (6); fenced queryable gateway (5); complete non-equivocating terminal evidence (7); complete mediation (9) Late-completion safety Durable R → Q cut; and reclaim gateway-visible monotone epoch; authoritative success/no-effect result Partition confinement Exclusive preallocation before the cut; no unfenced cross-cut acceptance Conditional concrete Adapter preservation end-to-end result (Assumption 8), a handler-by-handler proof of Equation (19), plus the assumptions of each selected abstract result

Failure if omitted

Not concluded

Forged issuance, torn moves, or copied inputs can duplicate or lose atoms

Fair allocation, low stranding, or timely completion

A numeric balance may remain bounded while purpose, audience, or ancestry widens

Correctness of the policy classifier or optimal task decomposition

Duplicate or conflicting evidence can move the same reservation twice, or one transport retry can create multiple logical outcomes

Exactly-once delivery or honesty of an arbitrary third-party receiver

An effect can bypass its obligation, alias another effect identity, or be refunded on a false result

Coverage of covert, direct-credential, or otherwise unmediated effects

Timeout refund or store-only fencing permits old and new generations to use one right

Rollback of an irreversible effect or eventual recovery of stranded rights

Disconnected branches may spend the same cached remainder

Availability after local escrow is exhausted

Concrete fields, write order, or protocol keys may fail to implement the abstract move proved safe

Byzantine storage/gateway tolerance, production SLOs, or model-task quality

Table 4. Assumption–conclusion boundary for the safety results. Ledger integrity alone does not establish external-effect conservation; the latter requires normalization, complete mediation, and a terminal-evidenceproducing fenced gateway.

7.9 What the Theorems Permit The results intentionally permit conservative outcomes. A right may remain in T𝑔 because a transfer cannot be canceled safely, in Q𝑔 because the receiver outcome is unknown, or in F𝑔 because an administrator retires unresolved authority. Such states reduce utilization but preserve the exact equation and keep potential effects covered. The theorems also permit coordination during rebalancing, fan-in, and reclaim. Proposition 1 shows why removing that coordination while retaining universal partition availability would change, rather than strengthen, the safety contract. Conversely, a perfectly conserved internal ledger does not prove that a provider reported the true cost, that two protocol encodings normalize to the same effect, or that an agent lacked a bypass credential. Those are precisely the boundaries isolated by Assumptions 4, 7, and 9. The artifact therefore tests state-machine invariants and terminal-evidence contracts as separate evidence layers. Adapter conformance remains a handler-level trace-lifting obligation; passing either tested layer is not reported as evidence for that obligation.

Fault-Tolerant Budget Conservation in Agent Delegation

39

cancel decision

Available Asrc source owns

seal

Transit T sealed handoff

accept decision

Available Acurrent accepted owner

tim

eou

t re

fun

d fo

Committed C receipt settled

rbid

den

success: actual 𝐷𝑜

reserve expose

Quarantined Q effect may exist

r

Reserved R durable, unexposed

ess:

rem a

inde

local reserve

succ

retire

Available Areturn decision-bound target

t:

ec eff

l al

𝑋𝑜

Forfeited F never reusable

-

ed

c en

no

f

late evidence annotates

Fig. 3. Per-right lifecycle. A timeout can trigger reconciliation but never changes ownership. Only an authenticated settlement or a fenced proof of non-execution releases a quarantined right. A success receipt canonically partitions 𝑋𝑜 : 𝐷𝑜 commits, while 𝑋𝑜 ∖ 𝐷𝑜 moves to the separate decision-bound ReturnTarget box. A fenced no-effect proof moves all 𝑋𝑜 to that box along a distinct dashed path. Separate source, currentowner, and return-target boxes prevent the three ownership roles from being visually conflated.

8 Reference Architecture and Implementation Boundary The abstract machine is intentionally independent of a database, transport, agent framework, or model provider. This section gives a reference profile that is implementable without weakening the proof obligations. It is not a claim that any ordinary message queue or API automatically satisfies those obligations. 8.1

Lifecycle Realization

Figure 3 realizes one logical right as a state machine. Solid arrows show ordinary ownership progress, including both branches of an authenticated success receipt. Dashed arrows specifically denote exclusion/no-effect or reversal evidence; they are not a legend for every authenticated record. There is deliberately no timeout edge from Q to A. The F bucket is absorbing; later evidence may annotate its outcome but cannot reclassify or make it spendable. 8.2

Durable Records

The reference architecture requires an authoritative local store per branch. The store may itself be replicated, provided that a successful local transaction is linearizable and durable under Assumption 2. Table 5 gives the minimum logical records. Fields shown as immutable participate in a canonical digest; mutable phase fields are updated only by the transition that owns them. SQLite executable binding. Table 5 is a logical schema, not a claim that every field is a literal standalone SQL column. In the compact profile, the representation map encodes the absorbing local gate as operations.state = aborted, abort_mode = local_unexposed, and outbox.dispatchable = 0. The only dispatch CAS requires the operation still be reserved, so this product state cannot later become dispatchable. The 𝑊3 CAS simultaneously records the permit authority, domain-separated permit identifier, digest, and Ed25519 signature; no dispatchable row can have a partial permit. The logical terminaloutcome digest is reconstructed from the terminal operation/evidence row by the independent checker rather than stored as a separate outbox column.

40

Zhu and Wang

Record

Immutable identity/binding

Mutable state

Uniqueness or integrity rule

root_grant

root, issuer, resource schema, issued vector, label digest root, logical slot/reissue-chain ID, credit ID, parent credit ID, generation, epoch, issuer, credit authority/owner, source-label digest, lineage and rights commitments

status, current policy version, installed fence epochs available ranges, lifecycle, current marker

root, transfer ID, source generation, destination, ranges, label root, logical slot, operation ID, source lineage/rights commitments, epoch, effect digest, receiver, key, 𝛽𝑜 , maximum vector, source/operation labels, witness, selector schema version 𝑖𝑖𝑑 , key, 𝛽𝑜 , receiver, effect digest, acceptance sequence

sealed / accepted / rejected / fenced reserved/quarantined/terminal phase; write-once return target and 𝐻 (𝐷𝑜 ), 𝐻 (𝑋𝑜 ∖ 𝐷𝑜 ) inside the terminal decision

issuer signature; one issued vector per root generation immutable predecessor identity; at most one current generation per logical slot/reissue chain; disjoint split siblings may be current concurrently, but live ranges never overlap unique (𝑟𝑜𝑜𝑡, 𝑡𝑟𝑎𝑛𝑠𝑓 𝑒𝑟 _𝑖𝑑); terminal decision immutable unique (𝑟𝑜𝑜𝑡, 𝑜𝑝𝑒𝑟𝑎𝑡𝑖𝑜𝑛_𝑖𝑑); immutable replay, partition, and return binding

evidence ID, tagged variant, 𝛽𝑜 , root/slot/operation binding, authority/signature; success adds 𝑖𝑖𝑑 , acceptance sequence, and actual vector; no-effect adds fence epoch event ID, aggregate ID, payload digest, terminal-outcome digest; dispatch-permit authority, permit ID, permit digest, and signature

verification result and application time

credit

transfer operation

gateway_effect terminal_evidence

outbox

audit_node

previous hash, transition digest, authority, causal parents

accepted/effect/terminal outcome

dispatch gate: nondispatchable/dispatchable/localabort; delivery: ready/sent/observed publication/checkpoint state

one immutable acceptance binding and at most one instance per key unique evidence ID and one compatible terminal variant per operation inserted in the same transaction as the state transition; permit fields are complete iff dispatchable; local-abort is absorbing append-only hash link; no authority to move rights

Table 5. Logical durable records. A cryptographic audit chain detects post-hoc modification but does not replace atomic ownership transitions.

The prototype persists a 16-field executable-beta row. Its digest preimage is the following 15field projection: SQL

𝛽𝑜

= (issuer_id, root_id, credit_id, op_id, epoch, op_key, lineage_commitment, rights_commitment, effect_digest, receiver, max_usd, max_calls, source_label_digest, operation_label_digest, witness_digest), SQL

and the sixteenth field is beta_digest = 𝐻 (FTBC_EXECUTABLE_BETA_V1 ∥ encode(𝛽𝑜 deliberately single-chain profile, define the authenticated representation

)). In this

𝜒SQL (𝑔) = 𝐻 (sqlite-single-slot ∥ 𝑔). Because exactly one logical slot exists per root in the profile and root_id is committed inside SQL both the concrete key and 𝛽𝑜 , the gateway and checker recompute the same 𝜒SQL (𝑔); the root fence is the physical representation of the abstract fence for (𝑔, 𝜒SQL (𝑔)). No standalone slot_id column is implied. Thus “complete executable-beta” in Section 10 means complete with respect to this concrete prototype schema: every field and the digest are persisted or independently recomputed across the exercised branch, gateway, effect, and terminal-evidence rows. It does not claim that the SQLite prototype implements the abstract atom-selector schema, nor does it discharge the universal refinement obligation or a multi-slot adapter. That executable profile has one serial reissue chain per root and materializes a single root.current_credit_id; this is a projection of per-chain currentness, not a restriction on the full DAG schema, which permits pairwise-disjoint current split siblings.

Fault-Tolerant Budget Conservation in Agent Delegation

41

The compact gateway implements the permit branch of the abstract first-acceptance guard. In the same 𝑊3 transaction that persists R → Q and marks the outbox dispatchable, the branch perSQL sists an operation-scoped Ed25519 permit over the complete 𝛽𝑜 . For an unseen key, the gateway verifies that permit and the current root fence before atomically recording acceptance. An exact accepted replay returns the stored decision without requiring a new permit; a durable no-effect proof excludes later acceptance of a delayed permit. The independent checker, outside the enforcement TCB, separately verifies the permit signature, ordering, and branch/gateway correspondence. These finite traces exercise the declared guard but do not prove universal refinement for arbitrary adapters or the complete end-to-end theorem. When the SQLite profile creates a fresh successor during its final local abort, no-effect return, or success settlement, the transaction simultaneously moves the predecessor’s already safe available balance and the terminal return footprint. Its abstract image is the explicit TerminalRollover action in Equations (17)–(18), not a purported single Settle, Return, or Reissue step. 8.3

Write Ordering and Crash Cuts

For a protected operation, the required order is:

𝑊1 𝑊2 𝑊3 𝑁1 𝑊4

= validate current credit and joint witness, = atomically persist A → R, operation, obligation, outbox, and audit node, = atomically persist R → Q and a branch-signed permit over 𝛽𝑜 , then mark the same outbox row dispatchable in that transaction, = send through the fenced gateway, = atomically verify and settle an authoritative outcome.

A crash before 𝑊2 exposes no work and owns no reservation. A crash after 𝑊2 but before 𝑊3 leaves an unexposed reservation that local recovery can prove safe to abort. A crash after 𝑊3 , including before 𝑁1 , leaves a quarantined obligation. This can sacrifice availability, but it eliminates the opposite crash cut in which an effect exists without a charged right. A crash after 𝑁1 and before 𝑊4 is reconciled by the canonical operation key rather than by reissuing a semantically new request. The outbox is therefore a durability protocol, not a statement that message delivery is exactly once. Duplicate sends are expected. The gateway’s idempotency and receipt query turn duplicates into observation of one logical operation. 8.4

Reference Components

The reference profile separates six logical components; the compact artifact implements the exercised subset of these roles: (1) Issuer. Validates the root authority and fixes resource units, quantization, settlement authority, maximum-charge policy, and initial vector. (2) Credit authority. Executes split, sealed transfer, acceptance, disjoint join, return, and epoch transitions. (3) Branch ledger. Executes reserve, quarantine, settlement, and retirement in local transactions. (4) Gateway emulator. Enforces stable keys and epochs, verifies the branch-signed dispatch permit before first acceptance, durably binds acceptance to 𝛽𝑜 , records effect instances and acceptance sequences, and exposes queryable outcomes. (5) Reconciler. Resolves nonterminal transfers and operations without interpreting timeout as non-execution. (6) Independent checker. Independently recomputes the declared keys, bindings, ownership totals, conservation, and coverage predicates at every retained durable snapshot/prefix.

42

Zhu and Wang

Transition

Local work

Coordination

Reserve / settle Split Cross-store transfer Join

𝑂(𝑑) 𝑂(𝑑 + ℓ) 𝑂(𝑑 + ℓ) 𝑂(𝑝𝑑 + 𝑝ℓ)

Reconcile

𝑂(𝑑) per operation

Audit replay

𝑂(𝑑) per transition

one local durable transaction one local durable transaction source seal + destination accept one authority over all consumed inputs gateway query; reclaim additionally needs fence + non-acceptance proof none on enforcement path

Table 6. Asymptotic costs for compressed footprints. Cryptographic verification adds work proportional to the chosen signature and commitment formats.

The checker is intentionally outside the mutation path. Agreement between runtime assertions and an independently implemented checker is stronger evidence than either alone, but is neither a complete abstract-transition replay nor a handler-by-handler refinement proof of the production database or cryptography. 8.5

Concurrency and Placement

Credits are the unit of locality. Operations on disjoint credits need no shared counter and can proceed concurrently. A branch serializes transitions for one credit generation, for example with a row-version compare-and-swap or a local transaction lock. Cross-branch transfers serialize only the source seal and destination acceptance; the rights remain unavailable in T between them. A hot root does not imply a hot root row during ordinary spending. Root totals can be reconstructed from credit and operation records or maintained as non-authoritative aggregates. Coordination is required to move unused rights between partitions, join credits at one authority, change resource semantics, or reclaim a lost generation. This is the intended “just-right” boundary: spending preallocated rights is local; changing exclusive ownership is not. 8.6

Complexity and Metadata

Let 𝑑 = |𝒦|, 𝑝 be the number of parent credits in a join, ℓ the compressed lineage witness length, and 𝑧 the number of nonterminal records scanned during recovery. With range-compressed rights, ordinary vector operations are 𝑂(𝑑); the implementation does not materialize the logical atoms of Definition 1. Each operation stores identifiers and digests plus 𝑂(𝑑) quantities. A transfer additionally stores a lineage/rights commitment. Full ancestry need not travel on every request if the verifier trusts a checkpointed Merkle or accumulator proof; that optimization changes proof format, not the ownership invariant. 8.7

Trusted Computing Base and Profiles

The ledger profile trusts the issuer, credit/branch stores, and cryptographic verification. It proves only internal right conservation. The mediated-effect profile additionally trusts effect normalization, complete mediation, the fenced gateway, and terminal-evidence authority, yielding the coverage theorem. The accounting profile may rely on a provider’s usage receipt. If the provider can omit hidden tokens, canceled-stream usage, taxes, or asynchronous charges, the theorem covers the reported metric rather than the eventual invoice. An endpoint can advertise one of three capabilities:

Fault-Tolerant Budget Conservation in Agent Delegation

43

profile(𝑟) ∈ {FencedQueryable, ReceiptOnly, SelfReported}. The deployment must not silently upgrade these profiles. In particular, ReceiptOnly can preserve no-amplification by quarantining ambiguity but cannot promise eventual release, and SelfReported cannot support an effect-coverage claim about receiver state. 9 Evaluation Methodology The evaluation is claim-driven and intentionally performed after the model, protocol, theorem assumptions, and failure semantics are fixed. This order reduces the risk of fitting definitions to favorable measurements. The artifact uses no hosted model or provider. Agent decisions are deterministic event generators because the evaluated claims concern distributed ownership and settlement, not task quality. We use frozen cases, explicit oracles, and machine-readable denial reasons. The present oracle is a distributed state invariant, and each paired variation is a crash, message, permit, or epoch schedule rather than a natural language authorization context. MAS-FIRE provides a complementary taxonomy and injection framework for semantic, cognitive, and inter-agent coordination faults in LLM-based multi-agent systems [19]. Our evaluation targets a different layer: durable crash cuts, duplicated or reordered protocol events, epoch fencing, and preservation of ownership and effect-accounting invariants. It does not measure reasoning robustness. 9.1

Research Questions

RQ1: Model safety. In the declared finite scopes, do the settlement/generation and delegation-lineage machines preserve their stated ownership, conservation, settlement, and fencing invariants? RQ2: Necessity. Does timeout refund yield a short mechanism-specific counterexample, and does a compound fan-in certificate-validation mutant that substitutes historical inputs and omits disjointness produce the predicted ownership amplification? RQ3: Crash-fault runtime. Across the declared 𝑊2 , gateway-acceptance, and 𝑊4 pre/post-commit cuts, duplicate receipt, stale epoch, response loss, and pre-fence-accept/late-completion schedule, does an independent checker find any prefix violation in the safe SQLite profile? RQ4: Mechanism cost sanity. Do all injected process deaths recover durable SQLite state, and what local RPC and restart timings characterize this prototype execution? These observations are health checks, not a comparative performance claim. 9.2

Evidence Strata

No single experiment establishes the end-to-end theorem. We therefore use four deliberately separated evidence strata: (1) two complementary TLA+ specifications explored by TLC: one for settlement/generation recovery and one for lineage/fan-in [25]; (2) a dependency-free JavaScript encoding that exhausts the same declared settlement scope and runs named schedules; (3) two SQLite service processes, driven through separate durable files, with real SIGKILL cuts and an independent newline-delimited JSON (JSONL) trace checker; and

44

Zhu and Wang

(4) lightweight local RPC/restart timing captured while those correctness schedules execute. The TLA+ and JavaScript artifacts are separate executable encodings, not independent conceptual specifications. The SQLite checker imports neither encoding, protocol implementation, SQL, scenario, nor oracle module; it recomputes properties from durable snapshots. This reduces, but cannot eliminate, common-specification error. None of the strata proves an arbitrary deployment, endpoint, database, signature library, or the universal trace-lifting obligation in Equation (19). The settlement TLA+ and JavaScript encodings deliberately type each logical unit with one location. Their ExactConservation check is therefore a transition-accounting and regression sanity check, not independent evidence for the manuscript’s raw-relation ownership-partition lemma. The hand proof establishes that lemma without a location-function type; the complementary lineage model can represent multiple tagged occurrences and its mutant exercises that multiplicity. We do not report bounded state counts as a machine-checked proof of arbitrary raw-relation ownership. 9.3

Analytical Comparison Points

The following mechanisms structure the threat and novelty comparison; they are not presented as measured reimplementations: (1) Read–check–decrement. Replicated remaining balances with last-writer-wins merge; this isolates the invariant-convergence error. (2) Central linearizable counter. One Raft-style authoritative decrement and settlement record [34]; safe when reachable, unavailable to isolated branches. (3) Static escrow / Bounded Counter profile. Rights are preallocated and never dynamically reclaimed during faults [5]; this is the strongest numeric baseline. (4) Affine local budget. A single-process move-only credit modeled after Token Budgets [22]; cross-process crash state is outside its type envelope. (5) Allocation-contract monitor. Child vectors must sum within the parent as in Agent Contracts [48], but external execution has no durable obligation. (6) Shared replay registry. AIP/AAT-style attenuated tokens plus a linearizable operation-ID registry; this prevents some replay but lacks exclusive consumable transfer semantics. (7) Fail-closed coordinator. MPAC-style centralized current state rejects mutation while the coordinator is unavailable [37]. (8) Proposed profile. Exclusive credit lineage plus reserve/quarantine/terminal-evidence settlement and gateway fencing. RIFL, Beldi, and ExoFlow are architectural reference points for durable completion records and exactly-once workflows [27, 49, 54]. The reference artifact evaluates this paper’s conservation and crash-cut obligations; these systems remain architectural comparison points rather than reimplemented performance baselines. 9.4

Finite Scopes and Concrete Schedules

The settlement/generation model contains two logical atoms, two actors, epochs and operation generations 0..1, transfer seal/accept/verified cancel, reserve, dispatch, timeout, gateway effect, settlement, fencing, verified abort, successor-generation reuse, forfeiture, crash, and restart. The JavaScript encoding explores the complete reachable graph of the same finite abstraction and executes named traces. Those settlement models sequence terminal resolution and ordinary reissue; they do not contain a separate fused TerminalRollover transition. The fused action is covered by the inductive proof and the selected SQLite transactions, not by a claimed TLC/JavaScript bisimulation.

Fault-Tolerant Budget Conservation in Agent Delegation

45

Fault injection point

Ambiguity created

Required safe state

Bug exposed if weakened

After reserve commit, before dispatchable

No exposure possible by durable evidence

R, then verified abort

After quarantine commit, before send

Send may not have happened

Q until gateway proof

After gateway effect, before reply After receipt arrival, before ledger commit During sealed transfer

Effect exists, response absent Receipt can replay

Q, then receipt settlement same settlement applied once T until accept/exclusion old gateway requests fenced require current active inputs, reject overlap, and consume atomically commit exact subset; return authenticated remainder

leaked reservation or unsafe send without outbox utilization loss if safe; double spend if blindly refunded timeout-refund/lateeffect overspend duplicate charge or duplicate remainder both-side ownership after retry stale-generation spend after reclaim join amplification

During epoch advance During fan-in

During partial-vector settlement

Source debited, destination unknown Old worker may retain credentials Two references may share ancestry or be stale

Actual charge smaller than maximum

invented remainder or cross-dimension substitution

Table 7. Required crash and concurrency cuts. Each outcome is checked after every durable prefix, not only after recovery completes.

The complementary lineage model contains two dimensions (usd and tokens), two rights per dimension, root/left/right/join credits, generations 0..2, epochs 0..1, an atomic disjoint split, a legal current-input fan-in, and sequential full transfers and returns. The safe join consumes the two current, active, pairwise-disjoint branches atomically; a retained reachability witness confirms that this legal join is not vacuously disabled. The sequential workflow separately produces two overlapping historical return certificates without duplicating live ownership. The safe model never treats those stale certificates as join inputs. A deliberately compound validation mutant both substitutes them for current active inputs and omits their disjointness check; its counterexample must therefore not be interpreted as isolating either check independently. The concrete SQLite profile issues vector (100, 2) in dimensions usd and calls. It runs ten safe cases and one timeout-refund mutant. Each case creates fresh branch and gateway databases. The safe schedules cover pre/post-commit death at 𝑊2 , pre/post-commit death at 𝑊3 , pre/postcommit death at gateway acceptance, effect persistence with reply loss, pre/post-commit death at 𝑊4 , receipt replay, stale-epoch rejection, and a request accepted before a fence that completes after it. Table 7 states the broader protocol cuts and identifies which are exercised by which artifact layer. The SQLite layer uses real process death at the 𝑊2 reservation transaction, the 𝑊3 quarantine/permit transaction, the separate gateway-acceptance transaction, effect/reply-loss cut, and 𝑊4 settlement transaction; it also exercises stale-epoch rejection and pre-fence acceptance followed by late completion. Transfer cancellation and partial charge are likewise exercised in the executable settlement traces; the lineage model exercises a legal current fan-in plus an invalid

46

Zhu and Wang

historical-certificate path. These scopes are reported separately so model-level coverage is not mistaken for a distributed runtime implementation of transfer or DAG join. 9.5

Metrics

The primary safety metrics are counts of:

𝑉own = #ownership-partition violations, 𝑉sum = #bucket-conservation violations, 𝑉cover = #uncovered or multiply covered effects, 𝑉bound = #external-exposure bound violations, 𝑉settle = #conflicting/double settlements, 𝑉epoch = #accepted stale-generation effects. All must be zero for the proposed safe profile. Mutation success is the opposite: each intentionally weakened rule must produce at least one independently validated counterexample in a schedule that exercises the weakened assumption. Capacity state can be reported as:

𝑠𝑇 =

‖T‖1 , ‖B‖1

𝑠𝑄 =

‖Q‖1 , ‖B‖1

𝑠𝐹 =

‖F‖1 . ‖B‖1

For the concrete artifact, restart time is measured from process death to a ready service against the same database. We report only RPC sample count, per-case median/p95, and aggregate restart median captured by the correctness run. We do not infer throughput, tail SLOs, capacity, or comparative overhead from those samples. Safety is never combined with timing into one score. 9.6

Decision Rules and Statistical Treatment

Bounded model checking is reported as explored distinct states, generated states, depth/diameter when available, completed search status, and invariant violations. A zero count means no counterexample exists in that declared finite scope; it is not reported as an unbounded proof. Deterministic transition and fault cases are pass/fail with an exact case manifest. The local timings are descriptive observations over the RPCs and restarts that actually occur in those cases; there is no warm-up, random-sampling model, confidence interval, or hypothesis test. Runtime, hardware, SQLite version, topology, and the fact that CLI process startup is included are recorded with the results. 9.7

Predeclared Interpretation Boundaries

The following outcomes would narrow or falsify claims:

• any safe-model or proposed-runtime prefix with 𝑉own + 𝑉sum > 0 falsifies ledger conservation; • any mediated gateway effect without exactly one bound Q/C/F obligation falsifies effect coverage; • a mutant not detected within the exercised scope weakens evidence for necessity and must be reported rather than reclassified; • a timeout-only reclaim that appears safe merely indicates the schedule omitted the delayedeffect twin; • provider self-reported usage cannot validate actual invoice bounds; • fault-free microbenchmark speed cannot establish fault tolerance; and • a bounded TLC completion cannot establish correctness outside its constants or assumptions.

Fault-Tolerant Budget Conservation in Agent Delegation Evidence

Declared finite scope

Generated or edges

Settlement TLC Lineage TLC JavaScript graph

2 atoms, 2 actors, epochs/generations 0..1 54,477 2 dimensions, 4 rights, 4 credits 23 2 atoms, 2 actors, complete reachable 54,476 graph

47 Distinct states

Depth

Safe outcome

16,592 21 16,592

29 8 28

exhausted; no violation exhausted; no violation exhausted; no violation

Table 8. Completed bounded safety checks. The generated-or-edges column denotes TLC generated states for the TLA+ rows and explored transitions for JavaScript. Completion applies only to the constants shown.

Weakening

Detection

Shortest retained witness

Observed failure

Timeout refund after exposure

TLC and JavaScript

Historical-certificate validation (compound)

lineage TLC

TLC depth 4; JS depths 3 and 5 6 states

unsafe reclaim; then loss of effect coverage after the accepted request completes late ownership uniqueness; 8 live occurrences for 4 rights (maximum multiplicity 2)

Table 9. Targeted mutant results. Witness lengths are breadth-first counterexamples in the declared finite models, not field-failure probabilities. The historical-certificate row weakens both currentness and disjointness validation.

9.8

Reproducibility Protocol

The artifact entry point runs formal exploration, mutation, named transition, fault injection, aggregation, and internal consistency checks in that order. Every result file records the command, source digest, seed or schedule ID, runtime version, start/end time, and declared scope. Generated LaTeX tables are derived from JSON results; hand-entered benchmark numbers are forbidden. Appendix F gives the exact commands and expected artifacts. 10 10.1

Evaluation Results Bounded Model-Checking Results

All three safe finite graphs completed with an empty work queue and no invariant violation. The settlement TLC model explored 54,477 generated and 16,592 distinct states; the JavaScript encoding reached the same count of 16,592 distinct states. Equality of counts does not establish equality of state sets, a bisimulation, or independent specification evidence; it is only a coarse cross-encoding consistency check. The separate expected-failure reachability profile retained a 3-state legal current-input join witness. Both inputs were active, their live footprints were pairwise disjoint and covered all 4 rights, and the output retained multiplicity one. This establishes that the safe join action was reachable; it is not a safety counterexample. The deterministic executable suite then ran 19 named schedules (132 scheduled steps). All 18 safe schedules passed with zero final invariant violations, including gateway acceptance before a fence followed by completion after the fence, and the corresponding forfeiture case. These schedules test particular executions; they do not enlarge the exhaustive finite scope. 10.2

Targeted Necessity Checks

Both predeclared weakened mechanisms produced short, mechanism-specific counterexamples. The lineage mutant is compound: it substitutes returned historical certificates for current active inputs and bypasses pairwise disjointness validation. It must not be interpreted as an overlap-only ablation.

48

Zhu and Wang

Safe schedule W2 pre-commit rollback W2 post-commit recovery gateway-accept pre-commit rollback/retry gateway-accept post-commit dedupe effect/reply loss; W4 pre-commit W4 post-commit dedupe stale epoch rejection pre-fence accept; late completion W3 pre-commit rollback W3 post-commit permit recovery

Kills Records Checker 1 1 1 1 2 1 0 0 1 1

29 23 33 24 29 27 39 30 25 25

pass pass pass pass pass pass pass pass pass pass

Table 10. Independent checks over ten concrete safe traces. Each case uses fresh branch-ledger and gateway databases.

10.3

Multi-Process Crash-Fault Results

The concrete artifact executed 10/10 safe SQLite cases without a prefix violation under the independent checker. It injected 9 actual SIGKILL process deaths and retained 313 JSONL records. The checker also detected the timeout-refund mutant through dispatch_coverage, effect_coverage, and effect_budget_bound. It recomputed 25 canonical keys and 59 complete executable-beta rows, verified 11 signed success receipts and 1 signed no-effect proof, and checked 14 terminal return decisions including 3 fresh successors. All 12 negative handler assertions were observed without durable mutation. The compact gateway enforces the evaluated first-acceptance guard online: the branch persists and signs an operation-scoped dispatch permit in the same 𝑊3 transaction that moves the reservation to quarantine, and the gateway verifies and records that permit before accepting an unseen key. Exact replay returns the stored outcome, while a later authoritative no-effect proof excludes acceptance of a delayed permit. The independent checker separately recomputes permit signatures and cross-store dispatch coverage from the trace. These finite schedules validate the reference profile; they do not prove universal refinement for arbitrary runtime adapters. All 22/22 retained SQLite databases returned ok from PRAGMA integrity_check. This is evidence that the captured crash cuts left readable database images; it is not a proof of SQLite internals. The safe late-completion case binds the gateway-assigned effect instance and acceptance sequence through settlement and moves its partial remainder to a fresh, same-lineage successor rather than the stale source. The stale-epoch case separately exercises local unexposed abort and gateway-proved no-effect return; both create fresh successors only after predecessor closure and exact reusable-balance computation. The correctness run collected 111 local RPC samples. Per-case medians ranged from 9.702 to 12.007 ms, the largest per-case p95 was 28.111 ms, and the 9 restart observations had median 30.76 ms. These measurements include local process and SQLite CLI startup and serve only as mechanism health checks; they establish neither throughput nor a production latency SLO. 10.4

Interpretation and Residual Limits

The result is bounded but falsifiable: zero safe violations in the declared finite models, zero violations across all 10 retained safe runtime traces, and detection of both targeted weakenings. It does not establish liveness, Byzantine tolerance, production cryptographic assurance or receiptauthority integrity, arbitrary runtime refinement, cross-store credit transfer, or DAG join in the SQLite prototype. In particular, the SQLite profile exercises the implemented first-acceptance guard but does not furnish a universal handler-level refinement proof for GatewayAccept or the conditional end-to-end theorem. Its fused terminal-settlement/successor transactions have the

Fault-Tolerant Budget Conservation in Agent Delegation

49

explicit analytical image TerminalRollover, but no universal handler simulation proof is claimed. The Ed25519 fixture exercises authentication and negative verification paths but provides no production key isolation. External-effect claims remain conditional on a cooperating, idempotent, fenced, and queryable gateway with complete mediation. 11 11.1

Security Analysis Safety Against a Malicious or Confused Agent

The agent is not trusted to report a balance, choose a credit generation, forge terminal evidence, or decide that a timeout is a refund. It may emit arbitrarily many proposals, retries, delegations, cancellations, and joins. The branch store accepts a proposal only if the current credit exclusively owns the selected footprint, the label and joint witness authorize the normalized effect, and the immutable operation binding either does not yet exist or matches exactly. Consequently, prompt injection can influence the proposed action but cannot by itself duplicate a right. A compromised worker can still waste its own authorized escrow by reserving unproductive work, creating indeterminate obligations, or intentionally withholding completion. Conservation is a safety property, not a defense against budget denial. Deployments need rate limits, per-child reservation caps, bounded delegation depth, admission control, and human escalation for large or long-lived quarantines. 11.2

Replay, Equivocation, and Identifier Substitution

Every transfer, operation, and terminal-evidence item has a stable identifier, but identifier uniqueness alone is insufficient. The branch/gateway enforcement verifier, which is inside the safety TCB, recomputes the single canonical operation binding in Equation (6), including the selector schema version 𝜈sel , and rejects any field mismatch. Transfers use their separate domain-separated certificate and decision binding; they are not silently interpreted through the operation formula. The independent audit verifier in Figure 2 is outside the TCB and can detect divergence but cannot make an unsafe request safe. An exact replay is a stutter. Reuse of an identifier with a different tuple is an equivocation and is rejected. Domain separation prevents an operation ID from being reinterpreted as a transfer or receipt ID. Receiver and effect class are included so two services cannot accidentally share an idempotency namespace. Settlement also binds where unused rights may return. A target must satisfy Equation (7): it has the same root, is a successor of the source lineage that is current in the committed successor state under the settlement authority, and has a label no broader than the source credit. An agent therefore cannot use a valid partial receipt to redirect the remainder into an unrelated, broader, or stale credit. Terminal-evidence equivocation is detected when two authenticated terminal outcomes bind the same operation. Under Assumption 7, at most one can be valid. If a deployed terminal-evidence authority can sign inconsistent outcomes, the main effect theorem no longer applies; the ledger can quarantine the conflict, preserve no-amplification, and expose evidence, but cannot establish receiver truth. 11.3

Stale Generations and Split Brain

Epoch fencing protects against a lost controller or worker that later resumes. The critical check is at the last trusted boundary before the effect, not only at the branch database. A gateway accepts a new request for (𝑐𝑖𝑑, 𝜂) only while that generation is current. After an authenticated 𝜂+ > 𝜂 is installed, it may return the already recorded result for an old idempotency key but must reject a new old-generation effect.

50

Zhu and Wang

If two authorities can independently declare themselves current for the same credit generation, exclusive ownership is already violated. Consensus, single-writer placement, or another correct ownership service is required within that authority. The protocol confines this requirement to ownership changes; it does not solve consensus and does not claim Byzantine split-brain tolerance. 11.4

External-Effect Ambiguity

The most consequential attack surface is a receiver that completes work and drops or falsifies the response. The safe response is not to guess. Under the fenced-queryable profile, reconciliation obtains the recorded result. Under the receipt-only profile, missing evidence leaves the right in Q or eventually F. Under self-report, only the internal ledger claim survives. This tiering follows the same fundamental requirement as systems that provide exactly-once RPC or workflow execution: a completion record must be durably coupled to the mutation or returned by a cooperating transactional endpoint [27, 49, 54]. A client-side retry library cannot manufacture that coupling for an arbitrary third party. 11.5

Underreporting and Variable Charges

A maximum reservation u is sound only if the gateway can prevent an actual charge above it. For a paid API, that can mean preauthorization, provider-side hard caps, chunked metering with renewal, or reserving the maximum billable unit. If the provider reveals usage only afterward and may exceed u, no local algorithm can prove a hard bound on the real charge. The appropriate choices are to refuse the hard-bound profile, reserve a conservative worst case, or state a softer monitoring claim. Partial settlement is safe when the receipt authenticates d ⪯ u. The remainder returns only after that receipt. For streaming calls, the gateway can use successive sub-operations with separate reserved chunks; canceling a stream is not itself a zero-charge receipt. 11.6

Normalization and Path Aliasing

Two syntactically different requests may cause the same effect, while two similar strings may address different recipients or preconditions. Normalize is therefore part of the trusted policy boundary. Its test obligations include canonical encoding, default parameters, redirects, indirect identifiers, locale and unit conversion, recipient resolution, protocol-specific retries, and relevant domain preconditions. Unknown semantics fail closed. Complete mediation is equally important [39]. An agent with direct cloud credentials can bypass an MCP proxy; a browser can activate an effect through a UI path; a tool can invoke a second tool internally. The theorem covers only credentials and routes that the deployment actually interposes. Network egress policy, workload identity, receiver-side enforcement, and credential isolation are deployment controls, not consequences of the budget data structure. 11.7

Audit Integrity and Rollback

A hash-linked log reveals deletion or reordering relative to a trusted checkpoint, but a compromised store could roll back both state and its local log. Production profiles should bind store generation, credit epoch, and checkpoint sequence to a monotonic external witness, replicated log, hardware counter, or consensus state. This strengthens forensic detection; exclusive ownership still depends on the authoritative transition service. Audit records contain sensitive purpose, recipient, spend, and graph metadata. The default evidence plane should use digests and stable opaque identifiers, encrypt detailed receipts at rest, separate operational and audit roles, and enforce retention and deletion policies. Public verifiability does not justify publishing task content.

Fault-Tolerant Budget Conservation in Agent Delegation

51

Attack or failure

Prevented or detected by

Residual consequence

Outside the theorem

Duplicate child allocation Lineage alias at fan-in

atomic exclusive split + stable ID disjoint rights commitment + input consumption operation binding + gateway idempotency Q retention + reconciliation gateway-visible epoch fence signature and full binding verification

duplicate request stutters

corrupt authoritative store unsound commitment implementation

authenticated hard-cap profile external checkpoint / monotonic epoch per-child caps and admission policy

weaker reported-usage claim detect or confine rollback availability loss within authorized escrow

Dispatch replay Timeout refund race Stale worker Forged/changed receipt Provider underreporting Audit rollback Reservation flooding

join rejected

prior outcome returned

non-cooperating receiver

stranded capacity

guaranteed eventual receiver response direct credentials bypassing gateway compromised terminal-evidence authority correctness of an arbitrary invoice Byzantine consensus if not deployed agent usefulness or fair allocation

old request rejected or observed quarantine and investigation

Table 11. Security coverage and residual risk. The protocol prefers explicit loss of utility to an unsupported conservation claim.

12

Related Work Beyond the Closest Mechanisms

12.1

Agent Economies and Governance Receipts

EpochX treats tasks as bounties, supports recursive budgeted delegation, and uses lock and settle operations [46]. It is therefore direct prior art for hierarchical economic allocation; our focus is the failure semantics around duplicate delivery, persistent ownership, quarantine, fencing, and late settlement that are not established by EpochX’s reported model and evaluation. AgentBound centralizes pre-execution governance and emits signed governance receipts [21]. Those receipts attest to a policy decision, while our effect receipt attests to a receiver outcome and actual charge. Human Delegation Provenance (HDP), a lightweight cryptographic protocol, provides human-delegation provenance, while Aegon proposes ledger-bound tokens with attested receipts [6, 10]. We do not claim the first delegation chain, ledger token, or signed receipt. Agent Contracts and Token Budgets are the nearest resource-governance works [22, 48]. Their allocation law and affine ownership discipline motivate our model. The contribution here begins where one process or one allocation snapshot stops being authoritative: ownership must survive messages, durable crash cuts, joins, and uncertain effects. 12.2

Authorization Delegation

OAuth token exchange and Rich Authorization Requests provide standardized building blocks for audience-bound exchange and structured authorization [20, 29]. AIP and the current AAT InternetDraft extend these ideas to agent identity and attenuating chains [32, 36]; Overlaying Governance formalizes policy composition [18]. These answer which actions remain permitted. Our credits add linear consumption: two equally attenuated children must not both own the same last unit.

52

Zhu and Wang

Resource-bounded temporal logics have long represented strategies constrained by consumable or producible resources [2]. Our problem is operational rather than strategic: it specifies how authenticated rights move and settle under crash and partition. The logical connection is useful, but a model-checking semantics does not supply durable message protocols by itself. 12.3

Escrow, CRDTs, and Mobile Rights

Escrow transactions reserve rights so concurrent transactions preserve a numeric invariant [33]. Mobile escrow distributes rights to occasionally disconnected clients [23]. Bounded Counter CRDTs provide a particularly strong construction for partition-local decrement and rights transfer [5]. Just-Right Consistency combines such mechanisms with analysis that coordinates only invariant-sensitive operations [42]. We adopt, rather than rename, this lineage. The extension is that an agent credit carries an authorization label and dynamic delegation lineage, the task graph can join without merging aliased rights, and a spent unit remains coupled to an external-effect obligation through uncertainty. A numeric counter that converges to a valid value can still miss a duplicated payment or disclosure. 12.4

Transactions, Workflows, and Exactly-Once Semantics

Sagas decompose long-lived transactions into steps and compensations [12]; Atomix specializes transactional semantics to agent tool use [31]. RIFL couples request IDs with durable completion records [27]. Beldi supplies fault-tolerant transactional serverless workflows, and ExoFlow targets exactly-once DAG execution [49, 54]. These systems demonstrate that replay safety is a storage and endpoint property, not a property of a prompt. Our theorem is narrower in one dimension and broader in another. It does not claim a universal exactly-once workflow. It proves at-most-once settlement and continuous charged coverage for consumable delegated authority, including the safe but unavailable outcome in which an arbitrary effect cannot be authoritatively resolved. 12.5 Coordination and Impossibility CAP rules out simultaneous strong consistency and availability for every request during arbitrary partitions [13]; FLP limits deterministic consensus progress in an asynchronous system with a crash [11]. Invariant confluence and the Coordination Criterion more directly characterize when application correctness permits coordination-free execution [4, 16]. Our Proposition 1 is an application-specific consequence: exclusive preallocation permits local work, while creating or reallocating a shared spendable unit requires coordination or blocking. 13 13.1

Discussion What Is Actually Conserved?

The object conserved is authenticated authorization capacity, not money or physical energy. A dollar dimension means “authority to cause up to one dollar of charges under a named settlement rule.” If taxes, exchange rates, tips, later adjustments, or hidden provider usage are outside that rule, they are outside the invariant. A rigorous deployment must define each dimension’s unit, rounding, maximum charge, authority, and reconciliation semantics before issuing it. The exact equality in Equation (8) is stronger and more diagnostic than merely checking C ⪯ B. It distinguishes spendable, moving, not-yet-exposed, uncertain, consumed, and sacrificed capacity. Operators can therefore see whether apparent under-spending is true availability or merely hidden stranding.

Fault-Tolerant Budget Conservation in Agent Delegation

13.2

53

Why Keep Both R and Q?

Combining reserved and indeterminate rights preserves the numeric equation, but loses a crucial recovery fact. A durable R record whose outbox provably never became dispatchable can be locally returned. A Q record may correspond to a real effect and needs external evidence. The separation turns a crash cut into an auditable transition and prevents a generic “release pending reservations” job from creating authority. 13.3

Safety, Liveness, and Economic Utility

The protocol’s safety is prefix-closed; its liveness is conditional. A branch can progress during partition while it has suitable local rights and a reachable gateway. Once exhausted, it blocks even if another partition has idle capacity. A quarantined right can remain unavailable forever. These are not incidental implementation shortcomings but consequences of refusing to guess about exclusive ownership or external effects. Allocation policy can reduce the cost: assign escrow proportional to expected demand, keep small emergency reserves in multiple zones, rebalance before known disconnections, and choose queryable endpoints for large effects. Dynamic prediction may improve utilization but must not enter the safety theorem. 13.4

Vectors and Conversion

Vectors prevent a worker from exchanging, for example, ten low-risk reads for one high-risk write without authorization. Some applications legitimately convert resources: a dollar cap may purchase token calls, or a global risk budget may be divided among effect classes. Such conversion is a new protected effect. It needs a signed rate/rounding contract, consumes source rights, creates target rights once, and preserves a declared value invariant. Without that extra contract, conversion is undefined rather than inferred. 13.5 DAG Tasks, Forest-Owned Rights Task dependencies and budget ownership should remain different graphs. A synthesis agent can read results from many parents without owning their remainders. When it needs budget, each input branch may transfer a disjoint credit or one authority may perform an atomic join. This design prevents the common error of summing balances associated with incoming task edges. At large scale, full atom-set proofs are impractical. Range certificates, bounded-counter rights matrices, or cryptographic commitments can compress the footprint. The implementation must nevertheless expose a disjointness witness and consume each input generation exactly once. 13.6

Standards Integration

The protocol does not require a new wire protocol. AIP/AAT or OAuth can carry identity and attenuated scope; MCP or A2A can carry opaque credit and operation bindings; HTTP idempotency or conditional writes can implement a gateway primitive. Standardization value lies in a common semantic profile:

• authenticated resource schema and maximum-charge semantics; • stable root, logical-slot, transfer, credit-generation, operation, and terminal-evidence IDs; • immutable binding digest and the per-slot current epoch/fence; • endpoint capability declaration; • terminal outcomes including verified no-effect and forfeiture; and • machine-readable reason codes for conservative refusal.

54

Zhu and Wang

Interoperability testing should verify refinement of these meanings, not only JSON shape compatibility. 13.7

Deployment Migration

A practical rollout can proceed in increasing assurance: (1) instrument existing agents with stable operation IDs and observed usage, making no hardbound claim; (2) move counters into a durable branch ledger and reserve before effects; (3) route high-impact effects through idempotent, queryable gateways; (4) introduce exclusive child credits and disable copyable numeric “remaining” fields as authorities; (5) add epoch fencing, disjoint joins, reconciliation, and an independent trace verifier; and (6) publish only claims supported by the endpoint profile actually deployed. Legacy direct paths remain outside complete mediation until credentials and egress controls make bypass impossible. 14

Limitations and Validity

14.1

Model Limitations

The base model assumes crash faults, authenticated records, one correct local linearization point per branch, and a finite natural vector. It does not model Byzantine stores, signature compromise, side channels, probabilistic settlement, debt, negative balances, interest, speculative credit, or crossroot netting. Two independently authenticated roots are distinct authorizations; an issuer that accidentally signs overlapping grants can overspend a real-world cap without violating either perroot equation. Issuer-level escrow is required for an aggregate cap. The logical-atom construction is a proof device; a faulty compression or commitment scheme can violate the implementation mapping. Recent work on distributed agent governance under a compromised provider studies Byzantine replication, monitoring, auditing, and hybrid defenses [26]. Its adversary is outside our base theorem: we assume correct authoritative stores, gateways, and evidence services and establish safety only for the declared crash, retry, and partition model. The two guarantees are complementary rather than ordered by strength. The end-to-end effect theorem depends on sound normalization, complete mediation, an enforceable maximum-charge contract, gateway fencing/idempotency, and complete non-equivocating terminal evidence. These are substantial assumptions. The ledger theorem remains useful when some fail, but it must not be presented as conservation of actual external cost. 14.2

Formal-Method Limitations

The inductive proofs establish the mathematical transition system. TLA+/TLC and the independent explorer cover only their declared finite constants, fault schedules, and modeled transitions. Statespace completion increases confidence in the specification and detects regressions; it is not a proof of database durability, transport authentication, cryptographic libraries, or unmodeled adapters. In particular, the settlement TLA+ and JavaScript encodings assign each logical unit one location by type. Their exact-sum invariant checks transition bookkeeping but cannot represent the duplicate-tag raw states excluded by the ownership-partition proof. The lineage encoding admits origin-tag multiplicity and detects its compound fan-in mutant, but it is still a bounded model rather than a mechanized proof of the full raw-relation semantics.

Fault-Tolerant Budget Conservation in Agent Delegation

55

The trace-lifting result defines the criterion that every runtime handler must satisfy. A concrete event such as a receiver redirect or background retry outside the gateway must appear in the mapping; otherwise the deployment does not inherit the theorem. The SQLite profile discharges the exercised first-acceptance permit and crash-cut obligations. Production deployments must add a handler-by-handler discharge of Equation (19), supported where appropriate by verified storage procedures, refinement types, or proof-carrying adapters. 14.3

Experimental Limitations

The provider-free artifact isolates distributed-control behavior and supports deterministic internal verification. Its measurements characterize the stated formal scopes, named crash windows, and one local implementation and host. Model quality, real-provider accounting, Internet-scale latency, multi-region database failover, operator response, production failure frequency, and capacity planning are separate evaluation targets. The most important negative result is structural and does not depend on benchmark scale: without endpoint cooperation, a lost response cannot distinguish non-execution from completed execution. Experiments can demonstrate the race but cannot remove it. 14.4

Construct and External Validity

“Budget” spans tokens, currency, calls, disclosures, and risk units. These dimensions differ in metering authority and reversibility. Results transfer only when the deployment supplies a conservative maximum and an authoritative settlement relation. Quantization can over-reserve; coarse units trade utility for simple guarantees. The 2026 agent papers discussed here are recent and several are preprints or an Internet-Draft. Their reported systems and terminology may evolve. We use them to set a conservative novelty boundary, not as proof of deployment prevalence. Classical escrow, invariant-confluence, lease, and workflow literature remains the stronger foundation. 14.5

Internal Validity

Independent implementations, mutation tests with expected counterexamples, prefix checks, stable result manifests, and explicit claim/evidence mapping reduce correlated specification risk across the formal model, runtime, checker, and generated tables. Artifact results are regenerated from source; every failed or skipped case is reported. 15

Ethics and Responsible Deployment

Budget enforcement can reduce financial loss, excessive API use, unauthorized disclosure, and repeated high-impact effects. It can also create false confidence. A green ledger does not prove that a planner chose a beneficial action, that a price was fair, that a recipient was appropriate, or that complete mediation actually held. Interfaces should display endpoint profile, quarantined capacity, unresolved effects, and assumption failures alongside a remaining balance. Fine-grained receipts and delegation graphs reveal organizational structure, purposes, recipients, spending patterns, and potentially sensitive content. Evidence minimization, separation of duties, access logging, encryption, retention limits, and deletion procedures are necessary. Cryptographic commitments can reduce disclosure but do not make metadata harmless. Conservative quarantine can be abused to deny service or trap a competitor’s shared capacity. Issuers should cap the budget one child can reserve, define escalation and forfeiture authority, record human overrides as new authorizations, and avoid automatic punitive decisions based solely on an ambiguous external outcome or unverified assertion. The mechanism allocates authority; it does not decide whose goals deserve resources.

56

16

Zhu and Wang

Conclusion

Distributed agent delegation turns a budget from a number into a fault-tolerant authorization object. Parent/child allocation inequalities, affine local types, attenuated scopes, idempotency keys, or convergent counters each solve part of the problem. None alone prevents a refunded timeout from colliding with a late effect, an aliased fan-in from reminting capacity, or a stale worker from spending a reclaimed generation. We introduced a protocol in which exclusive, labeled credit moves through a delegation lineage; a protected effect is reserved before exposure; ambiguity is quarantined; and one idempotent terminal decision applies authenticated evidence at most once. A success receipt releases only its authenticated remainder. Full return from an exposed obligation requires a receiver-visible fence together with authoritative proof that the exact binding was never accepted and never occurred. The six-bucket equation keeps spendable, moving, reserved, uncertain, committed, and forfeited rights explicit. Under stated assumptions, distinct effect instances are injectively covered, and settled actual charge plus conservative outstanding exposure is bounded by the issued root vector. The construction also preserves ledger conservation, descendant non-amplification, late-completion safety, and partition confinement. The central systems result is precise: local availability comes from rights allocated before a partition, while uncertainty must remain charged until evidence resolves it. A system that hides this cost by refunding on timeout does not conserve authority; it merely delays discovery of the overspend. Data, Code, and Materials Availability The public preprint package contains the manuscript source and bibliography. The formal specification, bounded explorer, mutation suite, fault schedules, SQLite traces, trace checker, result aggregator, and digest manifest are maintained as a deterministic, provider-free research artifact using only synthetic identifiers and effects. Appendix F records its commands, declared scope, and expected outputs so the reported evidence can be audited against the frozen internal release. The executable artifact is not distributed with this preprint and no public archival URL is claimed. Author Contributions Both authors contributed to problem formulation, system design, formalization, analysis, artifact review, and manuscript preparation. The machine-readable manifest separates generated evidence from source and records the verification commands used for the reported results. Competing Interests The authors are affiliated with Accentrust, which develops agent-governance technology. The paper’s claims are restricted to the stated formal assumptions and accompanying artifact; no production deployment claim is made. A Notation and Semantic Domains Table 12 collects symbols used by the abstract model. A bold quantity is a resource vector; a setvalued footprint denotes logical rights. All vector relations are componentwise unless an authenticated conversion contract explicitly says otherwise. B Complete Abstract Transition Contract Tables 13–14 make the proof-relevant preconditions and postconditions explicit. “Same atoms” means identity-preserving movement, not numeric subtraction followed by unrelated issuance.

Fault-Tolerant Budget Conservation in Agent Delegation

57

Symbol

Domain

Meaning

𝒦 B𝑔 𝑈𝑔 𝑋𝑐 , 𝑋𝑜 , 𝑋𝑥 vec(𝑋 ) 𝜆

finite set ℕ |𝒦 | finite disjoint union subsets of 𝑈𝑔 ℕ |𝒦 | authorization-label domain

𝜆′ ⊑ 𝜆 𝒢𝑇 𝒢𝐶 𝑐, 𝑥, 𝑜 𝜖, 𝑟 + , 𝜋¬𝑒 𝜔, 𝜁 , 𝜋local

partial order DAG DAG records externally authenticated terminal evidence terminal-outcome witnesses

authenticated resource dimensions vector issued by root grant 𝑔 logical unit rights underlying B𝑔 credit, operation, and transfer footprints per-dimension cardinality of footprint 𝑋 root, principal, purpose, audience, effect class, expiry, and policy version child label is no broader than parent label task dependency graph; edges do not imply ownership credit lineage; edges represent consumed input and fresh output credit, sealed transfer, and operation success receipt or fence-backed no-effect certificate

𝜂 𝜒𝑐

monotonic epoch logical slot identifier

Current𝑠 (𝑐, 𝜂)

state predicate

𝜅

receiver-scoped key

𝛽𝑜

digest

ReturnTarget

predicate over 𝑜, 𝑐𝑟 , 𝑠, 𝑠 ′

ReissueTarget

predicate over 𝑐, 𝜂, 𝜂+ , 𝑐 + , 𝑠, 𝑠 ′

Avail, SafeA

atom sets

TerminalRollover

abstract action

Φ𝑜 u𝑜 d𝑟 + 𝜈sel

witness ℕ |𝒦 | ℕ |𝒦 | selector schema version

A, T, R, Q, C, F

ℕ |𝒦 |

Obs(𝑠) 𝜄

effect-instance log effect-instance record

Covered(𝜄, 𝑜, 𝑠) 𝛼

relation abstraction function

closed tagged sum of external evidence and a durable, authenticated local never-dispatchable witness; 𝜁 excludes success receiver-visible fencing epoch stable identifier of one reissue chain; split and join outputs receive fresh slots authority records 𝑐 as the unique active generation for slot (𝑔, 𝜒𝑐 ) at epoch 𝜂; disjoint sibling slots may be current concurrently, and singleton input ownership is a separate guard idempotency/query key for one normalized effect and source generation; the separate acceptance digest binds the slot complete gateway-acceptance binding from Equation (6), including (𝑔, 𝜒𝑐 ) same-root, current in the committed successor state, same-source-lineage, same-authority, label-non-widening destination for unused rights authenticated same-root, same-authority, non-widening successor generation all raw available atoms of a generation, and the subset with retained reclaim provenance; successor installation requires equality one atomic final terminal partition, predecessor closure, and normalized same-slot successor installation joint current authorization, route, closure, effect, and credit evidence maximum amount reserved for operation 𝑜 authenticated actual charge in success receipt 𝑟 + immutable public ordering used to derive an exact charged footprint from a charge vector available, transit, reserved, quarantined, committed, and forfeited totals protected instances observed by the gateway in state 𝑠 distinct gateway occurrence with 𝑖𝑖𝑑 , key, acceptance binding, digest, receiver, and acceptance sequence instance 𝜄 has one compatible charged operation 𝑜 in state 𝑠 concrete event to abstract transition or stutter

Table 12. Notation. Logical unit sets make aliasing explicit; the runtime may use compact balance and lineage certificates.

C

Concrete-to-Abstract Refinement Obligations

A concrete implementation trace is a sequence of committed database transactions, gateway observations, and authenticated terminal evidence. Volatile steps that neither expose an effect nor change durable state map to stutter. Tables 15 and 16 list the minimum simulation obligations. D Adversarial Trace Catalogue D.1 Timeout Refund and Late Completion Let 𝑈𝑔 = {𝑢}. The safe prefix is: Reserve(𝑜)

Dispatch(𝑜)

A(𝑐) −−−−−−−−→ R(𝑜) −−−−−−−−−→ Q(𝑜).

58

Zhu and Wang

Action

Precondition

Postcondition

Replay/failure behavior

Issue

authenticated fresh root; vector and label schema valid

duplicate root ID rejected or returns identical issuance

Split

current owner generation/epoch; pairwise-disjoint subsets; attenuated labels

Delegate seal Delegate decision

current source; subset available; destination/label bound valid current certificate or destination-exclusion proof; decision pending

Delegate materialize

terminal transfer decision and matching footprint

all 𝑈𝑔 in one root A credit with a fresh logical slot; install matching epoch and active-generation registers parent loses exactly union; install every child under a pairwise-distinct fresh logical slot; close and clear the parent only if its complete responsibility is consumed same atoms A → T; signed certificate/outbox durable CAS to exactly one of accepted or cancelled and logically moves the footprint to the unique destination child or back to the source; acceptance installs the child under a fresh logical slot with matching current registers durable rows materialize the logical owner already selected by the decision register; abstract stutter

Reserve

current credit/epoch; available footprint; valid effect and joint witness durable unexposed reservation; outbox binding intact; current epoch and witness rechecked if key exists, stored binding must equal 𝛽𝑜 ; if unseen, matching durable dispatchable marker, 𝑋𝑜 wholly in Q/F, recomputed 𝛽𝑜 , and current epoch/witness for the authenticated (𝑔, 𝜒𝑐 ) slot prior accepted binding; no instance for key in the one-effect profile

Dispatch GatewayAccept

EffectOccurs

same atoms A → R; operation, obligation, outbox, audit atomically durable same atoms R → Q before possible effect

same request stutters; conflicting replay rejected

send retries preserve transfer ID; timeout stays T duplicate returns prior decision; competing terminal decision rejected

crash recovery repeats the same materialization; stale source or destination rows are never authoritative duplicate identical operation stutters; changed binding rejected duplicate gateway send observes same key; crash remains Q

existing exact binding stutters; otherwise one per-key accepted 𝛽𝑜 is durable

exact replay remains readable after terminal bucket moves; unexposed, stale, or conflicting first acceptance rejects

append one fresh 𝜄 to Obs

transport retry cannot append a second instance

Table 13. Abstract action contract for issuance, transfer, reservation, dispatch, acceptance, and effect occurrence. Preconditions are part of the mechanism, not optional validation advice.

The controller sees no response. In execution 𝐻0 , no gateway effect occurred; in 𝐻1 , the effect occurred and its response is delayed. The controller’s local view is identical. A timeout refund would place 𝑢 in A in both histories. Spending it under a fresh operation in 𝐻1 creates two covered effect instances for one issued atom. The safe machine instead stutters until a query distinguishes the histories, or moves the atom to F. D.2 Duplicate Transfer Acceptance The source seals 𝑋 under 𝑥𝑖𝑑 and retries after losing the acknowledgment. If the destination interprets the certificate as a bearer balance, it can create 𝑐1 and 𝑐2 , each with numeric value vec(𝑋 ). The required uniqueness decision over (𝑔, 𝑥𝑖𝑑) returns the previously created 𝑐1 ; it does not re-import the ranges. Source cancellation is equally dangerous unless the destination has durably fenced 𝑥𝑖𝑑 . D.3 Aliased Diamond Join A parent credit is referenced by task branches 𝑎 and 𝑏 , but only one actual transfer occurs. Both task results point to the same descendant credit 𝑐 . A naive join computes a𝑐 + a𝑐 . The set model instead tests 𝑋𝑐 ∩ 𝑋𝑐 = 𝑋𝑐 ≠ ∅ and rejects. Task multiplicity does not create credit multiplicity.

Fault-Tolerant Budget Conservation in Agent Delegation

59

Action

Precondition

Postcondition

Replay/failure behavior

Settle success

full footprint in Q(𝑜); valid receipt for 𝜄 ∈ Obs, matching 𝛽𝑜 ; when the remainder is nonempty, a decision-bound return credit satisfying Equation (7); 0 ⪯ d ⪯ u type-matched 𝜁 : local no-dispatch precondition for 𝜋local , or gateway fence plus authoritative 𝜋¬𝑒 proof that the exact binding was never accepted and cannot occur; return target satisfies Equation (7) unresolved quarantined operation and authorized administrative decision source is current; authenticated target 𝜂+ > AuthoritativeEpoch(𝑔, 𝜒𝑐 ) = 𝜂𝑐 ; gateway installation protocol satisfied

version-bound Take𝜈sel (𝑋𝑜 , d) Q → C; complement Q → A; bind 𝐻 (𝐷𝑜 ) and 𝐻 (𝑋𝑜 ∖ 𝐷𝑜 )

identical receipt stutters; conflicting receipt or partition rejects

all operation atoms move from the branch-specific R/Q → A; write terminal decision and audit; the local branch also persists 𝜋local and sets the dispatch gate to absorbing local-abort all operation atoms Q → F

timeout or local lease expiry alone has no transition

install the gateway fence, mark the old credit closing, clear its active generation, and advance the slot authority epoch without moving balance or creating a successor; old generation cannot initiate a new effect and recorded old outcomes remain queryable one transaction moves only that footprint and installs 𝑐 + as current for the same logical slot

old messages reject or return prior result

Return

Retire Fence

Reissue

TerminalRollover

Join

old generation closed at installed 𝜂+ ; exact Reusable footprint uniquely available; SafeA = Avail; write-once key selects (𝜂+ , 𝑐 + ) for normalized predecessor (𝑔, 𝜒𝑐 , 𝑐𝑖𝑑, 𝜂𝑐 ); target satisfies Equation (16) fenced predecessor is closing; 𝑜 is its final nonterminal operation with a type-matched terminal-outcome witness; source and settlement authority agree; SafeA = Avail; both decision keys are unassigned; normalized reissue target satisfies Equations (17)–(18) current, operation-free, pairwise-disjoint same-root inputs controlled by one transition authority

one transaction fixes the terminal partition, moves only its return footprint plus disjoint SafeA to 𝑐 + , closes 𝑐 , and installs 𝑐 + , writes both keys, sets the witness-specific operation/outbox outcome, and appends its audit node; the local branch additionally sets the absorbing local-abort dispatch gate inputs consumed; same-root output owns their exact union under lower-bound label and a fresh logical slot; fully consumed inputs close and clear, and the output’s current registers are installed

availability never increases; F is absorbing

committed, forfeited, accepted, or unresolved atoms never move; exact replay stutters and changed target rejects exact replay stutters; changed evidence, partition, epoch, or successor rejects

duplicate stutters; overlap or mixed root rejects

Table 14. Abstract action contract for settlement, return, retirement, fencing, reissue, fused rollover, and join (continued).

D.4 Stale Epoch After Reclaim Worker 𝑤 holds generation 𝜂, partitions, and prepares operation 𝑜 . The controller first installs the gateway fence and advances the authority epoch to some 𝜂+ > 𝜂. That step neither rewrites the old credit’s epoch, moves its balance, nor creates a successor. Reallocation occurs later and only after Closed and exact Reusable hold: each exposed obligation has complete terminal settlement or authoritative, fence-backed proof that its exact binding was never accepted and never occurred. When 𝑤 reconnects, the gateway rejects a new key under 𝜂. If 𝑜 ’s key was already recorded before the fence, the gateway returns that outcome for settlement; it does not execute a second effect. An epoch checked only in the controller database cannot provide this property.

60

Zhu and Wang

Concrete event

Abstract image

Required evidence

Forbidden mapping

Root row commit

Issue

Source debit + transfer row commit Transfer-decision CAS

Delegate seal

issuer signature, fresh generation, exact vector one transaction, same compressed ranges valid certificate/exclusion proof and monotone decision register same terminal decision and exact compressed ranges; logical ownership is read from the decision register atomic debit and immutable slot/effect binding durable R → Q before gateway exposure existing exact binding, or, for first acceptance only, matching durable dispatchable marker and Q/F ownership, authenticated logical slot, its current epoch/fence, recomputed 𝛽𝑜 , witness, and maximum vector prior accepted binding, fresh 𝑖𝑖𝑑 , complete maximum-charge contract

editing an existing issued vector message send before source debit accepted and cancelled both becoming terminal

Destination/source finalization

AcceptTransfer or CancelTransfer, including the one logical ownership switch stutter (materialization only)

Operation/outbox commit

Reserve

Dispatchable marker commit Gateway acceptance row

Dispatch

Gateway effect log

EffectOccurs

GatewayAccept

treating a stale row as authoritative or moving the abstract footprint a second time reserving after tool execution network send while still only R reapplying first-acceptance bucket guards to an exact terminal replay, or accepting an unexposed, stale, or changed binding

an unbound direct receiver call or a second instance for one key

Table 15. Refinement obligations for issuance, transfer, dispatch, and gateway effects.

D.5 Partial Charge and Duplicate Receipt Operation 𝑜 reserves vector (1000 cents, 3 calls). A receipt authenticates (730, 1). One transaction commits a matching subset and returns (270, 2). Replaying the receipt returns the same terminal decision. A second receipt claiming (820, 1) is not a second partial update; it conflicts with the immutable terminal decision and is quarantined for investigation. E Claim–Evidence Matrix F

Artifact and Reproduction Protocol

F.1 Directory Contract formal/ BudgetConservation.tla DelegationLineage.tla budget_model.mjs bounded_model.mjs configs/ safe.cfg timeout_refund_mutant.cfg lineage_safe.cfg

Fault-Tolerant Budget Conservation in Agent Delegation

61

Concrete event

Abstract image

Required evidence

Forbidden mapping

Terminal-outcome transaction

Settle, Return, or, when fused with successor installation, TerminalRollover

treating a success receipt as no-effect evidence, choosing a noncanonical partition, applying a textual worker assertion, or widening/redirecting a remainder

Timeout / worker death Epoch installation

stutter + reconciliation request Fence

Ordinary successor-generation transaction

Reissue

Fused final-outcome/successor transaction

TerminalRollover

Audit-only append

stutter

a tagged external signature or trusted durable local no-dispatch witness, 𝛽𝑜 including selector version, one terminal CAS, exact committed/remainder footprint commitments, and Equation (7) for every returned atom no ownership change monotone successor visible at every protected gateway closed-generation proof at the installed 𝜂+ , exact uniquely available reusable footprint, write-once unique reissue decision, and authenticated target satisfying Equation (16); decision, current metadata, and move are atomic Equations (17)–(18); canonical terminal partition and status; complete SafeA; atomic terminal and normalized reissue decisions digest of an already authoritative decision

Q→A local-only epoch bump followed by reuse copying old C/F/T/Q atoms or widening/changing the successor lineage, root, or authority

mapping the fused commit to only Settle, Return, or Reissue, or copying an input atom

moving rights solely because a log entry exists

Table 16. Refinement obligations for terminal resolution, fencing, and successor installation. A trace that cannot be mapped without violating Tables 15–16 is outside the implementation theorem.

lineage_current_join_witness.cfg lineage_historical_certificate_validation_mutant.cfg bench/ run_tlc_model_checks.mjs run_lineage_tlc.mjs fault_injection_eval.mjs sqlite_process_service.mjs sqlite_multiprocess_eval.mjs sqlite_trace_checker.mjs run_all.mjs aggregate_results.mjs verify_artifact.mjs results_tla_model_check.json results_lineage_tla_model_check.json results_bounded_model.json

62

Zhu and Wang

Claim

Analytical support

Ownership partition

transition induction over raw ownership relations

Exact six-bucket conservation Descendant non-amplification At-most-once settlement Effect-instance coverage and external exposure bound Late-completion safety Partition confinement

Concrete trace lifting Prototype timing characterization

Executable support

lineage tagged-occurrence model, legal-join witness, and compound invalid fan-in mutant; settlement model separately checks the single-location obligations partition lemma + vector corollary finite transition-accounting checks and runtime prefix checks cut/lineage induction split, transfer, join, and alias schedules immutable binding + terminal duplicate and conflicting CAS receipt cases injective gateway binding + effect-instance log joined to complete-charge theorem operation and maximum-vector trace Q retention + fence argument effect-before-response-loss and delayed receipt cases exclusive preallocation theorem exclusive-transfer and coordinator-outage schedules in bounded models; the theorem is the primary support conditional criterion under independent checks of selected Appendix C binding and prefix obligations plus invalid-trace cases no theorem local durable-store diagnostic timings

Explicit exclusion Byzantine/corrupt authoritative store

real-world value not represented by resource schema task quality and fair allocation exactly-once network delivery unmediated paths or dishonest charge authority automatic eventual refund full availability after local escrow exhaustion a universal refinement proof for unexamined handlers or deployments Internet-scale or production SLO

Table 17. Claims are linked to distinct analytical and executable evidence. The exclusions are part of the claim, not deferred implementation details.

results_fault_injection.json results_aggregate.json artifact-manifest.json sqlite_runtime_results/<run>/ summary.json checker-summary.json traces/ db/ generated-results.tex

The two TLA+ files are complementary: one covers settlement, acceptance, effects, fencing, and generations; the other covers lineage and fan-in. The JavaScript model is a second executable encoding of the settlement abstraction, not an independent conceptual specification. Concrete SQLite results retain one branch-ledger and one gateway database per case. The compact branch persists a signed dispatch permit in its 𝑊3 transaction; the gateway verifies and records the permit before accepting an unseen key. Its independent checker separately validates the signature, temporal order, and cross-store binding. This exercises the evaluated first-acceptance guard without substituting finite traces for universal adapter or end-to-end refinement. results_aggregate.json is the sole numeric source for generated-results.tex; generated output is never treated as a source model. F.2 Canonical Commands # Verify retained TLC/SQLite evidence and rerun JS layers: node bench/run_all.mjs --skip-tlc # Rerun both pinned TLC models:

Fault-Tolerant Budget Conservation in Agent Delegation

63

TLA2TOOLS_JAR=/absolute/path/tla2tools.jar \ JAVA_BIN=/absolute/path/java \ node bench/run_all.mjs # Also create a fresh, non-overwriting SQLite run: TLA2TOOLS_JAR=/absolute/path/tla2tools.jar \ JAVA_BIN=/absolute/path/java \ node bench/run_all.mjs --rerun-sqlite # Regenerate/verify from the retained concrete run: node bench/aggregate_results.mjs \ --sqlite-dir \ bench/sqlite_runtime_results/dispatch-permit-v1-20260925 node bench/verify_artifact.mjs tectonic -X compile main.tex --outdir build \ --keep-logs --keep-intermediates --only-cached

The --rerun-sqlite mode always allocates a new timestamped directory; it neither removes nor overwrites a retained run. The verification command fails if a source or result digest is stale, a required safe or mutant case is absent, a safe-profile invariant count is nonzero, the aggregate and generated LaTeX differ, a JSONL record count changes, or any of the 22 retained SQLite databases fails PRAGMA integrity_check. It also re-executes the independent SQLite snapshot checker, the dependency-free finite explorer, and the schedule suite, compares their outputs byte-for-byte, and directly checks persisted terminal return targets, successor lifecycle rows, and transaction guards. F.3 Environment Disclosure The artifact manifest records operating system, architecture, CPU, memory, Node.js, Java and TLC versions, the pinned TLC JAR digest, and SHA-256 plus byte length for every retained source and result. The concrete SQLite evidence additionally records SQLite version, process topology, command, UTC start/completion times, and source hashes. TLC uses one worker, a fixed fingerprint polynomial, and a fixed seed where applicable; the named JavaScript and SQLite schedules are deterministic. The provider-free artifact requires no network access after the pinned TLC JAR is available. F.4 Result Reporting For each model:

• report constants, distinct and generated states, search depth or graph depth, queue/completion status, and invariant result; • retain the shortest available counterexample for every mutant; • identify whether symmetry, state constraints, or liveness checking was used; and • never translate “no error in scope” into “proved for all sizes.” For each concrete case, the artifact retains the full JSONL event trace, durable branch/gateway snapshots, effect/terminal-evidence binding, expected outcome, actual outcome, and independent pass/fail decision. It also retains per-case RPC and restart summaries from the same correctness runs so every reported descriptive timing can be regenerated. These timing samples are health checks, not a throughput experiment or production SLO.

64

Zhu and Wang

G Deployment Assurance Checklist (1) Define every resource dimension, unit, rounding rule, maximum-charge rule, and authoritative settlement source. (2) Enumerate every route to each protected effect; remove direct credentials or mark the deployment outside complete mediation. (3) Verify that reserve, obligation, outbox, and audit records share one durable local transaction. (4) Verify that possible gateway exposure occurs only after the durable R → Q transition. (5) At first acceptance, require a signed single-use dispatch permit or an authoritative branch query proving the matching dispatchable marker and Q/F ownership; an offline audit is insufficient. (6) Scope operation keys to receiver and normalized effect; make exact replay a stable decision and conflicting replay an error. (7) Recompute 𝛽𝑜 and test terminal-evidence signatures and every immutable binding, including root, logical slot, lineage, footprint, epoch, effect, receiver, maximum, and actual charge. (8) Require Equation (7) for every partial remainder or no-effect return; use a separate sealed transfer for cross-store or ancestor return. (9) Before reusing a lost generation, install fences at every protected gateway and obtain terminal settlement or authoritative proof that each returned binding was never accepted and never occurred; a fence or lease expiry alone is not effect-absence evidence. (10) Reject numeric fan-in unless ownership inputs are pairwise disjoint and atomically consumed. (11) Monitor T, Q, F separately from committed spend and available capacity. (12) Bound per-child reservations and define escalation, reconciliation, and forfeiture authorities. (13) Run the conformance suite for each MCP, A2A, HTTP, browser, shell, or framework adapter. (14) Publish the actual endpoint capability profile and preserve the assumptions beside every assurance claim. H

Proof and Evidence Dependency Map

The logical dependency chain is: authenticated exclusive issuance ⇓ ownership-preserving transitions ⇒ partition lemma ⇒ exact vector conservation ⇓ disjoint lineage ⇒ descendant non-amplification ⇓ reserve before exposure + immutable operation binding ⇓ settlement uniqueness + injective effect-instance coverage ⇓ complete charge or conservative maximum ⇒ external exposure bound ⇓ gateway-visible epoch fence ⇒ late-completion safety ⇓ handler-level trace-lifting obligations ⇒ conditional runtime result. Formal exploration targets the first five arrows. Concrete trace checking targets the final refinement arrow. Fault injection demonstrates that the runtime reaches the declared recovery cuts. None substitutes for verifying the environmental assumptions named above.

Fault-Tolerant Budget Conservation in Agent Delegation

65

References [1] A2A Project. 2026. Agent2Agent (A2A) Protocol Specification, Version 1.0.0. https://a2a-protocol.org/v1.0. 0/specification/ Protocol specification, accessed 25 September 2026. [2] Natasha Alechina, Brian Logan, Hoang Nga Nguyen, and Abdur Rakib. 2010. Resource-Bounded Alternating-Time Temporal Logic. In Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems. 481–488. [3] Andreas Andreakis. 2026. Machine-Checked Dual-Write Recovery from a Commit Log. https://doi.org/10. 48550/arXiv.2608.00501 arXiv:2608.00501 [cs.DB] [4] Peter Bailis, Alan Fekete, Michael J. Franklin, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. 2014. Coordination Avoidance in Database Systems. Proceedings of the VLDB Endowment 8, 3 (2014), 185–196. https://doi.org/10. 14778/2735508.2735509 [5] Valter Balegas, Diogo Serra, Sérgio Duarte, Carla Ferreira, Marc Shapiro, Rodrigo Rodrigues, and Nuno Preguiça. 2015. Extending Eventually Consistent Cloud Databases for Enforcing Numeric Invariants. In 2015 IEEE 34th Symposium on Reliable Distributed Systems (SRDS). IEEE, 31–36. https://doi.org/10.1109/SRDS.2015.32 [6] Amrish Baskaran, Nirbhay Pherwani, and Raghul Krishnan. 2026. Aegon: Auditable AI Content Access with LedgerBound Tokens and Hardware-Attested Mobile Receipts. https://doi.org/10.48550/arXiv.2604.06693 arXiv:2604.06693 [cs.CR] [7] Andrew D. Birrell and Bruce Jay Nelson. 1984. Implementing Remote Procedure Calls. ACM Transactions on Computer Systems 2, 1 (Feb. 1984), 39–59. https://doi.org/10.1145/2080.357392 [8] Mike Burrows. 2006. The Chubby Lock Service for Loosely-Coupled Distributed Systems. In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation. 335–350. https://www.usenix.org/ conference/osdi-06/chubby-lock-service-loosely-coupled-distributed-systems [9] Leo Cao, Luoxi Meng, Deian Stefan, and Earlence Fernandes. 2024. Stateful Least Privilege Authorization for the Cloud. In 33rd USENIX Security Symposium (USENIX Security 24). USENIX Association, Philadelphia, PA, 3477–3494. https://www.usenix.org/conference/usenixsecurity24/presentation/cao-leo [10] Asiri Dalugoda. 2026. HDP: A Lightweight Cryptographic Protocol for Human Delegation Provenance in Agentic AI Systems. https://doi.org/10.48550/arXiv.2604.04522 arXiv:2604.04522 [cs.CR] [11] Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. 1985. Impossibility of Distributed Consensus with One Faulty Process. J. ACM 32, 2 (1985), 374–382. https://doi.org/10.1145/3149.214121 [12] Hector Garcia-Molina and Kenneth Salem. 1987. Sagas. In Proceedings of the 1987 ACM SIGMOD International Conference on Management of Data. 249–259. https://doi.org/10.1145/38713.38742 [13] Seth Gilbert and Nancy Lynch. 2002. Brewer’s Conjecture and the Feasibility of Consistent, Available, PartitionTolerant Web Services. ACM SIGACT News 33, 2 (2002), 51–59. https://doi.org/10.1145/564585.564601 [14] Cary G. Gray and David R. Cheriton. 1989. Leases: An Efficient Fault-Tolerant Mechanism for Distributed File Cache Consistency. In Proceedings of the Twelfth ACM Symposium on Operating Systems Principles. 202–210. https://doi. org/10.1145/74850.74870 [15] Pat Helland. 2017. Life Beyond Distributed Transactions: An Apostate’s Opinion. Commun. ACM 60, 2 (2017), 46–54. https://doi.org/10.1145/3009826 [16] Joseph M. Hellerstein. 2026. Complete CALM: A Coordination Criterion for Specifications. https://doi.org/10. 48550/arXiv.2602.09435 arXiv:2602.09435 [cs.DC] [17] Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Transactions on Programming Languages and Systems 12, 3 (1990), 463–492. https://doi.org/10.1145/78969. 78972 [18] Amjad Ibrahim and Yong Li. 2026. Overlaying Governance: A Compositional Authorization Framework for Delegation and Scope in Agentic AI. https://doi.org/10.48550/arXiv.2606.03518 arXiv:2606.03518 [cs.AI] [19] Jin Jia, Zhiling Deng, Zhuangbin Chen, Yingqi Wang, and Zibin Zheng. 2026. MAS-FIRE: Fault Injection and Reliability Evaluation for LLM-Based Multi-Agent Systems. https://doi.org/10.48550/arXiv.2602.19843 arXiv:2602.19843 [cs.MA] [20] Michael B. Jones, Anthony Nadalin, Brian Campbell, John Bradley, and Chuck Mortimore. 2020. OAuth 2.0 Token Exchange. Technical Report RFC 8693. Internet Engineering Task Force. https://doi.org/10.17487/RFC8693 [21] Anuj Kaul, Qianlong Lan, and Pranay Gupta. 2026. Behavioral Governance for Autonomous AI Agents: The AgentBound Framework. https://doi.org/10.48550/arXiv.2606.30970 arXiv:2606.30970 [cs.AI] [22] Sajjad Khan. 2026. Token Budgets: An Empirical Catalog of 63 LLM-Agent Budget-Overrun Incidents, with an AffineTyped Rust Mitigation as a Case Study. https://doi.org/10.48550/arXiv.2606.04056 arXiv:2606.04056 [cs.SE] [23] Narayanan Krishnakumar and Ravi Jain. 1997. Escrow Techniques for Mobile Sales and Inventory Applications. Wireless Networks 3 (1997), 235–246. https://doi.org/10.1023/A:1019161318592

66

Zhu and Wang

[24] Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 (1978), 558–565. https://doi.org/10.1145/359545.359563 [25] Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. AddisonWesley. [26] Matthew D. Laws, Alina Oprea, and Cristina Nita-Rotaru. 2026. Attacks and Mitigations for Distributed Governance of Agentic AI under Byzantine Adversaries. https : / / doi . org / 10 . 48550 / arXiv . 2605 . 12364 arXiv:2605.12364 [cs.CR] [27] Collin Lee, Seo Jin Park, Ankita Kejriwal, Satoshi Matsushita, and John Ousterhout. 2015. Implementing Linearizability at Large Scale and Low Latency. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP ’15). Association for Computing Machinery, 71–86. https://doi.org/10.1145/2815400.2815416 [28] Jiapeng Li. 2026. Where Does Exactly-Once Live? Model, Harness, and Tool-Contract Effects on Duplicate Side Effects in LLM Agents. https://doi.org/10.48550/arXiv.2609.29095 arXiv:2609.29095 [cs.LG] [29] Torsten Lodderstedt, Justin Richer, and Brian Campbell. 2023. OAuth 2.0 Rich Authorization Requests. Technical Report RFC 9396. Internet Engineering Task Force. https://doi.org/10.17487/RFC9396 [30] Model Context Protocol. 2026. Authorization. https://modelcontextprotocol.io/specification/2026-0728/basic/authorization Protocol specification, version 2026-07-28; accessed 25 September 2026. [31] Bardia Mohammadi, Nearchos Potamitis, Lars Klein, Akhil Arora, and Laurent Bindschaedler. 2026. Atomix: Timely, Transactional Tool Use for Reliable Agentic Workflows. https://doi.org/10.48550/arXiv.2602.14849 arXiv:2602.14849 [cs.LG] [32] Niki Aimable Niyikiza. 2026. Attenuating Authorization Tokens for Agentic Delegation Chains. Internet-Draft draftniyikiza-oauth-attenuating-agent-tokens-01. Internet Engineering Task Force. https://datatracker.ietf.org/ doc/draft-niyikiza-oauth-attenuating-agent-tokens/01/ Work in Progress. [33] Patrick E. O’Neil. 1986. The Escrow Transactional Method. ACM Transactions on Database Systems 11, 4 (1986), 405–430. https://doi.org/10.1145/7239.7265 [34] Diego Ongaro and John Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In 2014 USENIX Annual Technical Conference. 305–319. https://www.usenix.org/conference/atc14/technical- sessions/ presentation/ongaro [35] Vladyslav Parakhin. 2026. The Bureaucracy of Speed: Structural Equivalence Between Memory Consistency Models and Multi-Agent Authorization Revocation. https : / / doi . org / 10 . 48550 / arXiv . 2603 . 09875 arXiv:2603.09875 [cs.MA] [36] Sunil Prakash. 2026. AIP: Agent Identity Protocol for Verifiable Delegation Across MCP and A2A. https://doi. org/10.48550/arXiv.2603.24775 arXiv:2603.24775 [cs.CR] [37] Kaiyang Qian, Xinmin Fang, and Zhengxiong Li. 2026. MPAC: A Multi-Principal Agent Coordination Protocol for Interoperable Multi-Agent Collaboration. https : / / doi . org / 10 . 48550 / arXiv . 2604 . 09744 arXiv:2604.09744 [cs.MA] [38] Ashay Raut. 2026. Transaction Tokens for Agents. Internet-Draft draft-araut-oauth-transaction-tokens-for-agents-02. Internet Engineering Task Force. https://datatracker.ietf.org/doc/draft- araut- oauth- transactiontokens-for-agents/02/ Active individual Internet-Draft; Work in Progress. [39] Jerome H. Saltzer and Michael D. Schroeder. 1975. The Protection of Information in Computer Systems. Proc. IEEE 63, 9 (1975), 1278–1308. https://doi.org/10.1109/PROC.1975.9939 [40] Igor Santos-Grueiro. 2026. Context-to-Execution Integrity for LLM Agents. https://doi.org/10.48550/arXiv. 2607.06000 arXiv:2607.06000 [cs.CR] [41] Igor Santos-Grueiro. 2026. Temporary Authority, Permanent Effects: Commit-Time Authorization for LLM Agents. https://doi.org/10.48550/arXiv.2607.10487 arXiv:2607.10487 [cs.CR] [42] Marc Shapiro, Annette Bieniusa, Nuno Preguiça, Valter Balegas, and Christopher Meiklejohn. 2018. Just-Right Consistency: Reconciling Availability and Safety. Data Science and Engineering 3, 4 (2018), 358–368. https: //doi.org/10.1007/s41019-018-0080-z [43] Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. 2011. Conflict-Free Replicated Data Types. In Stabilization, Safety, and Security of Distributed Systems (Lecture Notes in Computer Science, Vol. 6976). 386–400. https: //doi.org/10.1007/978-3-642-24550-3_29 [44] Reshabh K. Sharma, Linxi Jiang, Zhiqiang Lin, and Shuo Chen. 2026. PAuth: Precise Task-Scoped Authorization for Agents. https://doi.org/10.48550/arXiv.2603.17170 arXiv:2603.17170 [cs.CR] [45] Artem Trofimov, Igor E. Kuralenok, Nikita Marshalkin, and Boris Novikov. 2019. Delivery, Consistency, and Determinism: Rethinking Guarantees in Distributed Stream Processing. https://doi.org/10.48550/arXiv.1907. 06250 arXiv:1907.06250 [cs.DB] [46] Huacan Wang, Chaofa Yuan, Xialie Zhuang, Tu Hu, Shuo Zhang, Jun Han, Shi Wei, Daiqiang Li, Jingping Liu, Kunyi Wang, Zihan Yin, Zhenheng Tang, Andy Wang, Henry Peng Zou, Philip S. Yu, Sen Hu, Qizhen Lan, and Ronghao

Fault-Tolerant Budget Conservation in Agent Delegation

67

Chen. 2026. EpochX: Building the Infrastructure for an Emergent Agent Civilization. https://doi.org/10.48550/ arXiv.2603.27304 arXiv:2603.27304 [cs.AI] [47] Jinghan Xu, Longze Fan, Zeyuan Wang, Xinjin Li, and Hankai Liu. 2026. Beyond Single-Use Tokens: Durable Authorization State for Replay-Resistant LLM Agent Actions. https://doi.org/10.48550/arXiv.2608.01710 arXiv:2608.01710 [cs.AI] [48] Qing Ye and Jing Tan. 2026. Agent Contracts: A Formal Framework for Resource-Bounded Autonomous AI Systems. https://doi.org/10.48550/arXiv.2601.08815 arXiv:2601.08815 [cs.MA] Accepted for oral presentation at COINE 2026, co-located with AAMAS 2026. [49] Haoran Zhang, Adney Cardoza, Peter Baile Chen, Sebastian Angel, and Vincent Liu. 2020. Fault-Tolerant and Transactional Stateful Serverless Workflows. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, 1187–1204. https://www.usenix.org/conference/osdi20/presentation/ zhang-haoran [50] Genliang Zhu and Chu Wang. 2026. Explanation-Bound Tool Execution for AI Agents: Server-Verified Action Claims Without Trusting Model Rationales. https://doi.org/10.48550/arXiv.2607.25364 arXiv:2607.25364 [cs.AI] [51] Genliang Zhu and Chu Wang. 2026. Intent-Governed Tool Authorization for AI Agents. https://doi.org/10. 48550/arXiv.2606.22916 arXiv:2606.22916 [cs.AI] [52] Genliang Zhu and Chu Wang. 2026. Versioned Transitive Dependency-Closure Binding and Operation-Time Effect Governance for Agent Skills: ClosureBound. https : / / doi . org / 10 . 48550 / arXiv . 2609 . 05920 arXiv:2609.05920 [cs.CR] [53] Genliang Zhu, Chu Wang, Ziyuan Wang, Zhida Li, and Qiang Li. 2026. OpenPort Protocol: A Security Governance Specification for AI Agent Tool Access. https://doi.org/10.48550/arXiv.2602.20196 arXiv:2602.20196 [cs.CR] [54] Siyuan Zhuang, Stephanie Wang, Eric Liang, Yi Cheng, and Ion Stoica. 2023. ExoFlow: A Universal Workflow System for Exactly-Once DAGs. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23). USENIX Association, Boston, MA, 269–286. https://www.usenix.org/conference/osdi23/presentation/ zhuang

Related documents

• Fault-Tolerant Budget Conservation in Distributed Multi-Agent Delegation#1154972
• Bounded Agents: Delegation Security for Multi-Agent AI Systems#617017
• Bounded Agents: Delegation Security for Multi-Agent AI Systems#616517
• Bounded Agents: Delegation Security for Multi-Agent AI Systems#459567
• Decomposition Buys Integrity, Not Yield#1123825