HALO: Heterogeneous Admission through Localized Obligations for Safe Agentic Execution Taewoo Park, Kyeonghyun Yoo, Kiseok Kim, Seunghyun Yoo, and Hwangnam Kim∗ Korea University Seoul, Republic of Korea {taewoopark, seven1705, kisuk528, seunghyunyoo, hnkim}@korea.ac.kr
Preprint. This manuscript has not yet been peer reviewed.
arXiv:2607.27636v1 [cs.AI] 30 Jul 2026
Abstract Recent agentic AI systems may return a heterogeneous response containing notices, requests, handoffs, and actions. Conditions can change before external use, so components from the same response need not remain supported together. Rejecting the whole response discards useful components, whereas checking components independently can leave a dependent without its prerequisite. We present Heterogeneous Admission with Localized Obligations (HALO), a runtime protocol that preserves supported components whose declared prerequisites also remain supported, rechecks each exact action before dispatch, and allows blocked actions to be replaced only by fresh candidates. HALO matched all 96 admission expectations and passed all 20 protocol tests. In structuredresponse replay, it retained 248/248 supported components, including 128/128 unaffected by unrelated changes, while a whole-response policy retained 0/248. Across ten cold-start PX4/Gazebo sessions, HALO blocked every tested stale route, observed no matching stale setpoint, and completed all fresh recoveries.
Introduction Large language model (LLM) responses are no longer merely textual. They can now include tool calls, software modifications, and commands for external systems. LLM-based systems that combine language models with these external actions are called agentic AI systems (Yao et al. 2023; Schick et al. 2023; Zhan et al. 2024). This change creates a new safety problem. A wrong answer may mislead a user, but a wrong action can corrupt software, damage equipment, disrupt critical operations, or put people at risk. Safe execution therefore becomes a responsibility of the runtime, the software layer that controls how an agent interacts with external systems. An LLM needs time to generate a response. While a response is generated or waits for external use, the external system may continue to change. Sensor data may become outdated, authorization may expire, software state may change, or the physical environment may move. An action may therefore be outdated when generation finishes or before it reaches the controlled interface. ∗
Corresponding author: [email protected]
This issue will become more serious as future agents use more tools, produce more complex responses, and coordinate more actions. We call this problem runtime support drift. It occurs when the conditions supporting an output change before the output is returned or used. Runtime support drift is harder to handle when one response contains several outputs. Consider an unmanned aerial vehicle (UAV) agent that returns an operator notice, a sensor report, a flight action, and a status message that depends on that action. If the map or traffic information supporting the flight action changes, the action and its dependent status should be blocked. However, the notice and sensor report may still remain valid. Simple approaches do not handle this situation well. Rejecting the entire response discards valid outputs. Checking every output independently may leave a dependent output without what it requires. Checking only once may also miss changes before the action reaches the external system. We present Heterogeneous Admission with Localized Obligations (HALO), a runtime protocol for this problem. HALO treats each output as a separate component. It preserves valid components, removes invalid ones, and rechecks each action immediately before dispatch to the external system. When a blocked action can be corrected, HALO records what must be updated and which component may receive a replacement. The old action is not reactivated. A fresh candidate must return with current information and new authorization, then pass the runtime checks again. We evaluate HALO in UAV operation, where sensor data, geometry, authorization, and vehicle state can change quickly. This setting makes runtime support drift observable at the PX4 setpoint interface. The same runtime process can apply to other domains when an agent returns multiple components, current support can be checked, and actions pass through a runtime-controlled interface. Our contributions are: • a component-level admission model for heterogeneous responses under runtime support drift; • a runtime process combining dependency-consistent retention, exact dispatch, and fresh readmission; • layered evidence from structured-response replay, protocolconformance tests, and PX4/Gazebo execution.
Research line
What it governs
Runtime role
Relation to HALO
Guardrails / schemas AgentSpec
Output or tool call Protected operation
Content and interface constraints Programmable runtime decision
SAFEFLOW / Mnemosyne
Workflow or transaction
Freshness / assurance
Evidence or controller action Component within one response
Coordination, commitment, and repair Freshness and downstream checks
Supply typed interfaces HALO adds dependencies, late rechecks, and recovery Govern broader workflow or transaction state Supply component-specific support inputs Defines the proposed component runtime process
HALO
Partial retention, final dispatch gate, scoped recovery
Table 1: Related approaches by what they govern and where they act in the runtime process.
Related Work
Method
Table 1 compares prior approaches by what they govern and where they act. Existing work controls generated content, individual operations, larger workflows, or downstream safety signals. HALO instead focuses on several dependent components returned together in one response. Guardrails, agent-security benchmarks, sandboxed evaluation, and tool schemas constrain generated content or external interfaces (Ruan et al. 2024; Zhan et al. 2024; Inan et al. 2023; Rebedea et al. 2023; OpenAI 2026; Model Context Protocol Contributors 2025). They help prevent invalid outputs from reaching external systems, but do not decide which parts of one response should remain when changing conditions affect only some components. AgentSpec provides programmable checks for protected operations (Wang, Poskitt, and Sun 2026) and is the closest executable runtime-policy comparator. With matched inputs and current state, AgentSpec-Scoped reproduces HALO’s admission-time decision. HALO additionally preserves declared dependencies, binds authorization to one exact action, rechecks it at the controlled interface, and limits how a blocked component may return. SAFEFLOW coordinates multi-agent information flow and transactions (Li et al. 2025), while Mnemosyne studies admission, commitment, and repair for generated workflow actions (Chang, Geng, and Chang 2026). These systems govern broader workflow or transaction state. HALO instead governs the components within one response and preserves the still-valid subset without leaving unsupported dependents. Freshness metrics, robotic affordance checks, runtime assurance, shielding, and control verification provide support signals or downstream checks (Yates et al. 2021; Ichter et al. 2023; Liang et al. 2023; Desai et al. 2019; Seto et al. 1998; Alshiekh et al. 2018; Ames et al. 2019; Parasuraman, Sheridan, and Wickens 2000). HALO uses these results as current support for individual components rather than replacing them. Selective agentic recovery for UAV autonomy decides when to invoke an external reasoner and validates one returned recovery choice (Park et al. 2026). HALO instead governs which components remain, which dependents are removed, which exact actions may be dispatched, and how blocked components may re-enter. Because these systems govern different objects and stages, we use AgentSpec and mechanism-removal variants to isolate HALO’s runtime process.
Figure 1 turns the problem introduced in the Introduction into HALO’s runtime process. The figure follows one response from its components to admission, dispatch, and recovery. HALO preserves outputs that remain supported and removes outputs whose prerequisites are missing. It then rechecks each action before it crosses the controlled interface. A recoverable action may return only as a fresh candidate.
Runtime Overview The agent returns one structured response. Each output has a declared type, payload, identifier, and optional prerequisite references. We call each output a component, and write the b complete response as R. Figure 1 also shows the running UAV example used throughout this section. The response contains an operator notice, an independent sensor report, a flight action, and a status message released only after that action is dispatched. We denote them by e1 , e2 , e3 , and e4 , respectively. Thus, e4 requires e3 , while e1 and e2 remain independent. HALO does not infer types or prerequisites from free text. The agent proposes them in the structured response, and HALO checks them against trusted rules. A response object is well-formed only when its type, identifier, payload, and prerequisite references follow those rules. Malformed references, cycles, and unsupported component types are rejected rather than guessed or silently repaired. Trusted rules. A trusted domain catalog K is a rule set defined outside the agent. It defines the allowed component types, required prerequisites, support checks, recovery routes, and output paths for one external interface. Trusted state providers supply the current evidence, authorization, versions, provenance, approvals, and operating conditions needed by those checks. We write this current snapshot as Ct . The adapter G is the controlled software interface that sends an authorized action to the external system. In the UAV setting, the adapter publishes an authorized PX4 setpoint. A component that does not request an external state change is a non-action. HALO emits it through its configured output path. HALO dispatches an action only through the adapter. HALO does not replace sensing, planning, geometric verification, or downstream vehicle control.
Figure 1: HALO’s runtime process for one structured response. HALO preserves supported components under declared prerequisites, sends eligible actions to the final dispatch gate, and allows blocked actions to be replaced only by fresh candidates. Component-specific support. Not every change matters to every component. A map update may affect the flight action e3 , but not the operator notice e1 . We call the fields of Ct that matter to component e its support footprint, written πe . This lets HALO react only to changes that are relevant to each component. The component-specific state is Cte = πe (Ct ).
(1)
The catalog then checks whether the component is supported under the current state: LCt (e) = LocalOKK (e, Cte ).
(2)
A change outside πe does not affect e. A change inside πe causes HALO to reconsider that component and any components that require it. Trust model. HALO trusts catalog K, faithful state providers, adapter G, and a trusted authorization ledger. The ledger records whether the authorization for a dispatch attempt is fresh or has already been used. Returned payloads and prerequisite references are untrusted. These assumptions define the boundary within which HALO’s guarantees apply. HALO’s claims cover only the declared response graph, trusted current-state inputs, and actions that cross the enforced adapter. Table 2 provides a map of the notation used below. Admission uses πe and A⋆t , dispatch uses be and G, and recovery uses oe .
Component-Level Admission Table 2 maps admission to the current state. The support footprint πe selects the fields that matter to component e, while A⋆t denotes the set retained by HALO. Admission answers the first runtime question: which components may remain together under the current state? A component that passes admission is retained. Retention means that the component may remain in the runtime; it does not yet authorize an action to be dispatched. A component that fails admission is withheld, meaning that HALO prevents it from reaching its configured output or action path. The agent proposes prerequisite references, and HALO validates their types, directions, and required processing phases against catalog K. A validated reference (p, e, q) means that component e may proceed only after prerequisite component p reaches processing phase q, such as emission or dispatch. Let Dϕ contain these validated references. The resulting response graph is GR = (V, Dϕ ), (3) where V is the finite set of response components. In the running example, e4 requires e3 to be dispatched. Later checks must refer to the same admitted payload. HALO canonicalizes each component and computes a fixed identifier, called a digest: de = Digest(Canonicalize(e)). (4) This prevents a modified payload from reusing earlier support or authorization.
Layer / object
Provided by
Role
b Response: R Response graph: GR Catalog: K Current state: Ct Support footprint: πe Retained set: A⋆t Action binding: be Adapter: G Obligation: oe
Agent HALO Domain designer State providers Catalog K HALO HALO Domain integration HALO
Contains typed components and prerequisite references. Stores validated prerequisite relations and phases. Defines schemas, checks, paths, and recovery rules. Supplies current evidence, authorization, and conditions. Selects state fields relevant to component e. Largest supported set closed under declared prerequisites. Binds one action instance to one authorized dispatch. Sends an action after final dispatch authorization. Records required updates and the allowed replacement.
Table 2: Main objects in HALO’s runtime process. Local support alone is not enough. A component cannot remain when a declared prerequisite has been removed. We call the repeated removal of such components dependency closure. Let
A component remains pending until all required prerequisites reach their specified phases. If a prerequisite fails permanently, HALO invalidates its unemitted or undispatched dependents but leaves unrelated components unchanged.
Parents(e) = {p : ∃q, (p, e, q) ∈ Dϕ }
Exact action binding. Conditions may change while an action waits, and a payload may be modified or replayed. HALO must therefore recheck the same action instance that passed admission. It records an admission witness We , which identifies the canonical payload and stable support data checked at admission, and an action binding be , which ties that witness to one dispatch attempt. At admission time ta , HALO creates
denote the declared prerequisite components of e. HALO retains the largest set in which every component is currently supported and every declared prerequisite also remains: A⋆t = νX. {e ∈ V : LCt (e) ∧ Parents(e) ⊆ X}.
(5)
Here ν denotes the greatest fixed point. Operationally, HALO repeatedly removes unsupported components and components whose prerequisites were removed until no further change occurs. In the running example, stale flight action e3 and dependent status e4 are removed, while notice e1 and sensor report e2 remain. Lemma 1 (Correctness of dependency-closed retention). For fixed catalog K and current state Ct , after malformed and cyclic references are rejected, A⋆t is the unique greatest locally supported subset closed under all declared prerequisites. This repeated-removal procedure reaches A⋆t in O(|V | + |Dϕ |) time after local support checks are evaluated. Proofs are in the supplementary material.
Dispatch Process Table 2 separates retention from external use. Binding be identifies one action instance, while adapter G sends it only after the final dispatch gate succeeds. Admission retains; the final dispatch gate authorizes dispatch. A retained non-action, such as notice e1 , may be emitted after its prerequisites are ready. A retained action remains only a candidate. Before it is sent to the external system, HALO performs one last check. We call this check the final dispatch gate. It confirms that the same action instance is still supported and authorized. Processing-phase readiness. A component’s processing phase records its current progress, such as retained, pending, emitted or dispatched, invalidated, or failed. Let σt (p) denote the phase of prerequisite component p, and let ⪰ mean “at or beyond.” Component e has ready prerequisites when DepsReadyt (e) ⇐⇒ ∀(p, q) such that (6) (p, e, q) ∈ Dϕ , σt (p) ⪰ q.
We = CanonWitnessK (de , Ctea ), be = H(We , seqe ).
(7)
CanonWitnessK selects stable fields, including the catalog version, checked identities, and required certificate metadata. The associated record also stores the admission generation and a one-dispatch token, which authorizes at most one dispatch of that action. Values requiring a live check remain in Ct for the final dispatch gate. Together, these records prevent authority from being transferred to a modified or replayed action. Final dispatch gate. The final dispatch gate asks whether the exact retained action may cross the controlled adapter boundary now. Immediately before dispatch, HALO evaluates DispatchOKt (e) ⇐⇒ e ∈ A⋆t ∧ DepsReadyt (e) ∧ WitnessOKt (We ) ∧ FreshAutht (e, be ).
(8)
These conditions require current retention, ready prerequisites, unchanged bound identities, and unused authorization for the same action binding. Changes outside the support footprint remain irrelevant, while changes to bound support data require readmission. The final recheck, token consumption, and adapter call occur in one gate-owned critical section. Its decision point tℓ is the instant when the gate commits its result. If DispatchOKtℓ (e) holds, HALO consumes the token and calls adapter G. A recoverable denial creates an obligation; a terminal denial ends that action instance. This guarantee covers the adapter call, not every downstream physical outcome.
Localized Recovery
Algorithm 1 The HALO runtime protocol
Blocking an action is not sufficient; the runtime must also control how it may return. As summarized in Table 2, HALO represents a recoverable denial with a small recovery record called a localized obligation oe . It records why the action was blocked, what support must be refreshed, the permitted recovery route, and the replacement scope S(oe ). The replacement scope identifies the blocked component and any permitted fresh replacement. An obligation performs no repair and grants no dispatch authority. Components outside S(oe ) keep their state. In the running example, recovery may replace flight action e3 , but cannot authorize notice e1 or sensor report e2 . A catalog-defined recovery handler may refresh support or produce a revised action using updated evidence, a planner, or rule-based logic, but cannot authorize dispatch. Any returned candidate must re-enter admission, obtain a fresh binding and authorization, and pass the final dispatch gate.
b catalog K; state providers; adapter G Require: Response R; Ensure: Updated component states, emitted non-actions, dispatched actions, and scoped obligations b and its prerequisite 1: Admission: Read current Ct ; validate R references; form GR ; compute A⋆t ; retain selected components pending; create action bindings and one-dispatch tokens. 2: while a support, expiry, path, or phase event affects e do 3: Refresh Ct and recompute the affected dependency closure. 4: if a required prerequisite of e failed terminally then 5: Invalidate e and its unemitted or undispatched dependents. 6: else if e ∈ / A⋆t then 7: Withhold e and dependents removed by closure. 8: Create oe if the local denial is recoverable. 9: else if DepsReadyt (e) = 0 then 10: Keep e pending. 11: else if e is a non-action then 12: Emit e through its catalog-defined path; update σt (e). 13: else Final dispatch gate: Within the gate-owned critical 14: section, refresh Ct , recompute closure, and evaluate DispatchOKt (e). 15: if DispatchOKt (e) = 1 then 16: Consume the token; invoke G. dispatch(e, be ); update σt (e). 17: else 18: Withhold e; create oe only if recoverable. 19: end if 20: end if 21: end while 22: Recovery: If oe remains live, readmit a candidate within S(oe ) with current support, a new one-dispatch token, a later generation, and an unused sequence; otherwise terminate the obligation.
Fresh readmission. A blocked action is never revived with its previous authority. Instead, a new candidate undergoes fresh readmission with current evidence, a later generation, a new one-dispatch token, and an unused sequence. Discharging oe only makes the candidate available; it must repeat validation, support checking, dependency closure, exact binding, and the final dispatch gate. Only components inside S(oe ) may receive fresh instances; ledger details and retry policies are in the supplementary material. Algorithm 1 summarizes admission, processing-phase readiness, final dispatch, and scoped fresh readmission. Relevant events recompute only the affected dependency closure.
Protocol Properties These properties assume a fixed trusted catalog, faithful state providers, an acyclic response graph, and enforced adapter and replacement-scope boundaries; proofs are in the supplementary material. Corollary 1 (Preservation under irrelevant drift). If local support remains unchanged for e and every declared ancestor from t to t′ , then e ∈ A⋆t =⇒ e ∈ A⋆t′ . (9) Thus, unrelated route drift preserves e1 and e2 rather than causing whole-response rejection. Proposition 1 (Gate-boundary integrity). If adapter G is called for action e at decision point tℓ , then e ∈ A⋆tℓ , DepsReadytℓ (e), (10) WitnessOKtℓ (We ), FreshAuthtℓ (e, be ) hold simultaneously, and the token bound to be authorizes at most one adapter call. Thus, the final dispatch gate blocks stale or substituted action instances. Proposition 2 (Fresh scoped recovery). If an action derived from a blocked action reaches dispatch after discharge of oe , it has passed ordinary readmission with current support, a later generation, a new one-dispatch token, and an unused sequence. Discharge creates no recovered authority for any component outside S(oe ).
UAV Instantiation A domain supplies the catalog, state providers, recovery handler, and adapter for one external interface. These details change, but HALO’s core runtime process remains the same. The UAV catalog uses time-stamped evidence, operational rules, map or traffic epochs, geometric bounds, approval, authorization, and vehicle state. For source s, age of information (AoI) is the time since its latest valid update: ∆s (t) = t − us (t),
(11)
where us (t) is that update time (Yates et al. 2021). Catalog K assigns the source-specific limits. POINT checks support at one instant, INTERVAL requires support throughout a declared interval, and ROLLING rechecks support before each new sequence. Together with the operational rules, these checks instantiate LocalOKK in Eq. (2). Selected Federal Aviation Administration (FAA) Part 107 provisions inform catalog rules for pilot authority, airspace, operating limits, preflight support, and traffic separation (Office of the Federal Register 2026). The 410 PX4 profile replays test agreement with these rules, not regulatory compliance. The final dispatch gate rechecks epochs, bounds provenance, corridor support, exact identity, and authorization. The adapter call is the formal boundary; PX4 setpoints are downstream observations, not guarantees of motion.
Variant
(a) Structured-response replay: 248 supported components; 72 epoch, 72 bounds, and 70 prerequisite opportunities Supported kept↑ Stale-epoch leak↓ Wrong-bounds leak↓ Orphan leak↓
AgentSpec-Global AgentSpec-Scoped† IndependentFilter HALO-Admission HALO-Full Variant
0/248 248/248 248/248 248/248 248/248
0/72 0/72 0/72 72/72 0/72
0/72 0/72 0/72 72/72 0/72
0/70 0/70 70/70 0/70 0/70
(b) PX4/Gazebo: 240 supported components; 50 stale, 100 prerequisite, and 200 overblocking opportunities Supported kept↑ Stale setpoint↓ Orphan leak↓ Supported blocked↓
WholeResponse IndependentFilter HALO-Admission HALO-Full
40/240 240/240 240/240 240/240
0/50 0/50 50/50 0/50
0/100 100/100 0/100 0/100
200/200 0/200 0/200 0/200
Table 3: Mechanism comparison. WholeResponse overblocks, IndependentFilter leaves orphaned dependents, and HALOAdmission misses post-admission drift. AgentSpec-Scoped matches the admission-time decision but lacks HALO’s later binding, gate, and recovery process. HALO-Full avoids all tested failures. † Matched admission-time control.
Evaluation RQ1 tests mechanism necessity, RQ2 protocol conformance, RQ3 fresh scoped recovery, and RQ4 runtime cost.
Setup Paired variants share the response, catalog, graph, mutation, timing, and adapter. WholeResponse removes partial retention, IndependentFilter removes dependency closure, and HALO-Admission removes the final recheck. HALO-Full keeps the complete runtime process. AgentSpec-Global applies one response-level decision, while AgentSpec-Scoped shares HALO’s component-scoped predicates and current state. Separate controls test modification and replay. Experiments use Python 3.10 on Windows Subsystem for Linux 2 (WSL2), PX4 software-in-the-loop (SITL) (Meier, Honegger, and Pollefeys 2015), Gazebo (Koenig and Howard 2004), live OpenClaw server-sent events (SSE), and a Crazyflie 2.1 platform for the physical UAV sequence. Coldstart sessions use a new PX4 process; AgentSpec steady-state repetitions do not. The replay, PX4-profile, controlled-timing, and AgentSpec panels are separate cohorts whose denominators are not pooled. We report case-level outcomes separately from PX4 setpoints.
RQ1: Mechanism Necessity Table 3 should be read across each reduced variant: its failure column identifies the missing runtime mechanism. WholeResponse overblocks, IndependentFilter leaves dependents without required parents, and HALO-Admission misses post-admission drift; HALO-Full avoids all three in the evaluated cases. Across 300 calls in 15 families, 226 replay-eligible responses produced 7,910 paired evaluations, while separate controls rejected modified instances and reused authorization. The PX4/Gazebo panel evaluates 12 predefined conditions under four protocol variants across ten cold-start SITL sessions, yielding 480 condition–variant executions. RQ3 additionally presents one controlled UAV operation. Together, these results show that retention, dependency closure, exact binding, and final-gate revalidation address distinct failures.
Comparison with AgentSpec. An action fingerprint is a log identifier used to match an action with an internal PX4 setpoint. With matched inputs and current state, AgentSpecScoped reproduced HALO’s admission-time decision. Without HALO’s binding and final dispatch gate, it produced fingerprints for stale actions in all tested post-decision cases and accepted all replayed tokens. Adding HALO’s runtime process removed both failures and completed all fresh recovery cases. A separate cold-start confirmation showed the same pattern; detailed denominators are provided in the supplementary material. This isolates HALO’s contribution as the post-decision dispatch and recovery process rather than a richer rule language.
RQ2: Runtime Protocol Conformance We ask whether the implementation matches the formal protocol. It matched all expected outcomes across 96 admission cases, 135 exhaustively enumerated graphs of up to 16 components, 45 independently checked graphs of 32 components, 20 protocol cases, and 10,000 valid or fault-injected schedules. These cases exercise local support, closure, event ordering, final rechecks, one-dispatch token enforcement, and recovery transitions, providing protocol-conformance rather than openworld success evidence. Agreement across exhaustive small graphs and independently checked larger graphs indicates that conformance is not tied to one graph size or test construction.
RQ3: Fresh Scoped Recovery The PX4 profiles combine UAV-specific catalog conditions— source-specific freshness, POINT/INTERVAL/ROLLING semantics, operational rules, authorization, epochs, and geometric support—with HALO’s exact-identity and unusedsequence checks. Recovery requires current evidence, a later generation, a new one-dispatch token, and an unused sequence; terminal or out-of-scope cases create no authority. Across 48/48 recovery-oracle matches, all 36 executable cases returned through admission, while 12 terminal cases ended without authority. Controls rejected five attempts to reuse prior authorization and one out-of-scope recovery.
Figure 2: Physical Crazyflie realization of Figure 1. HALO first retains the forward action, then withholds it after support changes while preserving the independent range report, and finally readmits a fresh recovery candidate.
Test
Observed result
Crazyflie operation
10/10 stale actions withheld; 10/10 range reports emitted; 0/10 matching stale setpoints; 10/10 fresh readmissions. 410/410 decisions matched; 0/250 denied actions reached PX4; 60/60 recoveries were fresh. 48/48 outcomes matched; 12 terminal; 36 returned through admission.
PX4 dispatch checks Recovery checks
Table 4: Repeated Crazyflie, PX4, and recovery outcomes; the first row corresponds to Figure 2.
Physical operation. Figure 2 instantiates the three transitions in Figure 1: the initial forward action is retained after admission (1 → 3a), the unsupported forward action is withheld (2 → 3b) while REPORT(z_range) continues to be emitted, and a fresh backtrack-and-land candidate re-enters admission, receives a new binding and authorization, and passes the final dispatch gate (3b → 2/3a). Table 4 quantifies this Crazyflie sequence and summarizes the broader PX4 and recovery checks.
RQ4: Runtime Cost We finally ask how the core checking cost grows with response size after domain-specific predicates have been evaluated. Admission takes O(|V | + |Dϕ |), (12) and the final dispatch gate is linear in action e’s declared prerequisites and footprint size |πe (Ct )|. With up to 32 components, the largest median admission cost was 0.333 ms and the 95th percentile was 0.453 ms. With up to 16 direct dependencies and 32 footprint fields, the largest median pre-consumption gate cost was 0.035 ms and the 95th percentile was 0.061 ms. Median-based regressions yielded R2 = 0.9978 for admission and R2 = 0.9975 for final-gate compute, consistent with but not proving the source-level bounds. Measurements exclude model generation, domain predicates, token mutation, and downstream execution; the tested core checks are therefore small in this setting without establishing general scalability.
Discussion HALO separates two decisions often conflated: whether a component remains eligible and whether an exact action may cross the controlled interface. Partial preservation requires dependency-consistent retention, while admission alone cannot protect a waiting action as runtime support changes. Localized obligations identify what must be refreshed without reviving the blocked instance or expanding its authority. HALO’s guarantees are boundary-scoped. Under a trusted catalog, faithful state providers, an enforced authorization ledger, and a gate-owned adapter, HALO provides dependency coherence, exact-instance binding, one-dispatch token enforcement, and fresh scoped readmission. Semantic correctness, undeclared dependencies, provider failures, distributed atomicity, and downstream physical outcomes remain outside this boundary. PX4 setpoints record governed interface crossings; the Crazyflie motion remains a downstream observation. The contribution is not a new predicate language, freshness metric, or authorization primitive, but a reusable typedcomponent runtime protocol above existing runtime-policy and domain-assurance mechanisms. The same process can apply when a domain supplies support rules, current state providers, and an enforced effect boundary. A supplementary cross-domain check shows that HALO can be applied at a versioned software boundary without losing the tested preservation, blocking, or fresh recovery behavior.
Conclusion Components from one agent response do not share one validity state. HALO preserves the largest supported set whose declared prerequisites also remain supported, then separately determines whether each exact action has current dispatch authority. A localized obligation records required updates and replacement scope, but only a fresh candidate may return. Across structured replay, protocol-conformance tests, and PX4/Gazebo experiments, HALO-Full preserved unaffected components, removed unsupported dependents, excluded all tested stale dispatches, and completed fresh scoped recovery. These results establish heterogeneous component admission as a distinct runtime layer between structured responses and controlled external actions. As LLMs evolve into agents that act on external systems, HALO provides a component-level runtime paradigm for governing effect-bearing responses.
Scope of This Supplement This supplement expands the formal arguments, evaluation cohorts, measurement boundaries, and reproduction conditions behind the four research questions in the main paper: mechanism necessity, runtime-protocol conformance, fresh scoped recovery, and runtime cost. It uses the main paper’s b is the agent-returned bundle, GR = (V, Dϕ ) is notation: R the catalog-validated response graph, K is the trusted domain catalog, and Ct is the time-indexed runtime support state. The primary evidence remains the structured-response and UAV/PX4 evaluation reported in the main paper. A final, explicitly supplementary software-boundary check evaluates whether the same runtime process can be instantiated with a different catalog and adapter; it is not an additional main-paper research question.
Formal Model and Protocol Core and Domain Interface HALO defines a fixed component-level protocol over a domain interface. Its core governs dependency closure, processing state, exact dispatch authority, and scoped recovery; domains supply component types, footprints, predicates, recovery routes, providers, and governed adapters. Table 5 first records the main-paper UAV instantiation and then the supplementary repository instantiation. The latter tests interface transfer at a sandboxed versioned-software boundary; it does not claim a new merge algorithm or replace Git’s native consistency mechanisms.
Component-Level Admission The trusted catalog, rather than the returned bundle, determines each type’s schema, canonicalization, mandatory footprint, support predicates, allowed dependency phases, certificate requirements, and recovery route. The response supplies only typed payloads and component references. This is the assumption under which the following oracle comparison is interpreted. Typed binding model. The agent returns the typed bundle b HALO validates its component types and dependency R; references against catalog K and constructs the finite phaselabeled graph GR = (V, Dϕ ),
Dϕ ⊆ V × V × Q,
(13)
where V = {e1 , . . . , en } is the set of typed components and (p, e, q) ∈ Dϕ states that dependent e requires parent p to reach phase q ∈ Q. We write Dϕ (e) = {(p, q) : (p, e, q) ∈ Dϕ }, D(e) = {p : ∃q, (p, q) ∈ Dϕ (e)}.
(14)
for the phase-labeled and positive prerequisite dependencies of e, respectively. Duplicate identifiers, missing references, and cycles fail closed before a dispatch authorization is issued. For each component, the runtime first computes the canonical digest de = Digest(Canonicalize(e)).
(15)
The catalog-defined footprint selects the current state relevant to e: Cte = πe (Ct ). (16) The stable subprojection βe (Ct ) contains source identities, epochs or versions, bounds and provenance identifiers, and approval or certificate identity. Admission stores We = CanonWitnessK de , βe (Cta ), certificatee , vK .
(17)
The exact action binding used by the main paper is be = H(We , seqe ).
(18)
The associated admission record stores the component type, footprint, dependency references, admission generation, and a one-dispatch token bound to this exact action instance. The token authorizes at most one dispatch. These fields support validation and ledger checks; the dispatch identity itself is be . Clock time, age, and changing telemetry are not hashed as immutable witness bytes; catalog predicates reevaluate them from the live projection at the final gate. HALO distinguishes generation tg , admission ta , final authorization tc , first enqueue tp , and optional downstream observation tx . The binding at dispatch checks the witness against current support rather than hashing the proposal-wide mutable state. Temporal support semantics. The following equations restate the main-paper UAV definitions so that the temporal conventions are self-contained. For source s, let us (t) be the generation time of its newest available update. Its Age of Information is (Yates et al. 2021) ∆s (t) = t − us (t).
(19)
For component e, let Se be its relevant sources and He,s their catalog thresholds. The represented freshness predicate is ^ FreshOK(e, t) ⇐⇒ ∆s (t) ≤ He,s . (20) s∈Se
Equality is admitted: ∆s (t) = He,s is valid. AoI is distinct from source epoch, bounds provenance, certificate validity, information correctness, and operational-rule truth. A separate RuleOK predicate checks the represented operational condition. The UAV adapter combines the two dimensions: SupportOK(e, t) ⇐⇒ FreshOK(e, t) ∧ RuleOK(e, t).
(21)
Freshness therefore cannot substitute for rule truth, and rule truth cannot substitute for current evidence. The temporal certificate determines the time region that support must cover. For a POINT component, freshness is checked at its first downstream effect: POINT_OK(e) ⇐⇒ FreshOK(e, tfirst ).
(22)
For an INTERVAL component, support is certified to cover the declared interval by the conservative condition tend + δg < tvalid_until (e),
(23)
Interface element
Fixed HALO role
UAV instantiation
Supplementary repository instantiation
Component types
Units of admission and processing state Runtime-state fields relevant to one component Inputs to LocalOK
notice, refresh request, route action, status traffic age, map epoch, vehicle state, bounds freshness, authority, geometry, operating rules route dispatch or observed completion
review notice, evidence request, merge action, completion notice target head, patch digest, CI, approval
Support footprint Support predicates Dependency phases Recovery route Predicate provider Governed adapter Observation hook
Parent milestones required before progress Source of a fresh candidate Supplies the current runtime support state Gate-owned effect boundary Downstream empirical evidence
version, protection, CI, approval
evidence refresh, approval, replan telemetry and runtime services
merge dispatch before completion notice updated CI, approval, rebase repository and review state
PX4 setpoint adapter call PX4 internal setpoint
merge-commit creation call Git ancestry audit
Table 5: The fixed HALO interface under the main-paper UAV instantiation and the supplementary repository transfer check. The two instantiations change the catalog, providers, recovery route, and governed adapter while preserving the same HALO protocol core. where δg is the adapter guard. Equality fails closed. This is an interval-coverage check over the certificate horizon, rather than continuous live monitoring during execution. For a ROLLING component, every tested window requires refreshed support and a new admission before the next actionbearing sequence. The following profiles are informed by selected FAA Part 107 provisions (Office of the Federal Register 2026). Dependency-closed admission. runtime support state Ct , let
For fixed catalog K and
LCt (e) = LocalOKK (e, πe (Ct )) denote component-local support, excluding dependency checks, and let D(e) denote declared parents. The corresponding closure operator is FCt (X) = {e ∈ V : LCt (e) ∧ D(e) ⊆ X}.
(24)
At dispatch, the declared relation is phase-labeled: a dependent component must wait for the required parent phase, not merely for parent admission. The final gate also checks the exact canonical component digest, current component support projection, certificate, horizon, and unused one-dispatch token. Under unique component identifiers, a finite acyclic declared graph, a fixed runtime support state, independently valid unused component-bound tokens, and no cross-component resource-allocation conflict, the greatest fixed point of FCt is the greatest dependency-closed locally supported subset. The implementation rejects duplicate identifiers, missing references, and cycles before an effect can be emitted. The broader graph-oracle benchmark below tests this construction independently across multiple graph sizes. Matched admission-time control. A customized policy using the same component predicates and declared prerequisites can reproduce HALO’s initial retained set. We therefore use this configuration only as a matched admission-time control. It does not provide HALO’s exact-instance binding, final dispatch recheck, component-bound one-dispatch token
enforcement, dependency-aware processing, or scoped fresh readmission. The expanded dependency-DAG oracle benchmark contains 180 deterministic cases. For 135 graphs with 4, 8, or 16 components, exhaustive subset enumeration is the oracle. For 45 graphs with 32 components, a separately implemented descending-rejection oracle is used. The oracle code does not import HALO’s admission procedure or share its selection helpers, uses a different rejection-propagation traversal, and is driven by the frozen graph artifact rather than HALO’s traversal order. Its maximality check starts from locally invalid, catalog-invalid, missing-reference, and cyclic nodes, then rejects every descendant whose parent has been rejected. The harness checks local soundness, dependency closure, and greatest-set maximality separately from exact-set agreement. The graph-generation seed is recorded independently; the oracle execution is deterministic and performs no randomized sampling. The tested grid has zero local-validity, dependency-closure, and greatest-set mismatches. Once local predicate results are available, dependency closure requires O(|V | + |Dϕ |) time. Including predicate evaluation, total admission cost is O(|V | + |Dϕ | + PredicateCost).
Dispatch and Recovery Details Component processing state. HALO separates the current runtime support state Ct , the exact action binding be , and processing state σt (e). State Ct contains mutable world and system support. The admission record contains the canonical digest, component footprint, support witness, certificate metadata, catalog version, token, sequence, and admission generation; be identifies the exact action instance and dispatch attempt. The gate instance fixes the governed adapter. The processing state records whether that exact component instance has progressed far enough to satisfy a phase-labeled dependency.
Profile
Anchor
Represented machine-checkable support
Fresh recovery
AUTH-1
14 CFR 107.19
AUTH-2
14 CFR 107.41
AUTH-3
14 CFR 107.51
Fresh authority evidence and new admission Fresh authorization evidence and new admission Corrected scope and new admission
OPS-1
14 CFR 107.49
SEP-1
14 CFR 107.37
Remote-PIC designation, current authority token, and override or abort availability Airspace authorization not required, or represented authorization present and current Operation inside represented time, geometry, altitude, and configured operating-limit scope Current environment assessment, healthy command link, sufficient energy, and current preflight evidence Current traffic epoch and age, available bounded tube, and represented separation predicate
Refreshed preflight support and new admission Fresh traffic, a new tube, and new admission
Table 6: FAA-anchored engineering profiles used by the benchmark. Each profile maps a selected operational provision to machine-checkable support conditions and a fresh recovery route. The represented component states are σt (e) ∈ {PROPOSED, RETAINED, PENDING, EMITTED, DISPATCHED, OBSERVED_SUCCESS, WITHHELD, FAILED, INVALIDATED}.
(25)
WITHHELD denotes a component prevented from reaching its catalog-defined output path. INVALIDATED denotes an undispatched retained instance that cannot proceed under its current binding. FAILED denotes an instance that passed the final gate but failed to reach a required downstream milestone. A dependent is ready only when every parent reaches its catalog-required phase: DepsReady(e, σt ) ⇐⇒ ∀(p, q) ∈ Dϕ (e) : σt (p) ⪰ q.
(26)
A terminal parent failure invalidates unemitted or undispatched descendants. It does not roll back already emitted or dispatched components or unrelated lineages. A declared parent also remains a current support prerequisite until its dependent proceeds; the phase label adds the processing milestone checked by DepsReady. Obligations use a separate recovery state CREATED → DISPATCHED → EXTERNAL_SUPPORT_RECEIVED → READY_FOR_READMISSION → DISCHARGED, (27) with explicit failure and timeout exits. Readiness is evidence that the routed support arrived, not dispatch authorization: ωt (oe ) = READY_FOR_READMISSION ̸⇒ Dispatch(e).
(28)
Executable admission procedure. The following numbered procedure is the supplement counterpart of the compact method equations in the main paper. 1. Validate the typed envelope, catalog version, identifiers, references, and dependency phases. Reject duplicate identifiers, unknown types, missing references, cycles, and catalog mismatches.
2. Canonicalize each component and compute its exact digest. Check that any support certificate is bound to that digest. 3. Read one runtime support state and evaluate the catalog predicates over each component’s required footprint. 4. Initialize the candidate set with locally supported components. Repeatedly remove a component whose declared prerequisite parent is absent; the remaining set is A⋆t . 5. For each retained action-bearing component, create a binding over its canonical bytes, component-relevant support witness, certificate, catalog version, sequence, and admission generation. Issue a component-bound one-dispatch token. 6. On a support or parent-phase event, reevaluate the affected component and its dependent closure. An unmet nonterminal phase leaves the component pending; a terminal failure or currently unsupported ancestor invalidates unemitted or undispatched descendants. 7. At the sole governed-adapter entry, read current support, check membership in the current dependency closure, validate the stable witness, dependency phases, horizon, and unused current-generation token, then atomically consume the token and invoke the adapter. 8. On a recoverable denial, create the catalog-routed obligation. External support may create a fresh candidate, but that candidate returns to Step 1 with a later generation, current evidence, a new one-dispatch token, and an unused sequence. A terminal denial produces no dispatch authorization. Proof details. Theorem 1 (Greatest dependency-closed admission). For a finite acyclic represented graph with fixed catalog K and runtime support state Ct , A⋆t = νX.FCt (X) is the unique greatest locally supported set closed under declared positive dependencies. Proof. The operator is monotone on the finite lattice 2V and maps every subset to a subset of the locally supported set. Descending iteration from the locally supported set therefore stabilizes at a fixed point. Any other locally supported dependency-closed set is contained in the initial set and,
by monotonicity, in every subsequent iterate. It is therefore contained in the limit A⋆t , establishing greatestness and uniqueness. Theorem 2 (Preservation under irrelevant drift). Suppose a mutation from Ct to Ct′ leaves the support projection and local support of e and every declared ancestor unchanged. If e ∈ A⋆t , then e ∈ A⋆t′ . Proof. The mutation preserves each local predicate result in the finite ancestor closure. Induction from roots to e preserves membership in the corresponding fixed point, so e remains retained. Theorem 3 (Gate-boundary integrity). Assume the final gate is the sole governed adapter entry and predicate providers faithfully represent the state checked at the gate decision point. If the component is outside the current dependency closure, a required phase is unmet, its stable witness is invalid, or its dispatch authorization is stale at tℓ , no adapter call is made for that component instance. Conversely, if adapter G is called for e at tℓ , then e ∈ A⋆tℓ ∧ DepsReadytℓ (e) ∧ WitnessOKtℓ (We ) ∧ FreshAuthtℓ (e, be )
(29)
holds, and the token bound to be authorizes at most one call.
Proof. The obligation manager accepts fresh candidates only when their component identifiers are contained in S(oe ), and obligation transitions themselves issue no dispatch authorization. The fresh-admission transition updates only the accepted candidate identifiers. A trusted dispatcher passes that validated candidate set unchanged to fresh admission. Components outside the set receive no new recovery authority, although ordinary parent-phase or support events may still advance or invalidate them under existing bindings. Together, Theorems 4 and 5 establish the main-paper proposition on fresh scoped recovery. Protocol-conformance cohorts. The fixed admission oracle contains 96 predefined outcomes spanning local support, malformed references, dependency removal, and maximal coherent retention. The graph oracle adds 135 exhaustively enumerated graphs with 4, 8, or 16 components and 45 independently checked graphs with 32 components. A separate protocol-transition suite contains 20 hand-authored transition cases and 10,000 seeded valid or fault-injected schedules covering event ordering, final rechecks, token nonreuse, terminal parent failure, and scoped recovery. The implementation matched every expected fixed outcome, graph oracle, protocol-transition case, and generated schedule. These are deterministic protocol-conformance checks rather than estimates of field failure probability.
Evaluation Details Live Structured-Agent Stress Check
Proof. Every checked mismatch falsifies a conjunct of DispatchOKtℓ (e). The gate therefore denies before token consumption and the adapter call. When every conjunct holds, the gate commits the decision, consumes the componentbound token, and invokes G within the gate-owned critical section. Because the gate is the adapter’s sole entry and the token authorizes one dispatch, a denied instance has no alternate governed path and an accepted binding authorizes at most one call. Theorem 4 (No revival of prior authorization). Let bb be a withheld, undispatched binding. If recovery passes through the obligation process and governed dispatch uses the same final gate, then bb cannot authorize a later dispatch. Proof. Obligation transitions issue no token. Fresh admission increments the generation, rejects every prior sequence, and revokes prior-generation tokens. It may retain certificate bytes only when the certificate remains current and bound to the exact component. The final gate accepts only the current component instance and its unused current-generation token, so any recovered dispatch must use br ̸= bb . Theorem 5 (Recovery locality). Let S(oe ) be the replacement scope carried by obligation oe . Discharging oe creates no new binding, token, admission generation, or recovered component instance for any u ∈ / S(oe ). A component outside the scope may advance only under its existing binding and the ordinary dependency rules.
This cohort is a repetition-based implementation stress check, not a response- diversity or generalization benchmark. It contains 100 OpenClaw Server-Sent Events responses for one controlled four-component template. The collector saves a terminal event, response provenance digest, parsed envelope, completion ledger, and paired-replay linkage without storing the gateway token. Every accepted response is replayed unchanged over 12 conditions and four variants, producing 4,800 paired rows. Valid kept counts supported components, Stale dispatched counts stale action effects, and Dependency leak counts dependency-inconsistent host-runtime notices.
Structured-Response Cohorts The diversity cohort is separate from the fixed-template cohort above. It uses 300 live OpenClaw calls across 15 frozen response-family schemas. The collection funnel is 300 → 274 schema-valid → 226 replay-eligible → 7,910 paired replay rows. All accepted records have validated provenance and unique endpoint response identifiers. The 74 rejected records comprise 28 family-schema mismatches, 20 missingdependency schema failures, 20 dependency-cycle failures, and six unknown-type schema failures. They remain in the failure ledger and do not enter replay. This cohort measures structural variation within one controlled endpoint and model, not naturally occurring response distributions or cross-model generalization. The endpoint reported the model identifier openclaw; it did not expose a more specific model revision. Each of the 15 families received 20 calls using its frozen prompt-state
Main-paper question
Primary comparison
Evidence boundary
RQ1: mechanism necessity RQ2: protocol conformance RQ3: fresh scoped recovery RQ4: runtime cost Supplementary transfer
reduced variants and AgentSpec controls fixed cases, graph oracles, and schedules recovery oracle, profiles, and UAV operation graph and gate size sweeps six repository variants
component trace and PX4 setpoint protocol decisions new binding and sequence protocol-only computation sandboxed merge ancestry
Table 7: Mapping from evaluation questions to comparisons and observation boundaries.
Variant
Valid kept
Stale dispatch
Dep. leak
Method
WholeResponse IndependentFilter HALO-Admission HALO-Full
400/2400 2400/2400 2400/2400 2400/2400
0/1000 0/1000 500/1000 0/1000
0/1000 1000/1000 0/1000 0/1000
AgentSpec-Global AgentSpec-Scoped IndependentFilter HALO-Admission HALO-Full
Table 8: Repeated fixed-template stress check. One hundred response repetitions share a controlled structure so that paired mechanism effects can be measured directly. Cohort
Input
Eligible
Response diversity
300 calls
226
AgentSpec comparison Independent-valid subset
62 responses 62 responses
62 62
Evaluation unit 7,910 paired policy evals. 248 supported components 128 components
Table 9: Structured-response cohort accounting. Variant
Retained mechanism
Removed or changed mechanism
WholeResponse AgentSpec-Global AgentSpec-Scoped
bundle decision global state rule post-mutation scoped rules proposal snapshot local support current predicates component admission all HALO mechanisms
partial preservation local support footprint no native dispatch-process test local support footprint
GlobalSnapshot IndependentFilter Local-Unbound HALO-Admission HALO-Full
dependency closure exact admission binding final dispatch gate none
Table 10: Baseline definitions.
template and response schema. Temperature was omitted from the request, the endpoint exposed no sampling-seed field, and the collector used a 90-second timeout with at most two transient retries and a one-second backoff. The separate 62-response AgentSpec cohort contains every provenancevalid, schema-valid, family-schema-conforming record from its frozen source collection; no outcome-based subsampling was performed. The late-policy replay freezes the baseline definitions be-
Kept
Epoch
Bounds
Orphan
0/248 248/248 248/248 248/248 248/248
0/72 0/72 0/72 72/72 0/72
0/72 0/72 0/72 72/72 0/72
0/70 0/70 70/70 0/70 0/70
Table 11: Structured-response comparison on 62 live envelopes. AgentSpec-Scoped is the matched admissiontime control, isolating initial predicate expressiveness from HALO’s later binding, gate, and recovery process.
fore reading results. GlobalSnapshot checks a proposal-wide current snapshot. Local-Unbound checks the componentlocal freshness footprint but omits digest-bound epoch and bounds provenance. The two are separated because their expected failure modes differ. IndependentFilter evaluates current component-local support at the same decision boundary as HALO but ignores declared dependencies. AgentSpecScoped evaluates explicitly encoded component predicates at the post-mutation decision point; it measures policy expressiveness rather than AgentSpec’s native dispatch process. AgentSpec can therefore express equivalent admission predicates when they are configured explicitly. HALO instead defines a coupled component-level protocol that connects dependency-consistent admission, exact-instance dispatch authority, late revalidation, and scoped fresh readmission across one effect-bearing response. These controlled prompts and schemas test structural variation across 15 response families while holding the model endpoint and replay conditions fixed.
Final-Gate and Authorization Controls The protected dispatch adapter uses one process-local critical section: read the current component projection, validate applicable predicates, consume a one-dispatch token, and enter the sole enqueue adapter. In six deterministic cases, a post-validation mutation produced zero stale enqueues; only one of two concurrent consumers could enqueue; used-token, restart-token, and duplicate-sequence replay were rejected. A failed enqueue consumes its token and requires fresh admission. This supports the gate-owned critical-section behavior described in the main paper, not distributed atomicity or remote exactly-once delivery. The AgentSpec reference-interpreter comparison contains six scenarios with ten warm repetitions. Policy-only AgentSpec produced 40/40 post-decision stale internal finger-
prints and allowed 10/10 token replays. Adding HALO’s final binding, component-bound one-dispatch token enforcement, and fresh recovery protocol produced zero stale fingerprints, blocked all ten replay attempts, and completed 20/20 fresh recoveries, matching HALO-Full at the measured PX4 boundary. Each token is also bound to a component-local admission generation. Fresh admission accepts only a failed or invalidated component instance, rejects every prior sequence identity, revokes outstanding tokens from the previous generation, and increments that generation. The gate checks the current component instance and generation before token consumption. Consequently, obligation readiness cannot revive the prior authorization: any recovered dispatch must use current evidence, a later admission generation, a fresh token, and an unused sequence. For each recoverably withheld action-bearing component, the adapter can create oe = (e, r, S, Q, a, ρ, τ, d),
(30)
where r is the reason, S the required support, Q = S(oe ) the replacement scope, a the assignee, ρ the route, τ the expiry, and d the discharge condition. Exists(oe ) ̸⇒ Dispatch(e): an obligation does not authorize the withheld effect. Retry scheduling is catalog-defined. HALO provides the obligation state, expiry, timeout and terminal exits, and the hook through which a candidate may be resubmitted; every retry remains inside S(oe ) and repeats ordinary admission with a new one-dispatch token and unused sequence.
Cross-Domain Portability Check This check asks whether HALO can be instantiated at a versioned software boundary without losing the tested preservation, blocking, and fresh recovery behavior. We attach the unchanged core admission, binding, final-gate, and recovery logic to a sandboxed bare-Git merge adapter. Git already supplies versioning, ancestry, and merge semantics; HALO’s role is only to decide whether an agent-returned merge component, its dependent notice, and any recovered candidate may reach that adapter under current external evidence and authorization. The repository panel contains 12 predefined cases, six protocol variants, and ten repetitions, yielding 720 executions. Cases cover all-valid operation, unrelated branch or issue updates, changed target head or patch digest, changed or failed continuous-integration evidence, revoked approval, changed branch protection, merge conflict, a dependent completion notice after a blocked merge, and fresh recovery. Stale target-head, CI, approval, branch-protection, and patchdigest cases withhold the merge candidate and its dependent merged_notice; catalog routes request rebase or replanning, fresh CI, new approval, protection refresh, or patchdigest validation. Across the complete cohort, Full HALO retained 40/40 unaffected outputs, produced 0 stale merge observations and 0 dependent-notice leaks, and completed 10/10 fresh readmissions. The reduced variants exposed the intended failures: Local-Unbound produced 40 stale merges, HALO-Admission produced 90, No-Dependency produced 90 dependent-notice leaks, and GlobalSnapshot falsely denied
Variant WholeResponse IndependentFilter HALO-Admission HALO-Full
Kept
Stale
Dep.
Valid block
40/240 240/240 240/240 240/240
0/50 0/50 50/50 0/50
0/100 100/100 0/100 0/100
200/200 0/200 0/200 0/200
Table 12: PX4 results across ten cold starts. Stale dispatch counts fingerprint-matched internal setpoints; dependency leaks are host notices.
20/30 fresh controls. Git ancestry provides the downstream observation of which merge commit, if any, was created. This is a sandboxed bare-Git effect-boundary result, not a hosted-forge or distributed-transaction claim. The effect-boundary catalog maps each represented type to its first protected downstream effect: operator queue insertion, evidence-provider dispatch, handoff enqueue, sandboxed merge enqueue, PX4-bound adapter enqueue, or statuschannel enqueue. A seeded 10,000-schedule property panel found zero tested locality, local-validity, dependency-closure, greatest-set, token-nonreuse, or blocked-parent-emission violations. It is implementation validation, not a failureprobability estimate.
PX4/Gazebo Observation Boundary The live PX4/Gazebo baseline panel (Meier, Honegger, and Pollefeys 2015; Koenig and Howard 2004) has 12 conditions and four variants, for 480 case–variant executions across ten complete cold-start SITL sessions in one fixed environment. A predeclared NED-position-plus-yaw fingerprint links a component trace to an internal trajectory_setpoint observation. PX4 does not carry a native HALO case identifier. Independent notices and dependency-inconsistent notices are therefore evaluated at the HALO component-runtime boundary; only action-bearing segments use the internal topic. The late-drift experiment uses the following order: ta : admission −→ tm : mutation, tm −→ tc : final gate, tc −→ tp : host enqueue, tp −→ tx : ULog observation.
(31)
The experiment requires ta < tm < tc for the injected epoch and bounds mutations. Host timestamps (ta , tm , tc , tp ) and PX4 boot-time tx remain different clocks. Alignment is used only to attribute broad process phases; the internal fingerprint itself is matched directly in ULog coordinates. The analysis observed all 170 expected internal fingerprints and no matching fingerprint for any of 350 denied candidates. The 20 Full-HALO recoveries were observed only with fresh sequence identifiers. Hold intervals use direct PX4 target fingerprints; execution and recovery use coarse host–PX4 process-phase alignment, whose maximum residual was 108.04 ms. The alignment locates broad process phases, while the internal setpoint evidence is matched directly in PX4 ULog coordinates.
Across the ten cold sessions, required ULog topics and selected structured fields were present. All 350 denied hold acquisitions and their steady observations met the preregistered error and drift limits, and no selected true status flag was attributed to an execution, deny-hold, or recovery interval. Status samples outside those intervals remain separately reported in the artifact rather than being counted as runtime-clean evidence.
Measure
UAV support-profile replication. A separate panel repeated 11 AoI conditions and 30 FAA Part 107-informed engineering-profile conditions across ten cold-start sessions. The 41 unique conditions yielded 410 replays with 410/410 expected outcomes, no matching internal setpoint for 250 denied actions, matching internal setpoints for all 160 admitted actions, and fresh dispatch sequences for all 60 recoveries. The AoI subset contributed 110 replays, 0/50 denied setpoints, 60/60 admitted setpoints, and 10/10 fresh sequences; the FAA subset contributed 300 replays, 0/200 denied setpoints, 100/100 admitted setpoints, and 50/50 fresh sequences.
Table 13: Constrained-motion latency decomposition using the floor-index quantile estimator. Long adapter and completion intervals include setpoint transmission, fingerprint dwell where applicable, host polling, telemetry, PX4/Gazebo response, and target convergence; they are not HALO protocol computation overhead.
Physical Crazyflie operation. The main-paper Crazyflie 2.1 sequence instantiates the same runtime process with a forward action and an independent downwardrange report. Across ten repeated operations, HALO withheld 10/10 stale forward actions, emitted 10/10 range reports, observed 0/10 matching stale setpoints, and returned 10/10 recovery candidates through fresh readmission. The representative trace shows initial retention, a support change before the governed effect, selective withholding of the action while the report remains available, and a fresh backtrack-and-land candidate. The Crazyflie photographs visualize this sequence; the formal evidence remains the component trace, adapter decision, and matching setpoint check.
Constrained-Motion Evidence The constrained-motion panel uses 14 scenarios with 20 warm repetitions in one fixed PX4/Gazebo configuration. It records 200 denied and 80 admitted or recovered segments. There were zero denied adapter calls, zero denied matching target-telemetry observations, 40/40 fresh recoveries, 40/40 detected post-final epoch or bounds mutations, and 280/280 oracle coverage. These warm repetitions characterize timing and configuration stability under the fixed PX4/Gazebo configuration. The separate post-final race panel removes one binding mechanism at a time. Within its tested epoch and bounds mutations, removing the final check, epoch binding, or bounds binding selectively exposes the corresponding stale component internally, while Full HALO blocks it. This is controlled ablation evidence at the measured boundary; it is not a general formal proof.
Recovery Cost The fixed recovery panel contains 48 routes. Thirty-six routes are executable after refreshed support, and 12 are terminal by catalog policy. Table 16 reports the final-state recovery oracle. Old-token, prior-sequence, and out-of-scope candidate
n Median (ms) p95 (ms) Max (ms)
Validation Final recheck Gate to adapter Adapter loop Motion completion Target activation Fresh recovery
280 280 280 80 80 79 40
0.325 0.491 0.005 0.010 0.005 0.011 1577.832 1747.882 1577.811 1747.859 1039.377 1155.511 1649.957 1763.999
23.205 0.030 0.031 1764.751 1764.739 1255.655 1765.188
rejection are tested separately in the deterministic protocol suite. These controls rejected five prior-authorization reuse attempts and one out-of-scope recovery candidate.
Protocol Computational Cost The computational-cost panel separates HALO protocol work from domain-specific predicate evaluation and downstream transport or execution. Table 14 reports pooled descriptive samples across the tested size configurations. Admission total begins at response validation and ends after binding-record creation, using predicate results computed before the timed interval. Fresh readmission begins after candidate production and ends after creation of the later-generation binding. Finalgate compute begins at gate entry and ends immediately before token consumption; token mutation and the adapter callback are excluded. All new intervals use time.perf_counter_ns with a reported one-nanosecond clock resolution. Admission and readmission values are per-call averages from batches of 50 calls after 20 explicit warm-up calls; garbage collection is disabled only within timed batches. Gate configurations use 301 direct timed calls after 50 warm-up calls. These measurements are steady-state Python-process measurements and do not mix PX4 cold starts. No benchmark invariant or execution failures occurred, and all measured samples, including the maximum gate observation, are retained. The size sweep varied |V | ∈ {4, 8, 16, 32} and graph density, reaching |Dϕ | = 200 at |V | = 32. The largest configuration-level admission median was 0.333 ms, with a largest p95 of 0.453 ms. A median regression of the form medianadm = α + βV |V | + βE |Dϕ | 2
yielded R = 0.9978. The gate sweep varied |Dϕ (e)| ∈ {0, 1, 2, 4, 8, 16} and |πe (Ct )| ∈ {1, 2, 4, 8, 16, 32}. Its largest median pre-consumption compute was 0.035 ms and largest p95 was 0.061 ms; the corresponding two-variable median regression yielded R2 = 0.9975. The observed scaling closely tracks the source-level bounds O(|V | + |Dϕ |) for admission after predicate evaluation and O(|Dϕ (e)| + |πe (Ct )|) for the final gate. Table 14 reports the shared core timing panel. The repository check supplies transfer evidence, while the 280-run PX4
Measured interval
Layer
n
Min
Median
Mean
p95
Max
Response validation Local-support aggregation Dependency closure Retained-set materialization Binding-record creation Admission total Fresh readmission total Final gate, pre-token Domain-predicate evaluation
Protocol Protocol Protocol Protocol Protocol Protocol Protocol Protocol Domain
1,212 1,212 1,212 1,212 1,212 1,212 1,212 10,836 1,212
0.0018 0.0004 0.0059 0.0003 0.0209 0.0348 0.0343 0.0038 0.0016
0.0063 0.0010 0.0203 0.0008 0.0850 0.1242 0.1233 0.0123 0.0059
0.0105 0.0012 0.0266 0.0008 0.0922 0.1448 0.1448 0.0157 0.0062
0.0349 0.0036 0.0716 0.0015 0.2063 0.3381 0.3415 0.0352 0.0125
0.0677 0.0061 0.1267 0.0037 0.3437 0.5344 0.5838 0.5967 0.0295
Table 14: Protocol and domain-predicate compute in milliseconds. Values use the nearest-rank p95 and retain all measured samples. Model generation, candidate production, token mutation, adapter callbacks, PX4 activation and motion, polling, and downstream transport are outside these intervals. The reported values therefore isolate the protocol and domain-predicate layers. Boundary
Trusted or enforced
Claim boundary
Raw structured proposal
Untrusted; it has no retention or dispatch authority Trusted computing base; malformed or mismatched inputs fail closed
Free-form semantic decomposition or intent recovery
Trusted inputs checked against the current component footprint Component-bound one-dispatch token enforcement at one process-local gate Measured internal-topic observation; direct hold markers and coarse process-phase alignment Downstream of governed adapter dispatch
Truth, availability, or completeness of providers
Schema, canonicalization, catalog, and dependency compiler Certificates, predicates, epochs, and bounds Token ledger and final gate PX4 ULog fingerprints and clocks Controller and physical world
Completeness of types, payload detection, or generic dependency compilation
Distributed transaction atomicity or exactly-once PX4 execution Full PX4 queue coverage or a shared host/PX4 clock Controller correctness, collision avoidance, or physical-flight safety
Table 15: Trusted inputs, enforced boundaries, and the corresponding scope of HALO’s claims.
Outcome
Result
Final-state oracle agreement Fresh executable recovery Terminal safe no-op Unauthorized dispatch Stale executable recovery
48/48 36/36 12/12 0/48 0/36
Table 16: Fresh component-local recovery outcomes.
validation interval measures domain tube validation. Adapter activation, motion, and recovery-total intervals are reported separately as downstream system behavior.
Reproduction and Validity Artifact Reproduction The submitted artifact contains raw JSONL/CSV traces, ULog analyses, JUnit XML, console logs, exact commands, environment records, and SHA-256 manifests. The claim-evidence matrix records each claim’s evidence layer, observation boundary, sample count, supported wording, and scope. The release launcher captures the base commit, porcelain status, binary diffs, submodules, untracked-file hashes, build settings, binary hash, logger profile, and launch allowlist before build and launch. Manifest-complete runs anchor the
reproduction package; earlier session-specific traces remain available as auxiliary evidence.
Threats to Validity The raw structured proposal is untrusted; the schema, canonicalization, catalog, and declared-dependency compiler are trusted computing-base components. The process-local token ledger and final gate define the enforced dispatch boundary. The FAA-anchored profiles evaluate the represented operational predicates, and PX4 status analyses use the preregistered runtime intervals associated with each component trace.
References Alshiekh, M.; Bloem, R.; Ehlers, R.; Könighofer, B.; Niekum, S.; and Topcu, U. 2018. Safe Reinforcement Learning via Shielding. Proceedings of the AAAI Conference on Artificial Intelligence, 32(1): 2669–2678. Ames, A. D.; Coogan, S.; Egerstedt, M.; Notomista, G.; Sreenath, K.; and Tabuada, P. 2019. Control Barrier Functions: Theory and Applications. In 2019 18th European Control Conference (ECC), 3420–3431. IEEE. Chang, E. Y.; Geng, L.; and Chang, E. J. 2026. Mnemosyne: Agentic Transaction Processing for Validating and Repairing AI-Generated Workflows. arXiv preprint arXiv:2607.00269. arXiv:2607.00269. Desai, A.; Ghosh, S.; Seshia, S. A.; Shankar, N.; and Tiwari, A. 2019. SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems. In Proceedings of the 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 138–150. Ichter, B.; Brohan, A.; Chebotar, Y.; Finn, C.; Hausman, K.; Herzog, A.; Ho, D.; Ibarz, J.; Irpan, A.; Jang, E.; Julian, R.; Kalashnikov, D.; Levine, S.; Lu, Y.; Parada, C.; Rao, K.; Sermanet, P.; Toshev, A. T.; Vanhoucke, V.; Xia, F.; Xiao, T.; Xu, P.; Yan, M.; Brown, N.; Ahn, M.; Cortes, O.; Sievers, N.; Tan, C.; Xu, S.; Reyes, D.; Rettinghouse, J.; Quiambao, J.; Pastor, P.; Luu, L.; Lee, K.-H.; Kuang, Y.; Jesmonth, S.; Joshi, N. J.; Jeffrey, K.; Ruano, R. J.; Hsu, J.; Gopalakrishnan, K.; David, B.; Zeng, A.; and Fu, C. K. 2023. Do As I Can, Not As I Say: Grounding Language in Robotic Affordances. In Liu, K.; Kulic, D.; and Ichnowski, J., eds., Proceedings of the 6th Conference on Robot Learning, volume 205 of Proceedings of Machine Learning Research, 287–318. PMLR. Inan, H.; Upasani, K.; Chi, J.; Rungta, R.; Iyer, K.; Mao, Y.; Tontchev, M.; Hu, Q.; Fuller, B.; Testuggine, D.; and Khabsa, M. 2023. Llama Guard: LLM-Based Input-Output Safeguard for Human–AI Conversations. arXiv preprint arXiv:2312.06674. arXiv:2312.06674. Koenig, N.; and Howard, A. 2004. Design and Use Paradigms for Gazebo, an Open-Source Multi-Robot Simulator. In 2004 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), volume 3, 2149–2154. IEEE. Li, P.; Zou, X.; Wu, Z.; Li, R.; Xing, S.; Zheng, H.; Hu, Z.; Wang, Y.; Li, H.; Yuan, Q.; Zhang, Y.; and Tu, Z. 2025. SAFEFLOW: A Principled Protocol for Trustworthy and Transactional Autonomous Agent Systems. arXiv preprint arXiv:2506.07564. arXiv:2506.07564. Liang, J.; Huang, W.; Xia, F.; Xu, P.; Hausman, K.; Ichter, B.; Florence, P.; and Zeng, A. 2023. Code as Policies: Language Model Programs for Embodied Control. In 2023 IEEE International Conference on Robotics and Automation (ICRA), 9493–9500. IEEE. Meier, L.; Honegger, D.; and Pollefeys, M. 2015. PX4: A Node-Based Multithreaded Open Source Robotics Framework for Deeply Embedded Platforms. In 2015 IEEE International Conference on Robotics and Automation (ICRA), 6235–6240. IEEE. Model Context Protocol Contributors. 2025. Model Context Protocol Specification, 2025-06-18: Tools.
https://modelcontextprotocol.io/specification/2025-0618/server/tools. Accessed 2026-07-21. Office of the Federal Register. 2026. 14 CFR Part 107: Small Unmanned Aircraft Systems. https://www.ecfr.gov/current/ title-14/chapter-I/subchapter-F/part-107. Current electronic edition; Sections 107.19, 107.37, 107.41, 107.49, and 107.51; accessed 2026-07-24. OpenAI. 2026. Function Calling. https://developers.openai. com/api/docs/guides/function-calling. Online documentation; accessed 2026-07-21. Parasuraman, R.; Sheridan, T. B.; and Wickens, C. D. 2000. A Model for Types and Levels of Human Interaction with Automation. IEEE Transactions on Systems, Man, and Cybernetics–Part A: Systems and Humans, 30(3): 286–297. Park, T.; Yoo, K.; Yoo, S.; and Kim, H. 2026. Selective Agentic Recovery for UAV Autonomy with a Persistent Mission Runtime. arXiv preprint arXiv:2606.14219. arXiv:2606.14219. Rebedea, T.; Dinu, R.; Sreedhar, M. N.; Parisien, C.; and Cohen, J. 2023. NeMo Guardrails: A Toolkit for Controllable and Safe LLM Applications with Programmable Rails. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing: System Demonstrations, 431– 445. Singapore: Association for Computational Linguistics. Ruan, Y.; Dong, H.; Wang, A.; Pitis, S.; Zhou, Y.; Ba, J.; Dubois, Y.; Maddison, C. J.; and Hashimoto, T. 2024. Identifying the Risks of LM Agents with an LM-Emulated Sandbox. In The Twelfth International Conference on Learning Representations. Schick, T.; Dwivedi-Yu, J.; Dessì, R.; Raileanu, R.; Lomeli, M.; Hambro, E.; Zettlemoyer, L.; Cancedda, N.; and Scialom, T. 2023. Toolformer: Language Models Can Teach Themselves to Use Tools. In Advances in Neural Information Processing Systems. Seto, D.; Krogh, B.; Sha, L.; and Chutinan, A. 1998. The Simplex Architecture for Safe On-Line Control System Upgrades. In Proceedings of the 1998 American Control Conference, volume 6, 3504–3508. IEEE. Wang, H.; Poskitt, C. M.; and Sun, J. 2026. AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents. In 2026 IEEE/ACM 48th International Conference on Software Engineering (ICSE ’26), 1–12. Association for Computing Machinery. Yao, S.; Zhao, J.; Yu, D.; Du, N.; Shafran, I.; Narasimhan, K.; and Cao, Y. 2023. ReAct: Synergizing Reasoning and Acting in Language Models. In International Conference on Learning Representations. Yates, R. D.; Sun, Y.; Brown III, D. R.; Kaul, S. K.; Modiano, E.; and Ulukus, S. 2021. Age of Information: An Introduction and Survey. IEEE Journal on Selected Areas in Communications, 39(5): 1183–1210. Zhan, Q.; Liang, Z.; Ying, Z.; and Kang, D. 2024. InjecAgent: Benchmarking Indirect Prompt Injections in Tool-Integrated Large Language Model Agents. In Findings of the Association for Computational Linguistics: ACL 2024, 10471–10506. Bangkok, Thailand: Association for Computational Linguistics.