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

TL;DR - This paper introduces a machine-checkable contract for checkpoint, interrupt, and resume behavior in agent workflow frameworks. Testing five frameworks reveals inconsistent semantics and failures involving duplicate effects, invalid checkpoints, and crash recovery.

• The contract defines six properties, including exactly-once effects, deterministic recovery, checkpoint validity, and consume-once delivery.
• TLA+ exhaustively checks the reference semantics across 7.4 million states; a deterministic harness tests pinned framework releases.
• LangGraph, CrewAI, and pydantic-graph exhibit distinct conformance failures, and no two evaluated frameworks share a profile.
• REMIT provides a verified reference sequencer and an opt-in shared-store gate that prevents concurrent resumes from executing the same effect multiple times.