Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
Sajjad Khan
cs.LG, cs.DC, cs.LO, cs.SE
2026-08-04
A TLA+ contract and an LLM-free harness test five agent frameworks' resume semantics; none honors its own promises, and LangGraph ignores a second resume and re-runs completed work after a crash.
Agent frameworks like LangGraph, CrewAI and LlamaIndex Workflows ship with a persistence layer: they record how far a run has gotten so it can pause for human approval, recover after a crash, or resume after preemption. The promise is old. What is new is that it now sits under developers building LLM agents who gate payments, messages and file writes behind a checkpoint.
What "continue" means is something no framework states cleanly. When the same interrupt is answered twice with different values, which already-fired effects run again? The five frameworks give incompatible answers. CrewAI's docs claim restoration "resume[s] without re-running completed work." LlamaIndex's docs tell users to "make any preceding work safe to re-execute." LangGraph memoizes completed @task results across a resume. Three frameworks, three answers that contradict each other, and on measurement two of them do not even meet the semantics they themselves state.
The paper calls this incoherence: it is not that nobody wrote a spec, it is that the ones who did disagree, including with themselves.
The authors do not rank frameworks. They first write a machine-checkable contract. The RESUME CONTRACT defines six properties over the persistence API:
A seventh property, FI (fork-intent expressibility), requires the branch discriminator to be expressible on the wire. CO is the only property that splits: its consumption clause is independent of all six others, while its effect clause is a definitional restriction of EO.
The contract is checked in two layers. The first is a TLA+ model, ResumeContract.tla (251 lines), with six fault switches that inject mechanisms observed in deployed frameworks, exhaustively checked by TLC. The reference config R0 holds all six invariants over 87 generated / 59 distinct states; scaled config R8 (10 tasks, 4 fork values, 5 resumes, 4 crashes) holds at 7.4 million distinct states, depth 24, with verdicts unchanged. A 39-cell single-fault matrix yields the separating models that independence requires (Proposition 2).
The second layer is a deterministic harness that makes no LLM calls: pure Python protocol sequences hit framework persistence APIs directly, with no timing windows, and crashes come from an exception matrix plus a SIGKILL gated on a filesystem barrier (probe 133). Effect counts come from process-local counters, cross-checked on durable backends against an on-disk SQLite ledger. Because the ledger append is itself the irreversible effect, it can only undercount, so every reported duplicate is a floor.
The matrix is blunt: no two probed frameworks share a conformance profile.
| Framework | Property | Measured behavior |
| LangGraph 1.2.9 | FD (#6663) | Durably records the second resume value and never reads it; resume(False) still returns the first value 1; reproduces 40/40 across 5 versions and 3 backends including live PostgreSQL |
| LangGraph 1.2.9 | CV (#6491 class) | Persists schema-invalid state silently; on 1.2.9 nothing raises, the thread stays readable with a corrupt value |
| LangGraph 1.2.9 | EO | On one API, exactly-once across interrupts but at-least-once across crashes |
| CrewAI 1.15.2 | EO/PC | Re-runs completed effect-bearing methods on checkpoint restore, against its own "without re-running" docs |
| LlamaIndex Workflows 2.22.2 | EO | Docs openly acknowledge at-least-once prefix replay |
| pydantic-graph 1.107.1 | PC | Cannot resume after a mid-node crash; the resume entry point is defeated |
| AutoGen AgentChat 0.7.5 | CV | The only probed framework that loudly rejects tampered state |
Concurrency is the one setting consume-once cannot hold. k processes resuming one parked interrupt fire the gated effect k times; 36 of 40 cells hit saturation 1.0, neither durable backend drops below 0.933, and two racers on separate machines duplicate in 10 of 10 repetitions. A kill-point sweep (probe 160) shows that every incomplete persistence boundary licenses re-execution of completed work. A small but telling side note: LangGraph behaviors #7361 and #6792 shipped as 1.1.x regressions and were fixed in 1.2.9, so without a contract the semantics drift even inside one framework.
The repair artifact is REMIT, a reference sequencer that interposes at the checkpointer interface every framework already routes through: a Rust core, PyO3 bindings and a LangGraph shim, with a Verus-verified recovery-decision core line-identical to the shipped executable (on PyPI as v0.1.2). It maps the six properties to local invariants (EO/CO to ledger uniqueness, PC to frontier monotonicity, FD to ⟨checkpointId, resumeIndex⟩ branch keying, CV to write-time validation, RD to the sequencer's total order). In measurement it repairs three cells: a validating saver turns LangGraph's silent persistence into a loud rejection (probe 123, ✗ to ✓); the fork fix lives on the read path rather than the write path, where overriding gettuple strips the recorded resume pending writes so the invocation's own value is consulted, repairing #6663 (probe 134); the concurrent consume-once cell is repaired by an opt-in shared-store gate that serves one racer and refuses the rest, {1:10} on both backends. Overhead stays within 5% of stock in the container and around 1.7% on the developer host.
These are exactly the things AI engineers do today on LangGraph and CrewAI: gating a tool call, a payment or a message behind human approval or crash recovery. The paper's warning is specific. The "it recovers" layer you depend on is often under-specified, and in the worst case it silently re-runs work or silently stores corrupt data. The fallout is concrete: double charges, duplicate messages, corrupt state no one can detect.
Practitioners can take away three things. First, the six properties are themselves a checklist for auditing whichever framework you use. Second, the LLM-free, timing-free harness shows these bugs reproduce deterministically, independent of model or race, so they belong in CI. Third, REMIT is a reference that drops in at the checkpointer interface.
This is infrastructure-correctness work, not a capability advance. It will not make an agent smarter, but it turns "recoverable" from marketing copy into a property you can check.
The authors are unusually restrained about what they have proven, with a dedicated "what is and is not claimed" section. They do not claim the property set is minimal, complete or sufficient; they give no prevalence rates for any violation; the five frameworks do not represent the ecosystem; and a framework fails only the properties it is measured on. REMIT's verification reaches only the recovery-decision core: Verus proves that core function, line-identical to the shipped binary, but no end-to-end refinement is claimed, and the composite package and compiled binary are out of scope.
Two concerns stand out. Every conclusion holds "on the probed paths," and the authors concede they make no claim about unmeasured properties, while real agent deployments have a state space far larger than these deterministic protocols cover, with races from the network, multiple workers and shared-store latency that the 40-cell matrix may not exhaust. The concurrent consume-once failure is measured and repaired, but the repair is an opt-in shared-store gate on the read path, which amounts to bolting a distributed-lock semantics onto the framework; its long-term maintainability and whether it introduces new failures are not discussed.