Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
The paper argues that major agent workflow frameworks do not give a checkable, consistent meaning to “resume.”
It defines a RESUME CONTRACT with six persistence properties, then checks a reference semantics with TLA+ and TLAPS. A deterministic harness tests pinned releases of five frameworks and finds divergent behavior, including re-executed effects, invalid persisted state, and crash recovery that changes delivery guarantees. The paper also describes REMIT, a reference sequencer with a verified recovery core, and an opt-in shared-store gate meant to stop concurrent resume races before node execution. HF Daily Papers' note
It defines a RESUME CONTRACT with six persistence properties, then checks a reference semantics with TLA+ and TLAPS. A deterministic harness tests pinned releases of five frameworks and finds divergent behavior, including re-executed effects, invalid persisted state, and crash recovery that changes delivery guarantees. The paper also describes REMIT, a reference sequencer with a verified recovery core, and an opt-in shared-store gate meant to stop concurrent resume races before node execution. HF Daily Papers' note
score 5