# Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers

arXiv: https://arxiv.org/abs/2608.03836 · HTML: https://mlsanity.com/paper/2608.03836/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 97 references that are in the map.
- First posted on arXiv 4 Aug 2026.

## Builds on (most cited first, 15 of 15)

- [AgentBench: Evaluating LLMs as Agents](https://mlsanity.com/paper/2308.03688/) (2023)
- [Why Do Multi-Agent LLM Systems Fail?](https://mlsanity.com/paper/2503.13657/) (2025)
- [Ray: A Distributed Framework for Emerging AI Applications](https://mlsanity.com/paper/1712.05889/) (2017)
- [SagaLLM: Context Management, Validation, and Transaction Guarantees for Multi-Agent LLM Planning](https://mlsanity.com/paper/2503.11951/) (2025)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation](https://mlsanity.com/paper/2510.05156/) (2025)
- [Crab: A Semantics-Aware Checkpoint/Restore Runtime for Agent Sandboxes](https://mlsanity.com/paper/2604.28138/) (2026)
- [ACRFence: Preventing Semantic Rollback Attacks in Agent Checkpoint-Restore](https://mlsanity.com/paper/2603.20625/) (2026)
- [DART: Semantic Recoverability for Structured Tool Agents](https://mlsanity.com/paper/2605.23311/) (2026)
- [What You Approve Is What Executes: Consent Integrity for Black-Box LLM Agents](https://mlsanity.com/paper/2606.02668/) (2026)
- [Elle: Inferring Isolation Anomalies from Experimental Observations](https://mlsanity.com/paper/2003.10554/) (2020)
- [Engineering Record And Replay For Deployability: Extended Technical Report](https://mlsanity.com/paper/1705.05937/) (2017)
- [AgentRFC: Security Design Principles and Conformance Testing for Agent Protocols](https://mlsanity.com/paper/2603.23801/) (2026)
- [Stop Means Stop: Measuring and Repairing the Enforcement Gap in Agent-Framework Control Primitives](https://mlsanity.com/paper/2607.14166/) (2026)
- [LogicHunter: Testing LLM Agent Frameworks with an Agentic Oracle](https://mlsanity.com/paper/2607.06195/) (2026)

## Built on by (most cited first, 3 of 3)

- [Safe to Resume? Breaking Execution Continuity of Agent Execution via Rollback](https://mlsanity.com/paper/2608.29381/) (2026)
- [Janus: Evidence-Before-Effect Sagas and Offline-Verifiable Provenance for Agentic LLMs](https://mlsanity.com/paper/2609.38266/) (2026)
- [RippleCP: Measuring Counterfactual Checkpoint Advantage in Coding Agents](https://mlsanity.com/paper/2610.09088/) (2026)

## Abstract (arXiv)

A framework that persists execution state so a run can be interrupted, survive a crash, and continue must decide what a resume means for effects that already happened. Five widely deployed agent workflow frameworks answer differently, none exposes a machine-checkable contract, and measured behavior violates even the fragments they state. The RESUME CONTRACT states six properties over the persistence API (prefix continuation, effect exactly-once, fork determinism, checkpoint validity, consume-once, recovery determinism), plus fork-intent and liveness obligations. A TLA+ model checks a reference semantics exhaustively, unchanged at scaled bounds (7.4 million states), and the reference conjunction is additionally TLAPS-proved unbounded (196 obligations); a 39-cell fault matrix and two companion modules yield the separating models independence requires. A deterministic, LLM-free harness measures them at pinned releases. LangGraph 1.2.9 durably records a second resume value and never consults it, persists schema-invalid state silently, and re-executes durably recorded work after a real SIGKILL: exactly-once across interrupts, at-least-once across crashes, on one API. CrewAI 1.15.2 re-executes completed effect-bearing methods against its written claim; pydantic-graph 1.x cannot resume after a mid-node crash; no two probed frameworks share a conformance profile. Consume-once holds sequentially and fails under concurrent delivery: k processes resuming one parked interrupt fire the gated effect k times, saturation 1.0 in 36 of 40 cells, and the failure crosses hosts. REMIT, a reference sequencer whose Verus-verified recovery core is line-identical to the shipped executable, repairs the fork and validity cells. The cross-process cell is repaired at the read path: an opt-in gate claims consumption in the shared store, serving one racer and refusing the rest before any node executes.