Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
Sajjad Khan
cs.LG, cs.DC, cs.LO, cs.SE
2026-08-04
用 TLA+ 形式化加一个不调 LLM 的确定性 harness 检验五大 Agent 框架的断点恢复语义,无一兑现自己写的承诺:LangGraph 会忽略第二次 resume、并在崩溃后重跑已完成的副作用。
LangGraph、CrewAI、LlamaIndex Workflows 这些 agent 框架都内置了一个持久化层:把图的执行进度存下来,好让运行可以为了人工审批暂停、崩溃后恢复、抢占后继续。这个承诺本身很老,新的是它现在被交给了一群用 LLM 做代理、把付款、发消息、写文件这些不可逆操作挡在 checkpoint 后面的开发者。
「继续」到底意味着什么,没有一个框架说得清。同一个中断被用不同值回答两次时,哪些已完成的效果会重跑?这五个框架给出了互不兼容的答案:CrewAI 的文档声称恢复「不会重跑已完成的工作」,LlamaIndex 的文档让用户「把前面已完成的工作做成可安全重跑的」,LangGraph 则跨 resume 记忆已完成的 @task 结果。三套框架,三个互相打架的答案。作者实测下来,其中两个连自己声称的语义都达不到。
作者把这种状况叫「不自洽」(incoherence):不是没人写过语义,而是写过的彼此打架,甚至自己打自己。
作者没有比谁的框架更好,先立一条机器可查的契约。RESUME CONTRACT 在持久化 API 上定义了六条性质:
外加第七条 FI(fork 意图可表达):分支判别符必须在协议线上能表达。CO 是六条里唯一会分裂的,它的消费条款与其余六条都独立,效果条款则是 EO 的定义性限制。
契约分两层机器检验。第一层是 TLA+ 模型 ResumeContract.tla(251 行),用六个故障开关注入已部署框架里观察到的故障机制,再由 TLC 穷举检查。参考配置 R0 在 87 生成/59 个不同状态下六条不变式全成立;放大到 R8(10 个任务、4 个 fork 值、5 次 resume、4 次崩溃)的 740 万个不同状态、深度 24,判定不变。39 格单故障矩阵给出独立性所需的分隔模型(Proposition 2)。
第二层是一个不调任何 LLM 的确定性 harness:纯 Python 协议序列直接打框架的持久化 API,没有 LLM 调用、没有靠时间窗的竞态;崩溃用异常矩阵加带文件系统屏障的 SIGKILL(probe 133)实现。效果计数用进程内计数器,在持久化后端的探测里再和磁盘上的 SQLite 外部账本交叉核对。账本本身就是那个不可逆副作用,所以它不会多算,只会少算,每个报出来的重复都是下界。
矩阵的结论很硬:没有任何两个被测框架拥有相同的合规画像。
| 框架 | 性质 | 实测行为 |
| LangGraph 1.2.9 | FD(#6663) | 持久化记下第二次 resume 的值却从不读它,resume(False) 返回的还是第一次的值 1;跨 5 个版本、3 个后端(含在线 PostgreSQL)复现 40/40 |
| LangGraph 1.2.9 | CV(#6491 类) | schema 不合法的状态被静默存下,1.2.9 上不再报错,线程仍可读但带脏值 |
| LangGraph 1.2.9 | EO | 同一 API 上,跨中断是 exactly-once、跨崩溃却退化成 at-least-once |
| CrewAI 1.15.2 | EO/PC | checkpoint 恢复时重跑已完成的带副作用方法,违反自己「不重跑已完成工作」的文档 |
| LlamaIndex Workflows 2.22.2 | EO | 文档明确承认 at-least-once 前缀重放 |
| pydantic-graph 1.107.1 | PC | 节点中途崩溃后无法 resume,恢复入口被绕过 |
| AutoGen AgentChat 0.7.5 | CV | 被测框架里唯一对篡改状态大声报错拒绝的 |
并发是 consume-once 唯一扛不住的场景。k 个进程同时 resume 一个挂起的中断,被门控的效果就触发 k 次;40 个格子里 36 个饱和度(saturation)为 1.0,两个持久化后端都没低于 0.933,两个 racer 分处两台机器时 10/10 次重复全部重复触发。kill-point 扫描(probe 160)进一步显示,每一个未完成的持久化边界都允许已完成的副作用被重跑。一个小但有力的旁证:LangGraph 的 #7361、#6792 两个行为作为 1.1.x 回归上线、又在 1.2.9 里修掉,说明没有契约时语义连同一个框架内都会漂移。
作者给了参考实现 REMIT,插在所有框架都要经过的 checkpointer 接口上,由 Rust 核心、PyO3 绑定和 LangGraph shim 组成,恢复决策核心用 Verus 证明且与发布版逐行一致(已上 PyPI,v0.1.2)。它把六条性质映射成本地不变式(EO/CO 对应账本唯一性、PC 对应前沿单调、FD 对应按 ⟨checkpointId, resumeIndex⟩ 分支键、CV 对应写入校验、RD 对应序列化器全序)。实测里它修掉了三个格:校验型 saver 把 LangGraph 的静默持久化变成大声报错(probe 123,从 ✗ 到 ✓);fork 修复不在写路径、在读路径,重写 gettuple 剥掉记下的 resume 挂起写、让本次 resume 的值被读到,修掉 #6663(probe 134);并发的 consume-once 由一个 opt-in 的共享存储门控修掉,只放一个 racer 进、其余拒绝,两个后端都是 {1:10}。开销在容器内不到 stock 的 5%,开发机上 ±1.7% 量级。
这五件事正是 AI 工程师当下在 LangGraph、CrewAI 上做的:把工具调用、付款、发消息挡在人工审批或崩溃恢复后面。这篇的提醒很具体:你依赖的那层「能恢复」的承诺,很多时候既没定义清楚,又会在最坏情况下静默重跑或静默存脏数据。后果是重复扣款、重复发消息、状态被损坏还查不出来。
对从业者,有三样可以直接拿走。第一,这六条性质本身就是一张 checklist,审自己用的框架时可以逐条问。第二,那个不调 LLM、不靠竞态的 harness 说明这些 bug 能脱离模型、脱离时间窗确定性复现,放进 CI 就能查。第三,REMIT 给了一个能接入 checkpointer 接口的参考实现。
诚实地说,这是基础设施正确性研究,不是模型能力进展。它不会让你的 agent 更聪明,但能把「可恢复」从营销话术变成可检验的属性。
作者对能证明什么极其克制,正文专门列了「声称了什么、没声称什么」。明确没声称的包括:这组性质不宣称最小、完备或充分;没给出任何违规的流行率;被测的五个框架不代表整个生态;一个框架只在被测的性质上算违规。REMIT 的验证也只到恢复决策核心:Verus 证明的是那个核心函数,它与发布版二进制逐行一致,但没有端到端的精化(refinement)证明,组合包和编译产物都不在证明范围内。
读下来还有两点存疑。所有结论都是「在被探查的路径上」成立,作者自己也说对没测的性质不作判断,而 agent 工作流真实部署里的状态空间比这套确定性协议覆盖的要大,网络、多 worker、共享存储延迟带来的竞态可能比 40 格矩阵更复杂。另外,consume-once 的并发失败虽被实测并修复,但修复是「读路径上 opt-in 的共享存储门控」,等于在框架之上又加了一层分布式锁语义,它长期的可维护性、以及它自己会不会引入新故障,论文没有展开。