cs.SEAug 20, 2026
SaveBounded Loops: Pre-Run Spend Bounds, Proved Termination, and Verified Completion for Agent Harnesses
Organizations: Qualixar / Independent Researcher, India · Independent Researcher, India
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 (, 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.
Figures & tables
Figure 1: One bounded loop. The worker writes only ; the gate reads the artifact and the anchors, never the worker’s transcript, and the worker’s write to an anchor is refused rather than merely discouraged ( Definitions 3.6 and 3.3 ). The verdict, not the worker, selects the outgoing edge. incapacity is omitted here and treated separately in Figure 4 , because the whole argument of Section 4 is about how narrow that third edge must be.
Figure 2: F1 — a bounded loop, end to end, with the trust boundary drawn. Everything above the controller is declared and readable before the run ( Corollary 5.1 ). Everything inside the dashed region is written by the party under judgement. The two solid paths into the ledger are the only ones that can produce a completion: the gate reads the workspace and records a verdict. The dotted path is the worker’s own account of itself — it is stored, and it reaches no guard in the procedure ( Lemma 7.1 ). The ledger and the receipt sit outside the untrusted region: they are written beside the loop package, not inside the workspace, so an agent cannot edit the record that judges it.
Figure 3: M3 — which facts can decide a completion. Shaded boxes are authored by the party under judgement. Solid arrows are the only inputs any guard in the procedure reads; the worker’s self-report and its transcript reach the ledger and stop there. This is the drift guarantee ( Theorem 7.1 ) as a picture: an agent cannot route to done by asserting it, because no branch consults the assertion. The adversarial test for this claim inverts it — a runner that always claims completion, paired with a gate that always refuses, must reach halt and never done .
Figure 4: The verdict trichotomy of Theorem 4.1 . The single distinguishing test is ownership, read off the loop’s own forbid set rather than inferred from the failure. Every path into incapacity passes through a file the worker was never permitted to write, which is what makes Corollary 4.1 hold.
Figure 5: F2 — one attempt, with every declared bound shown where it is actually enforced. Heavy boxes are the points that can end a run; the annotations name what each reads. Two of the five checks happen before a turn, which is why the ledger flags whether an attempt was spent — without it, a ceiling halt at writes an -th row and utilisation computed from the receipt reads for a bound that held exactly ( Definition 13.1 ). The clamp on the worker turn is the one enforcement point that was added last; every other box on this diagram predates it.
Figure 6: F4 — the spend contract on a time axis. The solid box is what the manifest declares. is dashed because it is the one term outside the declaration: a gate is never cut short, since terminating a check part-way yields no verdict and a check that could not run must never be recorded as having judged. A verdict costing a few seconds past the ceiling is worth strictly more than no verdict, so we pay it and publish it rather than buying a tidier inequality with an unusable outcome.
Figure 9: F3 — two edge kinds, one budget. Solid edges carry data and form a DAG. The dashed edge is a repair : it points backward, and on ’s failure it returns and everything reachable from to pending for another pass. The data graph stays acyclic; the repair relation does not, and that is the whole difficulty ( Definition 3.16 ). On the right is the construction a per-node repair budget admits. repairs , repairs , each decrements only its own counter, and each sees credit remaining after every round — so the run never terminates while every declared bound is respected. One global counter, decremented across the whole graph and never reset at a boundary, is what makes Theorem 5.2 provable, and bounding repairs per node — as every other budget in this system is bounded — is precisely what breaks it. The engine now refuses a plan whose nodes disagree about the budget rather than adopting the first value it finds, because there is no correct way to choose among conflicting global bounds.
| Workload | Predicted | Observed | Terminal | |
|---|---|---|---|---|
| 1 | 1 | 1 | done | 0.1 |
| 2 | 2 | 2 | done | 0.2 |
| 3 | 3 | 3 | done | 0.3 |
| 4 | 4 | 4 | done | 0.4 |
| 6 | 6 | 6 | done | 0.6 |
| 8 | 8 | 8 | done | 0.8 |
Table 1: Bound utilisation against a declared ceiling of . Predicted equals observed in 9 of 9 cases. rises linearly with workload up to the ceiling and then caps at exactly : past the ceiling the run halts rather than borrowing an eleventh attempt.
| Productive attempts | Observed | Attempts saved | |
|---|---|---|---|
| 0 | 3 | 3 | 7 |
| 1 | 4 | 4 | 6 |
| 2 | 5 | 5 | 5 |
| 4 | 7 | 7 | 3 |
Table 2: The soft bound with , . Predicted equals observed in 4 of 4 cases, and every run halted on no-progress rather than on the hard ceiling. “Attempts saved” is the difference against spending the full declared cap.
Figure 10: Layering. Dependencies point inward and only composition may name a concrete adapter, checked by an AST walk over every module. Below the engine, the receipt log is the single durable artifact and each surface is a view over it, so two surfaces cannot disagree about a run.
| Reads as a judgement call | What the gate actually computes |
|---|---|
| objective is measurable | a numeric target , a non-empty unit , and a deadline matching ˆ\d{4}-\d{2}-\d{2}$ |
| prose is readable | mean words per sentence |
| runbook is complete | seven required heading strings are present, and each has content beneath it |
| privacy policy is complete | six required disclosure phrases occur in the normalised body |
Table 3: Requirements that sound as though they need a judge, and the decidable predicate each was reduced to. The reduction is not free and it is not always faithful — the second row is a proxy and nothing more, and the third row’s “ and each has content beneath it” clause is there because the version without it passed a runbook with all seven headings and nothing under any of them ( Section 12.3 ). The claim is not that judgement is unnecessary, but that it belongs in authoring the predicate, where it is written down once and can be audited, rather than in the loop, where it is re-exercised on every attempt and recorded nowhere.
| Tier 1 | Tier 2 | |
| mutants | 233 | 38 |
| destroying (label incorrect ) | 171 | 38 |
| preserving (label correct ) | 62 | 0 |
| judged | 233 / 233 | 38 / 38 |
| gate errors ( incapacity ) | 0 | 0 |
| false accepts over destroying | 0 / 171 | 0 / 38 |
Table 4: The held-out mutant corpus after the defects of Sections 12.3 and 12.5 were fixed. Each rate has its own denominator and they are not the same number. can only be measured on mutants labelled defective; only on mutants labelled conforming. Reporting both against the full 233 and 38 would imply every mutant was checked for both, and for Tier 2 would assert over an empty set ( Remark 12.1 ).
Figure 11: Tier-1 coverage by gate kind. Before the fix the corpus resolved only command gates, so every jsonschema , pytest and composite loop produced no verdict and appeared in no count — not as errors, not as exclusions, absent. The guard against unprincipled exclusion inspected only loops already outside the eligible set, and both predicates defining that set read a command gate’s argv, so it was vacuous over exactly the loops that had gone missing. The grey band is the 11 loops excluded for the stated reasons of Section 12.1 .
| Direction | Defect | Disclosed? |
| false accept | data-processing terms: substring match inside a denial | yes |
| false accept | runbook: required headings present, no content under any | yes |
| false accept | alt-text: attribute absent, image passes | yes |
| false accept | citations: pattern derived from the reference set ( Example 8.2 ) | no |
| false reject | conventional commits: ! breaking-change marker refused | no |
| false reject | dependency pinning: extras and spacing legal under the spec refused | no |
Table 5: The six defects found by hand, by direction and by whether the gate’s own documentation disclosed the behaviour. Three of four false accepts were disclosed; neither false reject was. The sample is too small to carry a rate, and the pattern is nonetheless the one we would predict.
| loop | how the gate was evaded |
|---|---|
| test-presence-per-module | a test with no import and no assertion; a test importing a different module; a test asserting on a standalone calculation; renaming the source so the import orphans |
| nda-required-clauses , gdpr-dpa-terms | the required heading kept, the obligation underneath it negated |
| okr-measurable , dependency-pinning , conventional-commits | the offending item deleted rather than repaired |
| dependency-pinning | pinned to a version that was never released; pinned below the file’s own stated floor |
| conventional-commits | subject substituted wholesale; a docs change typed build ; an already-conforming line rewritten |
| secret-scan-keyless | credential split across a concatenation; password renamed to passwd ; the config deleted rather than moved to the environment |
Table 6: The 16 Tier-2 defects. Every one satisfies the requirement as literally stated and defeats it in substance — the failure mode a mechanical operator cannot construct, because constructing it requires understanding the purpose.
| estimand | anytime-valid | fixed-time |
|---|---|---|
| — mean propensity of the attempts in the log | 1.0000 | 0.9590 |
| population marginal, 1 node pooled | 0.8333 | 0.6067 |
| population marginal, 6 nodes pooled | 0.9717 | 0.8450 |
| population marginal, 30 nodes pooled | 0.9983 | 0.9783 |
| population marginal, heterogeneous ( ) | 0.8267 | 0.6000 |
Table 7: Empirical coverage at nominal 95%, by estimand. The sequence is anytime-valid for ; coverage of a population marginal is a different quantity that rises with the number of independent nodes pooled and falls with their heterogeneity.
| loop | gate kind | provider | terminal | attempts to done | wall (s) |
|---|---|---|---|---|---|
| citation-existence-check | command | A | done | 1 | 26.6 |
| B | done | 1 | 27.5 | ||
| C | done | 1 | 54.9 | ||
| D | done | 1 | 86.6 | ||
| bug-fix-red-green | pytest | A | done | 1 | 24.3 |
| B | done | 1 | 36.0 |
Table 8: Cross-model convergence: four independent provider models, four loops, one gate each. Letters are assigned within each loop by ascending wall time and do NOT identify a provider across rows ; letters are not mapped to vendor names because sixteen observations cannot support a product comparison and a named table would invite one. Wall time is reported only to show the arms differ in something while agreeing on everything the gate decides, and must not be read as a per-provider figure. Tokens are unavailable through this path and are not estimated.
| Tier 1 (saturated) | E7 (post-freeze) | |
| loops covered | 57 | 54 |
| destroying mutants | 171 | 60 |
| preserving mutants | 62 | 35 |
| gate errors ( incapacity ) | 0 | 0 |
| false accepts | 0 / 171 | 14 / 60 = 23.3% |
| Wilson 95% |
Table 9: The saturated corpus and the post-freeze corpus against the same frozen gates. The left column is what an exhausted operator set reports; the right is what a fresh one finds behind it. The comparison is the result, not either column. A reader should take from this that a gate suite reporting zero against the corpus that repaired it has established exhaustion and not quality and that the remedy is another operator family, which is cheap, rather than more mutants from the same one, which is free and worthless.
Appendix figures & tables5 assets
Supplementary material from the paper’s appendix.
Appendix
| Pattern | n | Verdict is | Choose it when |
|---|---|---|---|
| Schema | 10 | a document validates against a declared schema | the requirement is about shape , and the schema is the contract a consumer already relies on |
| Predicate | 44 | a purpose-built program exits zero | the requirement is about content and reduces to a computation over one artifact |
| Executable spec | 9 | a test suite passes | the requirement is behavioural, and the artifact is code that can be exercised |
| Conjunction | 3 | every child gate passes | two independent obligations must both hold, or a model judge is being admitted ( Theorem 10.3 ) |
| External tool | 2 | a third-party analyser reports clean | a mature checker already exists and re-implementing it would be worse |
Table 10: The five gate patterns the catalogue uses, with the count of loops choosing each. The distribution is itself a finding: two thirds of real requirements were served by a purpose-built predicate over a single artifact, not by a schema and not by a test suite. An author’s instinct to reach for a schema generalises less far than the catalogue suggests it should.
| Failure mode | The gate passes because | Evidence |
|---|---|---|
| Absence | the artifact it quantifies over is gone, so every universal claim holds | 47 instances; Example 8.1 |
| Hollowing | the artifact keeps its structure and loses its content, and the gate checked structure | 14 instances; Section 12.12 |
| Self-derived scope | the checker builds its search pattern from its own reference data, so anything outside it is never examined | Example 8.2 |
| Misfiled incapacity | a diagnosis the gate reached was returned as an inability to diagnose, so the loop stopped instead of retrying | 84 of 233 mutants; Section 4 |
| Scope blindness | the measurement resolved one gate kind and silently returned nothing for the others | 24 loops; Figure 11 |
| Prompt-only obligation | the requirement was stated to the worker and never to the gate | Example 8.1 |
Table 11: Seven ways a gate passes work it should refuse. Four are properties of a gate; rows four, five and seven are properties of the machinery around gates, and we keep them in the same table deliberately, because in this project they cost more evidence than the gate defects did. The counts in the third column are not commensurable: the first five come from instrumented measurement over the catalogue, the last from a release audit whose grade is stated in Remark 9.2 .
| domain | gate kind | n | representative requirement |
|---|---|---|---|
| legal / contract | command | 9 | required clauses present and not negated in the body ; citations resolve against shipped reference data |
| finance | pytest, command | 8 | three-way invoice match; a ledger reconciles and no seeded transaction disappeared |
| clinical | jsonschema | 5 | a note carries every required field with the stated types |
| security | command | 7 | no credential-shaped literal, including across string concatenation and renamed keys |
| infrastructure | command, external | 8 | resources declare required tags; scanned policies pass |
| software eng. | pytest, command | 14 | a failing suite goes green; every module has a test that imports it and asserts on what it imported |
Table 12: Catalogue composition by domain. The count column does not sum to 69, and should not. A loop declares one or more domain tags — 28 of the 69 declare more than one, so the tags total 96 across 24 distinct labels — and the groupings above merge related tags for readability. The authoritative count of loops is 69, obtained from the manifests and pinned by a packaging test; the authoritative partition by gate kind , which is disjoint and does sum to 69, is in Section 12.1 . The requirements in the right-hand column are stated as they are after the fixes of Sections 12.3 and 12.5 .
| reason | n | why, and how it is verified |
|---|---|---|
| unshipped SDK | 4 | the runner needs an agent framework the package does not vendor. Probed against the live environment in both directions — a loop claimed excludable that in fact runs fails the check, as does the converse |
| external tool | 3 | the gate invokes a security scanner not assumed present |
| negative requirement | 1 | the requirement is that an artifact must not acquire a property; a mutation that introduces the property is a conforming input, not a defect, so the operator set cannot construct a labelled defective case |
| Tier-1 inexpressible | 3 | the requirement is a relation between artifacts. A single-artifact operator has no notion of consistency across two files. Covered by Tier 2, which found four defects in one of them |
Table 13: Exclusions. This table is the denominator: every rate in the paper is over loops.
| result | command, and what it pins |
|---|---|
| E1, E2 — Table 4 | uv run pytest tests/evaluation The corpus is a test: a regression in any gate fails the build rather than moving a number in a paper. |
| Blindness — Theorem 10.1 | ... test_generator_is_blind.py AST assertion over every generator module. |
| Tier-2 prompt integrity | ... test_tier2_authoring_was_blind.py Recomputes each mutant’s authoring digest from the repository. |
| E3 — Table 7 | ... test_reported_interval_estimand.py Includes the three shrink/shift controls that must fail if the interval were vacuous. |
| E4 | ... tests/graph/test_gate_gaming.py Adversarial workers. |
| E6 | ... test_no_test_asserts_only_inside_a_loop.py Carries a deliberately vacuous case it must flag. |
Table 14: Reproduction map.