Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
工作流持久层恢复语义的机器检验一致性契约
针对五个 Agent 工作流框架的 checkpoint/resume 行为，提出可机器检验的六项一致性契约并测量实际严重违规
📌 工作参考价值
- 框架选型前自测恢复语义：参考论文的确定性无 LLM 测量套件，对 LangGraph、CrewAI 等候选框架注入真实 SIGKILL，观察持久化状态是否正确、effect 是否重放，避免线上事故。
- 为业务工作流定义契约：将 RESUME CONTRACT 的六个属性（前缀延续、effect 精确一次、fork 确定性、checkpoint 有效性、consume-once、恢复确定性）落地为内部工作流引擎的回归测试项。
- 关注并发恢复竞态：论文揭示 k 个并发 resume 会导致 effect 重复执行 k 次，饱和率 1.0。若业务中有多实例同时尝试恢复同一任务，必须引入分布式消费锁（如 REMIT 的读侧 gate），否则商品状态变更、消息推送可能重复触发。
- 检查点 Schema 校验：LangGraph 会静默持久化与 schema 不一致的状态，导致恢复后行为异常。在自研工作流引擎中，应当在 checkpoint 写入时强制校验状态 schema，避免线上污染。
动机：企业 Agent 工作流依赖持久化层保存中断状态并在崩溃后恢复执行，但五大主流框架（LangGraph、CrewAI 等）对“resume 到底意味着什么”行为不一，文档模糊且实测违反自身说明，缺乏可验证的契约。
方法：作者提出 RESUME CONTRACT，定义持久化 API 需满足的六项关键性质：前缀延续（继续执行未完成步骤）、effect 精确一次、fork 确定性、checkpoint 有效性、consume-once（门控效果仅执行一次）、恢复确定性，以及活跃性义务。随后在 TLA+ 中建立参考语义并穷举模型检查（720 万状态），生成 39 格故障矩阵，证明五项性质独立，consume-once 可进一步拆分为效应条款与消费条款。开发确定性无 LLM 的测量套具，在固定版本下测量五个真实框架行为，并构建 REMIT 参考排序器修复违规。
关键结果：LangGraph 1.2.9 持久化第二个 resume 值但从不使用，静默持久化 schema 非法状态，在真实 SIGKILL 后重放已完成工作——同一 API 上中断呈现 exactly-once，崩溃却 at-least-once；CrewAI 1.15.2 违反宣称承诺，重新执行已完成的效果方法；pydantic-graph 1.x 无法从节点内崩溃恢复；并发场景下 consume-once 完全失败：k 个进程恢复同一暂停中断时 effect 重复 k 次，40 格实验中 36 格饱和率 1.0，跨机器复现。REMIT 修复 fork 与有效性缺陷，并在读侧实现消费门，以 opt-in 方式提供修复。