"Resume Means Resume": machine-checked audit finds LangGraph 1.2.9, CrewAI 1.15.2 and pydantic-graph all violate their own durability claims

arXiv·high signalXBlueskyLinkedInCopy link

A formal RESUME CONTRACT of six properties (prefix continuation, effect exactly-once, fork determinism, checkpoint validity, consume-once, recovery determinism) was model-checked in TLA+ across 7.4 million states, then measured against pinned releases with an LLM-free harness. LangGraph 1.2.9 durably records a second resume value and never consults it, persists schema-invalid state silently, and re-executes durably recorded work after a real SIGKILL — exactly-once across interrupts but at-least-once across crashes on the same API; CrewAI 1.15.2 re-executes completed effect-bearing methods against its written claim, and pydantic-graph 1.x cannot resume after a mid-node crash. No two probed frameworks shared a conformance profile, and consume-once collapsed under concurrency: k processes resuming one parked interrupt fired the gated effect k times, saturating in 36 of 40 fault cells.