PaperlayerView exact revision on arXiv

Source-linked AI summary

Runtime Authorization of Self-Generated Subgoals in Long-Horizon Tool-Using AI Agents

Genliang Zhu, Chu Wang

arXiv:2610.04975v1cs.AIcs.CR

TL;DR

Long-horizon agents can change goals and compose subgoals, while per-tool permission checks do not establish that the evolving task remains authorized. The paper checks structured, version-bound goal mutations and protected effects against a root contract; it reports formal safety results and supports useful replanning within its registered domain.

  • Problem

    Per-tool permission checks cannot establish that an evolving goal graph remains within the principal-approved task, particularly when authorization depends on action composition or changing state.

    Source: §1 · p. 1, §1.2 · p. 2

  • Method

    The mechanism checks version-bound structured goal mutations against the active contract and mediates protected effects against the active goal and residual permitted trace language.

    Source: §1.3 · p. 2, §4.4 · p. 11

  • Results

    The formal results establish root-policy safety under stated assumptions and preserve required terminal predicates when the authorized goal graph closes.

    Source: §4.6 · p. 12

  • Takeaways & Limitations

    Within the stated scope, goal creation, replacement, delegation, and joining are authorization events, while each protected effect remains subject to mediation.

    Source: §11 · p. 29

    The secondary study is a single-host characterization of synthetic one-factor-at-a-time fixtures and does not estimate production throughput or performance on unseen contracts.

    Source: §10 · p. 28

Abstract

from arXiv · show

Long-horizon tool-using AI agents create subgoals, replan, delegate work, and compose sibling results. Per-tool permission checks cannot establish that a changing goal graph remains within the principal-approved task. We address this authorization gap in a finite structured domain with one principal and one authorization root. Each proposed goal-graph mutation carries a version-bound witness that its continuation traces, resources, obligations, invariants, and closing condition refine the active root contract; every protected effect is rechecked at an atomic commit boundary. Free-form goal text supplies no authority. We prove trace-policy and modeled forbidden-state preservation under explicit mediation, abstraction, freshness, and atomicity assumptions, plus conditional root-success preservation, a separation result for memoryless allowlists, exact finite-domain decidability, and universal-safety monotonicity under sound abstraction refinement. An executable model explores 340 states and 419 transitions. Across 96 matched cases covering 25 structural schemas, the complete mechanism commits zero forbidden states in 48 drifted cases and completes all 48 benign counterparts. Two public upstream runtime paths execute 258 native dispatches across 32 cases, with every case-level decision and receipt chain matching. A frozen host-local study covers 129 synthetic one-factor-at-a-time cells, all matching fixed decisions and reasons. A history-aware continuation comparator blocks every modeled bad trace prefix but commits all operations in 11 cases whose violations lie in typed resources, freshness, or explicit-join evidence outside its trace projection. Within the registered structured domains, runtime authorization preserves useful replanning while preventing self-generated subgoals from becoming a source of new authority.

1 Introduction

Long-horizon agents can change plans and compose subgoals, so checking each tool call alone cannot establish that the evolving goal graph remains within the principal-approved task. The paper proposes version-aware authorization of structured goal changes and protected effects, without treating free-form goal text as authority.

1 Introduction

  • Per-tool checks cannot determine whether a changing goal graph still implements the task the principal authorized, especially when policy depends on the composition of actions.Locally permitted writes, recovery actions, or delegated tasks can collectively expand resources or replace a completion condition with an easier proxy.Source: §1 · p. 1

1.1 Problem statement

  • The paper treats child creation, replacement, delegation, and same-root joining as authorization events, using structured contracts rather than free-form text as authority.An upstream component may translate a request, but the principal or trusted policy service must approve the structured contract used for enforcement.Source: §1.1 · p. 2

1.2 Why local authorization is insufficient

  • A memoryless checker sees the same locally permitted production-routing action in safe and unsafe histories, although the committed prefix and outstanding review obligation make the decisions differ.A final-state checker detects the violation only after both effects commit; transition authorization rejects the unsafe replacement before routing becomes reachable.Source: §1 · p. 1, §1.2 · p. 2

1.3 Approach

  • A separate checker evaluates typed goal-graph mutations against the active contract and version, while protected effects are checked against the active goal and residual trace language.Relevant policy or state changes suspend execution for reauthorization; only an Allow activates the proposed transition.Source: §1.3 · pp. 2–3

1.4 Contributions

  • The contributions include formalizing goal changes as authorization-relevant state changes and proving safety under stated assumptions, with conditional terminal-predicate preservation and finite-domain decision procedures.The evaluation includes matched benign and drifted workflows, public tool-execution paths, and a separate 129-cell synthetic study.Source: §1.4 · p. 3

2 Motivating Counterexample and Threat Model

The motivating deployment trace shows why locally permitted effects can still violate a task contract when their order leaves an obligation outstanding. The paper models the threat and states safety, conditional success, and scope boundaries for its structured single-root setting.

2.1 A matched pair with identical local permissions

  • The same locally permitted production-routing action requires different decisions depending on the committed prefix and whether review has been recorded.The executable fixture rejects the drifted goal replacement before routing becomes reachable because its completion condition and continuation traces do not refine the parent.Source: §2.1 · p. 4

2.2 System boundary

  • The model represents a trusted principal, a finite structured root contract, and an agent-created goal graph; protected external effects cross a commit adapter.Effects outside the registered mediation boundary are outside the modeled execution.Source: §2.2 · p. 4

2.3 Adversary

  • The adversary may manipulate proposed goals, memory, worker output, retries, ordering, and effect arguments, but cannot compromise the trusted checker or bypass the registered effect boundary.Fail-closed authorization leaves denial of service possible when evidence is incomplete.Source: §2.3 · p. 5

2.4 Security and functional properties

  • The primary property is prefix safety for committed effects and admitted continuations; root-success preservation is conditional on valid witnesses, invariant preservation, discharged obligations, and root closure.The model does not require the agent to find a plan or terminate.Source: §2.4 · p. 5

2.5 Scope

  • The claims are limited to finite structured domains with one principal and one authorization root, excluding natural-language policy compilation, unmodeled physical consequences, and compromised trusted components.Combining independent authorization roots is also outside scope.Source: §2.5 · p. 5

3 Background and Related Work

The paper builds on trace enforcement, hierarchical planning, refinement, and tool-agent security research, while focusing its contribution on authorization of runtime changes to a structured goal graph. Its distinction is the connection between versioned refinement evidence for graph mutations and mediation of each protected effect.

3 Background and Related Work

  • The work connects reference monitoring, trace-policy enforcement, hierarchical planning, and safety evaluation to the question of authorizing runtime changes to an agent-produced goal graph.Prior work supplies sequence-aware policies and planning formalisms; the open systems question is how to connect a changing goal graph to enforcement.Source: §3 · p. 5, §3.1 · p. 6

3.1 Authorization and trace enforcement

  • Temporal policies and online intervention are established; the paper instead checks proposed changes to the authorized goal structure and modeled continuations before new protected effects become reachable.Finite bad prefixes can justify blocking, but preventing them does not guarantee eventual task progress.Source: §3.1 · p. 6

3.2 Hierarchical planning and refinement

  • Hierarchical planning and refinement explain structured decomposition, but do not decide whether an untrusted runtime proposal remains authorized or whether its evidence is current after policy or state changes.The paper uses a registered finite transition model and ordinary refinement obligations as inputs to authorization, rather than introducing a planning formalism.Source: §3.2 · p. 6

3.3 Tool-using-agent security and long-horizon evaluation

  • Tool-agent benchmarks and security studies provide stateful, multi-step tasks and adversarial trajectories, but success in one environment is not treated as evidence of universal safety.The cited environments motivate independent task origins and state-based oracles in the evaluation.Source: §3.3 · pp. 6–7

3.4 Runtime controls for language-model agents

  • Related runtime controls cover behavioral constraints, temporal auditing, capabilities, plan verification, drift monitoring, and contracts, constraining novelty claims based on those mechanisms alone.The comparison distinguishes initial plan verification from authorization of graph changes introduced during execution, including invalidation and reauthorization after version changes.Source: §3.4 · p. 7

3.5 Residual contribution boundary

  • The residual contribution connects these foundations through versioned, machine-checkable refinement evidence for goal mutations and commit-time checks of protected effects against the active goal and residual trace.The stated boundary excludes arbitrary natural-language entailment, independent roots, and unmodeled real-world consequences; Table 1 compares control objects and enforcement points rather than ranking systems.Source: §3.5 · p. 7, Table 1 · p. 8

4 Structured Goal-Transition Semantics

The section models goal-graph changes as authorization events that must refine a principal-approved root contract, with protected effects checked against fresh evidence. Its results establish conditional safety and root-success properties, plus finite-domain decision and abstraction claims.

4.1 Transition system and root task contract

  • A root contract fixes permitted traces, forbidden states, required closure, resource bounds, and unresolved obligations; current policy and relevant-state versions determine witness freshness.The contract must be supplied or explicitly approved by the principal; deriving it from unrestricted natural language is outside the model.Source: §4.1 · p. 9

4.2 Versioned goal graph and same-root composition

  • The finite acyclic goal graph represents refinements and sibling precedence; sibling effects become jointly executable only through an explicit join checking registered interleavings.Graph edits stale other sibling-path witnesses, and delegation remains within the same authorization root; cross-root joins are outside the model.Source: §4.2 · p. 10

4.3 Transition witnesses

  • A transition witness binds the proposed edit to current versions and proves continuation, policy, forbidden-state, frame, resource, obligation, and parent-closure constraints.A stale version requires reauthorization, while an unsafe abstract path that is not concretely established yields Indeterminate rather than Allow.Source: §4.3 · pp. 10–11

4.4 Operational rules and invalidation

  • Authorization installs a checked graph revision, while each protected effect is committed only against a current selected-path witness and modeled successor.Relevant out-of-band changes suspend execution and invalidate dependent witnesses; validated root closure additionally requires resolved descendants, permitted completion, discharged obligations, and the root predicate.Source: §4.4 · pp. 11–12

4.5 Assumptions and claim boundary

  • The guarantees depend on complete mediation, faithful effect normalization, sound modeled transitions and checks, atomic freshness, and a well-formed initial root; they do not cover arbitrary natural-language entailment or unmodeled physical consequences.The safety theorem is conditional: it does not itself establish that a concrete implementation satisfies its fidelity, soundness, checker, and atomicity premises.Source: §4.5 · p. 12, §4.6 · p. 12

4.6 Results

  • Under A1–A8, every committed protected effect uses a fresh same-root witness and produces no modeled root-forbidden successor.The theorem also preserves the permitted root trace language and prevents installed goals from exceeding root and parent resource envelopes or discarding unresolved obligations.Source: §4.6 · p. 12
  • Theorem 2 guarantees the root closing predicate only when the finite goal graph closes under the stated assumptions and validated leaf closure.It does not guarantee termination, finding a closing plan, or avoiding Indeterminate decisions.Source: §4.6 · p. 12
  • The results also establish memoryless-allowlist insufficiency, exact finite-domain authorization, and universal-safety monotonicity under sound abstraction refinement.The executable model corroborates selected obligations but does not independently verify the full transition system, freshness lifecycle, or reference implementation.Source: §4.6 · p. 13

5 Runtime Authorization Protocol

The protocol separates authorization of goal-graph mutations from authorization of protected effects. Typed proposals are checked against current versions and the root contract, and each effect must pass a fresh commit-boundary check.

5 Runtime Authorization Protocol

  • The monitor exposes typed goal mutations and effect operations; a planner’s explanation or earlier allow decision cannot bypass the later commit check.Proposals are requests rather than persisted goal state, and transition witnesses bind the relevant goal digests, trace, versions, checker profile, and decision.Source: §5 · p. 14, §5.1 · p. 14

5.2 Transition decision

  • A transition decision checks graph structure and freshness, then evaluates typed resources, obligations, and reachable continuations; unsafe uncertainty never becomes Allow.Concrete counterexamples return Deny, while an unsafe path found only in a sound over-approximation returns Indeterminate.Source: §5.2 · pp. 14–15, §5.6 · p. 16

5.3 Effect reservation and commit

  • Effect execution reserves a normalized operation for one current context, then commits that exact effect and records its outcome at one linearization point.Version changes invalidate outstanding reservations; retries return the retained receipt, while a conflicting retry is denied.Source: §5.3 · pp. 15–16

5.4 Delegation, joins, and replanning

  • Delegation changes the worker, not the root; replanning checks a replacement against the parent’s current residual language, and sibling effects require an explicit join.Cancellation removes future effects but is not completion evidence; recovery requires a separately checked replacement.Source: §5.4 · p. 16

5.5 Receipts and auditability

  • Canonical hash-linked receipts let an independent checker reconstruct graph, trace, versions, obligations, and decisions without importing the runtime checker.The independent path makes auditability a second implementation path rather than a copy of the decision function.Source: §5.5 · p. 16

5.6 Fail-closed behavior

  • Unknown fields, missing observations, unsupported predicates, unbounded continuations, stale versions, or abstraction ambiguity yield Indeterminate or Reauthorize, not authority.A deployment may seek a more precise abstraction or principal approval, but uncertainty cannot be silently treated as authorization.Source: §5.6 · p. 16

6 Reference Implementation

The reference implementation realizes a finite, provider-independent authorization profile with typed state, a transition checker, a monitor, and a separate receipt auditor. It also connects two public runtime paths and retains the materials needed to reproduce its evidence.

6 Reference Implementation

  • The artifact is provider-independent: runtimes connect through adapters, while authorization decisions and deterministic state oracles remain outside the model.Its executable evidence uses deterministic finite state transformers, although the mathematical model permits nondeterministic transitions.Source: §6 · p. 16, §6.1 · p. 17

6.1 Typed state and trace representation

  • Goals use typed finite state and trace representations; stored maximal completion traces define permitted continuations through their prefix closure.Canonical serialization rejects duplicate or unknown security-relevant fields and hashes the resulting bytes; hashes do not authenticate callers.Source: §6.1 · pp. 16–17

6.2 Transition checker

  • The checker enumerates registered continuations, reachable prefix states, explicit join shuffles, and closing conditions, while failing closed when registered bounds are exceeded.Success refinement is checked separately: parent closure requires its predicate, inherited obligations to be discharged, and active frame predicates preserved.Source: §6.2 · pp. 17–18

6.3 Reference monitor and store

  • The reference monitor serializes updates and binds effect reservations to expected trace and state versions before checking and committing the normalized effect.Concurrent or distributed deployments must preserve the same freshness and linearization conditions.Source: §6.3 · p. 18

6.4 Independent checker

  • A separate audit checker reconstructs receipts, graph, trace, versions, and decisions without importing the runtime’s policy-decision or reachability functions.Semantic mutations recompute outer hashes, so rejection cannot rely solely on detecting a broken checksum.Source: §6.4 · p. 18

6.5 Runtime adapters

  • Two adapters route native AgentDojo and τ-bench tool calls through a local broker to the same deterministic service; witnesses remain in broker state.These are public evaluation paths, not production deployments.Source: §6.5 · pp. 18–19

6.6 Reproducibility

  • The retained artifact includes code, receipts, protocols, generated tables, and verification scripts for reproducing decisions and validating the frozen evidence.Reacquiring upstream repositories and retiming host-local studies are separate commands; providers and credentials are not prerequisites for the reported decisions.Source: §6.6 · p. 19

7 Evaluation Design

The evaluation uses registered questions, matched finite workflows, defined comparator classes, and frozen execution protocols. It reports exact outcomes over those registries, with separate evidence gates for the controlled cases, runtime paths, and host-local sensitivity study.

7 Evaluation Design

  • The evaluation separates seven evidence classes and does not treat bounded exploration, public-source mappings, or sensitivity cells as evidence from other classes.Public-source mappings are not benchmark executions, and bounded exploration is not an unbounded proof.Source: §7 · p. 19

7.1 Research questions

  • The questions test separation, prevention, benign completion, comparator distinctions, runtime portability and cost, and finite-envelope sensitivity.The research questions ask whether locally permitted effects can compose into violations and whether registered valid continuations remain executable.Source: §7.1 · pp. 19–20

7.2 Controlled workflow registry

  • The registry contains 96 matched cases from 48 templates, each pairing benign and drifted workflows across eight transition classes.Twenty-four templates map structurally to frozen public task identifiers; source prompts, outcomes, and expected answers are not copied, and repeated contexts are not treated as independent replication.Source: §7.2 · p. 20

7.3 Compared controls

  • Six control classes range from memoryless allowlists to complete transition authorization, with a strong continuation comparator that checks its trace projection before and during execution.That comparator does not authorize typed resource, obligation, lineage, version, or explicit-join-evidence changes unless they alter its projection.Source: §7.3 · p. 20

7.4 Public tool-execution paths

  • Portability testing requires native dispatch through AgentDojo’s FunctionsRuntime.run_function or τ-bench’s Env.step and Tool.invoke paths.Both adapters use a local deterministic service; malformed requests, version mismatches, crashes, or validator disagreements count as failed runs.Source: §7.4 · p. 21

7.5 Secondary finite-envelope study

  • The secondary sensitivity study freezes 129 synthetic cells, with fixed warm-up and measurement procedures and no asymptotic fitting or population significance testing.Its finite-profile characterization distinguishes graph structures and notes that the amplification family varies two factors together, so it does not isolate either causally.Source: §7.5 · p. 21

7.6 Outcomes and analysis

  • Outcomes cover safety, utility, runtime costs, receipts, retained state, and memory; ground truth comes from registered finite transition semantics and an independent receipt checker.Primary and secondary studies use separate denominators, and host-local performance is not extrapolated to production deployments.Source: §7.6 · pp. 21–22

7.7 Evidence gates

  • Evidence gates require expected decisions, checker agreement, rejection of semantic mutants, and reproducible denominators; the runtime and sensitivity layers have additional run-level checks.The frozen protocol and component digests are retained with the artifact.Source: §7.7 · p. 22

8 Results

Across the deliberately constructed finite registry, the complete mechanism prevents forbidden commits while preserving benign completion. Results also cover the formal separation, comparator coverage, implementation conformance, native runtime paths, and host-local finite-envelope behavior.

8.1 RQ1: separation and formal checks

  • The executable model explores 340 states and 419 transitions without invariant violation, and all 13 initial proposal decisions agree with a separately coded static oracle.Each of 13 single-defect formal variants has a retained counterexample; the memoryless allowlist enters a forbidden state in 33 of 48 drifted cases.Source: §8.1 · p. 23

8.2 RQ2 and RQ3: prevention and benign completion

  • All 48 benign cases complete, while none of 48 matched drifted cases commits a forbidden state; 43 are denied and five require reauthorization.The outcomes span eight transition classes, with graph edits, resource expansion, invalid orders, incomplete joins, and stale witnesses stopped through their respective checks.Source: §8.2 · p. 23, Table 5 · p. 23

8.3 RQ4: comparison with trace and local controls

  • The history-aware trace comparator prevents 37 drifted cases but commits 11 with resource, freshness, or explicit-join-evidence violations outside its trace projection.The complete mechanism blocks those 11 through typed checks; the comparison does not establish superiority over other runtime monitors, planners, or learned classifiers.Source: §8.3 · pp. 23–24

8.4 Implementation conformance and independent checking

  • All 65 protocol checks pass, and the independent checker reconstructs 96 records and replays 867 receipts while rejecting 2,692 mutants from 48 families.The mathematical safety claim still depends on its stated assumptions.Source: §8.4 · p. 24

8.5 RQ5: upstream paths and local cost

  • Two frozen upstream paths execute 258 native dispatches across 32 cases, with every case decision and receipt chain matching the reference records.Median retained authorization state is 5,470 bytes after a transition decision and 8,866 bytes after an effect commit; these are not production-capacity estimates.Source: §8.5 · p. 24

8.6 RQ6: host-local finite-envelope sensitivity

  • All 129 frozen sensitivity cells match their fixed decision and reason, and every declared direct representation boundary is accepted while corresponding over-limit inputs return Indeterminate.The policy-predicate series stops at its study ceiling and establishes no separate policy-list limit; internal enumeration guards are distinct from successful output capacity.Source: §8.6 · pp. 24–26
  • Within-family Allow median ratios reach 7.45 for trace length, 139.80 for continuation count, and 146.51 for active-frame predicates.These are descriptive endpoint-to-reference ratios, not cross-family or asymptotic comparisons.Source: Figure 3 · p. 25, §8.6 · p. 26
  • At 64 goals, retained state is 296,080 canonical JSON bytes; at 256 joined continuations, it is 117,996 bytes.These host-local measurements are distinct from decision latency, and memory snapshots are not portable per-call costs.Source: §8.6 · p. 26

9 Discussion

The discussion treats goal-graph changes as authorization-relevant when they alter reachable effects. It relates that boundary to plan verification, deployment patterns, abstraction choices, and other security controls.

9.1 Authorization follows planning state

  • Activating a child, replacement, delegation, or join is security-relevant when it changes reachable effects; internal alternatives can remain planner-explored.The exposed boundary lets reference monitoring, version checks, receipts, and fail-closed decisions govern behavior without policing private reasoning text.Source: §9.1 · p. 26

9.2 Relationship to plan verification

  • Whole-plan verification and transition authorization are complementary; the contribution is the authorization protocol and invariant, not a claim that incrementality is universally faster.Rechecking a complete model after each plan change may be appropriate for small graphs.Source: §9.2 · p. 26

9.3 Deployment patterns

  • Typed operation and state boundaries can be hosted in API gateways, transaction services, CI/CD controllers, or tool brokers.The runtime needs to expose goal mutations and carry witness identifiers with protected calls.Source: §9.3 · p. 27

9.4 Abstraction and operator choices

  • Sound abstraction and bounded domains can make reachability practical; coarser abstractions tend to increase Indeterminate decisions rather than unsafe allows if universal allow rules are preserved.Operators also declare which versioned changes invalidate witnesses.Source: §9.4 · p. 27

9.5 Security composition

  • Goal-transition authorization assumes authenticated identities, trusted state versions, and an exclusive commit path, and it does not replace several other security controls.Its stated composition property keeps the current graph and still-reachable effects within one approved structured root task.Source: §9.5 · p. 27

10 Validity Conditions and Scope

The paper bounds its claims to enforcement over registered structured domains, with empirical and formal conclusions conditioned on explicit validity assumptions. It does not establish unrestricted deployment performance, planner progress, or safety beyond mediated effects.

Construct validity

  • The primary outcomes measure authorization over registered predicates, normalized effects, and trace membership, not every harmful real-world consequence.Matched benign and drifted cases hold prefixes and affordances constant, while an independent checker avoids using the runtime implementation as its own oracle.Source: §10 · p. 27

External validity

  • The study covers four operational domains, one access-grant join fixture, and two public tool-execution paths, not every framework, policy, or physical environment.The adapter evidence is not evidence of deployment within upstream projects; proposal frequency and planning quality are separate outcomes.Source: §10 · p. 28

Scale-study validity

  • The scale study is a single-host, one-factor-at-a-time study of synthetic deterministic fixtures, so it does not estimate interactions, production throughput, distributed behavior, or unseen-contract performance.A successful boundary cell is not a recommended sustained capacity, and fixed-cell fail-closed behavior does not establish behavior beyond those cells.Source: §10 · p. 28

Formal validity

  • The safety theorem assumes sound transition semantics and trace over-approximation, fresh versions, complete mediation, and a faithful commit adapter.Bounded exploration supports finite instances but does not replace proof; exact finite decision applies only when reachability and typed constraints are decidable in the registered domain.Source: §10 · p. 28

Structured-policy boundary

  • The enforcement boundary starts from a trusted, principal-approved structured root and covers only protected effects passing through registered adapters.The paper does not infer authority from free-form explanations or claim control over unregistered channels; already completed physical actions may require domain-specific compensation.Source: §10 · pp. 28–29

Availability and progress

  • Fail-closed enforcement can permit denial of service, and conditional success preservation neither guarantees a valid plan nor planner termination.The evaluation measures benign completion and recovery to expose this availability cost.Source: §10 · p. 28

11 Conclusion

The paper treats goal evolution as part of authorization, activating replans and delegation only when their structured continuations refine the root contract. Its formal and executable evidence supports this approach within registered domains and stated mediation assumptions.

11 Conclusion

  • Goal creation, replacement, same-root delegation, and joining become explicit authorization events, and protected effects are checked against the resulting residual permitted trace language.A proposed transition activates only when its structured continuation refines the current root contract.Source: §11 · p. 29
  • The formal result establishes root-policy safety under explicit assumptions and preserves required terminal predicates when the authorized goal graph closes.The conclusion does not claim that a planner will find a closing plan or terminate.Source: §11 · p. 29

A.1 Auxiliary lemmas

  • Lemma 2 is identified as residual preservation for a prefix-closed language, with its proof beginning from the empty execution trace.The supplied lemma passage states only this setup, not the full lemma conditions or conclusion.Source: §A.1 · p. 31

A.7 Bounded executable model

  • The bounded model explores 340 states and 419 transitions with no invariant violation, and an independent static oracle agrees on 13 registered proposal decisions.All 13 single-defect variants retain counterexamples, while the abstraction test checks 256 nested language triples.Source: §A.7 · p. 34
  • The retained bounded-model counts support the registered finite artifact, not unbounded programs, unrestricted natural language, or multi-principal composition.The finite abstraction test does not replace the mathematical proof.Source: §A.7 · p. 34

A.2 Proof of Theorem 1

The proof preserves root-policy safety across authorized graph changes, protected commits, invalidation, reauthorization, and closure. It separately shows that validated closure preserves the root success predicate, conditional on closure.

A.2 Proof of Theorem 1

  • Authorized goal edits commit only after W1–W7 hold; graph revisions stale earlier sibling witnesses, while explicit joins check all admissible interleavings.The proof also uses these checks to exclude cross-root edits and preserve resource and obligation conditions.Source: §A.2 · p. 32
  • A protected effect commits only when normalized, fresh, and root-safe, with residual updates at the same atomic commit boundary.The proof relies on mediation and faithful modeled transitions to connect the checked effect to its actual successor.Source: §A.2 · p. 32
  • Invalidation suspends execution without claiming safety for an exogenously changed world, while failed reauthorization leaves the configuration suspended and commits no effect.Cancellation or non-root closure also blocks later commits until an active path is reauthorized.Source: §A.2 · p. 33
  • Every operational case preserves the permitted root trace language, so committed traces remain allowed and protected effects from runnable configurations are current, same-root, and root-safe.The proof states that these cases exhaust the operational rules.Source: §A.2 · p. 33

A.3 Proof of Theorem 2

  • Validated root closure satisfies the root predicate, but this preservation result is conditional on closure and does not imply a closing trace or termination.The proof lifts validated child predicates and discharged obligations through the goal hierarchy before checking the completed root trace and obligations.Source: §A.3 · p. 33

A.4 Proof of Lemma 1

The appendices establish limits of memoryless checks, finite-domain decision and abstraction properties, and the structure of the experimental registry. The scale fixtures expose fixed enumeration boundaries rather than general operating capacity.

A.4 Proof of Lemma 1

  • A memoryless allowlist must either admit forbidden trace ab or reject safe singleton b when it cannot distinguish prefixes ε and a.The same current effect and unchanged allowlist produce identical inputs after both histories.Source: §A.4 · p. 33

A.5 Proof of Proposition 1

  • The finite checker terminates by enumerating registered finite sets, and exact-domain premises make its Allow result equivalent to satisfaction of W1–W7.The result does not claim completeness for a strict over-approximation.Source: §A.5 · p. 34

A.6 Proof of Proposition 2

  • Sound abstraction refinement preserves successful universal-safety checks and concrete denial witnesses, but set inclusion alone cannot establish a concrete denial.The monotonicity conclusion is limited to the universal safety subcheck, not separate non-monotonic policy predicates.Source: §A.6 · p. 34

B.1 Case schema

  • Each workflow record fixes its source, contract, initial state, identical prefix, benign and drifted updates, candidate effects, expected outcomes, versions, and reset instructions.Unknown security-relevant fields are rejected, and expected outcomes must follow from registered semantics.Source: §B.1 · p. 35

B.2 Baseline interface

  • Controls receive different information projections; only the complete mechanism receives typed lineage, obligations, versions, resources, graph revisions, and transition witnesses.The comparison is among specified control classes, not claims of identical information or reimplementations of cited systems.Source: §B.2 · p. 35

B.3 Run retention; B.4 Mutation categories

  • Runs count only after registry and runtime versions, reset, receipt, denominator, and validator checks pass; the registered mutations target represented trusted premises.The evidence gate assigns no policy outcome to failed checks, and the retained mutants have minimal counterexamples and expected rejection reasons.Source: §B.3 · p. 35, §B.4 · p. 35

B.5 Result generation

  • Verified JSON bundles generate manuscript counts and tables, while latency percentiles are descriptive and cannot replace failed security or utility gates.The build fails when generated files are stale.Source: §B.5 · p. 35

B.6 Secondary scale-study registry and execution

  • The secondary registry contains 100 non-join cells, 23 join cells, and six internal-boundary cells, with five process blocks per cell.At the fixed boundaries, 4,096 trace choices are denied as incomplete composition, 256 is the largest successful joined output, and 258 fails closed without truncation.Source: §B.6 · p. 36

B.7 Complete scale-study results

Table 8 reports registered scale-sensitivity measurements as descriptive single-host evidence, not an asymptotic fit.

B.7 Complete scale-study results

  • Ratios are within-family median latency comparisons against a predeclared reference cell with the same decision class.A dash indicates an inapplicable comparison.Source: §B.7 · p. 36
  • The table is descriptive single-host evidence, not an asymptotic fit.Source: §B.7 · p. 36
  • 129 cells report latency in microseconds over 200 retained samples, with ratios omitted when no same-decision reference applies or for over-limit fail-fast cells.The table caption defines State B as canonical retained-state JSON bytes after the measured operation.Source: Table 8 · p. 36
  • Heap/RSS deltas are snapshot differences rather than peak-allocation measurements, while process maxRSS includes fixture setup.One isolated subprocess snapshot was retained per cell; heap/RSS deltas may be negative.Source: §B.7 · p. 38
Loading 2610.04975v1…