恢复即恢复：工作流持久层中检查点、中断与恢复语义的机器可检查一致性契约
Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
浏览论文内容
中文总结 AI 辅助
该研究提出了RESUME CONTRACT契约，用TLA+模型等方法验证了五个智能体工作流框架的一致性问题，并通过REMIT修复了相关故障。
中文摘要 AI 辅助
一种用于持久化执行状态的框架可使运行过程被中断、在崩溃后存活并继续执行，但必须确定恢复操作对已触发的效果意味着什么。五个广泛部署的智能体工作流框架对此给出了不同的答案，且没有一个框架公开了机器可检查的契约，其行为甚至违反了它们自身声明的部分内容。RESUME CONTRACT 在持久化 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 验证的恢复核心与已部署的可执行文件逐行相同，修复了分叉和有效性单元；跨进程单元在读取路径处被修复，且该修复已部署：一个可选的门控在共享存储中声明消费，在任何节点执行前服务一个竞态者并拒绝其余竞态者。
英文摘要
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 happened. Five widely deployed agent workflow frameworks answer differently, none exposes a machine-checkable contract, and measured 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), and the reference conjunction is additionally TLAPS-proved unbounded (196 obligations); a 39-cell fault matrix and two companion modules yield the separating models independence requires. 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: an opt-in gate claims consumption in the shared store, serving one racer and refusing the rest before any node executes.
