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

Analysis

Why This Paper Matters

Workflow persistence layers are critical for agent frameworks that need to survive crashes and resume execution. However, the semantics of what 'resume' means for already-fired effects are often ambiguous and inconsistent across frameworks. This paper addresses a significant gap by proposing a formal conformance contract, the RESUME CONTRACT, which specifies six properties that any persistence API should satisfy. This is crucial because without a machine-checkable contract, developers cannot reason about the behavior of their workflows under failure, leading to subtle bugs and data inconsistencies.

The paper's empirical findings are alarming: five widely deployed frameworks (LangGraph, CrewAI, pydantic-graph, and others) violate even the fragments of semantics they claim to support. For instance, LangGraph exhibits exactly-once across interrupts but at-least-once across crashes on the same API, while CrewAI re-executes completed effect-bearing methods. This inconsistency highlights the need for a standardized contract and testing methodology, which this paper provides.

Technical Contributions

• Formal Contract: The RESUME CONTRACT defines six properties (prefix continuation, effect exactly-once, fork determinism, checkpoint validity, consume-once, recovery determinism) plus fork-intent and liveness obligations. This is the first machine-checkable contract for resume semantics in workflow persistence.
• TLA+ Model: A TLA+ specification of the reference semantics is exhaustively checked at scaled bounds (7.4 million states), providing a rigorous foundation for the contract.
• Fault Matrix: A 39-cell fault matrix is used to separate frameworks based on their conformance profiles, revealing that no two frameworks share the same profile.
• Deterministic Harness: An LLM-free, deterministic harness measures conformance at pinned releases, ensuring reproducibility.
• REMIT and Opt-in Gate: REMIT, a Verus-verified reference sequencer, repairs fork and validity cells. An opt-in gate claims consumption in the shared store, fixing the cross-process consume-once cell.

Results

The empirical evaluation shows that LangGraph 1.2.9 durably records a second resume value but never consults it, persists schema-invalid state silently, and re-executes durably recorded work after a real SIGKILL. This means exactly-once across interrupts but 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. The consume-once property holds sequentially but fails under concurrent delivery: k processes resuming one parked interrupt fire the gated effect k times, with saturation 1.0 in 36 of 40 cells, and the failure crosses hosts. REMIT repairs the fork and validity cells, and the opt-in gate repairs the cross-process cell.

Significance

This paper sets a new standard for workflow persistence by introducing a formal contract that can be machine-checked. It provides a methodology that framework developers can adopt to test and verify their implementations. The findings expose critical flaws in popular frameworks, urging the community to prioritize conformance and reliability. The REMIT reference implementation and opt-in gate offer practical solutions that can be integrated into existing systems. This work has the potential to influence the design of future agent frameworks, ensuring that they provide consistent and predictable behavior under failures, which is essential for production-grade AI applications.