Bounded Loops: Pre-Run Spend Bounds, Proved Termination, and Verified Completion for Agent Harnesses
Varun Pratap Bhardwaj (Qualixar) with Garima Singh and Arun Pratap Bhardwaj define a bounded loop, a worker plus an independent gate the worker cannot write to plus a declared budget, and prove termination, completion and spend guarantees for graphs of such loops.
Ask this paper
Problem. In common agent frameworks a step ends when the agent's own output says it is done, and checkers usually live in the same codebase as the work.
Three proved guarantees. Termination under repair with a closed-form worst-case attempt count if the repair budget is global; no node reaches DONE without a gate verdict in an append-only hash-chained ledger; and a spend ceiling enforced inside each attempt.
Two gate defects. Vacuity (the check passes when the thing checked is absent) and self-attestation (the subject supplies the value being checked).
Audit. On a 69-loop catalogue the instrument found 47 vacuous gates in shipped, reviewed code; repaired gates showed no false accepts over 209 mutants, but a fresh mutant family exposed a 23.3% false-accept rate.
Release. Engine, catalogue and mutant corpus are Apache-2.0.
Abstract
In mainstream agent frameworks, a step ends when the agent's own output says it has finished. Durable-execution platforms bound retries and time, but their checker conventionally lives in the same codebase as the work: a discipline the deployment is trusted to keep, not a property the harness enforces. We state what an agent harness must guarantee, prove it, and build the instrument that measures whether a harness delivers it. A bounded loop is a worker, an independent gate the worker cannot write to, and a declared budget; a bounded-loop graph composes them with a repair relation that lets a downstream failure re-run a finished upstream node. Three guarantees follow. It finishes: termination holds under repair, with the worst-case attempt total in closed form, if the repair budget is global not per node. It does not drift: no node reaches DONE without a gate verdict in an append-only hash-chained ledger, proved from control flow, since repair leaves no topological order to induct along. It does not overspend: the ceiling is enforced inside an attempt, not between attempts. Gates are measured against a two-tier held-out mutant corpus. We characterise two classes that let a sound-looking check pass anything: vacuity, satisfied by the absence of the thing checked, and self-attestation, where the subject supplies the value the check is applied to. On a 69-loop catalogue the instrument found 47 vacuous gates in shipped, reviewed code. Against the repaired gates it reports no false accepts over 209 destroying mutants ($α\le 1.8\%$, Wilson 95%); that figure is saturation, not quality: freezing the gates and applying a fresh operator family recovers a 23.3% false-accept rate where the exhausted corpus reported none. A rate belongs to a specific gate; the apparatus, not our number, is the contribution. Engine, catalogue and corpus are Apache-2.0.