恢复即恢复：工作流持久化层中检查点、中断和恢复语义的机器检查符合性契约

摘要

一个持久化执行状态以使运行可被中断、在崩溃后幸存并继续的框架，必须决定恢复对于已触发的副作用意味着什么。五个广泛部署的智能体工作流框架给出了不同的答案，没有一个暴露可机器检查的契约，且其行为甚至违反了它们所声明的片段。RESUME 契约规定了持久化 API 上的六个性质（前缀延续、副作用恰好一次、分叉确定性、检查点有效性、消费一次、恢复确定性），外加分叉意图和活性义务。一个 TLA+ 模型穷尽地检查参考语义，在缩放边界上保持不变（740 万个状态）；一个 39 格故障矩阵产生了独立性所需的区分模型，而消费一次发生分裂，其消费子句独立于所有其他六个。一个确定性、无 LLM 的测试框架在固定版本上对其进行测量。LangGraph 1.2.9 持久地记录第二个恢复值但从不查阅它，静默地持久化模式无效的状态，并在真实 SIGKILL 后重新执行持久记录的已完成工作：在同一 API 上，跨中断为恰好一次，跨崩溃为至少一次。CrewAI 1.15.2 与其书面声明相反，重新执行已完成且带副作用的方法；pydantic-graph 1.x 在节点中途崩溃后无法恢复；所探测的框架中没有任何两个共享相同的符合性剖面。消费一次在顺序执行下成立，在并发投递下失败：k 个进程恢复一个挂起的中断会触发门控副作用 k 次，在 40 个格子中有 36 个饱和度为 1.0，且该失败跨越主机。REMIT 是一个参考序列器，其经 Verus 验证的恢复核心与发布的可执行文件逐行相同，修复了分叉和有效性格子。跨进程格子在读路径上被修复，且该修复已交付：一个自愿加入的门控在共享存储中声明消费，在任何节点执行之前，为一个竞态者提供服务并拒绝其余竞态者。

English

A framework that persists execution state so a run can be interrupted, survive a crash, and continue must decide what a resume means for effects that already fired. Five widely deployed agent workflow frameworks answer differently, none exposes a machine-checkable contract, and behavior violates even the fragments they state. The RESUME CONTRACT states six properties over the persistence API (prefix continuation, effect exactly-once, fork determinism, checkpoint validity, consume-once, recovery determinism), plus fork-intent and liveness obligations. A TLA+ model checks a reference semantics exhaustively, unchanged at scaled bounds (7.4 million states); a 39-cell fault matrix yields the separating models independence requires, and consume-once splits, its consumption clause independent of all six others. A deterministic, LLM-free harness measures them at pinned releases. 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, 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; no two probed frameworks share a conformance profile. Consume-once holds sequentially and fails under concurrent delivery: k processes resuming one parked interrupt fire the gated effect k times, saturation 1.0 in 36 of 40 cells, and the failure crosses hosts. REMIT, a reference sequencer whose Verus-verified recovery core is line-identical to the shipped executable, repairs the fork and validity cells. The cross-process cell is repaired at the read path, and that repair ships: an opt-in gate claims consumption in the shared store, serving one racer and refusing the rest before any node executes.