Audit: LangGraph, CrewAI, Pydantic-graph Break Resume Contract

If you ship agents on LangGraph, CrewAI, or Pydantic-graph and you assume "resume after crash" means the side effects that already fired won't fire again, a new arxiv paper from Sajjad Khan says that assumption is wrong at the framework layer. The audit tests five widely deployed agent workflow frameworks against a formal RESUME CONTRACT of six properties (prefix continuation, effect exactly-once, fork determinism, checkpoint validity, consume-once, recovery determinism) and reports that none of them exposes a machine-checkable contract, and that observed behaviour violates even the fragments the vendors do state.

The specifics are the interesting part. LangGraph 1.2.9, per the paper, "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 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." These are not performance quirks. Under fault, a side-effecting node (a payment, an email, an outbound tool call) can fire twice or lose its output entirely.

Why this matters if you are running any of these in production: your idempotency assumptions are load-bearing, and the paper's claim is that the persistence contract you are trusting does not hold. Khan's setup walks a TLA+ reference semantics through 7.4 million states and a 39-cell fault matrix, so the failures are not "in one config we saw a weird thing" — they are separating models produced by an exhaustive checker.

The honest caveats are the ones the abstract itself leaves open. It does not say whether the three named framework maintainers were told before publication or have patches on the way, it does not identify the other two of the five frameworks probed, and it does not tell you how often these bugs actually fire under production traffic versus the paper's adversarial fault injection. Take the specifics as reported by a single-author preprint, not as settled.

The forward-looking part is that the paper does not just diagnose. It ships REMIT, described as "a reference sequencer whose Verus-verified recovery core is line-identical to the shipped executable," which repairs the fork and validity cells the audited frameworks miss. The useful thing for a platform team is that there is now a formal target to test framework conformance against, rather than a vendor blog post to argue with.