When Can Agents Safely Checkpoint, Fork, Restore, and Merge? Exact Checking for Execution Edits

When Can Agents Safely Checkpoint, Fork, Restore, and Merge? Exact Checking for Execution Edits Yusheng Zheng∗ , Xiaoyu Song† , Yanpeng Hu‡ , Lebin Cheng§ , Yuxi Huang¶ , and Wei Zhang∥ ∗ University of California, Santa Cruz † University of Texas at Dallas ‡ ShanghaiTech University

arXiv:2608.22928v1 [cs.PL] 24 Aug 2026

§ RailXia

¶ Eunomia Labs

Abstract—Agent runtimes can Checkpoint an execution, Fork it, Restore a checkpoint, or Merge branches without restarting a task. We call these operations execution edits, with Checkpoint recording the current execution for later use and Fork, Restore, and Merge changing what the Agent will do next. An execution edit cannot undo an earlier authorization or a tool request already sent. An unsafe edit can therefore authorize the same tool action twice, discard a result the task still requires, or conflict with a call that began before the edit. The Agent is untrusted, so the runtime uses its execution record to determine which past actions an edit must account for and which required results it must preserve to keep the subsequent execution safe. Yet existing Agent systems support such operations without deriving what each edit must preserve from the running execution, whereas prior methods for computing safe behavior take that requirement as input. We give an algorithm that decides exactly whether an edit is safe. It returns all safe ways to continue, or proves that none exists. To make this decision, the algorithm lists every way the task can finish without violating policy. It removes any way that could make a still-required result impossible to finish later. If none remain, it returns a checkable proof that no safe implementation exists. Otherwise, the remaining ways describe exactly what the runtime may allow. Our formal results cover Checkpoint and the six forms of Fork, Restore, and Merge, together with extensions, atomic enforcement, and the information every exact checker needs. Lean mechanizes the finite checker and runtime invariant, and tests validate all six edit forms. The source code, Lean proofs, and executable tests are available in the public GitHub repository at https://github.com/eunomia-bpf/agent-check-restore-safety.

I. I NTRODUCTION Tool-using Agent runtimes can change an execution while it is in progress. They let an Agent Checkpoint an execution, Fork it into alternatives, Restore an earlier checkpoint, and Merge branches [1], [2], [3], [4], [5], [6]. These operations support exploration, recovery, and reuse without restarting the task. We call all four operations execution edits. Checkpoint records the current execution for later use, while Fork, Restore, and Merge change what the Agent will do next. Consider an Agent buying one laptop for a school. Before asking the school to approve the purchase, it saves checkpoint k. The school approves one purchase, and the Agent later chooses supplier R and authorizes payment. The Agent then restores k to compare supplier L and merges the L branch into the current execution. If the runtime sees only the restored

∥ University of Connecticut

workspace, it may request the same approval again or continue with L even though payment to R is already authorized [7]. Either behavior breaks the school’s purchasing rules because the first repeats a one-time approval and the second combines incompatible supplier actions. This example shows that the runtime cannot rely on the Agent’s account of the execution. The Agent may request an edit that omits an earlier action or a result the task still requires. The trusted runtime instead determines what may happen next from an execution record that the Agent cannot modify; in this example, the record remembers the one-time approval and the authorized payment to R. A tool action is an external operation governed by policy, such as approval, payment, or shipment. The runtime checks every tool action against policy. The runtime makes its security decision when authorizing a tool request. Sending the request later and recording its return cannot undo that decision. The runtime stores that decision in an authorization record, which later calls may reuse. Our security goal is therefore to prevent an edit from authorizing a tool action forbidden by policy or discarding a result that the task still requires. Meeting this goal requires four facts: (1) the task structure and its required results, (2) which calls refer to the same action, (3) earlier authorizations and call progress, and (4) which rules govern a call that overlaps the edit. Each fact can change the correct answer. The restored workspace, an execution trace alone, an authorization log alone, and the Agent’s own description each omit information the checker may need. Before an edit takes effect, the runtime records the finite set of relevant tool calls, their possible orders, and results. The Agent’s internal reasoning remains unchanged. Existing approaches cover parts of this problem but do not derive its complete safety condition. Agent systems provide branching, staged effects, transactions, or recovery checks [8], [9], [10], [11], [12], [13], [14], [15]. Control and synthesis choose behavior after a model of possible executions and desired final states has been supplied [16], [17], [18], [19]. Neither line of work derives from a recorded execution everything that a particular edit must preserve before it takes effect. Our key idea is to derive from the execution record what

checkpoint copy: new call, same action R current workflow

b0

k

xa

choice Fork

select Merge

bR join Merge

other branch disabled

Restore k x′a and continue reuse(x′a , da ) reuses earlier authorization s

L append only recorded calls and authorization order

rules in force

r

η0

a

atomic swap

pR

atomic swap ηF : L, R

atomic swap

ηR

ηJ

Fig. 1. Fork, Restore, and Merge change the current workflow but do not erase recorded calls. Restore creates a new call that refers to the same action as the original call. The atomic rule update orders authorization creation and reuse against the rule change.

each edit must preserve: earlier authorizations and every result the Agent choose the edited execution. The model preserves that remains required. Every result required before the edit past actions and every still-required result and proves that must remain required, already be satisfied by the recorded exact checkers must distinguish answer-changing cases from execution, or be explicitly removed by the same authority that all four record parts. required it. The Agent requests an edit under a registered edit 2) Exact checking and atomic enforcement. We construct an rule. The trusted runtime checks the recorded task structure executable checker that returns every safe way to proceed or and determines from that record, rather than from Agent text, a proof that none exists. Checkpoint has an exact check, and what may happen next and which requirements carry over. The the checker accepts each of the six forms of Fork, Restore, Agent therefore cannot obtain a favorable answer by describing and Merge exactly when the safety condition is enforceable. an execution that omits earlier actions or required results. Our formal runtime protocol rechecks the record, makes This idea creates three technical problems. First, calls copied accepted rules take effect atomically, preserves safety across by Fork or Restore may refer to the same underlying action, so repeated edits and restarts, and has the same Agent-visible the runtime must distinguish a new authorization from reuse of behavior as an ideal atomic machine. an earlier authorization and return value. Second, throughout 3) Mechanization and executable validation. Six Lean every allowed execution, every result that is still required and modules mechanize registration, all six edit forms, the still possible must retain a safe way to finish. The checker atomic rule update, concurrent calls, and preservation must enforce this condition without forbidding additional safe across finite executions. Nineteen paper-specific tests and behavior. Third, the rules for an accepted edit must take effect measurements over 2–128 results exercise the executable atomically with calls that overlap the edit and remain valid if checker. the runtime or machine stops unexpectedly and later recovers. We give an exact checker that computes every safe way for II. E XECUTION -E DIT S AFETY a requested edit to proceed or proves that every possible way Imagine an Agent buying one laptop for a school. It reserves is unsafe. For a requested edit, the runtime constructs every allowed complete execution from the current record. It removes the budget, saves checkpoint k, receives one purchase approval, an execution if allowing its calls one at a time could leave a and then compares suppliers L and R. A careless Restore still-required result without a safe completion. If none remains, or Merge could request approval twice, pay both suppliers, the runtime returns an independently checkable proof that no or permit shipment before the selected supplier is paid. A runtime rule set can enforce the edit safely. Otherwise, the safe execution approves the purchase once, pays exactly one remaining executions contain every safe way for the edit to supplier, and permits shipment only after that payment. The resulting workflow records which calls may occur, proceed. Before the edit takes effect, the runtime checks the current execution record again and atomically switches to the in what order, and which results count as completion. In newly computed rules. Each overlapping call is checked entirely this example, it authorizes at most one purchase. The Agent under either the old or new rules. Figure 1 illustrates this reserves the budget and saves checkpoint k before approval. process for an approval task containing Fork, Merge, Restore, The approval is then authorized once, creating an authorization and calls that overlap the atomic rule update. After Restore, the record that Restore does not delete. The Agent next requests repeated approval call reuses the earlier authorization record a Fork between suppliers L and R. The workflow allows two results: order from L or order from R. In either result, payment instead of authorizing the approval again. authorization must precede shipment authorization: a) Contributions: oL : xpL ≺ xsL , 1) Safety model. We define Checkpoint, Fork, Restore, and (1) Merge safety from the execution record rather than letting oR : xp ≺ xsR , R

where xpi and xsi are payment and shipment calls. A workflow call x is one place in this structure where the runtime can invoke a tool. The function qact (x) = d records which tool action the call refers to. Calls that refer to the same action share one authorization record. In this example, both shipment calls authorize the same one-order shipment:

a) A smaller workflow can be less safe: In the laptop example, the current workflow allows the school to buy through supplier L or supplier R. Suppose the Agent edits it to keep only L. Every remaining call may obey the purchase policy, but the edit removes the still-required R result. The edit is safe only if the record shows that the R purchase has finished or that the school allowed its removal. The runtime must therefore derive what the edit must preserve from the execution record, not from the proposed workflow. qact (xsL ) = qact (xsR ) = ds . b) Two safe plans may have no safe way to run together: The two payment calls instead refer to different actions dpL Suppose a release workflow must support both normal release and dpR . and emergency release. The normal plan obtains approval The authorization log ∆ records newly authorized actions in y before deployment x, producing yx. The emergency plan order. The notation lab(∆) keeps only their authorization labels. deploys first and then files an emergency report z, producing xz. Budget reservation contributes r, approval contributes a, the The policy A = {ϵ, x, y, xz, yx} permits both orders, so either two payments contribute pL and pR , and shipment contributes plan is safe when checked alone. In the combined workflow s. At the Fork request, lab(∆) = ra. The policy allows every X ⊗ (Y ⊕ Z), both plans contain x. Allowing x first leaves partial authorization sequence of rapL s and rapR s, but never the normal plan able to finish only in the forbidden order xy, both payments or a payment before approval. Although the while blocking x makes the emergency plan impossible. The supplier results are exclusive, both must still have a safe way runtime cannot make either choice while keeping both plans safe, so the exact checker returns Reject. to finish when the Fork is checked. c) An edit can change from Accepted to Reject without a new authorization: An edit verdict applies only to the A. Accepted and Rejected Forks execution record that the checker examined. In figure 1, Restore The Agent sends u = ForkChoice(b, σ), which names a copies an approval call as x′a . The original call and x′a refer current branch and a registered edit rule. Here, the rule to the same authorized action da . Processing x′a therefore identified by σ turns branch b into the exclusive supplier-L and adds no authorization-log entry, but it still moves the restored supplier-R copies shown below. The trusted runtime constructs branch past approval. A concurrent Merge or Restore that was the edited workflow from the execution record. It also derives Accepted before this call may be rejected afterward. If the new the results that remain required and the action referred to by verdict is Reject, the edit must not take effect in that execution every workflow call. state. Requesting authorization for da again cannot undo this Write Mo for the ways to complete result o while obeying progress because the runtime reuses da ’s existing authorization the policy. Each result has one allowed call order: record. The runtime must discard the earlier verdict and check the edit against the new record. A later check can change its zL = new(xpL , dpL )new(xsL , ds ), answer after a relevant fact changes, such as completing a required result or authorizing its removal, but not by resetting zR = new(xpR , dpR )new(xsR , ds ). recorded history. Thus MoL = {zL } and MoR = {zR }. These sequences contain d) Saving every call and authorization is still not enough: the calls after the edit, while the existing log contributes the Suppose the runtime retains all workflow calls, actions, and earlier authorization sequence ra. The verdict is Accepted: authorization records but loses the links among them. It can both supplier results remain possible, the calls performed so no longer tell whether a restored “approve purchase 42” call far always obey policy, and each result can be completed. reuses purchase 42’s authorization or needs a new one. The tool If policy excludes rapR s, then MoR = ∅, and the Fork is name and call text cannot recover this information. Theorem 4 rejected because pruning supplier R would change its meaning. proves that two records containing the same calls, actions, and Rejection returns a proof listing the order in which completions authorizations can require opposite verdicts when these links were removed and the reason for each removal, rather than differ. An exact runtime must therefore record which action letting the Agent weaken the requested edit. each workflow call and authorization refers to. e) There is one largest safe set of call orders: Safety could in principle admit several incomparable rule sets, each allowing III. I MPLICATIONS OF E XECUTION -E DIT S AFETY call orders that the others block. Section IV instead proves that This section explains six consequences of our formal results the checker returns one safe execution set containing every for runtime design. Here, a result means one way the task can other safe execution set. The generated runtime rules therefore finish, such as completing the laptop purchase through supplier combine all call orders that can coexist without violating policy L or R. It is not a value returned by a tool. A result remains or preventing a required result from finishing. required until the execution record shows that it has finished f) Exactness survives later calls, edits, and restarts: or that the party requiring it allowed its removal. The exact guarantee is not limited to the first accepted edit.

After allowed calls have run, checking the remaining workflow words containing each member of Xp once and respecting ≺p . again gives the same safe ways to finish as the installed rules. A workflow contract C = (O, {po }o∈O ) assigns one pomset Later Fork, Restore, and Merge requests, rule updates, stops, to each member of a finite nonempty result set O. For the and restarts preserve the same guarantee. Every later edit is laptop, the contract has results oL , oR , and poL orders the Ltherefore checked under the same exact safety condition as the payment call before the L-shipment call. Each index o names first. one allowed result. A result is complete once every workflow Section IV formalizes the execution record and safety goal. call in its pomset has been processed in an allowed order. Section V defines the checker, and sections VI and VII show Two results remain distinct even if the callsSstill required later become identical. Write XC = o∈O Xpo and how the runtime installs its rules atomically and preserves the for them S CL(C) = o∈O Lin(po ). We require the runtime to distinguish guarantees above. completed work from work that has more calls. For sequences IV. M ODEL AND S ECURITY O BJECTIVE v, w, write v ⪯ w when w = vs for some sequence s. The model leaves the Agent’s internal reasoning unrestricted v, w ∈ CL(C) ∧ v ⪯ w =⇒ v = w. and requires every tool call to pass through the trusted runtime. Each call identifies its registered place in the workflow, presents This condition permits incomparable traces and different results an authorization token, and submits a concrete tool request. with the same trace, so it does not require deterministic The runtime either creates a new authorization, reuses an results. It requires a registered workflow call whenever more authorization already recorded in the log, or rejects the call. work can follow the same sequence of processed calls. The We analyze calls in independently enforceable groups. Calls interface represents a choice between stopping and continuing governed by one policy, one authorization log, and one atomic by a registered terminal workflow call checked by the trusted rule change form a policy domain. For example, the laptop runtime. Contracts use the three partial constructors below. Each approval, payment, and shipment calls form one policy domain when they share the school’s purchase policy and authorization constructor requires operands with disjoint workflow calls and log. Policy domains with disjoint actions, logs, and policies preserves the condition that no complete call sequence can be compose independently. Every individual state is finite, while properly extended into another. the theory covers executions of arbitrary finite length. The OC⊕D = ({L} × OC ) ⊎ ({R} × OD ), execution record stores the workflow and checkpoints, which p(L,o) = po , p(R,v) = pv , calls refer to the same action, earlier authorizations and call OC⊗D = OC × OD , progress, queued requests, and the rules currently in force. The (2) trusted runtime protects this record from Agent modification. p(o,v) = po ⊎ pv , The model has one security objective. Every admitted execution OC▷D = OC × OD , must obey policy, remain completable, and preserve a safe p(o,v) = po ▷ pv . completion for every still-required result. The remainder of this section defines the execution facts needed to state that Before adding a registered or copied operand, the trusted objective precisely. runtime deterministically assigns fresh workflow-call IDs and extends ρ while retaining which tool action each call refers to. A. Workflow results and call order Well-formedness already makes carried operands disjoint. In a) Basic objects: We capitalize Agent for the untrusted equation (2), ⊎ adds no cross-order and ▷ orders every event of principal requesting execution edits. A workflow call x is one p before every event of q, while choice uses a tagged union of place where the workflow can invoke a tool. The function result indices and parallel and sequence use Cartesian products. qact (x) = d records the tool action referred to by that call. Consequently, choice retains each arm’s full indexed family, Several workflow calls may refer to the same action d, in parallel pairs results while permitting every causal linearization, which case they share one authorization record. The first and sequence adds a barrier. After call sequence w, C/w retains authorized call creates that record, and calls copied by Fork each result whose pomset has a linearization beginning with w, or Restore later reuse it. In this paper, a workflow call is then removes the workflow calls in w and their order edges. The processed when the runtime either authorizes its tool action expression is undefined if no result remains. This operational for the first time or reuses that action’s existing authorization “remaining contract” preserves result and workflow call identity. record. Processing does not mean that the remote action has For example, after the L-payment call, the remaining contract completed: sending a newly authorized request and recording its for oL contains only the L-shipment call. returned value happen later, and neither adds another processed Lemma 1 (Completion remains unambiguous). For every workflow call. The execution record also stores where every defined C/w, no complete sequence can be properly extended copied workflow region came from. T, ∆, χ denote the current into another, and either every retained pomset is empty or none workflow, authorization log, and ordered record of processed is empty. workflow calls. A pomset p = (Xp , ≺p ) is a finite set of workflow calls Proof. If a remaining sequence v can be properly extended with a strict partial order. Its linearizations Lin(p) are the into v ′ , then wv can be properly extended into wv ′ in CL(C).

K maps checkpoint IDs to immutable earlier branch records. Write Ck = contract(K(k)) for the remaining contract stored by checkpoint k. Σζ is an immutable, versioned registry of typed edit rules. ρ records, for each workflow call, its action, authorization token, source region, scope, canonical tool request, B. Execution Record and request digest. The source region identifies the registered 1) Recorded structure and current workflow: The execution workflow region from which the call originates, while the record separates immutable past events, the current workflow, scope limits where its authorization token may be used. For registered edit rules, call identities, progress, and the active example, a copied payment call retains the source region of the registered payment step and its purchase-domain scope. rule version. The workflow part of the execution record is ρ ρ Write qact (x) for the action field of ρ(x). For d ∈ im(qact ), H = (ω, G, T, K, Σζ , ρ, β, χ, ver, η). (3) let invρ (d) be the common canonical-request field of calls x ρ ω identifies the policy domain, and η identifies the version of with qact (x) = d. Let U be the authorization-label alphabet. the rules currently in force. G records the finite sequence of Independently, ℓ(d) ∈ U is the authorization label certified for workflow versions. Its node IDs, registered contracts, signed tool action d by the registered call model. For each current result requirements, and Fork, Restore, and Merge records do workflow call x, β(x) = (j, η) records the rule entry j and not change. Each branch node b carries an immutable registered version η used to check it. χ records processed workflow contract Γb . Its ordered progress record χb lists the workflow calls in order, including whether each created or reused an calls already processed on that branch. The immutable records authorization record, and ver is the state version. χ records form a directed acyclic graph (DAG) whose edges record typed authorization and workflow progress, while the remote service Fork, Restore, and Merge operations. T is the current workflow. records completion and the returned value. Checkpoint(k, b) creates a checkpoint for a current branch T ::= b:C | T ⊕sg T | T ∥g T | join(T, T ) | T ; T. b under a fresh checkpoint ID k. A trusted transaction stores a signed copy of branch b’s remaining contract Cb , ordered s ∈ {open, L, R} records an unresolved choice or the arm progress record χ , relevant calls, and result requirements. b that made recorded progress, and g groups exclusive or jointly The checkpoint check requires C = Γ /raw(χ ), and the b b b active siblings. [[T ]] uses both arms of an open choice and only transaction advances ver without changing the current workflow, the selected arm thereafter. It interprets parallel and join with authorization records, β, the active rule version, or the ⊗, and sequence with ▷. The join marker records a completed authorization sequence. This internal transition changes H, Merge and prevents the same group from being merged again. so a rule update computed from the earlier record will fail its T is complete when every pomset in [[T ]] is empty. Lemma 1 final check. Restore accepts only records created by this rule. ensures that the remaining workflow cannot contain both empty 2) Well-formedness: and nonempty pomsets. Set heads(b:C) = {b}. An open choice makes both arms current, a selected choice makes its winner Definition 1 (Well-formed execution record). H is well formed current, parallel and join make both arms current, and sequence when the following groups hold. makes its left operand current until completion and then its 1) Structure. G is acyclic, and branch and group IDs are right. Processing a workflow call updates the work remaining globally unique across the recorded DAG and current at its leaf without deleting the recorded structure. Because workflow. Every ID that an edit may name has a unique sequence checks complete, it retains completed results from its context decomposition, and every node in heads(T ) is left operand, so an isolated completed leaf remains available currently maximal. Every checkpoint names an immutable for a later Fork or Restore. Joining removes g immediately node and stores copies of its remaining contract and ordered but keeps its remaining work behind a barrier until both arms progress record. Every original or edit-introduced result complete. A workflow call is enabled when it is minimal names exactly one policy authority in a signed record. The in some pomset of [[T ]]. Disjoint workflow calls and unique trusted runtime preserves that record when it carries or context decomposition give every enabled x a unique current copies the result or stores it in a checkpoint. leaf leaf T (x) = b. For a ∈ {new(x, d), reuse(x, d)}, define the 2) Identity and progress. For every recorded workflow call x, ρ paired execution update qact (x) = qact (x). Workflow-call IDs and the j identifiers
in β are unique, while workflow calls that refer to the same HStep((G, T ), a) = G ∥ (b, a), T /(x, a) , b = leaf T (x), action agree on which trusted runtime authorized them, their scope, canonical request, digest, and source region. where G ∥ (b, a) appends progress record (b, a), and T /(x, a) Processed workflow calls are downward closed in their removes the processed call from the current leaf and records pomset, consistent with every choice status, and absent any selected choice. Write HRes((G, T ), r) for iterating this from the remaining workflow. update over a resolved word r. addr(T ) is the set of branch and group IDs that an edit may 3) Current workflow. dom(β) = X[[T ]] , and β maps every currently name. It includes each current group and the current current workflow call x to exactly one entry jx under the part of a sequence. domain’s current rule version η. Every current leaf b:C If one retained pomset is empty and another is nonempty, choose a nonempty linearization v of the latter. Then w can be properly extended into wv. Both contradict the condition that no complete sequence can be properly extended into another.

equals its immutable registered contract Γb after removing the workflow calls recorded in χb ; the caller cannot replace it with a smaller result set. Every constructor in T is defined, so no complete sequence in any subtree can be properly extended into another. 4) Edit rules and domain. Every edge and introduced contract follows one immutable edit rule at version ζ. Every current, checkpoint, or rule-introduced workflow call, action, source region, and scope belongs to ω. Tool actions, authorization logs, and policies of distinct domains are disjoint, and an edit never crosses a domain. The policy domain has exactly one active rule version, namely the version recorded in H.

an unexpected stop and restart, each transaction appears entirely before or entirely after its linearization point. Before the checker reads the execution record, the trusted runtime may instantiate finitely many registered templates for tool calls. For tool request m, it computes canonical request m◦ = canonκ (m), reuses an action certified for m◦ or allocates a fresh one, and signs (x, j, d, scope, digest(m◦ ), origin) into the authenticated registry. The resulting finite model R contains the workflow’s tool calls and remains unchanged while the checker evaluates that execution record. The runtime rejects any call that does not match the registered model. One execution record outside the Agent’s control contains workflow W, finite model R, edit rules, request-normalization rules, policy, checkpoints, authorization log, and queued requests. From that record and an 3) Authorization and completion: The remaining parts of the Agent request naming an edit and its objects, the trusted runtime execution record are policy version κ, a regular authorization derives the edited workflow, required results, authorization policy A ⊆ U ∗ closed under truncation, authorization log ∆, decision for each call, safe execution set or rejection proof, and queue out of requests waiting to be sent. Authorization and the rule entry and authorization token for each remaining records can only be appended. A completion update advances call. Every derived object therefore comes from the execution an authorization record’s status and stores the returned value. record rather than being chosen by the Agent. Each authorization record binds its action, immutable canonical Registration turns the tool-call behavior of a typed Agent tool request, creator workflow call, and authorization label. workflow into the finite model R. CheckReg verifies exact Each entry in χ points either to the authorization record it correspondence of results, call order, actions, and first-time created or to the earlier record it reused, so (χ, ∆) determines authorization records. The model stores these traces as runs retry and return lookup. lab(∆) is the sequence of authorization labeled by result, written BRuns(R), together with a map λ labels on calls that create authorization records. Restore may from source traces. Write W ⊑ R when λ is a bijection preλ reconstruct workspace data but leaves ∆ unchanged. A returned serving results, which calls refer to the same action, call order, value may lead the Agent to request another registered edit, result authority, and authorization-log updates. Definition 6 which the runtime checks from the updated execution record. and lemma 13 give the exact finite check and proof. Registered The execution record (κ, H, ∆, out, A) is well formed when contracts enter through CheckReg, and an idempotent or H is well formed, lab(∆) ∈ A, each action has at most one queryable remote service supplies signed completion records authorization record, each processed call names the record it for its actions. created or reused, the authorization log, request queue, and policy belong to ω, and the queue preserves the order of new D. Security Objective authorizations. All definitions and results below quantify over The security objective is fixed independently of the checker such well-formed execution records. that will implement it. For an edit derived from the execution C. Adversary and trusted boundary The adversary controls Agent output, edit requests, tool arguments, copied workspace, retries, stale authorization tokens, and scheduling, including races between calls and edits. It cannot forge registries, the checkpoint directed acyclic graph (DAG), the record of which calls refer to the same action, the policy, or the authorization log. The policy authority signs policies, result requirements, and authorized removals. In the laptop example, the school is the policy authority: it signs the one-purchase requirement and any permission to remove a supplier result. The trusted runtime registers tool calls, actions, and authorization tokens, and it derives and checks each edit. The trusted runtime checks the answer again before atomically changing the rules in force. The policy authority, trusted runtime, registries, authorization log, proof verifier, and transaction mechanism form the trusted computing base (TCB). Within one policy domain, the TCB checks every tool call and commits every state change and edit answer returned to the Agent through a linearizable transaction. After

record, a safe execution set satisfies four requirements. First, it preserves every source result that is neither already satisfied nor explicitly authorized for removal, and every allowed execution belongs to the derived target workflow. Second, every allowed partial execution obeys the policy after accounting for authorization records already present in the append-only log. Third, each allowed partial execution extends to a complete allowed execution. Fourth, every result still compatible with an allowed partial execution retains such a completion. For example, at the laptop Fork, the set must retain both supplier results unless the school authorizes removing one, admit only approval–payment–shipment orders allowed by policy, and preserve a completion from every admitted partial execution for each supplier result still compatible with that execution. Thus the checker cannot call the edit safe merely because the surviving L execution obeys policy after all completions of R have been pruned. The last requirement rejects the two-result example in section III, where separately safe results cannot remain safe under one set of runtime rules. Definition 2 states these requirements over executions labeled by result. Lemma 4

then proves that the checker computes the largest safe execution set. V. E XACT C HECKING OF E XECUTION E DITS The checker first derives the edited workflow prescribed by the execution record and the requested edit. It then decides whether each workflow call creates or reuses an authorization record and removes precisely those complete executions that violate the security objective after some partial execution. A. Constructing the Edited Workflow 1) Checking an edit rule: Fork, Restore, and Merge have the six disjoint constructors of Edit6 shown in table I. Checkpoint, the initial rule update, later rule registration, and tool calls use their own transitions. An Agent request u names an edit kind, current object IDs, and edit-rule ID σ. Registry Σζ records the expected source and checkpoint patterns for σ, any workflow steps the edit adds, the source region for each copy, and the authority that signs each introduced result. The checker constructs explicit preservation maps for every region that the rule carries or copies. Consider a source contract C, target region D, and parent map µ : XD → XC . Write C ≼µ D when µ is a global bijection and preserves actions and source regions. The relation also requires a surjection π : OD ↠ OC that satisfies the conditions below for every target result v. x ∈ Xpv ⇐⇒ µ(x) ∈ Xpπ(v) , x ≺v y ⇐⇒ µ(x) ≺π(v) µ(y). Because µ is one global bijection and preserves which results contain each call, it cannot split a source call shared by several results into separate target calls. For candidate T ′ , let Ru index the disjoint regions carried or copied inside the replaced subtree. Pu = {(Cr , Dr , µr , πr )}r∈Ru collects these preservation maps. A separate identity map verifies that the surrounding workflow preserves syntax, results, workflow calls, actions, source regions, and order. Writing Xctx for its workflow calls and Xadded(u) for workflow calls added by the rule, the checker verifies the following disjoint cover. ] X[[T ′ ]] = Xctx ⊎ XDr ⊎ Xadded(u) . r∈Ru

The edit rule and surrounding workflow induce prur : O[[T ′ ]] ⇀ ODr . For choice, this map is defined only in the arm containing r, while product and sequence select the corresponding indexed component. Define EditedRequiredu = {(r, o) | r ∈ Ru , o ∈ OCr }, Coversu (t, r, o) ⇐⇒ ∃v ∈ ODr .

prur (t) = v ∧ πr (v) = o.

Let Ounchanged be the results outside the edited region, and let ιuctx : Ounchanged ,→ O[[T ′ ]] be their unchanged embedding

into the target. Define the results that remain required and the target results that cover them by StillRequiredu = EditedRequiredu ⊎ ({ctx} × Ounchanged ), Coversu (t, (ctx, o)) ⇐⇒ t = ιuctx (o).

(4)

For a = (r, o) ∈ EditedRequiredu , Coversu (t, a) denotes the relation above. The checker also requires ∀a ∈ StillRequiredu . ∃t ∈ O[[T ′ ]] . Coversu (t, a): every required source result has a complete target result, shared workflow calls remain shared, and inherited calls remain distinct from steps added by the edit rule. The edit-rule check uses the following judgment. Σζ ; H ⊢edit u ⇒ (T ′ , Pu ) It holds exactly when every named object belongs to addr(T ), every introduced object belongs to ω, the source pattern matches, the preservation maps and disjoint cover hold, every still-required result is covered, every removal carries the proper authority, and [[T ′ ]] is defined. The policy authority may authorize removal of the unselected arm of a typed MergeSelect or the current branch of RestoreReplace, using the signed sets defined below. 2) Preserving Required Results: The registered edit rule determines every result that the edit must account for. Fork accounts for both copies, Restore for the current and checkpoint branches, MergeSelect for the selected and unselected arms, and MergeJoin for both arms. Results outside the edited region remain unchanged. Definition 4 defines the results required before the edit, those already satisfied, and those whose removal the policy authority signed. The checker accepts the edit rule when the target-derived set from equation (4) satisfies StillRequiredu = RequiredBefore(H, u)
\ SatisfiedH,u ⊎ AuthorizedRemovalH,u , and hence the exact disjoint partition RequiredBefore(H, u) = StillRequiredu ⊎ SatisfiedH,u ⊎ AuthorizedRemovalH,u . This partition accounts for every source result and prevents an Agent request from dropping one without authorization. The preservation maps retain actions, source regions, and order, while the rule update retains the records for satisfied results and authorized removals. Let E[−] be the current workflow with one editable region replaced by a hole. carry preserves branch, result, and workflowcall IDs, pomset order, actions, signed result authorities, base contracts, ordered progress records, and nested choices. cloner assigns fresh branch, result, and workflow-call IDs while preserving pomset order, actions, scope, digest, source regions, and the authority for each result. Each copied branch starts from its registered remaining contract with an empty progress record. Branches added by an edit rule likewise start from their registered contract and an empty progress record. The

contracts EσL , EσR , EσJ are additional workflow steps derived from the rule registry. Define Lσ = cloneL (C) ▷ EσL ,

Rσ = cloneR (C) ▷ EσR .

winner, mismatched rule pattern, unauthorized removal, or undefined composition produces Invalid. Independent domains step by asynchronous product, and each domain replaces all of its runtime rules at once.

New identifiers and the target rule version η + are determinis- Lemma 2 (Exact edit derivation). For well-formed H, the tically allocated from (ω, ζ, ver, u, role). role identifies which judgment in equation (5) is deterministic. If it derives H ′ , then operation argument receives each new ID. Write Copyr (C) H ′ is well formed. It preserves required results and their signed for (C, cloner (C), µr , πr ), and Keep(C) for (C, carry(C), µ, π). authorities, retaining a record for every satisfied result and Each abbreviation asserts the corresponding ≼µ relation. For every still-required source result except a signed authorized a current workflow T0 , Keep(T0 ) abbreviates Keep([[T0 ]]) and removal. The surrounding-workflow identity map and family Pu has target contract [[carry(T0 )]]. Every b or g named below preserve which calls refer to the same action, source regions, must lie in addr(T ). the authority for each result, and causal order. For every In an open choice, the first processed workflow call atomi- a ∈ StillRequiredu , some complete target result t satisfies cally selects its arm and disables later calls from the other arm, Coversu (t, a), including every unchanged result outside the whether that first call creates or reuses an authorization record. edited region. Every current target workflow call x has β ′ (x) = Consequently, MergeSelect(g, w, σ) is valid precisely while (jx+ , η + ) and an authorization token for jx+ . the unselected arm has made no recorded progress. MergeJoin replaces the current ∥g node with join, removes g from the set Proof sketch. The six cases use the copy/keep bijections and of IDs an edit may name, and prevents the same pair from surrounding-workflow identity map to preserve action sharing, source regions, and order. They also construct a target result being joined again. 3) Preparing calls for the new rules: Every Fork, Restore, satisfying each required Coversu relation. The′ common+ state + or Merge edit prepares replacements for all runtime rules update establishes well-formedness and sets β (x) = (jx , η ) in its policy domain. Before the edit takes effect, β(x) uses for every current target workflow call. Section A-D1 gives the η − = η for every current call x. The judgment for these six full argument. forms consists exactly of one row of table I applied inside the This section defines the checker semantics in two steps. It well-typed workflow context E, followed by the state update first classifies each workflow call as a new authorization or below. Let eu contain the edit record and exactly the copied, reuse and then computes the largest set of executions that added, and group nodes prescribed by T ′ ; carried node IDs remains safe throughout execution. remain unchanged. For every current target workflow call x, Recall the authorization-label alphabet U and regular policy the trusted runtime deterministically creates a rule entry jx+ A ⊆ U ∗ , which is closed under truncation. For authorization ′ and authorization token h+ x . The updated record ρ preserves log ∆, lab(∆) ∈ A is its authorization sequence and D∆ is the the action, source region, scope, digest, and retry information. set of actions that already have authorization records. Fix Θ = Define (κ, H, ∆, out, A, u) and write state(Θ) = (κ, H, ∆, out, A). Hu+ = {(x, jx+ , h+ x ) | x ∈ X[[T ′ ]] }, Derive is a partial function. For a valid initial rule update, β ′ (x) = (jx+ , η + ). a Fork, Restore, or Merge edit, or a registered extension, it The new authorization tokens are inactive and inaccessible to produces a unique derived record. Otherwise, it is undefined. − + the caller before the rule update takes effect. The complete When defined, write Derive(Θ) = (κu , Hu , Au , Cu , η , η ). Root derivation additionally requires that CheckReg(W, R) judgment is shown below. accept. Each Fork, Restore, or Merge edit has (κu , Au ) = Σζ ; H ⊢ u ⇓(H ′ , CH,u , η − , η + ), (κ, A) and uses the unique edit judgment. Extend(ξ) adds signed entries for edit rules, calls, the authority for each result, H ′ = (ω, G · eu , T ′ , K, Σζ , ρ′ , β ′ , χ, ver + 1, η + ), ′ − and policies while preserving the current workflow, its progress, CH,u = [[T ]], η = η. (5) and all earlier authorizations. Section A-D2 gives the judgment. ′ Here H is the derived target record. It becomes current and Let ρu be the target registry in Hu , let OH,u = OCu , and use ′ ′ activates η + only through the atomic rule update. In this record, H = Hu and ρ = ρu where earlier notation is convenient. G · eu retains earlier progress, the authority record for each The execution sets below use Θ, the edit-rule registry, ρu , and result, and existing nodes. It initializes each copied or added target policy Au . Before the rules change, the trusted runtime branch from its remaining registered contract, gives each result checks the complete record again, including queued requests an inherited or rule-signed authority record, and records no out, so sending a request concurrently makes an earlier answer progress for the new branch. Thus the derivation preserves stale. We abbreviate the fixed parameters by writing H, u. K, Σζ , χ, appends one record of the edit and its target nodes, and prepares a new rule entry and authorization token for B. New and Reused Authorizations every target call under η + . Table constructors determine new The same tool action may appear at several workflow-call group modes, while carried nested modes remain unchanged. positions after Fork or Restore, but it must be authorized at A nonexistent checkpoint, wrong group mode, nonmember most once. Function Resolveρ∆u keeps every workflow call and

TABLE I T HE SIX FORMS OF F ORK , R ESTORE , AND M ERGE . Eσ• IS DERIVED FROM THE REGISTERED EDIT RULE IN Σζ . Operation u

Required current shape

Derived target shape

Checked preservation

ForkChoice(b, σ) ForkParallel(b, σ) RestoreReplace(b, k, σ)

E[b:C] E[b:C] E[b:C], k ∈ dom K

E[bL :Lσ ⊕open bR :Rσ ] g E[bL :Lσ ∥g bR :Rσ ] E[bk :clonek (Ck )]

RestoreLive(b, k, σ) MergeSelect(g, w, σ)

E[b:C], k ∈ dom K E[TL ⊕sg TR ], s ∈ {open, w}

E[b:carry(C) ∥g bk :clonek (Ck )] J E[carry(Tw ); bJ :Eσ ]

MergeJoin(g, σ)

E[TL ∥g TR ]

J E[join(carry(TL ), carry(TR )); bJ :Eσ ]

{CopyL (C), CopyR (C)} {CopyL (C), CopyR (C)} {Copyk (Ck )}; current branch removed {Keep(C), Copyk (Ck )} {Keep(Tw )}; other arm removed {Keep(TL ), Keep(TR )}

annotates it as creating a new authorization or reusing an earlier one. Starting with D0 = D∆ , it maps a call sequence w = ρu x1 · · · xn to annotated sequence z1 · · · zn . For di = qact (xi ), ( new(xi , di ), di ∈ / Di−1 , Di = Di−1 ∪ {di }; zi = (6) reuse(xi , di ), di ∈ Di−1 , Di = Di−1 . auth keeps the authorization label of each new authorization and contributes nothing for reuse. auth(new(x, d)) = ℓ(d),

auth(reuse(x, d)) = ϵ.

For annotated z, raw(z) drops the new/reuse annotation and action while preserving the ordered workflow-call IDs. A Retry repeats the same canonical request and adds no workflow call. Restored workflow calls that share an action remain distinct. The first call creates the authorization record, and later calls reuse it.

Here an execution is complete when every workflow call for its result has been processed, and requests and returns add no new or reuse events. For an annotated partial execution z, let Compat(z) = {o | raw(z) ⪯ w for some w ∈ Lin(po )}. For a set B of finite sequences, write ↓B = {z | ∃y ∈ B. z ⪯ b means that every result in y}. PreservesRequired(H, u, B) StillRequiredu is covered by some target result represented b in B: ∀a ∈ StillRequiredu .

b Coversu (t, a). ∃(t, y) ∈ B.

Definition 2 (Safe execution set). The checker tracks both the partial executions that the runtime may currently allow and the complete executions that justify allowing them. A b where L contains allowed safe execution set is a pair (L, B), b partial executions and B contains allowed complete executions Lemma 3 (New/reuse classification). Resolveρ∆u is determin- labeled by result, satisfying the conditions below. At the laptop b contains the L and R payment–shipment istic, preserves length, and gives the same annotations for Fork, for example, B the calls shared at the start of two sequences. Among calls executions labeled by oL and oR , while L contains their partial annotated as new, each action occurs at most once outside D∆ , executions. and dropping the annotations gives exactly the input sequence. 1) B b ̸= ∅; Moreover, if Resolveρ∆u (rv) = zv ′ , then z = Resolveρ∆u (r) 2) workflow and results: PreservesRequired(H, u, B), b B b ⊆ U S and v ′ = Resolveρ∆uz (v), where ∆z extends ∆ by the new o∈OH,u {o} × Ro (H, u), and L ⊆ ↓( o∈OH,u Ro (H, u)); authorizations in z. 3) policy: lab(∆) auth(z) ∈ Au for every z ∈ L; b and Proof. Induction on input length shows that each annotation is 4) completion from every partial execution: L = ↓(π2 B); determined by the calls seen so far and that Di changes exactly 5) every compatible result remains completable: for every when the function creates a new authorization. Set membership b extends z. z ∈ L and o ∈ Compat(z), some (o, y) ∈ B ensures at most one new authorization per action. Both cases Checking each result separately is insufficient. After a partial retain xi . Splitting after r gives the stated composition equation. execution shared by several results, every result still compatible with that partial execution must retain a policy-safe completion. Thus a retry changes neither the processed-call record nor The operator below removes exactly the complete executions the authorization sequence, although its successful API reply that violate this condition. Removing one completion may is observable as Return(t, [v]∼ = ). A copied workflow call that make another partial execution unsafe, so the checker repeats reuses an authorization record advances the processed-call this pruning until no further execution must be removed. Put record without changing the authorization sequence. ] b0 = B {o} × Mo . C. Safe Completion Throughout Execution o∈OH,u

1) Computing the largest safe execution set: For each derived result o ∈ OH,u , define all of its complete executions and the subset allowed by policy. Ro (H, u) = {Resolveρ∆u (w) | w ∈ Lin(po )}, Mo (H, u) = {z ∈ Ro (H, u) | lab(∆)auth(z) ∈ Au }.

(7)

b⊆B b0 , define the monotone operator For B   ∀z ⪯ y. ∀o′ ∈ Compat(z). b b b Φ(B) = (o, y) ∈ B0 . b z ⪯ y′ ∃(o′ , y ′ ) ∈ B. (8)

bi+1 = Φ( b B bi ). Since B b1 ⊆ B b0 , repeated application Set B removes executions until the finite set stops changing: b † = ν B. b Φ( b B) b = B H,u

\

b ⊆ Φ( b B) b B ⇐⇒ ∀o ∈ OH,u . TBb is (possibleo , doneo )-nonblocking.

bi , B

i≥0 † b† , BH,u = π2 B H,u

o ∈ Compat(z), and mark state y by doneo exactly when b Then (o, y) ∈ B.

† † WH,u = ↓(BH,u ).

Definition 3 (Safe Fork, Restore, or Merge edit). ( b † ̸= ∅, Derive(Θ) is defined; B H,u SafeEdit(Θ) ⇐⇒ false, otherwise. (9) At z = ϵ, the fixed-point condition retains a completion for every target result, and the checked coverage maps cover every required source result. The existential quantifier chooses a call order, and the universal condition keeps every compatible result completable after every partial execution. Lemma 4 (Largest safe execution set). A safe execution set † b† ) exists iff SafeEdit(Θ). When the edit is safe, (WH,u ,B H,u b is a safe execution set, and every safe execution set (L, B) † † b⊆B b satisfies B H,u and L ⊆ WH,u . Proof. The workflow, result, and policy conditions place every b0 . The final safe execution set’s complete executions inside B condition makes this set post-fixed, so monotonicity and b † , and the projected finite Knaster–Tarski place it inside B † b † = Φ( b B b†) partial executions give L ⊆ W . Conversely, B keeps every compatible result completable. At z = ϵ, this condition and the checked coverage witnesses from lemma 2 b† ⊆ B b0 ensures establish PreservesRequired. The inclusion B that complete executions follow the edited workflow and policy, while closure of Au under truncation makes every b † ) gives allowed partial execution safe. Finally, W † = ↓(π2 B a completion after every allowed partial execution. Hence the fixed point is a safe execution set exactly when nonempty. b means that (L, B) b is safe and contains MaxSafe(Θ; L, B) every other safe execution set. When such a pair exists, write its unique value as SafeBehavior(Θ). Lemma 4 proves that b † ̸= ∅ and then equals this witness exists exactly when B H,u † b † ). (WH,u ,B H,u 2) Why Result-by-Result Checking Fails: Section III introduced the contract X ⊗ (Y ⊕ Z) under policy {ϵ, x, y, xz, yx}. For its annotated calls, write x̄ = new(xo , dx ), ȳ = new(yo , dy ), and z̄ = new(zo , dz ). The candidate family initially contains ȳ x̄ and x̄z̄. The first fixed-point iteration removes x̄z̄. The second iteration removes ȳ x̄, because after the first removal z = ϵ no longer has a completion for the X ⊗ Z result. The empty fixed point is the formal reason the exact checker rejects. Proposition 1 (Exact correspondence with generalized nonb ⊆ B b0 , let T b be the trie for blocking). For nonempty B B b LBb = ↓(π2 B). Mark state z by possibleo exactly when

b † is nonempty, it is the largest nonempty Consequently, if B b0 satisfying the nonblocking concompletion subfamily of B dition for every result. If it is empty, no nonempty subfamily satisfies the conditions. Ordinary marker nonblocking of the unaugmented projected language is strictly weaker. Proof. From reachable partial execution z, a doneo -marked b extends state is reachable exactly when some (o, y) ∈ B z. Quantifying over exactly the states marked possibleo is therefore the post-fixed-point condition. Greatestness follows from the greatest-fixed-point construction. For strictness, the preceding instance has the marker-nonblocking projected pair (↓{ȳx̄, x̄z̄}, {ȳ x̄, x̄z̄}), but its indexed fixed point is empty. Proposition 1 relates the fixed point to generalized nonblocking after the trusted runtime has derived the completion condition for each result [16], [17]. The trusted runtime derives those conditions from the requested edit, authorized removals, actions, authorization records, and the execution record. It also decides whether each tool call creates or reuses an authorization, computes the largest safe execution set or a rejection proof, and puts an accepted edit into effect atomically. 3) Rejection Proofs: Each removed (orem , y) records its rank i, a partial execution z ⪯ y, and uncovered omiss ∈ Compat(z). Induction shows that every post-fixed P is contained in bi . An empty final family therefore proves that no every B safe execution set exists. Before the rule update, the trusted runtime recomputes both the removal order and the remaining completions. 4) Checking Again After a Permitted Partial Execution: To show that the checker can be applied again after each permitted partial execution, fix H, u, Au after deriving C, and write b † (C, ∆) with those parameters suppressed. W † (C, ∆) and B Lemma 5 (Rechecking after a partial execution). If z ∈ ′ W † (C, ∆), then Resolveρ∆ (raw(z)) = z, lab(∆z ) = lab(∆)auth(z), and W † (C, ∆)/z = W † (C/raw(z), ∆z ), b † (C, ∆)/z = B b † (C/raw(z), ∆z ), B b = {(o, v) | (o, zv) ∈ B}. b where B/z Proof sketch. Applying Resolve incrementally recovers the original calls, gives the authorization-log equality, and makes the candidate executions after z identical on both sides. b † gives a post-fixed Removing the executed sequence z from B family for the next check, while adding z to any such family gives one for the original check. Greatestness yields the fixedpoint equality, and ↓(B)/z = ↓(B/z) yields the generatedlanguage equality. The full proof is in section A-D3.

† † Thus every accepted partial execution retains a safe com- (WH,u , BH,u ). The automaton is the smallest deterministic pletion for every result that remains compatible with that marked partial automaton for this pair up to state renaming. execution. Proof. Induction on z shows that the automaton reaches 5) Checker Outputs: The checker returns Invalid when (W † /z, B † /z), enables a iff za ∈ W † , and marks the reached derivation fails, Reject with the ordered reasons for removing state iff z ∈ B † . Distinct states differ on a remaining generated every execution when the fixed point is empty, and Accepted or marked sequence and must remain distinct. The automaton with the largest safe execution set otherwise. Write Check(Θ) is the paired-language derivative construction [20]. for this deterministic output. Each answer includes a digest of the execution record that was checked. Section A-C gives the B. Atomic Rule Update exact returned data and verification rules. Proposition 2 proves Before the rules change, the trusted runtime re-derives an output-sensitive O(D + nΛ + |Gcov | + VB log(2 + VB ))-time, the edit and recomputes the fixed point from the execution O(D + Λ + |Gcov |)-space bound. Exponential growth occurs record. If any tool call has committed since the candidate only in explicitly emitted linearizations and pairs linking partial was computed, the candidate is stale and changes nothing. executions to required results. Otherwise, one policy-domain transaction closes the old rule version, activates the new automaton, replaces the rule entry VI. RUNTIME E NFORCEMENT and authorization token for every current workflow call, and The checker produces either a rejection proof or the largest only then returns success to the Agent. For each tool call, safe execution set. The trusted runtime turns a nonempty a transaction verifies its workflow-call ID, action, canonical safe execution set into rules checked before each tool call. request, authorization token, and enabled automaton transition It builds a finite automaton for the allowed partial executions, before recording progress. A new call creates one authorization records which version of the execution record was checked, and record and queues the canonical request. An reuse call advances atomically puts the new rules into effect. The protocol orders the workflow by linking to the existing record without extending every overlapping tool call either before or after the atomic the authorization sequence. rule update. The proof compares this runtime protocol with a) Invariant after the rule update: We write an ideal machine that puts an accepted edit into effect in one AgentSec(S; c, r) when five conditions hold: (1) the workflow atomic step and allows exactly its safe partial executions. The now in force and its required results come from the checked ideal transition system and the detailed runtime rules appear edit; (2) the stored nonempty execution set is the checker’s in section A-H and table III. This section gives the automaton largest safe execution set; (3) the workflow, authorization log, construction, the invariant after the rules change, and the atomic queue, and checkpoints match the processed-call sequence r; update used by the formal guarantees in the next section. (4) the automaton is in exactly the state reached after r; and (5) exactly one rule version is active, with one rule entry and A. Turning Safe Executions into Runtime Rules authorization token for every remaining workflow call. For a The runtime enforces an accepted safe execution set by track- submitted tool request, one transaction verifies the workflow ing exactly which safe partial executions remain possible after call, action, canonical request, authorization token, active rule each processed call. Removing result labels from the largest safe version, and enabled automaton transition before recording any † † execution set gives the finite pair (W, B) = (WH,u , BH,u ). For progress. The same transaction either creates the authorization L/z = {v | zv ∈ L}, let qz = (W/z, B/z) be the automaton record and queues the request, or records reuse of an existing authorization record and its return value. state after executing z. b) Final check: For current state S, write ΘS (u) = QW,B = {qz | z ∈ W }, (κ, H, ∆, out, A, u) for the safety-check instance obtained q 0 = qϵ = (W, B), (10) from its current components. Write Ready(S, u, Y ) when the a trusted runtime re-derives u from the current execution record, qz − → qza ⇐⇒ za ∈ W. recomputes the same nonempty fixed point and automaton Call this deterministic automaton Can(W, B). For the laptop carried by Y , confirms that the record has not changed since example, its initial state enables either supplier’s payment; after Y was computed, confirms that the old rule version is current, the L-payment transition, it enables the L-shipment transition and confirms that the new version is unallocated or inactive. but not the R-payment transition. Every state is reachable If these checks pass, one transaction closes the old version, and is marked exactly when ϵ ∈ B † /z. Thus a marked state activates the new automaton, replaces every current rule entry represents a completed execution, while an unmarked state and authorization token, and then returns success to the Agent. records safe work that may still continue. A changed state makes the candidate stale and forces a new Each transition symbol a contains workflow call x, action d, check. The complete state updates, retries, request sending, and its new or reuse mode, so one workflow call cannot use completion updates, and restart rules appear in section A-I another call’s rule entry. and table III.

Lemma 6 (Exact finite enforcement). The generated and marked languages of the automaton in equation (10) are exactly

Lemma 7 (Edit–call serialization). In every reachable wellformed runtime state, a visible edit answer and a tool call in

the same policy domain have a unique order at the atomic rule update. If the call commits first, it changes the execution record, so the earlier answer becomes stale and the edit cannot take effect. If the rule update commits first, the old call cannot resolve new or reuse. Steps in independent domains commute by product semantics.

c) Visible runtime behavior: Oapi includes Checkpoint decisions, edit answers tied to the checked record, edits put into effect, tool-call answers, sent requests, completion updates, and returned values. It hides internal computation, stale candidates, and restart bookkeeping. ( ℓ, ℓ ∈ Oapi ; obsapi (ℓ) = τ, otherwise.

Proof. If the call commits first, its recorded progress changes the execution record. If the rule update commits first, it closes the old rule version, so the old authorization token fails. Write S ≈di Oapi I when S and I are related by a divergenceAtomicity excludes a partially applied third case. Independent insensitive weak bisimulation under obsapi . B matches ideal and domains commute. runtime states on AgentSec and these visible fields. Section A-L gives the full relation. C. Trust Boundary The TCB is the trusted boundary defined in section IV. Theorem 1 (Faithful Registration). For finite-state W and finite Search, minimization, and candidate preparation remain un- R, CheckReg(W, R) accepts iff the stored λ witnesses W ⊑λ R. On acceptance, the source workflow’s tool-call traces and trusted because the final check recomputes them. BRuns(R) are order-isomorphic and preserve results, actions, VII. F ORMAL G UARANTEES new/reuse, the safety answer, and the largest safe execution The formal results connect derivation from the execution set. Malformed registrations fail before startup. record, exact checking, finite enforcement, the atomic rule For the remaining results, assume accepted registration, update, and every later runtime step. Their central exactness trusted checking of every tool call, and linearizable transactions result says that the checker accepts if and only if a safe runtime that remain atomic after a restart within each policy domain. implementation exists. The remaining results establish faithful registration, the information required for an exact answer, Theorem 2 (Exact Checkpoint). The ideal and runtime repeated use, and runtime correctness. machines make the same decision for Checkpoint(k, b). They When defined, write δ = Derive(Θ) = accept exactly when k is fresh, b is current, and the stored (κu , Hu , Au , Cu , η − , η + ). A safe runtime implementation is work matches the branch’s remaining registered work: Cb = bM Γ /raw(χ ). Acceptance preserves AgentSec without changing an automaton M together with complete executions B b b labeled by result. The partial and complete executions of M the current workflow or any earlier authorization. must form a safe execution set as defined in definition 2. The Let Ext = {Extend(ξ) | ξ is verified}. The theorems below atomic rule update activates this automaton at η + , closes η − , hold for every u ∈ Edit6 ⊎ Ext at every finite reachable and replaces the rule entries and authorization tokens for all AgentSec state. target calls. a) What the checker must know: Write V = Theorem 3 (Exact Safety Checking). The ideal and runtime Sec(S; c, r) = (P, I, E, C) for four parts of the checked record: machines return the same mutually exclusive and exhaustive (1) the workflow and its required results, (2) which calls refer answer for Θ = ΘS (u). Undefined derivation gives stateto the same action, (3) earlier authorizations and call progress, preserving Invalid. For defined δ = Derive(Θ), B b† = ∅ H,u and (4) which rules govern a call that overlaps the atomic rule gives state-preserving Reject with no safe runtime impleupdate. Suppose a checker receives only some function f (V ) mentation. Otherwise, for Y = Check(Θ), nonempty B b† , H,u of this record. The function is exact if any two records that it existence of a safe runtime implementation, Ready(S, u, Y ), makes indistinguishable always give the same answer to every and a successor that puts the edit into effect while preserving common decision or rule-update request. Write Exact(f ) for AgentSec are equivalent. The complete-execution component this property. For example, a view that erases the active rule of the largest safe execution set satisfies PreservesRequired, version can conflate a prepared update that may commit with and the derived record identifies every already-satisfied source the same update in a state where it must return NoCommit. result and every authorized removal. Internal identifiers may be renamed consistently because their spelling cannot affect the answer. For J ⊆ {P, I, E, C}, KeepJ Theorem 4 (Necessary Record Information). The full record is gives the checker exactly the parts named by J. Section A-F sufficient. If any one of the four parts is omitted wholesale while gives one record pair for each part and a fifth pair for the the others are retained, two records become indistinguishable even though the correct answer differs. correspondence between earlier authorizations and actions. b) Preserving required results: Exact(KeepJ ) ⇐⇒ J = {P, I, E, C}. b ⇐⇒ ∀a ∈ StillRequiredu . PreservesRequired(H, u, B) The four component-labeled rows in table II witness omission of b Coversu (t, a). ∃(t, y) ∈ B. P, I, E, C. The Drop row shows that retaining authorization ra

Thus every required source result appears in an accepted target result.

records and actions without recording which ones correspond is also insufficient. In particular, a checker is not exact if it

forgets which calls or authorization records refer to the same action, or if it sees only the caller’s description of what should happen next. Generalized nonblocking can serve as an exact solver only after the trusted runtime derives the workflow and the completion condition for each result. Theorem 5 (Repeated-Use Safety). Every enabled event preserves AgentSec. Therefore, the guarantees hold after every finite reachable sequence of edits, registered extensions, tool calls, authorization updates, rule updates, stops, and restarts. Theorem 6 (Runtime Correctness). B is a divergenceinsensitive weak bisimulation under obsapi , so every pair related by B satisfies S0 ≈di Oapi I0 . The observation records Checkpoint decisions, edit answers tied to the checked record, new authorization data, and returned values. d) Proof roadmap: Registration reflection follows by enumerating the finite tool-call traces and checking their order- and identity-preserving correspondence. The matching Checkpoint transitions prove exact Checkpoint. The editrule checks and greatest-fixed-point argument prove exact checking. Every safe execution set is contained in the computed family, and a nonempty computed family yields a safe runtime implementation. Five explicit pairs of execution records prove the information result. Induction over the runtime rules proves repeated use. A case analysis over edits, tool calls, races with the rule update, returns, and restarts establishes the weak bisimulation. The appendix gives the complete case proofs. VIII. M ECHANIZATION AND E XECUTABLE VALIDATION Six Lean modules pass --trust=0 and mechanize the finite linear-contract core used by the paper. The mechanization proves that the executable checker accepts exactly when a valid safe execution set exists. It proves that registration checks every tool call and preserves the exact answer for the current execution record. It also proves that executable workflow editing is sound and complete for all six edit forms. An accepted edit produces an atomic rule update, and every finite sequence of later calls preserves Lean’s AgentSec. Separate proofs cover both orders between a tool call and that update, as well as preparation before it takes effect. The appendix proves the general pomset lift, the maps that preserve source results, the information lower bound, and ideal–runtime weak bisimulation in sections A-A, A-D1, A-F and A-L. All 19 paper-specific tests pass, together with 62 authorization and checker regression tests for supporting components. Across accepted instances with 2–128 results, the checker takes 0.11–53.47 ms. Rejected instances take 0.11–5.51 ms, while enumerating 6–720 unordered completions takes 0.33–50.35 ms. Section A-M reports the complete measurement protocol and executable coverage. IX. R ELATED W ORK a) Recovery, workflow update, and synthesis: Outputcommit recovery reconstructs a fixed computation. Generalized nonblocking and Live Synthesis solve supplied transition systems and completion conditions, while workflow inheritance

and dynamic controller update connect supplied old and new specifications [21], [22], [16], [17], [18], [23], [24], [25]. Our runtime derives the edited workflow, action reuse, stillrequired results, completion conditions, and new runtime rules directly from the execution record. It computes the largest safe execution set and atomically makes rules take effect for new authorizations and reuse of existing ones. b) Agent recovery mechanisms: ACRFence blocks replay after Restore, DART selects checkpoints, Atomix delays external actions until commit, and Rebound provides atomic, auditable rollback [7], [15], [13], [26]. Our formal results give exact criteria for Checkpoint and all six forms of Fork, Restore, and Merge, together with a rejection proof and an information lower bound showing that omitting any record part wholesale can change the correct answer. These guarantees continue through the atomic rule update and arbitrary finite execution. X. C ONCLUSION Safe execution editing requires the runtime to derive from the execution record what each edit must preserve. Earlier authorizations remain fixed, and every still-required result retains a policy-safe completion. For Checkpoint, the six forms of Fork, Restore, and Merge, and registered extensions, our checker either applies the direct Checkpoint check, computes the largest safe execution set, or returns a finite proof that no runtime rule set can enforce the edit safely. The formal results connect this exact decision to decision-relevant distinctions from all four parts of the execution record, the atomic rule update, repeated execution edits, and equivalence with an ideal atomic machine.

A PPENDIX A S UPPLEMENTARY P ROOF A PPENDIX This appendix gives the proof details for theorem 3 over finite registered call models and atomic policy-domain rule versions. Independent domains retain the product interpretation stated in the paper. A. The Declarative Definition and the Computed Answer Fix a well-formed safety-check instance Θ = (κ, H, ∆, out, A, u) for which the edit derivation yields δ = (κu , Hu , Au , Cu , η − , η + ). All sets in this subsection retain result labels, so two equal resolved words belonging to different results remain different elements. Definition 4 (Required source results). Write kind(u) for the constructor of u. Call either Fork constructor a Fork and either Restore constructor a Restore. For the matching source row in table I, define u Fork Restore MergeSelect(g, w, σ) MergeJoin(g, σ)

SrcReg(H, u) {(L, C), (R, C)} {(cur, C), (k, Ck )} {(w, [[Tw ]]), (w̄, [[Tw̄ ]])} {(L, [[TL ]]), (R, [[TR ]])}

The full set of source results is RequiredBefore(H, u) = ({ctx} × Ounchanged ) ] ⊎ ({r} × OD ). (r,D) ∈SrcReg(H,u)

Write DoneH (r, o) when the recorded progress for region r shows that every event in result o’s pomset has completed. Only RestoreReplace treats completed current results as finished: DoneCurH = {(cur, o) | o ∈ OC ∧ DoneH (cur, o)}, u RestoreReplace(b, k, σ) otherwise

SatisfiedH,u DoneCurH ∅

For every a ∈ CanRemove(H, u), the removal request must contain a signature by reqauthH (a) over rmmsg(H, u) = (ω, κ, ζ, σ, H, CanRemove(H, u), origin(CanRemove(H, u))). Without all required signatures, the edit has no derivation. With them, AuthorizedRemovalH,u = CanRemove(H, u). Write Satu = SatisfiedH,u and Rmu = AuthorizedRemovalH,u . The checker requires StillRequiredu = RequiredBefore(H, u) \ (Satu ⊎ Rmu ), RequiredBefore(H, u) = StillRequiredu ⊎ Satu ⊎ Rmu .

Definition 5 (Preserving required results). b ⇐⇒ ∀a ∈ StillRequiredu . PreservesRequired(H, u, B) b Coversu (t, a). ∃(t, y) ∈ B. Here AuthorizedRemovalH,u contains the typed results of the unselected branch in MergeSelect or the current-branch results of an authorized RestoreReplace. SatisfiedH,u contains the completed current-branch results of RestoreReplace. Both sets are empty for every other row and for a registered extension. Thus StillRequiredu = RequiredBefore(H, u) \ (SatisfiedH,u ⊎ AuthorizedRemovalH,u ), so PreservesRequired covers exactly the source results that are neither completed nor authorized for removal. Let RΘ be the finite set of safe execution sets from definition 2, ordered componentwise by b1 ) ⊑ (L2 , B b2 ) (L1 , B

⇐⇒

b1 ⊆ B b2 . L1 ⊆ L2 ∧ B

Lemma 8 (The computed answer is exact). The declarative b holds for some pair if and only predicate MaxSafe(Θ; L, B) b † ̸= ∅. When such a pair exists, it is unique and equals if B H,u † b † ). The declarative object and the computed fixed (WH,u ,B H,u point are defined independently, and the lemma proves their equality.

b ∈ RΘ . The workflow, result, and policy Proof. Let (L, B) b⊆B b0 . For every (o, y) ∈ B, b every partial requirements give B Completion observability makes this set either all of {cur}×OC b execution z ⪯ y belongs to L = ↓(π B). Persistent result 2 or empty. The only sets eligible for signed removal are coverage therefore supplies, for every o′ ∈ Compat(z), a pair b extending z. Thus B b ⊆ Φ( b B). b By monotonicity CurOut = {cur} × OC , Otherw = {w̄} × O[[Tw̄ ]] , (o′ , y ′ ) ∈ B b0 B on the finite lattice 2 , every post-fixed set is contained in the u CanRemove(H, u) b⊆B b † . Taking the projected partial greatest fixed point, so B RestoreReplace(b, k, σ) CurOut \ SatisfiedH,u † executions yields L ⊆ W . MergeSelect(g, w, σ) Otherw b † ̸= ∅. The fixed-point equality keeps Conversely, suppose B otherwise ∅ every compatible result completable and, at ϵ, combines with reqauthH (a) is the authority identity named by the unique the checked preservation maps to establish PreservesRequired. b0 ensures that complete executions follow the signed authority record found through a’s source region in G. Inclusion in B When a comes from a checkpoint, the identity is taken from the target workflow and policy. Closure of Au under truncation stored copy in K. Context identity, carry, and clone preserve makes every generated partial execution safe, and W † = b † ) gives a completion after every partial execution. that authority identity, while every source region introduced by ↓(π2 B b † ) ∈ RΘ , and the preceding containment makes an edit rule receives the identity of the authority that signed the Hence (W † , B rule and policy version. Thus reqauthH is total and immutable it greatest. If two greatest elements existed, each would contain b † = ∅, on RequiredBefore(H, u), including Fork-created L/R copies. the other componentwise, so they would be equal. If B

the first half places every hypothetical safe execution set inside the empty set, contradicting its required nonemptiness.

All sets, partial executions, and compatibility checks are finite and use the canonical order fixed by the checker.

Corollary 1 (Exact checking). The ideal edit transition is enabled by the declarative SafeBehavior(Θ) exactly when the checker returns a nonempty fixed point. On that edge, the ideal language L∗ equals the generated language of Can(W † , B † ).

Lemma 9 (The rejection proof is sound and complete). The verifier accepts Cfp iff the descending fixed-point computation b † = ∅. In that case no safe execution set exists. reaches B

Proof. The first statement is lemma 8. The second combines that lemma with lemma 6. Proposition 2 (Output-sensitive checking). Fix a unit-cost model for the checker with constant-time finite-map lookup and policy-automaton transitions. Let D = |Θ|chk , X X Λ=

n = max|Xpo |, o

(|w| + 1),

b0 |, NB = |B

o w∈Lin(po )

X

VB =

(|y| + 1).

Gcov =

((o, y), z, o′ )

C. Exact Returned Proof Data Let enc be canonical and length-delimited, with κ authenticating A. The formal transition system treats the domainseparated authenticated digests Digestrules and Digestrecord as injective, so equal digests have equal encoded inputs. For Θ = (κ, H, ∆, out, A, u), define γ(Θ) = Digestrecord (enc(request, ω, ζ, κ, H, ∆, out, A, u)).

b0 (o,y)∈B



Proof. The initial equality check ties the proof to Θ, and every bi+1 = Φ( b B bi ), so canonical iteration verified round is exactly B supplies completeness. For soundness, induction places every bi , so an empty final family post-fixed family inside every B excludes every nonempty safe execution set.

 b0 , z ⪯ y, (o, y) ∈ B . o′ ∈ Compat(z)

b † ̸= ∅, also define When Derive(Θ) is defined and B H,u

† † autZ = Can(WH,u , BH,u ), Here D is the checked input size, Λ is the total size of b † )). Haut = Digestrules (enc(autZ , B H,u the emitted linearizations, and Gcov contains the triples of candidate execution, partial execution, and required result The digest checked before the rules change is examined by the checker. The checker runs in O(D + nΛ + cutZ = Digestrecord (enc(ω, ζ, κ, H, ∆, out, u, CH,u , |Gcov | + VB log(2 + VB )) time and O(D + Λ + |G (11) Pcov |) space, Haut , η − , η + )). including the data it returns. Moreover, NB ≤ o |Lin(po )|, |Gcov | ≤ NB (n + 1)|OCu |, and the number of nonempty strict- Because H contains χ, ver, ρ, β, the digest covers workflow removal ranks is at most NB . progress, record version, registry contents, active rule entries Proof. A backtracking topological-order enumerator emits and versions, the authorization log, and the request queue. The all indexed linearizations in O(nΛ) time, while resolution, verifier re-derives the edit-rule judgment†and† complete fixed policy simulation, and construction of raw and resolved tries point labeled by result, reconstructs (W , B ), verifies both are linear in emitted volume. For every support key (z, o′ ), digests, and checks the full automaton isomorphism

maintain the number of remaining pairs (o′ , y ′ ) extending autZ ∼ = Can(W † , B † ), z, initially enqueue candidates having a required result with zero support, and remove candidates in synchronous batches. including its initial state, marking, and every labeled transition. When removal makes a support count zero, enqueue exactly Canonical encoding order makes Invalid, Reject, and Accepted the candidates that depend on that requirement for the next unique and unchanged by consistent renaming of internal batch. Each candidate and each triple in Gcov is processed at identifiers. A concrete implementation may authenticate enc bi \ B bi+1 . Store one with signatures or collision-resistant digests. The corresponding most once, and the batches are exactly B rank and cause per removed candidate rather than copied sets, guarantee relies on signature unforgeability and digest collision and construct Can(W, B) by bottom-up sorting of finite-trie resistance, which the formal model represents with unforgeable identifiers. derivative signatures in O(VB log(2 + VB )) time. D. Proofs for Edit Rules and Rechecking

B. Ordered Rejection Proofs For an empty fixed point, the returned proof is

1) Edit-rule correctness:

Full proof of lemma 2. Unique object and edit-rule identifiers select one row and record, while context identity preserves b0 (Θ) and re- everything outside the edited region. The Fork rows check The verifier first recomputes the canonical B quires equality with the serialized first component. An entry both copies. RestoreReplace checks the checkpoint copy and ((o, y), z, o′ ) ∈ Ei verifies exactly when z ⪯ y, o′ ∈ the exact treatment of the current branch, while RestoreLive bi extends z. The verifier checks both the retained current branch and the checkpoint Compat(z), and no (o′ , y ′ ) ∈ B bi \ Φ( b B bi ), copy. MergeSelect checks the selected and unselected regions, requires the set of first components in Ei to equal B b b b sets Bi+1 = Bi \ π1 (Ei ), and accepts only when Bk+1 = ∅. while MergeJoin checks both retained regions before its barrier. b0 , E0 , . . . , Ek ), Cfp = (B

bi × ↓(π2 B bi ) × OH,u . Ei ⊆ B

Clone and carry supply the global bijections and preserve which workflow calls belong to each result and which authority controls each source region. Constructor induction defines prur , proves the cover, and supplies every Coversu witness. The common derived record fixes all remaining fields, preserves or initializes branch progress, and assigns each source region introduced by an edit rule its signed authority record. Fresh identifiers, partial-constructor checks, and lemma 1 preserve uniqueness, acyclicity, and contract well-formedness. Finally, + β ′ (x) = (jx+ , η + ) and (x, jx+ , h+ x ) ∈ Hu for every current target workflow call x.

3) Rechecking after a partial execution: Full proof of lemma 5. Because some projected member of b † has the form zv, the recoverability and composition B properties in lemma 3 give the recoverability and authorizationlog equalities. Removing the executed sequence from the executions labeled by result retains every compatible result and gives CompatC/raw(z) (s) = CompatC (zs). Together with authorization-sequence concatenation, applying Resolve incrementally yields

2) Registered extension: The Agent may name only an immutable record ξ that specifies the exact prior edit rules, b0 (C, ∆)/z = B b0 (C/raw(z), ∆z ), B registry, execution record, and policy, together with finite disjoint additions DΣ , Dρ , Dα and a successor policy A+ . The with the same retained result identities, policy, and target regb † /z is post-fixed for the next-check operator and set Dα contains the signed authority record for every newly istry. Thus B introduced result and its source region. The policy authority and lies within its greatest fixed point Y . Conversely, incremental trusted runtime verify ξ. Existing meanings remain unchanged, resolution and policy safety after z put zY = {(o, zy) | (o, y) ∈ b0 . The union B b † ∪ zY is post-fixed new identifiers are fresh and domain-scoped, and A ⊆ A+ . Y } inside the original B Let ζ + , κ+ , and A+ be the verified successor versions and because partial executions t ⪯ z use existing witnesses, while policy named by ξ. For every x ∈ X[[T ]] , the trusted runtime those of the form t = zs use witnesses in Y . Greatestness + b † , hence Y = B b † /z. Finally, ↓(B)/z = ↓(B/z) deterministically creates jx+ and h+ gives zY ⊆ B x . For fresh η , define yields the generated-language equality. G+ = G ⊎ Dα , Σζ + = Σζ ⊎ DΣ ,

Hξ+ = (ω, G+ , T, K, Σζ + , ρ+ , β + , χ, ver + 1, η + ),

Proof of lemma 10. The verified extension preserves the current workflow, which calls refer to the same action, every result label, and A ⊆ A+ . Every earlier safe completion and coverage witness therefore remains valid for the next fixedpoint computation. The current remaining family is therefore post-fixed, and greatestness gives its inclusion in a nonempty successor fixed point.

Cξ = [[T ]],

E. Lean Theorem Map

+

ρ = ρ ⊎ Dρ , Hξ+ = {(x, jx+ , h+ x ) | x ∈ X[[T ]] }, β + (x) = (jx+ , η + ),

RequiredBefore(H, Extend(ξ)) = StillRequiredExtend(ξ) , StillRequiredExtend(ξ) = {ctx} × O[[T ]] , SatisfiedH,Extend(ξ) = ∅, AuthorizedRemovalH,Extend(ξ) = ∅, CoversExtend(ξ) (t, (ctx, o)) ⇐⇒ t = o. The checked judgment is (κ, H, A) ⊢ Extend(ξ) ⇓ (κ+ , Hξ+ , A+ , Cξ , η, η + ). It preserves T, K, χ, ∆, out and every existing row of G, Σζ , ρ, appends Dα to the execution record, and authorizes no removal. Every current result, workflow call, action, source region, authority record, and causal edge therefore remains unchanged. It uses the same checker and atomic rule update as a Fork, Restore, or Merge edit. Lemma 10 (Registered extension preserves safety). For a verified Extend(ξ), the current safe executions after recorded progress form a post-fixed family for the extension instance and b† b† are therefore contained in B H,Extend(ξ) . Hence BH,Extend(ξ) ̸= ∅. Consequently, a valid registered extension cannot remove a currently required result or leave it without a safe completion.

Six Lean modules machine-check the claims used in the paper. FiniteCore proves the executable greatest-fixed-point checker equivalent to the declarative safe-execution-set predicate, including resolution over partial executions and greatestness. RegistrationRefinement proves that registration accepts the typed finite model, every registered call remains under trusted control, action identity is preserved, and the finite and semantic contracts agree. HistoryStructure proves deriveEdit_iff, well-formedness preservation, and executable fixtures for Choice/Parallel Fork, Replace/Live Restore, Select/Join Merge. OperationalSemantics proves invariant preservation across every runtime trace, closure of all six edit forms, registered extension safety, and both orders between a tool call and an atomic rule update. CompilationBridge constructs a secure atomic rule update from an accepted checker answer and reflects every successful update back to that answer. PaperTheorems combines these results into exact registered checking, six-edit derivation, preservation before rules take effect, trace safety, and serialization between calls and rule updates. The remaining appendix sections prove the general pomset lift, information lower bounds, and ideal–runtime weak bisimulation.

F. Why No Record Part Can Be Omitted Wholesale We prove that each of the four record parts contains an answer-relevant distinction and that no part can be omitted wholesale while retaining the other three. For each omitted part, we construct two valid records that become indistinguishable even though their correct answers are different. Let Qsec pair every valid checked record V = Sec(S; c, r) with a well-typed request q ::= Decide(u) | TryUpdate(u, Y ). For such a record, let ΘV (u) = ΘS (u) and ReadyV (u, Y ) = Ready(S, u, Y ). For Decide, Ans returns Check(ΘV (u)). For TryUpdate, it returns the updated runtime state exactly when ReadyV (u, Y ) holds, and returns NoCommit otherwise. Internal identifiers may be renamed consistently, while public identifiers remain fixed. We write (V, q) ∼ = (V ′ , q ′ ) when one type-preserving renaming maps the entire record and request to the other. We use the same symbol for checker answers and runtime states when the corresponding renaming maps every field of one to the other. An input function f is exact when indistinguishable reduced inputs always have the same correct answer up to such a renaming: Exact(f ) ⇐⇒ ∀(V0 , q0 ) ∈ Qsec . ∀(V1 , q1 ) ∈ Qsec . (f (V0 ), q0 ) ∼ = (f (V1 ), q1 ) =⇒ Ans(V0 , q0 ) ∼ = Ans(V1 , q1 ).

Omitted Record pair P

I

E

Correct answers

i qP = Decide(MergeSelect(gi , L, σ)); V 0 : safe; V 1 : Invalid because the mode is wrong. T 0 = bx :X ⊕open by :Y , g0 T 1 = bx :X ∥g1 by :Y . qI = Decide(RestoreLive(bL , k, σI )) (X ⊗ Yk ) ⊕ Y : one new, after safe accept; two new reject aa. empty-root/ForkChoice/Checkpoint; ∆ = ϵ, A = ↓{a}; 0 0 qact (x) = qact (y) = d0 ; 1 1 qact (x) = d0 ̸= d1 = qact (y); ℓ(d0 ) = ℓ(d1 ) = a. uE = RestoreReplace(bL , k, σE ), V 0 : rules take effect; V 1 : qE = TryUpdate(uE , Y0 ); Y0 is NoCommit because the checked at V 0 after safe checked record changed. empty-root/ForkChoice/Checkpoint/new; Dispatch(d)

V 0 −−−−−−→ V 1 , changing only whether a queued request was sent. reuse(xk , d): accept; Dropra q¬ar = Decide(RestoreReplace(bL , k, σ¬ar )) new(xk , d): reject aa. after safe empty-root/ForkChoice/Checkpoint/new; qact (x) = d, A = ↓{a}; same calls {c, x}, records {p}, and actions {d, e}; (qact (c), p) = (d, d) in V 0 , (e, e) in V 1. C qC = TryUpdate(u0 , Y0 ), with Y0 V 0 : rules take effect; V 1 : computed at V 0 , is identical in both; the NoCommit. current rule versions and dependent digests differ.

TABLE II R ECORD PAIRS THAT BECOME INDISTINGUISHABLE AFTER ONE FACT IS OMITTED BUT REQUIRE OPPOSITE ANSWERS .

The four parts of the record are as follows. P contains the corresponding step in the renamed record. Induction over the workflow, checkpoints, edit rules, required results, authorized finite acyclic dependency order proves the claim. removals, and the authority for each result. I records which Lemma 12 (Opposite answers require distinguishable records). workflow calls refer to the same tool action, together with If Ans(V0 , q0 ) ̸∼ = Ans(V1 , q1 ), then every exact f satisfies each action’s request, authorization label, scope, source region, (f (V0 ), q0 ) ∼ ̸ (f (V1 ), q1 ). = current rule entry, and authorization data. E records processed calls, current and saved progress, prior authorizations, retries, Proof. The claim is the contrapositive of the definition of returned values, queued requests, and the current policy state. C Exact(f ). records the policy version, edit-rule version, execution record version, and active rule version, together with the internal namespace and the digest checked before new rules take effect. G. A Common Initial State and Five Record Pairs Encodings, digests, authorization sequences, and returned proof Definition 6 (Checked registration). A typed Agent workflow data are computed from these four parts rather than treated as W is eligible for registration when it is a finite-state LTS whose additional facts. complete paths carry result labels, end at terminal states, and For J ⊆ {P, I, E, C}, KeepJ (V ) retains the facts in J. It yield finitely many tool-call traces after internal τ -steps are also removes every reference to an omitted fact and every erased. CheckReg rejects any reachable strongly connected computed value that depends on an omitted fact. This recursive component that can still reach a result and contains a tool-call deletion has a unique output because computed values depend edge within the component, permits erased τ -cycles, and then acyclically on the four recorded parts. Dropca (V ) removes only enumerates the resulting finite traces. R stores a candidate map the correspondence between workflow calls and tool actions, λ, and BRuns(R) is the finite language obtained by linearizing together with all data that could reconstruct it. Dropra (V ) its registered root pomsets, retaining each result label, and similarly removes only the correspondence between prior labeling every workflow call by its checked Use. W ⊑λ R authorization records and tool actions. means that λ gives a bijection from these traces to BRuns(R) that preserves results, call order, which calls refer to which Lemma 11 (Omitting information is well defined). Consistent tool actions, and the signed policy authority for each source renaming commutes with KeepJ , Dropca , and Dropra . Their region. For source executions e, e′ , write e ≡∂ e′ when erasing outputs therefore do not depend on the spelling of internal internal τ -steps yields the same tool-call trace with the same identifiers or the byte encoding of computed data. result label. The check requires every tool action to have one Proof. A type-preserving renaming preserves references and certified canonical request and requires every reuse of that dependencies. It therefore maps every deletion step to the action to retain the same request. It also requires λ to be total

and one-to-one, to contain no unregistered tool calls, and to preserve prior authorizations and every required result. Every pair below starts from a checked initial state and differs in one part of the execution record. After that part is omitted, the checker receives indistinguishable inputs even though the correct answers are opposite. We construct the finite pairs from one empty initial state S∅ . A registered call model R contains finite contracts, edit rules, policy, the checked registration map, and signed records for results, workflow calls, tool actions, canonical requests, source regions, scopes, and labels. Before the root rules take effect, it contains no prior authorization, execution progress, queued request, rule version, returned value, or automaton register(W,R,n) state. The registration relation has a step S∅ −−−−−−−−−−→ Reg(R, n) exactly when CheckReg(W, R) accepts and n is a fresh private namespace. A checked root update then initializes empty progress and request state, activates one rule version and the canonical automaton, and records signed data for every current rule entry and root result authority.

structure agree with the runtime state, and the recomputed nonempty fixed point establishes the condition on required results. Empty runtime progress matches the executed calls, the canonical automaton starts at qϵ , and the atomic assignments give every current call an entry in the active rule version. Only the initial rule update creates a root origin, and every successful later update stores the checked derivation that produced it. The following finite pairs use private names except for each displayed request and authorization label. Each state is reached from S∅ by the stated registration, initial rule update, Checkpoint, tool-call, and edit steps. a) P: workflow structure: Let X and Y be singleton contracts with distinct workflow calls x and y, a shared tool action, and a universal policy. From the same registered singleton root, a checked initial rule update followed by ForkChoice reaches VP0 with private group g0 , while the corresponding ForkParallel trace reaches VP1 with private group g1 . The two records differ only in VP0 .T = bL :X ⊕open g0 bR :Y,

VP1 .T = bL :X ∥g1 bR :Y.

Lemma 13 (Registration reflection). For finite-state W and Use the same registered MergeSelect schema with q i = P finite R, CheckReg(W, R) accepts iff the registered λ wit- Decide(MergeSelect(g , L, σ)). The choice record has a unique i nesses W ⊑λ R in definition 6. On acceptance, applying λ to edit derivation and a nonempty one-step safe execution set. source executions modulo ≡∂ gives a bijection with BRuns(R). The parallel record has no MergeSelect derivation because its The correspondence preserves result identity, causal order, group mode is wrong. Omitting P removes the constructor tag canonical requests, prior authorizations, and the safety-check and all computed signed data that depends on it. The private answer. renaming g0 7→ g1 then makes the remaining record-request Proof. The SCC check terminates because the state graph pairs indistinguishable. b) Common start for the correspondence pairs: Let 1 be is finite. A reachable SCC that can still reach a result and contains a tool-call edge can be repeated before that result, the singleton-result contract whose unique pomset is empty. producing projected words of unbounded length. Conversely, if Its completion ϵ gives a nonempty greatest safe execution set no such SCC contains a tool-call edge, contracting the SCCs under A = ↓{a}. Both pairs below put these safe root rules yields a DAG with a finite, enumerable projected language. into effect and then apply a checked ForkChoice. Any inactive The checker compares that language with BRuns(R). It checks edit-rule entry needed to equalize the individual tool actions results, call order, which calls refer to which actions, signatures is identical in both records and never becomes active. c) I: which calls refer to the same action: Let X, Y be on those actions, that registration is total and one-to-one, that no unregistered calls appear, and prior authorizations after singleton contracts with workflow calls x, y, and let d0 , d1 be every partial execution. It therefore accepts exactly when tool actions without authorization records, both labeled a. Two W ⊑λ R holds. Erasing internal steps gives a bijection checked call models contain the same workflow and the same between matching tool-call traces. Canonical-request equality individual calls and actions, but the calls refer to the actions and deterministic Resolve preserve prior authorizations after differently: qact (x) qact (y) every partial execution. The safe execution sets are therefore 0 V d0 d0 I order-isomorphic, so the fixed-point operator preserves the 1 V d d 0 1. I safety decision, greatestness, and corresponding automaton. From the 1 root now in force, the common Fork rule Lemma 14 (Checked initial state). If CheckReg(W, R) accepts derives bL :X ⊕open bR :Y . Each result uses one tool action, g and the registered root contract and policy have a nonempty so both Fork updates are safe under ↓{a}. Create a checkgreatest safe execution set, the checked root update reaches a point for bR before progress and issue the common query finite state SR with AgentSec(SR ; cR , ϵ). The execution record qI = Decide(RestoreLive(bL , k, σI )). Up to clone renaming, stores the checked root derivation, and every later rule update the target is (X ⊗ Yk ) ⊕ Y . In VI0 , the left result uses one stores the checked Fork, Restore, or Merge edit or registered new and one reuse on d0 , while the bypass result uses one extension that produced it. new, so every result has authorization sequence a. In VI1 , every Proof. Registration contributes only the checked R and n, and left-result linearization uses new on both d0 , d1 , so its word deterministic allocation constructs every runtime identifier from is aa ∈ / A. The left result is compatible with ϵ, so the first b round also removes the otherwise safe bypass completion them. The root judgment and checked maps make the registered Φ

and leaves the greatest fixed point empty. Applying Dropca Proof. Lemma 14 gives the common initial state, and makes the remaining records indistinguishable because their the traces above use only modeled Checkpoint, tool-call, individual calls and actions were already identical. Fork/Restore/Merge, and rule-update steps. For the two corred) E: authorization and execution progress: Let C, X be spondence pairs, the empty root completes with ϵ, and each singleton contracts with workflow calls c, x, let qact (c) = Fork arm has a one-new completion labeled a. Hence every qact (x) = d, and label d by a. From the safe 1 root, a displayed state before its request is reachable under ↓{a}. checked Fork update puts bL :C ⊕open bR :X into effect. Create Open choice enables the Checkpoint steps, and the active g a checkpoint for bR , then use c to complete the left arm, automata enable each stated left-arm new before that arm create authorization record p, and queue its canonical request. becomes a completed, still-addressable branch. For the E pair, At the resulting VE0 , check uE = RestoreReplace(bL , k, σE ) Dispatch preserves P, I, C but changes the checked record, to obtain Y0 . Its clone of x reuses d, so the update is safe giving a successful update versus NoCommit. The displayed Dispatch(d) under A = ↓{a}. Let VE0 −−−−−−−→ VE1 , which changes only edit-rule and resolution calculations give the other opposite whether the queued request has been sent and leaves P, I, C answers. Lemma 11 and the stated private renamings make the unchanged. For the same request qE = TryUpdate(uE , Y0 ), the reduced inputs indistinguishable. Each omission collapses its rules take effect at VE0 , while VE1 returns NoCommit because corresponding pair, so lemma 12 proves inexactness. the digest of the checked record has changed. Giving the P pair the same caller description of what should e) Dropra : which action a prior authorization names: happen next and the same completion conditions leaves their For a separate pair, keep the common active row qact (x) = d, opposite answers unchanged. The target alone is therefore insufcreator c, authorization record p, and tool actions d, e la- ficient. A generalized nonblocking solver becomes applicable 0 beled a, but set qact (c) = d and p 7→ d in V¬ar , versus only after the trusted runtime has derived the edited workflow, 1 qact (c) = e and p 7→ e in V¬ar . Both states follow the preserved result identities, and the completion condition for same safe empty-root/ForkChoice/Checkpoint/new shape above, each result. have authorization sequence a, and use the common query q¬ar = Decide(RestoreReplace(bL , k, σ¬ar )). The cloned xk H. Ideal Atomic Execution Machine 0 is reuse(xk , d) in V¬ar , but new(xk , d) produces forbidden An ideal state I = (κ, H, ∆, out, A, c, r), with c = 1 word aa in V¬ar . The two records contain the same creator, b ∗ ), contains the execution record, current rule (Hc , u, L∗ , B authorization record, workflow call, and tool actions, and version and entries, checked safe execution set, and current both retain x 7→ d. Dropra removes the only differing partial execution. Write ΘI (u) = (κ, H, ∆, out, A, u). The correspondence and every value that could reconstruct it, so runtime state additionally represents the automaton, transaction the remaining records are indistinguishable. This pair proves phase, authorization data, and a prepared rule update. that an exact checker must know which tool action each prior a) Edit transition: For current ΘI (u), an undefined authorization names. derivation gives state-preserving Invalid, while a defined derivaf) C: the active rule version: Let an initial namespace tion with no MaxSafe witness gives state-preserving Reject. be a family n = (ns )s∈Sort of injective, per-sort fresh supplies. Otherwise Derive(ΘI (u)) supplies the target and rule version, From the same empty initial state, register the same public b∗) and independently defined SafeBehavior(ΘI (u)) = (L∗ , B 0 1 call model R with supplies n , n that agree on every type + ∼ enables one atomic Edge(u, [Hu ]= ) that makes them current except the rule-version type. The checked root updates create and resets r to ϵ. All three answers are computed from the 0 1 distinct active versions η0 ̸= η1 . The resulting VC , VC have same current execution record and are mutually exclusive and identical P, I, E, while their active rule versions and dependent exhaustive. 0 digests differ. Check the same registered edit u0 at VC to b) Tool call: For submitted tool request m, an enabled x b0 , Z0 ), then submit qC = obtain Y0 = Accepted(δ0 , W0 , B passes the ideal automaton exactly when its current rule entry 0 TryUpdate(u0 , Y0 ) to both records. At VC , the final check and authorization data identify tool action d, canonκ (m) = reproduces cutZ0 , so the rules take effect. At VC1 , the active invρ (d), and ra ∈ L∗ . Here a = new(x, d) if d has no version is η1 rather than the η0 recorded in Z0 , so the update authorization record, and a = reuse(x, d) otherwise. One returns NoCommit. Omitting C also removes dependent rule atomic transition applies HStep, appends a to χ, advances entries, authorization data, and digests, leaving the recordver, removes x’s current rule entry, and sets r := ra. new request pairs indistinguishable. also creates the labeled authorization record and queues the Proposition 3 (Four answer-relevant record parts). Every canonical request, while reuse links to the existing return record. pair above consists of finite runtime states reached from the Any failed premise returns deny(x) without changing state or common empty initial state and satisfying AgentSec. After inventing a return value. the corresponding information is omitted, each pair becomes c) Checkpoint, retry, sending, and restart: indistinguishable even though the correct answers are opposite. Checkpoint(k, b), verified retry, Dispatch, completion Therefore every KeepJ with J ⊊ {P, I, E, C}, as well as updates, and restart after a stop have the state changes in Dropca and Dropra , is inexact. Every exact checker input must table III. The ideal and runtime machines apply the same distinguish all five pairs. freshness, current-branch, and remaining-work checks, so they

make the same Checkpoint decision. This transition system represents external-network completion after Dispatch as environmental behavior. By lemma 4, every reachable partial execution of the ideal machine retains a policy-safe completion until the next edit transition changes the workflow contract. The runtime implements this machine without enumerating the full completion set at every call. I. Runtime State and Atomic Transitions For Θ = (κ, H, ∆, out, A, u), let Cder (Θ) be the canonical record of the failed derivation. Check(Θ) = Invalid([γ(Θ), Cder (Θ)]∼ = ), if Derive(Θ) is undefined; Check(Θ) = Reject([γ(Θ), Cfp ]∼ = ), b † = ∅. if Derive(Θ) is defined and B H,u b † ̸= ∅, When Derive(Θ) is defined and B H,u † b † , Z). Check(Θ) = Accepted(δ, WH,u ,B H,u

where Z = (ω, ζ, κZ , cutZ , u, Haut , η − , η + ). Invalid carries the failed derivation, Reject carries the complete ordered rejection proof, and Accepted carries the unique derivation, coverage proof, canonical automaton, and Z. Z binds the checked execution record, derived target, automaton, and both old and new rule versions. The runtime state for one policy domain is S = (κ, H, ∆, out, A, phase, entry, aut, q, checked), where phase records whether each rule version η is unallocated (⊥), inactive, active, or closed. The initial rule runs only after CheckReg(W, R) accepts, and its exact construction appears in section A-G. Each active version stores b Z), which contains the checked c = (recordc , Hc+ , u, W, B, execution record, derived target, edit, safe partial executions, complete executions labeled by result, and data needed for the final recheck. Definition 7 (Agent runtime invariant). For c = b Z), recordc = (κc , Hc , ∆c , outc , Ac ), (recordc , Hc+ , u, W, B, and resolved r, AgentSec(S; c, r) holds exactly when the following clauses hold. 1) Checked record and edit rule. The state is well formed, c = checked(H.η), its origin derives the target now in force, and every required result has one signed authority record and a checked Coversu proof. b=B b† b 2) Required results. B Hc ,u ̸= ∅, W = ↓(π2 B), and Z verifies both against recordc . 3) Executed calls. (H.G, H.T ) = HRes((Hc+ .G, Hc+ .T ), r), H.χ = Hc+ .χr, and authorization records, queue entries, return links, and checkpoints match r and advance only monotonically. b and q(H.η) 4) Current automaton. aut(H.η) ∼ = Can(W, π2 B), is its derivative after r.

5) Current rule version. Only H.η is active, entry|X[[H]].T = H.β, and it provides exactly one signed rule entry for each current workflow call, while inactive or closed versions provide none. a) Atomic tool call: For submitted tool request m, set m◦ = canonκ (m). For a call x with current rule entry j in version η, VerifyToken(h, ρ(x), j, d, m◦ ) verifies the issuing runtime, scope, rule entry, tool action, source region, and signed digest and requires m◦ = invρ (d). Set a = new(x, d) if d ∈ / D∆ , otherwise a = reuse(x, d), and let Usex (m) = Use(x, j, h, m). Its sole state-changing transition is x enabled in T entry(x) = (j, η) η = H.η phase(η) = active a VerifyToken(h, ρ(x), j, d, m◦ ) q(η) − →aut(η) q ′ Usex (m)/a

.

(12)

S −−−−−−−→ S ′ The paired update HStep((G, T ), a) removes x, records any choice, preserves the other workflow constructors, and appends a to its branch progress. Advance(S, x, a, q ′ ) changes exactly (H.G, H.T ) := HStep((G, T ), a), H.ver := ver + 1,

H.χ := χa, H.β := β \ {x}, q(η) := q ′ .

entry := entry \ {x},

In addition, new appends the immutable labeled authorization record and queues the canonical request (d, invρ (d)), never an unchecked caller request. reuse records the tool action’s stored return link without changing ∆, and all other fields remain unchanged. A verified Retry follows the stored link from χ to the authorization record for the same canonical request and returns any stable value without changing state. b) Final check and atomic rule update: At the atomic update point, the trusted runtime ignores any workflow or rule version supplied by the caller, sets ΘS (u) = (κ, H, ∆, out, A, u), and re-runs Derive(ΘS (u)) from the current execution record. For a defined derivation, ReCut(S, u, Z) recomputes the righthand side of equation (11), while VerifyZ recomputes the fixed point, coverage proof, canonical automaton, and both digests. The rules may take effect only if κ = κZ ,

ReCut(S, u, Z) = cutZ , b † ), VerifyZ (W † , B † , B H,u

−

H.η = η ,

H,u +

H,u

(13)

phase(η ) ∈ {⊥, inactive}.

b † , Z), Ready(S, u, Y ) holds when Y = Accepted(δ, W † , B the current derivation is δ, and all state-dependent premises of equation (13) hold. The committing domain transaction makes (κu , Hu , Au ) current, closes η − , activates η + , assigns a rule entry to every target workflow call, starts the canonical automaton at q 0 , and stores the checked answer. For this successor, write † b† c+ δ = (state(ΘS (u)), Hu , u, WH,u , BH,u , Z).

Only after activation does it expose Hu+ and emit Edge(u, [Hu+ ]∼ = ). Old authorization data then fails, while Retry

still follows its stored authorization-record link. A stale answer returns NoCommit and must be recomputed from the current execution record. J. Atomic Events Preserve the Invariant Write A1 , . . . , A5 for the five clauses of AgentSec in their stated order. The following matrix covers every state-changing transition after the initial rules take effect. Initial registration occurs before the root safety check, and later additions use the registered-extension transition below.

K. Events Outside the Agent’s Control and Restarts The resolved alphabet contains only tool calls checked by the runtime automaton. Agent request arrival, scheduling, completion, delivery, and stop or restart events do not append a new or reuse symbol. Request arrival and scheduler choice do not change committed runtime state. Completion updates and delivery emit modeled API observations but leave the checked partial execution unchanged. Dispatch is observable only when the oldest queued request is recorded as sent, and it also leaves the checked partial execution unchanged. Therefore none of these events advances the automaton for tool calls.

Lemma 15 (Atomic events are well defined). The atomic update induces a partial function ∂ on runtime-state and event pairs modulo consistent renaming, written ⟨V, e⟩∼ = . If e AgentSec(S; c, r) and S − → S ′ , the witness in table III satisfies AgentSec(S ′ ; c′ , r′ ) and

Lemma 16 (Other events preserve the checked partial execution). If AgentSec(S; c, r), e is one of the modeled e events above, and S − → S ′ , then the checked partial execution and canonical automaton state are unchanged and AgentSec(S ′ ; c, r) holds.

[Sec(S ′ ; c′ , r′ )]∼ = = ∂(⟨Sec(S; c, r), e⟩∼ = ).

Proof. Request arrival and scheduling do not change committed state, while denial, retry, retrieval, delivery, and restart preserve the checked runtime state. Request sending and completion updates change only the queued-request status, authorizationrecord status, or stored return record permitted by the executedcalls clause of AgentSec. None changes H.T , H.χ, the authorization sequence derived from ∆, r, or q(η), and the corresponding row of table III preserves every other invariant clause.

Proof. All transition rules use typed equality, membership, order, canonical constructors, signature verification, and equality checks. These operations are unchanged by consistently renaming private identifiers in the state and event. For an event e, let Ge (V ) be its precondition and Ue (V ) its successor update when that precondition holds. For every such renaming π, Ge (V ) ⇐⇒ Gπe (πV ) and Uπe (πV ) = πUe (V ). Thus consistently renamed inputs have the same definedness and consistently renamed successors. This proves that ∂ is well defined. For new and reuse, lemmas 3, 5 and 6 establish the first two rows of the matrix. If x lies at b, HStep appends a to b’s progress, while the same atomic tool-call update appends a to the global resolved-call trace χ. Associativity of language quotients gives

The restart lemma uses the linearizable atomic transactions required by section IV. Let D be the committed runtime state, v the unfinished in-memory state, and t̄ = t1 · · · tn the finite sequence of domain transactions overlapping a stop, ordered by their linearization points. Atomicity selects t̄≤k = t1 · · · tk , containing exactly the transactions that committed before the stop, and gives Recover(D, v, t̄) = committk ◦ · · · ◦ committ1 (D),

(Γb /raw(χb ))/x = Γb /raw(χb a). Thus the updated leaf and any later Checkpoint remain synchronized with G. For a successful edit transition, lemmas 2, 6 to 8 and 10 establish the third row for all six edit forms and registered extension. Each remaining rule changes only the fields shown in the matrix, and its row checks every invariant clause whose fields change. Thus every successor has the displayed new state and preserves AgentSec. Corollary 2 (Finite-sequence preservation). Starting from any valid bootstrap, every finite sequence of the event classes in table III ends in a state satisfying AgentSec. The sequence length is unbounded, although every individual safety-check instance and event payload is finite. For a finite word ē, the iterated update is defined on ⟨V, ē⟩∼ = , where one renaming acts on the initial state and the whole word. Proof. The base case is lemma 14, and lemma 15 supplies the invariant-preserving inductive step and consistency under renaming the remaining events.

with k = 0 interpreted as D. No state reached after restart contains only part of one modeled atomic update. In particular, a new transaction cannot expose an authorization record without its global trace, branch progress, and queued request. A rule update cannot activate a new version without closing the old version and assigning every target rule entry. Lemma 17 (Restart preserves atomic commits). Let S0 → S1 → · · · → Sn be the modeled path whose atomic transitions correspond to t1 , . . . , tn in the order above. If committed state D refines S0 , then restarting after exactly t1 , . . . , tk have committed yields a state refining Sk . At committed-state boundaries, stopping and restarting without another commit is consequently a τ self-loop. Proof. Induction on k starts from D refining S0 . At each step, the complete atomic update committi is the update in the corresponding row of table III, so it maps a concrete state refining Si−1 to one refining Si . The recovery equation applies exactly the first k updates and no partial update, yielding the claim. Once the LTS records the restarted state, stopping

Event

Atomic change

new use

Apply HStep to (G, T ); append new(x, d) to (c, rnew(x, d)) global χ; advance ver, q; append one authorization record and queued canonical request; remove the current rule entry. Apply HStep to (G, T ); append reuse(x, d) to (c, rreuse(x, d)) global χ; advance ver, q; add only the return-record link; remove the current rule entry.

reuse use

Make derived (κ+ , H + , A+ ) and the checked automaton current; close η − ; activate η + ; publish new rule entries. Return the failed derivation or rejection proof; no runtime-state change. Record the current workflow and progress in a signed Checkpoint(k, b) checkpoint; advance ver. Preload Prepare content only in an inactive rule version assigned to no call. Retry, retrieval, delivery Emit Return(t, [v]∼ = ) for a stored value whose signature verifies; no runtime-state change. Denial Return deny(x); no state change. Mark exactly the oldest queued canonical request as Dispatch(d) sent. Completion update Emit Settle(d, [v]∼ = ), advance one authorization record phase, and fill its stable return record. Stale or malformed answer Return NoCommit; no runtime-state change. Stop and restart Discard unfinished in-memory work and expose the last committed runtime state. Successful edit transition, six edit forms or registered extension Verified Invalid or Reject

New state

(c+ δ , ϵ) (c, r) (c, r) (c, r) (c, r) (c, r) (c, r) (c, r) (c, r) (c, r)

Why the invariant remains true A1 : record and edit rules unchanged. A2 : rechecking after the partial execution. A3 : unique authorization record and request order. A4 : canonical derivative. A5 : remove exactly x’s rule entry. A1 : the signed record still names the same tool action. A2 : rechecking after the partial execution. A3 : link names an earlier authorization record and the authorization sequence is unchanged. A4 : canonical derivative. A5 : remove exactly x’s rule entry. A1 : edit-rule correctness and result preservation. A2 : exact checker. A3 : prior authorizations and queued requests retained. A4 : start at qϵ . A5 : complete rule update. All clauses unchanged; γ ties the answer to the checked execution record. A1 : immutable well-typed extension. A2 , A4 , A5 : unchanged. A3 : exactly the permitted K extension. A1 –A4 : unchanged. A5 : the version remains inactive and unavailable to calls. All clauses unchanged; retry additionally checks the same canonical request and prior-authorization link. All clauses unchanged. A3 : sent requests are exactly the earliest queued requests, in order. Other clauses unchanged. A3 : tool action, canonical request, creator, authorization label, and order are immutable. Other clauses unchanged. All clauses unchanged. All clauses unchanged because each atomic update appears either completely or not at all.

TABLE III E XHAUSTIVE EVENT CLASSES AND PRESERVATION OF THE FIVE AgentSec CLAUSES .

again changes only unfinished memory and is therefore a selfloop. L. Agent-API Weak Bisimulation After Restart We now prove theorem 6 by exhausting the observable and silent cases. For runtime state S = (κ, H, ∆, out, A, . . .), define Core(S) = (κ, H, ∆, out, A) and Current(H) = b Z), define icut(c) = X[[H.T ]] . For c = (recordc , Hc+ , u, W, B, + b For I = (KI , cI , rI ) with KI = (Hc , u, W, B). (κI , HI , ∆I , outI , AI ), let αI (I) = (KI , cI , rI , HI .η, HI .β),

data or Agent-visible answer, and preserves AgentSec. The ideal side takes its single atomic edge, and both successors have the same (κu , Hu , Au ), checked safe execution set, empty processed-call sequence, active rule version, and target rule entries. Deterministic allocation gives consistently renamed authorization data, so both expose Edge(u, [Hu+ ]∼ = ). Conversely, every successful runtime rule update has passed the edit-rule, fixed-point, and record-digest checks, so lemma 8 enables the matching ideal edge. This argument applies uniformly to all six forms of Fork, Restore, and Merge and to the registered extension.

b) Tool calls and submitted requests: For a submitted tool request m, both automata compute the same m◦ = canonκ (m). Define I B S iff some c, r satisfy AgentSec(S; c, r) and The runtime authorization check verifies the issuing runtime, ℓ τ αI (I) = αS (S; c, r). Write = ⇒= τ ∗ ℓτ ∗ and = ⇒= τ ∗ . Fix I B S scope, workflow call, rule entry, tool action, source region, ◦ with witness (c, r). Equality of αI (I) and αS (S; c, r) gives signed digest, current rule version, and equality m = invρ (d). both machines the same κ, current policy, execution record, The ideal automaton requires the same rule entry, tool action, authorization log, request queue, stored return records, checked and request equality. Both sides then inspect the same set D∆ of safe execution set, current partial execution, rule version, and tool actions with authorization records, so they choose the same a ∈ {new(x, d), reuse(x, d)}. By corollary 1 and lemma 6, the current rule entries. ∗ a) Edit transitions: The equality makes both machines runtime automaton enables a after r exactly when ra ∈ L in form the same current ΘI (u) and record digest γ(ΘI (u)). If the ideal machine. derivation is undefined, both sides return the same canonical In the new case, both successors apply the same workflow Invalid answer and leave their states unchanged. If deriva- update, append the same symbol to the global trace and branch tion exists but no safe execution set exists, lemma 8 and progress, advance ver, create the same authorization record, and deterministic fixed-point checking make both sides return the queue the same canonical request. The runtime request queue same canonical Reject answer and leave their states unchanged. stores (d, invρ (d)), while the ideal queue stores (d, m◦ ). The Otherwise the ideal machine enables its edit transition and, verified request equality makes these entries identical. In the by lemma 8, the runtime checker accepts the same edit and reuse case, both successors apply the same workflow update, computes the same largest safe execution set. The runtime append the same symbol to the global trace and branch progress, takes an explicit Preload transition that records the prepared and link the workflow call to the same stored return record answer in an inactive rule version, exposes no authorization without changing ∆ or the request queue. Both successors αS (S; c, r) = (Core(S), icut(c), r, H.η, entry|Current(H) ).

remove x’s current rule entry. Because the remaining workflow no longer contains x, their entries for current calls remain equal. In either case, lemma 15 re-establishes B with witness (c, ra). If any workflow call, rule entry, authorization datum, canonical request, rule version, branch, or automaton transition check fails, both automata fail. Both machines emit deny(x), preserve state, and remain related. c) Races between a tool call and a rule update: Tool calls and rule updates serialize on the same execution record and active rule version. If a new use commits first, it changes (G, T, ∆, χ, ver, out), all of which are covered by the digest of the checked record, so the prepared rule update becomes stale. If an reuse use commits first, it changes (G, T, χ, ver) even though ∆ and the request queue are unchanged, so the prepared rule update again becomes stale. If the rule update commits first, it atomically closes η − , activates η + , refreshes every current rule entry and its authorization data, and exposes the new authorization data only after activation. The old new or reuse use then fails the current-rule-version automaton and is denied without progress. The ideal atomic order has exactly the same two cases, so neither side allows a third race outcome. d) Replies, sent requests, and silent steps: A retry with valid authorization data, retrieval of that data, or delivery of a returned value leaves the runtime state unchanged. Both machines follow the same stored link and expose Return(t, [v]∼ = ). Dispatch(d) is enabled for the same oldest queued request and makes the same observable request-sent update. Settle(d, [v]∼ = ) is enabled for the same authorization record and produces the same stable returned value and normalized update. Checkpoint(k, b) takes matching visible steps and yields the same decision. Runtime preload and internal NoCommit answers are τ -steps matched by zero ideal steps because αS omits inactive prepared data and obsapi hides internal runtime answers. A stop and restart is matched by a τ self-loop on each committed-state machine by lemma 17. Theorem 7 (Agent-API weak bisimulation after restart, detailed). B is a divergence-insensitive weak bisimulation under obsapi . Proof. The transition rules in sections A-H and VI and the matrix in table III cover every possible case. For every step from either side, the corresponding case constructs a path with observation obsapi (ℓ) and a successor related by the witness in that matrix. The construction is symmetric because the ideal and runtime automata accept the same tool calls, while runtime-only steps preserve their common visible state. Arbitrary repetition of silent preload, internal NoCommit, or restart steps is ignored, which is precisely divergence-insensitive weak matching. M. Executable-Artifact Evaluation The performance script runs every sample in a fresh CPython 3.12 process and reports the median of five repetitions on a 16vCPU AMD EPYC 7R12. The 19 paper-specific tests exercise indexed pomset resolution, the greatest fixed point, and finite fixtures for all six constructors. The executable model covers

the checker core and all six edit fixtures, while the formal proofs establish immutable edit rules, authority-approved result removal, and the complete rule-update protocol for each policy domain.

AI U SE ACKNOWLEDGMENT OpenAI Codex was used throughout the manuscript for initial prose drafting and revision, and in the executable artifact for code scaffolding and test generation. It also served as an interactive aid for literature discovery, counterexample search, and the discussion and refinement of the formal theory, including definitions, assumptions, theorem statements, and proof structure. The authors chose and directed the research, made all final theoretical and methodological decisions, independently verified the cited sources, theorem statements, proofs, code, and experimental results, and remain responsible for every claim, proof, result, and citation. R EFERENCES [1] OpenAI, “Codex App Server,” Official documentation, 2026, accessed 2026-07-31. [Online]. Available: https://learn.chatgpt.com/docs/ app-server.md [2] Anthropic, “Manage sessions,” Official documentation, 2026, accessed 2026-07-31. [Online]. Available: https://code.claude.com/docs/en/sessions [3] ——, “Checkpointing,” Official documentation, 2026, accessed 2026-0731. [Online]. Available: https://code.claude.com/docs/en/checkpointing [4] C. Wang and Y. Zheng, “Fork, explore, commit: Os primitives for agentic exploration,” 2026, agentic OS Workshop 2026. [Online]. Available: https://arxiv.org/abs/2602.08199 [5] T. Wu, C. Chang, L. Cao, W. Gao, and W. Wang, “Crab: A semantics-aware checkpoint/restore runtime for agent sandboxes,” 2026. [Online]. Available: https://arxiv.org/abs/2604.28138 [6] Y. Zhang, “Agent libos: A runtime substrate for capabilitycontrolled self-evolving llm agents,” 2026. [Online]. Available: https://arxiv.org/abs/2606.03895 [7] Y. Zheng, Y. Yang, W. Zhang, and A. Quinn, “ACRFence: Preventing semantic rollback attacks in agent checkpoint-restore,” 2026, coDAIM Workshop 2026. [Online]. Available: https://arxiv.org/abs/2603.20625 [8] S. Yu, D. Chong, A. Nandi, D. Soylu, J. Sun, C. D. Manning, and W. Shi, “Shepherd: Enabling programmable meta-agents via reversible agentic execution traces,” 2026. [Online]. Available: https://arxiv.org/abs/2605.10913 [9] Y. Li, S. Ping, X. Chen, X. Qi, Z. Wang, Y. Luo, and X. Zhang, “AgentGit: A version control framework for reliable and scalable LLM-powered multi-agent systems,” 2025. [Online]. Available: https://arxiv.org/abs/2511.00628 [10] LangChain AI, “Use time-travel,” 2026, accessed 2026-08-03. [Online]. Available: https://docs.langchain.com/oss/python/langgraph/ use-time-travel [11] S. G. Patil, T. Zhang, V. Fang, N. C., R. Huang, A. Hao, M. Casado, J. E. Gonzalez, R. A. Popa, and I. Stoica, “GoEX: Perspectives and designs towards a runtime for autonomous LLM applications,” 2024. [Online]. Available: https://arxiv.org/abs/2404.06921 [12] E. Y. Chang and L. Geng, “SagaLLM: Context management, validation, and transaction guarantees for multi-agent LLM planning,” Proceedings of the VLDB Endowment, vol. 18, no. 12, pp. 4874–4886, 2025. [Online]. Available: https://www.vldb.org/pvldb/vol18/p4874-chang.pdf [13] B. Mohammadi, N. Potamitis, L. Klein, A. Arora, and L. Bindschaedler, “Atomix: Timely, transactional tool use for reliable agentic workflows,” 2026. [Online]. Available: https://arxiv.org/abs/2602.14849

[14] Z. Chen, H. Liu, D. Xu, D. Dong, J. Li, B. Pu, and J. Zhai, “Cordon: Semantic transactions for tool-using llm agents,” 2026. [Online]. Available: https://arxiv.org/abs/2606.17573 [15] K. Yang, P. Li, Z. Wu, K. Xu, H. Huang, and X. Huang, “DART: Semantic recoverability for structured tool agents,” 2026. [Online]. Available: https://arxiv.org/abs/2605.23311 [16] M. H. de Queiroz, J. E. R. Cury, and W. M. Wonham, “Multitasking supervisory control of discrete-event systems,” Discrete Event Dynamic Systems, vol. 15, no. 4, pp. 375–395, 2005. [17] R. Malik and R. Leduc, “Generalised nonblocking,” in Proceedings of the 9th International Workshop on Discrete Event Systems, 2008, pp. 340–345. [18] B. Finkbeiner, F. Klein, and N. Metzger, “Live synthesis,” Innovations in Systems and Software Engineering, vol. 18, no. 3, pp. 443–454, 2022. [Online]. Available: https://doi.org/10.1007/s11334-022-00447-5 [19] L. Aceto, I. Cassar, A. Francalanza, and A. Ingólfsdóttir, “On runtime enforcement via suppressions,” in 29th International Conference on Concurrency Theory (CONCUR 2018), ser. Leibniz International Proceedings in Informatics, vol. 118. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2018, pp. 34:1–34:17. [20] J. A. Brzozowski, “Derivatives of regular expressions,” Journal of the ACM, vol. 11, no. 4, pp. 481–494, 1964. [21] R. E. Strom and S. Yemini, “Optimistic recovery in distributed systems,” ACM Transactions on Computer Systems, vol. 3, no. 3, pp. 204–226, 1985. [22] E. Y. Elnozahy, L. Alvisi, Y.-M. Wang, and D. B. Johnson, “A survey of rollback-recovery protocols in message-passing systems,” ACM Computing Surveys, vol. 34, no. 3, pp. 375–408, 2002. [23] W. M. P. van der Aalst and T. Basten, “Inheritance of workflows: An approach to tackling problems related to change,” Theoretical Computer Science, vol. 270, no. 1–2, pp. 125–203, 2002. [24] L. Nahabedian, V. A. Braberman, N. D’Ippolito, S. Honiden, J. Kramer, K. Tei, and S. Uchitel, “Dynamic update of discrete event controllers,” IEEE Transactions on Software Engineering, vol. 46, no. 11, pp. 1220– 1240, 2020. [25] G. Amram, S. Maoz, I. Segall, and M. Yossef, “Dynamic update for synthesized GR(1) controllers,” in Proceedings of the 44th International Conference on Software Engineering (ICSE). ACM, 2022, pp. 786–797. [26] Q. Burke, A. Vahldiek-Oberwagner, M. Swift, and P. McDaniel, “It’s a feature, not a bug: Secure and auditable state rollback for confidential cloud applications,” 2025, accepted at the 2026 IEEE Symposium on Security and Privacy. [Online]. Available: https://arxiv.org/abs/2511.13641

Related documents

• A2A-ForensicTrace: Offline Verification of Tamper-Evident A2A Runtime Evidence#1118997
• SafePar: Monitoring Asynchrony in Microservices#1117793
• SafePar: Monitoring Asynchrony in Microservices#1108661
• LLM Agents Can Easily Tamper With Their Own Traces#1078337
• Not In My Git Yard: Catching Backdoors at Commit and Release Time#410940