Resume Means Resume

Workflow systems that survive crashes must decide what happens when they restart: do effects (like API calls) run again, and what does "resuming" actually mean? Five popular agent frameworks answer this question differently, document their answers poorly, and don't match even what little they claim. This paper formally specifies what resume should mean and measures how badly real systems fail against that spec.

The Conformance Contract

The authors define the RESUME CONTRACT—eight properties a persistence layer should satisfy:

1. Prefix continuation: resuming picks up where execution stopped.
2. Effect exactly-once: each side effect fires exactly once, whether interrupted or crashed.
3. Fork determinism: if execution branches (e.g., parallel tasks), the branch structure is deterministic.
4. Checkpoint validity: saved state is internally consistent.
5. Consume-once: a queued task runs at most once.
6. Recovery determinism: restarting from a checkpoint produces the same behavior.
7. Fork-intent and liveness obligations (guarantees about intent to fork and progress).

They formalized these in TLA+, a mathematical language for checking distributed systems properties, and verified a reference implementation exhaustively across 7.4 million state combinations. A fault matrix tested which properties hold under different failure modes (interrupts vs. crashes, single vs. multi-process).

What Real Systems Actually Do

The paper's empirical core is damning. Testing five frameworks at pinned releases with a deterministic harness (no LLM involved) reveals:

• LangGraph 1.2.9: saves a second resume value but never reads it; silently persists invalid schema; after a real SIGKILL, re-executes completed work. It's exactly-once for interrupts, at-least-once for crashes—inconsistent semantics.
• CrewAI 1.15.2: re-runs completed effect-bearing methods even after recording them done, violating exactly-once.
• pydantic-graph 1.x: cannot resume after a crash mid-node.
• No two frameworks share a conformance profile.

The consume-once failure is especially concrete: when multiple processes try to resume the same interrupt, all k processes fire the gated effect k times (saturation 1.0 in 36 of 40 test cases). This breaks across hosts.

The Fix: REMIT

The authors offer REMIT, a reference sequencer with a Verus-verified recovery core (cryptographic proof of correctness). Its executable code is line-identical to the verified spec. Two repairs: (1) fork and validity cells are fixed in the reference model, and (2) the consume-once cross-process failure is repaired at the read path—an opt-in gate in the shared store that serves one racer and rejects the rest before any node executes.

This matters because workflow systems (LangGraph, CrewAI, pydantic-graph) power production AI agents. Silent failures, duplicate side effects, and inconsistent semantics on crash are not theoretical: they corrupt data, re-bill customers, and send duplicate notifications. The paper proves five deployed systems fail conformance and offers a machine-checked contract and repair path.