From Bounded Tools to Bounded Agents: Execution-demand Certificates for Compositional Resource Containment

Bala Subramanyan, Verifoxx, United Kingdom

ABSTRACT

Resource bounds established for individual tools do not compose automatically across autonomous control. A tool-using agent may transform each returned observation into retry, fan-out, fallback, or delegated work;cumulative resource demand therefore depends on the controller–tool feedback closure rather than on anyinvocation in isolation. This paper introduces Execution-Demand Hypergraphs (EDHs), a compositionalabstraction in which nodes carry independently certified local bounds and observation-conditioned hyper-edges encode multisets of successor obligations. The induced monotone demand operator has a least fixedpoint equal to the exact worst-case local-bound demand represented by the abstraction, yielding a finitecertificate if and only if that demand is finite. A sound abstraction theorem transfers EDH certificates toconcrete controller executions, and an exact extractor is established for a core controller language withsequence, choice, retry, fan-out, delegation, and controlled recurrence. EDH-Check matched independentreference semantics on all 16 finite hand-designed models and 20,000 generated controllers; observationand recurrence stress tests further exercised the soundness boundary. EDH thus provides a reusable bridgefrom component-level resource certification to whole-agent resource containment.

KEYWORDS

Tool-using AI, formal verification, resource analysis, autonomous agents, WebAssembly.