PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Yusheng Zheng, Xiaoyu Song, Yanpeng Hu, Lebin Cheng, Yuxi Huang, Wei Zhang

arXiv:2608.22928v1cs.PLcs.CR

TL;DR

Agent runtimes need to decide which recorded authorizations and required results execution edits must preserve, because untrusted edits can repeat actions or discard obligations. This paper derives an exact checker that enumerates safe completions, removes unsafe ones, and returns either all safe continuations or a checkable impossibility proof. Its formal results cover the edit forms and atomic runtime enforcement, with Lean mechanization and executable tests.

  • Problem

    Existing Agent systems support execution edits without deriving from the running execution what each edit must preserve, while unsafe edits can repeat authorizations or discard required results.

  • Method

    The runtime constructs policy-compliant complete executions from the recorded execution, removes continuations that can make required results impossible, and atomically installs the remaining rules.

  • Results

    The checker returns every safe way to proceed or a checkable proof that none exists, covering Checkpoint and six forms of Fork, Restore, and Merge.

  • Takeaways & Limitations

    Exact runtime decisions require preserving action-reference links, earlier authorizations, and still-required results across repeated edits and restarts.

Abstract

from arXiv · show

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. INTRODUCTION

Execution edits let agents branch, restore, and merge ongoing work, but safety depends on preserving recorded authorizations, action links, and still-required results. The paper derives an exact checker that computes all safe continuations, rejects unsafe combinations with checkable proofs, and enforces accepted edits atomically across later edits and restarts.

  • Motivation: Execution edits support exploration, recovery, and reuse without restarting tasks, while changing future workflow does not erase recorded calls.Checkpoint records an execution; Fork, Restore, and Merge change what the Agent does next.
  • Motivation: A runtime cannot trust the Agent’s execution account because restoring or merging can repeat a one-time approval or combine incompatible supplier actions.The laptop example records the approval and payment authorization independently of the Agent’s edited workspace.
  • Safety model: Exact safety must preserve earlier authorizations and every result that remains required, while distinguishing copied calls from new authorizations and handling overlapping calls atomically.The checker needs task structure, required results, action-reference links, authorization progress, and rules governing calls that overlap the edit.
  • Exact checking: The checker enumerates complete policy-compliant executions, removes those that can strand a required result, and either returns every remaining safe continuation or a checkable proof of impossibility.For example, pruning one supplier can be rejected when it removes a still-required result, while incompatible safe plans can jointly yield Reject.
  • Enforcement and guarantees: The formal protocol rechecks the execution record, applies accepted rules atomically, and preserves exactness across later calls, execution edits, stops, restarts, and authorization-link distinctions.The checker returns one largest safe execution set, and later checks retain the same safety condition as the first.
  • Mechanization and validation: The results cover Checkpoint and six forms of Fork, Restore, and Merge, with Lean mechanization and executable validation supporting the finite checker and runtime invariant.The reported formalization includes registration and runtime components, while tests validate all six edit forms.

IV. MODEL AND SECURITY OBJECTIVE

The model treats tool-using workflows as finite contracts over results and partially ordered calls, while an immutable execution record tracks structure, progress, authorizations, and edit history.

  • Workflow results and call order: Several workflow calls may refer to one tool action, sharing an authorization record that the first processed call creates and later copied calls reuse.Processing records authorization or reuse; remote completion and returned values occur later.
  • Workflow results and call order: A workflow contract assigns a finite set of results, each with a pomset whose linearizations are allowed call orders.For the laptop example, oL orders L-payment before L-shipment, while results remain distinct.
  • Workflow results and call order: Choice, parallel, and sequence compose contracts differently: choice preserves indexed alternatives, parallel permits causal interleavings, and sequence imposes a barrier.The constructors require disjoint workflow calls and preserve unambiguous complete sequences.
  • Execution record: The execution record stores an immutable workflow DAG, current workflow, checkpoints, call identities, progress, authorization data, and the active rule version.Branch and group identifiers, contracts, progress records, and rule metadata support edits without losing recorded structure.
  • Execution record: Checkpoint stores a signed branch snapshot and advances the state version without changing the current workflow, authorizations, active rules, or authorization sequence.Its check requires the checkpoint contract to match the branch contract after recorded progress is removed.

2) Well-formedness:

Well-formedness binds the recorded workflow, authorization state, policy, and edit metadata into a trusted finite structure from which exact checks can be derived.

  • Well-formedness: The execution record is well formed only when its DAG, identifiers, checkpoints, contracts, and current workflow satisfy structural consistency conditions.Every editable identifier has a unique context, and checkpoints reference immutable nodes with stored contracts and progress.
  • Well-formedness: Current workflow calls must match the registered contracts after recorded progress, while processed calls remain consistent with pomset order and choice status.The caller cannot replace a current leaf with a smaller result set.
  • Authorization and completion: Authorization records bind actions to immutable canonical requests, scopes, digests, source regions, tokens, and trusted runtime entries.The authorization log is append-only, and the queue preserves the order of new authorizations.
  • Adversary and trusted boundary: The adversary controls Agent outputs, edit requests, arguments, copied workspace, retries, stale tokens, and scheduling, but cannot forge registries, policies, logs, or DAG structure.The policy authority signs requirements and removals, and the trusted runtime checks calls and edits.
  • Adversary and trusted boundary: The runtime registers finite tool-call templates, canonicalizes requests, reuses certified actions or allocates fresh ones, and builds the finite model R.CheckReg verifies correspondence among results, call order, shared actions, and first-time authorizations.
  • Security objective: The security objective requires preserving unsatisfied and unauthorized-to-remove results, obeying policy, completing every allowed partial execution, and retaining completion for compatible results.The checker derives the edited workflow, classifies authorization creation or reuse, and removes violating complete executions.
  • Checking an edit rule: Each edit request names an edit kind, object IDs, and registered rule, whose registry entry specifies source patterns, added steps, copy regions, and result authorities.The rule judgment checks object membership, pattern matching, preservation maps, coverage, authorized removals, and defined target composition.
  • Checking an edit rule: Preservation maps use a global bijection and result surjection to retain shared calls, source regions, order, and coverage across carried or copied regions.The surrounding-workflow identity map and disjoint cover account for unchanged, copied, and added calls.

2) Preserving Required Results:

The checker preserves required results and recorded execution relationships while atomically installing derived rules and rejecting edits whose target structure or authority conditions fail.

  • Preserving Required Results: The registered edit rule determines which results Fork, Restore, and Merge must account for, while results outside the edited region remain unchanged.The checker distinguishes already-satisfied results, still-required results, and removals authorized by the policy authority.
  • Preserving Required Results: Carry preserves identifiers and recorded structure, whereas cloning assigns fresh identifiers while retaining order, actions, scope, digests, source regions, and authorities.Each copied branch starts from its registered remaining contract with empty progress.
  • Preserving Required Results: MergeSelect is valid only before the unselected arm records progress, while MergeJoin prevents the same sibling pair from being joined again.An open choice becomes committed when its first processed call selects an arm, including when that call reuses an authorization.
  • Preserving Required Results: All six Fork, Restore, and Merge forms replace runtime rules in their policy domain and apply the derived state update atomically.The updated record preserves earlier progress and authorities while initializing copied or added branches without progress.
  • Preserving Required Results: Invalid derivations include nonexistent checkpoints, wrong modes, mismatched patterns, unauthorized removals, and undefined compositions.Independent policy domains advance by asynchronous product, replacing all rules in each domain together.
  • Preserving Required Results: The checker first classifies calls as new authorizations or reuses, then computes the largest execution set that remains safe throughout execution.This separates authorization accounting from the global required-result safety check.
  • Preserving Required Results: The derivation is deterministic and preserves every satisfied result and still-required source result except a removal signed by the proper authority.It also preserves shared actions, source regions, result authorities, and causal order, while providing a covering target result for each required result.
  • Preserving Required Results: Before rules change, the runtime rechecks the complete record, and newly created authorization tokens remain inactive and inaccessible until the update takes effect.The updated registry retains action, source region, scope, digest, and retry information.

B. New and Reused Authorizations

The authorization analysis distinguishes new actions from reused records and computes a largest safe set of complete and partial executions that preserves required-result completion.

  • New and Reused Authorizations: Resolve annotates each workflow call as creating a new authorization or reusing an earlier record, based on whether its action is already authorized.The authorization sequence includes labels for new authorizations and nothing for reuse.
  • New and Reused Authorizations: The six Fork, Restore, and Merge forms are presented as distinct edit constructors whose validity depends on the corresponding registered rule and execution-record state.The table enumerates the six forms covered by the checker.
  • New and Reused Authorizations: Retries repeat the same canonical request without adding workflow calls, while copied calls can advance processed-call progress without changing the authorization sequence.Restored calls sharing an action remain distinct workflow positions but reuse one authorization record.
  • New and Reused Authorizations: The finite annotation process is deterministic, preserves sequence length, and authorizes each action at most once outside the existing authorization set.Induction establishes that annotations depend only on calls seen so far.
  • Computing the largest safe execution set: A safe execution set pairs currently allowed partial executions with complete executions that justify them and preserve every required source result.Its conditions include nonemptiness, policy compliance, completion from every partial execution, and coverage of each required result.
  • Computing the largest safe execution set: The checker repeatedly removes complete executions that could leave a compatible result without a policy-safe completion after a shared partial execution.Pruning continues until the finite set reaches a fixed point.
  • Computing the largest safe execution set: A safe edit exists exactly when the fixed-point construction is nonempty; when it exists, the resulting set contains every other safe execution set.The largest set therefore combines all mutually compatible safe call orders.

2) Why Result-by-Result Checking Fails:

The checker must evaluate completion families jointly: removing one candidate can strand a result that another candidate still needs. A greatest fixed point therefore identifies exactly the nonblocking safe family, or proves that none exists.

  • Fixed-point checking: The candidate family is pruned iteratively because removing one completion can eliminate support for another required result.In the example, removing one candidate leaves a result without any completion, forcing removal of the remaining candidate.
  • Why result-by-result checks fail: Exact checking requires result-indexed nonblocking, not ordinary nonblocking of the projected execution language.The indexed condition tracks which completion belongs to each result and is strictly stronger than marker nonblocking on the unaugmented projection.
  • Fixed-point checking: The largest nonempty fixed point is the maximal completion subfamily satisfying nonblocking for every result.If the fixed point is empty, no nonempty completion subfamily satisfies the required condition.
  • Trusted derivation: The runtime derives completion conditions from the requested edit, authorization information, actions, and execution record before applying the fixed-point test.It also determines whether calls create or reuse authorizations and can recompute the check after partial execution.
  • Checker outcomes: The checker returns Invalid when derivation fails, Reject with ordered removal reasons when no fixed point remains, and Accepted with the largest safe execution set otherwise.Its output includes a digest of the checked execution record.

5) Checker Outputs:

The checker turns the maximal safe execution set into a finite automaton and atomically updates runtime rules. Its guarantees establish exact decisions, record-information requirements, repeated-use safety, and serialized interaction with tool calls.

  • Finite enforcement: A nonempty safe execution set becomes a deterministic automaton whose enabled traces and marked states represent safe partial and completed executions.The automaton enables exactly transitions whose extensions remain in the safe set and marks states corresponding to completed executions.
  • Atomic rule update: The runtime atomically replaces old rule versions, entries, and authorization tokens only after rechecking the current execution record.If a tool call commits first, the edit becomes stale; if the update commits first, the old authorization token fails.
  • Formal guarantees: The formal results make exact checking equivalent to the existence of a safe runtime implementation and preservation of required results.The checker returns Invalid, Reject, or Accepted according to derivation and the nonempty largest safe execution set.
  • Necessary record information: The full execution record must retain the workflow and required results, action correspondence, authorization and progress information, and overlapping-call rules.Omitting any one part wholesale can make two records indistinguishable despite different correct answers.
  • Scope boundary: Exactness fails when the checker loses call-to-action correspondence or relies only on the caller’s description of the next execution.Generalized nonblocking is exact only after the trusted runtime derives the workflow and result-specific completion conditions.
  • Repeated-use safety: Every enabled event preserves the runtime invariant, so the guarantees continue through finite sequences of edits, extensions, calls, updates, stops, and restarts.The runtime correctness result additionally relates the implementation to the ideal behavior through divergence-insensitive weak bisimulation.

VIII. MECHANIZATION AND EXECUTABLE VALIDATION

The paper mechanizes its finite checker and runtime invariant in Lean and validates the six edit forms with executable tests. Measurements show millisecond-scale checking across accepted and rejected finite instances.

  • Mechanization: Six Lean modules mechanize the finite linear-contract core and prove that the executable checker accepts exactly when a valid safe execution set exists.The mechanization also covers registration, exact answers for the current record, and sound and complete editing for all six edit forms.
  • Executable validation: All 19 paper-specific tests and 62 authorization and checker regression tests pass.The tests cover the supporting authorization and checker components in addition to the paper-specific cases.
  • Measurements: Across accepted instances with 2–128 results, checker time ranges from 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.
  • Runtime validation: The runtime derives edited workflows, action reuse, still-required results, completion conditions, and rules directly from the execution record.It then computes the largest safe execution set and applies rules atomically for new authorizations and reuse of existing ones.
  • Scope of guarantees: The formal results cover Checkpoint, all six Fork, Restore, and Merge forms, registered extensions, rejection proofs, and the record-information lower bound.The guarantees continue through the atomic runtime protocol.

APPENDIX A SUPPLEMENTARY PROOF APPENDIX

The appendix formalizes required-result preservation, fixed-point computation, exact checking, output-sensitive complexity, and the relationship between computed safe execution sets and declarative safety.

  • Scope assumptions: The appendix preserves the finite registered-call and atomic policy-domain assumptions, with independent domains interpreted by product semantics.The proof details are stated for theorem 3 under these assumptions.
  • Required-result preservation: Required results are partitioned into already satisfied, authorized for removal, and still required before the edit.Preservation applies exactly to source results that are neither completed nor authorized for removal.
  • Computed answer: The computed fixed point is nonempty exactly when a declarative maximal safe execution set exists, and that set is unique and largest.When the fixed point is empty, every hypothetical safe execution set would contradict the required nonemptiness condition.
  • Exact correspondence: Exact checking enables the ideal edit transition exactly when the checker returns a nonempty fixed point.On acceptance, the ideal language equals the generated language of the finite automaton built from the fixed point.
  • Complexity: The checker runs in O(D + nΛ + |Gcov| + VB log(2 + VB)) time and O(D + Λ + |Gcov|) space under the stated unit-cost model.D is checked input size, Λ is emitted linearization size, and Gcov contains examined candidate, partial-execution, and required-result triples.

B. Ordered Rejection Proofs

The checker represents rejection as a finite, verifiable descending fixed-point computation over possible safe executions. An empty result proves that no safe execution set, and therefore no safe enforcement, exists.

  • B. Ordered Rejection Proofs: The proof records a canonical initial family and successive finite execution sets.Each round verifies entries against compatibility and removes executions that cannot safely complete.
  • B. Ordered Rejection Proofs: The verifier checks the canonical initial state, each fixed-point round, and final emptiness.Soundness places every post-fixed safe family inside the computed sets, while completeness follows from canonical iteration.
  • B. Ordered Rejection Proofs: An empty fixed-point computation yields a rejection proof.The verifier accepts the proof exactly when the descending computation reaches an empty final family.
  • B. Ordered Rejection Proofs: The formal model authenticates the checked record and rule inputs through canonical, length-delimited encoding and domain-separated digests.The guarantee relies on injective digest behavior represented by unforgeable identifiers.
  • B. Ordered Rejection Proofs: The full record is preserved across registered extensions, so existing safe completions and required results remain available.A verified extension preserves current workflow, action identity, result labels, and the existing policy inclusion A ⊆ A+.

3) Rechecking after a partial execution:

Rechecking after partial execution requires retaining answer-relevant record distinctions and recomputing safety from the current execution. The paper shows that omitting any major record part can make opposite answers indistinguishable.

  • 3) Rechecking after a partial execution:: The greatest fixed point can be recomputed after removing an executed prefix while preserving result identities, policy, and the target registry.The resulting quotient equals the next-check fixed point, establishing the generated-language equality.
  • 3) Rechecking after a partial execution:: Every one of the four record parts contains an answer-relevant distinction.For each omitted part, the paper constructs valid records that become indistinguishable despite requiring opposite answers.
  • 3) Rechecking after a partial execution:: An exact checker must preserve workflow requirements, action correspondence, execution history, and overlapping-rule information.These are the four record parts P, I, E, and C used to define exact reduced views.
  • 3) Rechecking after a partial execution:: Registration is finite and checked by excluding reachable result-relevant tool-call cycles before comparing projected languages.Accepted registrations preserve result identity and causal order, and establish the checked initial state.
  • 3) Rechecking after a partial execution:: Dropping call-to-action or authorization-to-action links produces indistinguishable records with different correct answers.The paper separately demonstrates that tool-call text and shared authorization data cannot recover these correspondences.
  • 3) Rechecking after a partial execution:: The trusted runtime must derive the edited workflow, preserve result identities, and retain each result’s completion condition before applying generalized checking.The target or caller description alone does not determine the correct answer.

H. Ideal Atomic Execution Machine

The ideal atomic machine derives edit outcomes and safe behavior from the current execution record, then applies accepted edits in one atomic transition. Tool calls use stored action identity and authorization state.

  • H. Ideal Atomic Execution Machine: Accepted edits replace the current workflow contract with a derived target and safe execution set.The machine resets the transaction phase while making the new target and checked safe behavior current.
  • H. Ideal Atomic Execution Machine: Each edit request is classified as Invalid, Reject, or Accepted from the same current execution record.Undefined derivations preserve state, unsafe defined derivations return Reject, and accepted derivations enable one atomic edge.
  • H. Ideal Atomic Execution Machine: Tool calls are permitted only when the canonical request, action identity, authorization data, and safe-language state agree.The machine distinguishes new authorization from reuse of an existing authorization record.
  • H. Ideal Atomic Execution Machine: Checkpoint, retry, dispatch, completion updates, and restart apply the same freshness and remaining-work checks in the ideal and runtime machines.External-network completion after dispatch is modeled as environmental behavior.
  • H. Ideal Atomic Execution Machine: Every reachable partial execution retains a policy-safe completion until the next edit changes the workflow contract.The runtime implements this guarantee without enumerating the full completion set at every tool call.

I. Runtime State and Atomic Transitions

The runtime state stores the checked record, active rule version, automaton, execution progress, and authorization data needed for safe transitions. Atomic rechecking prevents stale or caller-supplied state from controlling an edit.

  • I. Runtime State and Atomic Transitions: Invalid answers carry failed derivations, Reject answers carry complete ordered proofs, and Accepted answers bind the record, target, automaton, and rule versions.Only after activation does the runtime expose the successor state and emit the transition edge.
  • I. Runtime State and Atomic Transitions: The runtime state combines cryptographic context, execution history, authorization data, policy, transaction phase, rule entries, automaton state, and checked results.Active versions also retain the derived target, safe partial executions, complete result-labeled executions, and final-recheck data.
  • I. Runtime State and Atomic Transitions: Runtime safety requires checked records, required-result coverage, executed-call consistency, a canonical current automaton, and a single active rule version.These conditions define the AgentSec invariant.
  • I. Runtime State and Atomic Transitions: Atomic tool calls verify the signed rule entry, action, source region, scope, and canonical request before changing state.New calls append an immutable authorization record; reuse follows the stored return link without changing authorization data.
  • I. Runtime State and Atomic Transitions: At the atomic update point, the runtime ignores caller-supplied workflow and rule versions and re-derives the edit from the current record.It recomputes the fixed point, coverage proof, canonical automaton, and digests before committing.
  • I. Runtime State and Atomic Transitions: A stale answer returns NoCommit and must be recomputed from the current execution record.

J. Atomic Events Preserve the Invariant

The runtime’s atomic event updates preserve AgentSec and the checked partial execution, including across edits, ordinary events, and restarts. Finite sequences therefore remain safe from any valid bootstrap.

  • Invariant preservation: Atomic updates preserve AgentSec by checking each changed invariant clause and applying state changes as one indivisible transition.The preservation matrix covers new and reuse calls, edits, rule updates, and other event classes.
  • Finite sequences: Every finite sequence of modeled event classes preserves AgentSec from any valid bootstrap, even though the sequence length is unbounded.Each individual safety-check instance and event payload remains finite.
  • Other events: Request arrival, scheduling, replies, delivery, and completion do not alter the checked partial execution, while dispatch and settlement change only permitted recorded fields.The corresponding transitions preserve AgentSec and leave H.T, H.χ, the authorization sequence, r, and q(η) unchanged except where explicitly allowed.
  • Restarts: Stopping and restarting exposes only the transactions committed before the stop, never a partial modeled atomic update.The restart lemma states that recovery after t1 through tk commits yields a state refining Sk; stopping at a committed boundary is a τ self-loop.
  • Invariant preservation: New and reuse calls update workflow state, traces, authorization data, and queued requests while preserving the corresponding runtime invariants.Reuse links an earlier authorization without changing the authorization sequence; new creates a unique authorization record.

L. Agent-API Weak Bisimulation After Restart

The paper proves that the runtime and ideal Agent-API models remain weakly bisimilar after restart. Their corresponding steps produce the same observations, while runtime-only steps preserve the shared visible state.

  • Bisimulation relation: The relation equates the runtime and ideal models on core state, execution records, authorization data, queues, return records, checked executions, versions, and current rule entries.The relation holds when both abstractions arise from the same AgentSec witness.
  • Matching transitions: Edit transitions match across all six Fork, Restore, and Merge forms and registered extension when derivation, fixed-point, and record-digest checks succeed.Undefined derivations and empty safe execution sets produce matching canonical failures without state changes.
  • Matching transitions: Tool requests are matched by canonicalization, authorization checks, current rule entries, and equality of the canonical request.Both automata inspect the same authorized tool actions and choose corresponding outcomes.
  • Concurrency and recovery: Rule-update races are serialized on the execution record and active rule version, making stale concurrent updates fail safely.Whichever operation commits first invalidates the other prepared operation or atomically installs the new rule version.
  • Conclusion: Theorem 7 establishes divergence-insensitive weak bisimulation under obsapi after restart.The proof covers every observable and silent transition, with runtime-only steps preserving common visible state.
Loading 2608.22928v1…