恢复即恢复：工作流持久化层检查点与恢复语义的机器验证契约
原标题：Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
AI 摘要
该论文提出RESUME CONTRACT，定义了工作流持久化层中检查点、中断和恢复语义的六项属性，并通过TLA+模型和确定性测试框架对五个主流代理工作流框架进行验证。结果显示LangGraph、CrewAI等框架在恢复语义上存在违反契约的行为，如重复执行已持久化的效果。论文还提出REMIT参考实现，其Verus验证的恢复核心与发布代码一致，修复了分叉和有效性缺陷。
正文节选
Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers Abstract 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 stat