Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
arXiv 论文 2608.03836v1 提出 RESUME CONTRACT，定义工作流持久化层中断/恢复语义的六个属性，并用 TLA+ 模型在 740 万状态规模下验证参考语义。对 LangGraph 1.2.9 和 CrewAI 1.15.2 的测试显示，LangGraph 在中断时保证 exactly-once，但在崩溃时表现为 at-least-once，且会持久化无效状态；CrewAI 会重新执行已完成的方法。
Development
- First ReportResume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence LayersarXiv cs.LG
- Current Assessment主流 agent 框架（如 LangGraph、CrewAI）在持久化语义上缺乏统一契约，可能导致生产环境中不可预测的行为。这为框架提供商提供了差异化机会：率先实现并公开机器可检查的恢复语义契约，可增强开发者信任。同时，形式化验证方法在 agent 基础设施中的应用可能成为新趋势。Agent Pulse · analysis
一篇 arXiv 论文（2608.03836v1）指出，五个广泛部署的 agent 工作流框架对中断/恢复语义的实现各不相同，且没有提供机器可检查的契约。论文提出 RESUME CONTRACT，包含六个属性（前缀延续、效果 exactly-once、分叉确定性、检查点有效性、消费一次、恢复确定性）以及分叉意图和活性义务。作者用 TLA+ 模型对参考语义进行了穷举检查，在 740 万状态规模下验证，并构建了 39 格故障矩阵来分离各属性。对 LangGraph 1.2.9 的测试发现，它在中断时保证 exactly-once，但在真实 SIGKILL 崩溃后表现为 at-least-once，且会持久化无效状态；CrewAI 1.15.2 会重新执行已完成的方法。
RESUME CONTRACT 将工作流持久化语义形式化为可检查的属性，其中 consume-once 属性独立于其他六个属性，表明消费语义是独立维度。TLA+ 模型在 740 万状态规模下验证，说明形式化方法可扩展到实际规模。LangGraph 的行为差异（中断 vs 崩溃）揭示了持久化层在故障模型上的不一致，这为设计可靠 agent 框架提供了可验证的规范基础。
主流 agent 框架（如 LangGraph、CrewAI）在持久化语义上缺乏统一契约，可能导致生产环境中不可预测的行为。这为框架提供商提供了差异化机会：率先实现并公开机器可检查的恢复语义契约，可增强开发者信任。同时，形式化验证方法在 agent 基础设施中的应用可能成为新趋势。
对于依赖 agent 工作流的企业，恢复语义的不可靠可能导致重复执行副作用（如重复计费、重复发送消息），造成经济损失和合规风险。采用符合 RESUME CONTRACT 的框架可降低此类风险，提升系统可靠性，从而节省运维成本并增强客户信任。
未来，框架可能采用类似 RESUME CONTRACT 的规范，并公开其符合性测试结果。可观察的下一信号是：LangGraph 或 CrewAI 发布更新，明确修复崩溃时的 exactly-once 语义，或提供符合性测试套件。