Resume Means Resume：Agent 工作流持久化层的可机器验证一致性契约

  • 关联论文：2608.03836
  • 作者：spark
  • 更新：2026-08-07

一句话结论

论文把"agent 框架里到底什么算 resume？"这个长期被各框架以模糊文档糊弄过去的语义问题，形式化成 6 条核心性质 + 2 条附带义务的 RESUME CONTRACT，再用 TLA+ 对参考语义在 740 万状态空间上做穷尽模型检测（结果不变），并用一个 39-cell 的故障矩阵和并发场景证伪：5 个主流框架都违反自己声明的契约片段；同时给出一个 Verus 验证到行级一致的参考实现 REMIT，把那些被违反的 cell 修上。

解决什么真问题

agent 工作流框架（LangGraph、CrewAI、pydantic-graph 等）都承诺"持久化执行状态 → 可中断 → 崩溃后存活 → 从检查点继续"。但"继续"到底是什么，长期没人定义清楚：

  • 已经触发过的副作用（HTTP 调用、写文件、转账、发邮件），resume 时是重放一次、不再执行、还是条件性补跑？
  • 检查点所在的 for/while 节点，resume 时是接着上次循环跑，还是整段重跑？
  • 并发恢复（k 个进程同时认领同一个 parked interrupt），是恰好一次还是饱和到 k 次？

每家框架各答一套，对外并不公布可机器验证的契约。论文的实证章节直接把这个抽象指控做成可复现实验——而且发现 5 个广泛部署的框架里没有一个在所有维度上自洽。在工业 Agent 部署里，这种"resume 含义不明"实际上是把数据风险藏在"恢复"的承诺里。

核心方法

1. RESUME CONTRACT：六性质 + 两义务

论文把"什么样的 resume 算对的"细化为 6 条性质加 2 条义务，写成对持久化 API 的形式规约：

性质 含义（白话）
prefix continuation（前缀延续） 检查点之后的执行必须是历史上某条合法前缀的延续，不能折回到更早状态
effect exactly-once（副作用恰好一次） 标记为幂等登记过的副作用，跨 crash 也不能重放
fork determinism（分支确定性） 检查点上的并发分支必须以确定性顺序落地，否则无法复现
checkpoint validity（检查点有效性） 检查点本身必须 schema 合法、语义自洽，不能存一段当前框架读不懂的内容
consume-once（消费一次） 中断 / 事件队列里的元素被一个恢复进程消费后，别的进程必须读不到
recovery determinism（恢复确定性） 同一检查点同一剩余输入，恢复出同一后续路径

附带的 2 条义务：

  • fork-intent：分支时显式标注 fork 意图（这是"应该分流"还是"应该广播"），不能暗中分支；
  • liveness：恢复后系统在有限步内必须取得进展，不能挂在死循环。

2. TLA+ 穷尽验证 + 39-cell 故障矩阵

  • TLA+ 模型：先用 TLA+ 对"参考语义"做穷尽模型检测，状态空间 7.4 million；模型在更高边界上仍然保持不变（unrefuted），证明参考语义在更大规模下也成立。
  • 39-cell 故障矩阵：覆盖"故障 × 恢复路径"组合；两个 companion module 给出 separating models，证明 6 条性质中至少有部分彼此独立（不能合并简化）。
  • consume-once 拆分：consume-once 单独具备"独立 consumption clause"——这意味着它不是其他 5 条的推论。
  • 并发故障：k 个进程同时认领一个 parked interrupt，consume-once 在并发送达下失效——36/40 cell 饱和到 1.0，即"k 个进程恢复同一个 interrupt，gated effect 触发 k 次"，且失败跨主机传播。

3. 实证：5 个框架都违约

论文用一个LLM-free 的确定性 harness在 pinned release 上对 5 个框架逐一测：

框架 测出的违约
LangGraph 1.2.9 第二次 resume 的值被持久化但从不读取；持久化 schema 不合法状态被默默接受；真实 SIGKILL 后重放已持久化工作（"interrupt 下 exactly-once，crash 下 at-least-once"在同一 API 上共存）
CrewAI 1.15.2 已经完成且携带副作用的方法，会对照其"已写入的 claim"再执行一次
pydantic-graph 1.x 节点中段 crash 后根本无法 resume
—— 5 个框架间没有两个共享同一 conformance profile

这意味着"resume 即 resume"这个承诺在主流框架里不是事实，而是一种"看场景的近似"。

4. REMIT：参考实现 + 修复

为把违反的 cell 修回去，作者给出一个参考 sequencer REMIT，并用 Verus 验证其恢复核：

  • 验证出来的恢复核与发布可执行文件行级一致，意味着不仅逻辑对，发布出去的二进制确实是验证过的那段代码。
  • 修复 fork cell 与 validity cell：在共享 store 上加一个 opt-in gate——最早声明消费的那一个 racer 获得通过，其余在执行前被拒。这条 read-path 修复随包发布。

关键实验与数据

指标 数值 含义
TLA+ 模型检测状态数 740 万 参考语义的穷尽验证规模
TLA+ 模型可扩展性 不变于更高边界 7.4 M 之上仍保持
故障矩阵 39 cell + 2 companion modules 多维度分离验证
实证框架数 5 LangGraph 1.2.9、CrewAI 1.15.2、pydantic-graph 1.x + 另两
consume-once 并发饱和 36 / 40 cell 饱和到 1.0 即"k 个 racer 触发 k 次"在多数 cell 上成立
修复后行级一致 recovery core 与发布二进制 line-identical Verus 验证产物
论文形式 26 页，11 张表，1 张图，附补充材料 v2 修订了 fork-fault counterexample 深度 9 → 8，TLC 版本号，separating models 的归属

亮点

  1. 形式化规约 + 工程实证绑在一起：不仅给契约，还用现实框架证明"为什么这件事得做"。
  2. TLA+ 状态空间 7.4 M 不变性：这个量级在并发规约里非常硬，避免了"模型小所以对"的常见质疑。
  3. Consume-once 显式独立：很多研究含糊地合并"消费一次"和"恰好一次"，论文证明它必须独立成条。
  4. Verus 验证产物与发布二进制行级一致：把"形式化方法"从论文带入二进制分发，治理价值远大于单点算法。
  5. 故障跨主机确认：很多框架只在单机测，论文显式承认并发问题会跨主机扩散，对云上多 zone / 多 region 部署尤其要紧。

局限与风险

  • 评测仅 5 个框架（pinned release），Python 生态之外的 Java/Go/Rust 工作流框架未覆盖；其他语言栈是否同样违约，abstract 未明确。
  • REMIT 修复粒度：修复了 fork 和 validity 两个 cell，"consume-once 并发"之外的其他 cell 是否都已修齐，原文未列明细。
  • Verus 验证范围：只 cover 了 recovery core，"是不是只有 recovery core 是关键路径"仍待审计。
  • 工业落地门槛：当前补丁写在 SDK patch level，是否被各上游仓库接纳、是否回写到主分支，原文未明确。
  • scale-up 风险：7.4 M 状态空间的 model checking 对工程团队门槛不低；规约改一版就要重跑模型检测。

对工程落地的启发

  • "我支持 resume"是工程黑话：把它翻译成 RESUME CONTRACT 的 6 性质 + 2 义务，才能在选型评审里挡住"重新执行一次副作用"这类隐患。
  • consume-once 必须在共享存储里集中做：单进程本地 gate 不够；分布式 race 必须用乐观并发或 saga 风格的 read-path gate 收口。
  • 消费前先声明：opt-in gate + 早期 claim 是当下最经济的兜底，比让所有副作用都升级成 idempotency key 划算。
  • 形式化方法回归 ML 工程：用 Verus / TLA+ 把恢复语义钉在二进制层，是 Agent 走向生产必需的一步。

与同方向工作的关系

工作流持久化已经有 Temporal / Cadence 这类以"持久化工作流"立身的成熟框架；近一两年迁移到 LLM Agent 上后，Agent 框架层（LangGraph、CrewAI、pydantic-graph、Letta 等）以"图状态 + 工具调用"快速扩张，但对 resume 的语义讨论一直停留在博客层。RESUME CONTRACT 是第一份把这个语义形式化 + 系统化检测的论文，且把 TLA+/Verus 直接用于工业框架审计，和同期出现的其他形式化工作（协议、KV 缓存、checkpoint 格式）一起构成 2026 年"形式化工程"回归潮的一部分。

适合谁读

  • 自研 Agent 框架 / 工作流引擎的架构师与 SRE；
  • 用 LangGraph、CrewAI、pydantic-graph 做生产级 Agent 的工程团队（无论选哪一家都该读，因为"5 家全违约"才可怕）；
  • 对分布式系统正确性有研究兴趣的工程师，TLA+/Verus 入门级实战案例；
  • 担心"LLM Agent 在生产里偷偷重放了一次扣款"的产品 / 风控负责人。

反方 / 边界段（强制 1 段）

论文未明确：①其余 4 框架（除 LangGraph / CrewAI / pydantic-graph 外的两个）的具体违约细节；②39-cell 故障矩阵上每个 cell 的失败率或偏差分布；③REMIT 修复后剩余 cell 的回归明细；④TLA+ 在更高 scale（如 7.4 M → 70 M）的不变性证明是 empirical 还是带数学证明；⑤SDK patch 在各上游的接受状态。表中所有数值均来自 abstract；v2 修正项已注明但未在正文中逐处重复对照；正文细节与附录尚未核验。

工程落地与核查（Jay）

1. 现状：所有主流框架的 resume 都是"近似承诺"

论文实测确认了一个业界讳莫如深的事实：LangGraph 1.2.9 在 SIGKILL 后会重放已持久化的副作用（interrupt 下 exactly-once，crash 下 at-least-once 在同一 API 共存），CrewAI 1.15.2 会重新执行已完成的副作用方法，pydantic-graph 1.x 在节点中段 crash 后根本无法 resume。

实践含义：如果你在生产环境里用这些框架做涉及写操作（发邮件、转账、写文件）的 agent 流程，没有任何一个框架能向你保证"同一个 checkpoint 恢复后副作用不会重放"。这不是 bug，是文档里从来没写清楚的事。

2. 最容易踩的三个坑

坑 A：误以为"持久化 = 幂等"

LangGraph 的常见用法是把"调用外部 API"放在工具节点里，很多团队以为只要把状态持久化了、重启后继续跑就是幂等的。实际上论文发现 LangGraph 1.2.9 对"同一个 interrupt 恢复两次"，会执行两次带副作用的工具调用——持久化和幂等性是两件正交的事。

避法：把副作用调用包装成 idempotency-key 模式，每次执行前先查"这件事我做过没有"，而不是依赖框架的 resume 语义。

坑 B：consume-once 在并发下完全失效

论文发现 36/40 个并发 cell 的 consume-once 饱和到 1.0（k 个 racer → k 次 effect）。在多进程 / 多 zone 部署下，如果你的 interrupt 队列（如 Kafka 消息、Redis stream）被多个 worker 节点共享，一个进程读走消息后，其他进程仍可能在同一时间窗口内拿到同一消息并触发 effect。

避法：用"声明式消费"：在共享存储（不能用本地内存）上做 claim(race_id, interrupt_id) 乐观锁，最早 claim 的 racer 才有执行权；这不是框架级配置，需要业务层自己实现（或等 REMIT 的 patch 合入上游）。

坑 C：checkpoint 有效性只在 crash 后才暴露

pydantic-graph 1.x 存了一个不合法的 schema 状态，框架并不会报错，只是默默接受，等到 crash 恢复时才发现自己读不懂。这是一个"欠的债在恢复时才还"的坑。

避法：在每次 checkpoint 写入后，加一个验证读：立即打开同一 checkpoint 文件并尝试加载，失败则报警。这比依赖框架的合法性保证便宜得多。

3. 如何把 RESUME CONTRACT 用于选型和评审

在实际工程中，不需要跑完 39-cell 故障矩阵，可以用下面这个快速检查清单评估一个框架的 resume 质量：

检查项 操作
前缀延续 在 for 循环中间打断点，resume 后确认是从循环当前位置继续，而不是整段重跑
副作用幂等 在工具节点里加一个"写一条带 UUID 的日志"，crash 后 resume，看日志里有没有重复 UUID
consume-once 用两个进程同时认领同一 interrupt，看 effect 是否触发两次
checkpoint 有效性 手动写一个非法 checkpoint 文件，框架是否能检测并报错而非静默接受

4. REMIT 的可操作性评估

REMIT 提供了修复 fork 和 validity 两个 cell 的参考实现，核心思路是"共享 store 上的 opt-in gate + 最早 claim 通过"。工程上可以这样落地：

# 最简化的 claim-gate 伪代码
def claim_and_execute(store, interrupt_id, racer_id, effect_fn):
    acquired = store.compare_and_set(
        key=f"interrupt:{interrupt_id}:claimant",
        expected=None,
        new_value=racer_id
    )
    if not acquired:
        existing = store.get(f"interrupt:{interrupt_id}:claimant")
        raise DuplicateClaimError(f"Already claimed by {existing}")
    try:
        return effect_fn()
    finally:
        store.set(f"interrupt:{interrupt_id}:status", "consumed")

注意这个方案要求 store 本身是原子的（Redis CAS、CockroachDB 事务等），不能用本地内存做 gate。生产部署建议用 Redis GETSET 或 etcd 的事务 API。

5. TLA+ 模型检测的工程门槛

7.4 M 状态空间听起来吓人，但 TLA+ model checking 的工程门槛主要在规约写作而不是计算资源。实践中：

  • TLC model checker 可以在一台 16 核机器上跑完 7.4 M 状态检测（论文未披露具体耗时，但同量级案例通常在分钟到小时级）；
  • 真正门槛是规约本身的可读性：让团队其他工程师理解和维护一份 TLA+ 规约，需要内部有至少一个懂 TLA+ 的人；
  • 建议路径：先用 PlusCal 写算法级规约（比纯 TLA+ 易读），验证后再翻译成 TLA+ 跑 model check；这样工程团队可以先通过 PlusCal 版本理解语义，再决定是否投入 TLA+ 生产。

核查注记

  • 论文数据（740 万状态空间、39-cell、5 框架实测结果）均来自 abstract，正文表格和附录未逐项核验，建议在引用具体数字前对照原文；
  • 表中"pydantic-graph 1.x + 另两框架"的违约细节原文未在 abstract 中给出，解读中"另两"为 abstract 原文表述；
  • v2 修订项（fork-fault counterexample 深度 9→8、TLC 版本号）来自 abstract 注释，尚未对照正文核实。