Formal Verification Reveals Inconsistent Resume Behavior Across Major AI Workflow Frameworks

Persisting workflow execution state so systems can survive crashes and resume cleanly is a critical requirement for reliable agent applications—yet five major frameworks implement this feature in incompatible and sometimes unsafe ways, according to a new formal analysis.

Researchers developed a machine-checkable specification called the RESUME CONTRACT that defines six key properties workflows must satisfy: prefix continuation, effect exactly-once semantics, fork determinism, checkpoint validity, consume-once guarantees, and recovery determinism. They also specified fork-intent and liveness obligations. The framework was validated using TLA+, a formal specification language that exhaustively modeled the correct behavior across 7.4 million states.

The Conformance Gap#

Testing five deployed frameworks against this contract revealed systematic failures. LangGraph 1.2.9 durably records a second resume value but never uses it, silently persists schema-invalid state, and can re-execute previously completed work after a system crash—yielding exactly-once behavior during controlled interrupts but at-least-once behavior after real SIGKILL signals. CrewAI 1.15.2 re-runs completed effect-bearing methods despite claiming otherwise in documentation. Pydantic-graph 1.x cannot resume at all after a crash occurs mid-node.

Strikingly, "no two probed frameworks share a conformance profile," meaning operators cannot reliably reason about recovery behavior when mixing tools.

Cross-Process Concurrency Failures#

The researchers uncovered a particularly dangerous failure mode in concurrent scenarios. The consume-once guarantee, which should ensure effects fire only once even if multiple processes attempt to resume the same interrupted execution, held up under sequential resumption but failed completely under concurrent delivery. When multiple processes tried to resume a single parked interrupt, the gated effect fired multiple times—failing in 36 of 40 test cells with saturation at 1.0, and the failure persisted across host boundaries.

A Reference Implementation with Verified Recovery#

To demonstrate the fix, the team built REMIT, a reference sequencer whose recovery core was formally verified using Verus and remains line-identical to the shipped executable. REMIT repairs the fork and validity failures. For the cross-process concurrency problem, an opt-in gate at the read path claims consumption in the shared store, ensuring only the first racer executes any effect while refusing all subsequent attempts before any node runs.