When Can Agents Safely Checkpoint, Fork, Restore, and Merge? Exact Checking for Execution Edits
2026-08-24 • Programming Languages
Programming LanguagesCryptography and Security
AI summaryⓘ
The authors study how an agent runtime manages changes during task execution, like saving progress (Checkpoint), branching off (Fork), restoring previous states, or merging different paths. They point out that not all edits are safe because some might repeat actions, lose important results, or conflict with ongoing processes. The authors created an algorithm that carefully checks if an edit is safe by exploring all possible ways a task can finish without breaking rules. Their method either finds safe options or proves none exist, and they verified their work with tests and formal proofs shared on GitHub.
Agent runtimeCheckpointForkRestoreMergeExecution editsAlgorithm safetyFormal verificationLean mechanizationRuntime invariant
Authors
Yusheng Zheng, Xiaoyu Song, Yanpeng Hu, Lebin Cheng, Yuxi Huang, Wei Zhang
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.