发表机构
Accentrust; Georgia Institute of Technology; University of Illinois Urbana-Champaign（Accentrust; 佐治亚理工学院; 伊利诺伊大学厄巴纳-香槟分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对分布式多智能体委托中的预算超支问题，提出基于独占托管信用和操作预留的容错预算保持机制，通过形式化证明与实验验证，确保在故障场景下预算界限不被突破。
AI 中文摘要
资源限制正成为AI智能体的授权边界，这些智能体在并发且易故障的工作者之间委托工作。当回复丢失、效果在超时后完成、消息重复、分支分区或DAG连接别名化一个谱系时，父子分配约束、仿射对象和分布式托管本身并不能防止超支。我们形式化了分布式多智能体委托的容错预算保持。预算是量化的资源向量，由通过委托DAG移动的独占托管信用表示。在分派前，分支将信用转换为绑定到谱系、纪元、规范化效果、最大费用、接收者和幂等键的操作预留。它持久化带有隔离的签名分派许可；网关在首次接受前验证该许可。不确定的效果在认证结算、有围栏的权威无效果证明或永久退役之前保持计费。我们证明了在明确的中介、持久性、认证、规范化和网关假设下的所有权分区、账本和效果保持、后代非放大、至多一次结算、晚完成安全性和分区隔离。一个不可区分性结果表明，分区本地可用性需要独占预分配。有界TLA+检查、独立的JavaScript探索器和崩溃注入的双进程SQLite实验验证了声明范围，并检测到超时退款和历史证书验证突变体。该机制在评估的崩溃、重试、重复、分区、连接和晚完成调度中保持已发行的预算界限。
英文摘要
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.
Comments67 pages, 3 figures, 17 tables, 4 algorithms, and 3 listings. Includes formal proofs, bounded model checking, mutation analysis, and crash-injected two-process SQLite experiments
