恢复即恢复：工作流持久化层中检查点、中断与恢复语义的机器可验证一致性契约 Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
提出六属性恢复契约，用TLA+与确定性测试揭示主流Agent框架在崩溃与中断恢复时的语义缺陷
前置知识
TLA+ 与 TLC 模型检验
TLA+ 是 Lamport 提出的形式规约语言，TLC 是对应的显式状态模型检验器，可对有限配置做穷举的广度优先遍历，验证状态不变式是否在所有可达状态上成立，并为违例生成最小深度的反例。本文用它对 RESUME CONTRACT 的参考语义与六个故障变体做穷尽检查。
本文的核心理论保证——六条性质在参考模型上无错误、每条故障触发深度 4–6 的反例——全部依赖 TLC 的穷举结果，理解边界配置（N=3 任务、IP=2、|V|=2）才能判断结论何时适用、何时是边界相对的。
Exactly-once / At-least-once 语义
Exactly-once 指一个效应（如扣款、发消息）在任何中断、崩溃、恢复序列中至多触发一次；At-least-once 允许重复触发，要求上层用幂等键去重。本文明确区分：EO 是状态管理保证（不约束消息投递），CO 是其在中断门处的特例。
论文的核心差异就是各框架在「已完成工作恢复时是否重执行」上分属两个阵营且常言行不一，读不懂这两个语义就无法理解 LangGraph 与 LlamaIndex 在 EO 列上 ✓/D 的差别。
Verus 与可验证可执行函数
Verus 是用线性 ghost 类型验证 Rust 程序的工具。本文把 REMIT 恢复决策核心写成 Verus 目标，使「证明过的函数」与「出货的可执行函数」逐行相同，并在 CI 中门控——这是介于「证明了模型」与「端到端精化」之间的中间强度。
理解 Table 10 的七级证据梯子必须区分「模型级证明」「可执行函数级证明」「复合包未证明」，否则会误以为整包被端到端验证——而作者明确否认了这一点。
隔离异常（Lost Update）
Lost update 是数据库隔离文献中的经典异常：两并发事务都读同一行、各自基于旧值计算并写回，后写者覆盖前写者。本文把跨进程 CO 违规定位为「中断消费是没人做成原子的 read–modify–write」，引用 ANSI 隔离级别批判 [19] 与 Adya 异常定义 [93]。
Probe 159 的跨进程双消费（10/10 重复）就是这一异常在恢复平面上的再现，理解它能解释为什么行级锁与 MVCC 都关不上窗口——问题在于 resume 路径自己没做 CAS。
研究动机
新一代面向 LLM agent 的工作流框架（LangGraph、LlamaIndex Workflows、CrewAI、pydantic-graph、AutoGen）都把持久化恢复机制交给开发者，用于人工审批、崩溃、抢占后继续运行。当这些机制把关支付、消息、文件写入等非幂等效应时，「继续」就成了正确性问题：哪些已完成效应可能再次触发、同一中断被以不同值回答两次时持久化什么、恢复决策是否是持久状态的纯函数。问题在于这些框架既无机器可检查契约，文档化碎片语义还互相矛盾：CrewAI 1.15.2 声称「resume without re-running completed work」[1]，LlamaIndex Workflows 2.22.2 要求用户把已完成工作「make safe to re-execute」[2]，LangGraph 1.2.9 用 @task 记忆化跨恢复结果。三种互不相容答案，作者实测发现其中两个连自己声称的语义都不满足。开发者移植带副作用工作流时无法通过任何类型或文档判断自己处在哪种规约下，论文复现的 GitHub issue 就是这种空白变成的真实事故。
本文的目标是本文要给 agent 框架的恢复平面建立一层网络协议和文件系统几十年前就有、但 agent 框架缺失的基础设施：一个显式的、机器可验证的契约，一个被模型检验的参考语义，以及一套跨框架的一致性测试套件。具体包括：(1) 定义一组跨不同执行模型通用的属性——只陈述在检查点、中断、恢复命令、状态查询这一共享接口之上，使一个文档化弱规约的框架只被记录为「偏离（D）」而非「缺陷」；(2) 用 TLA+ 把参考语义和六类观察到的违规机制都建出来，让 TLC 穷举发现每个故障的真实违规足迹而非人为规定；(3) 用一个确定性、无 LLM 调用、无定时窗口的测试 harness 在固定版本上测量五个主流框架；(4) 给出一个带 Verus 验证恢复核心、并在出货包中修复实测违规的参考实现 REMIT。整套契约要让一个 conformance suite 成为 CI job，让「resume」真的意味着 resume。
与已有工作不同的是，已有的强相关工作都和本文正交而不重叠：在框架 API 之下，Crab [4] 做的是 OS 级沙箱检查点/恢复（文件系统、进程、microVM），并在恢复时合成缓存的 LLM 响应避免重放；在 API 之上，DART [5] 判定一次机械可能的回滚在语义上是否可接受。两者都把框架恢复原语本身的语义当作给定，而本文问的是更前一层的问题——这个原语本身守不守约？这正是 GitHub issue 居住的层。横向的一致性检查工作（LogicHunter [7]）搜 bug，本文定义 bug 违反的契约并测一致性；同意完整性工作 [6] 把审批绑定到动作内容，FD/CO 治理审批的生命周期轴。据作者所知，没有先前工作把显式恢复契约、机器检查模型、跨框架一致性测量三者合在一起。
核心方法
整体思路是把网络协议、文件系统几十年沉淀的「显式契约 + 机器检查模型 + 一致性套件」三件套搬到 agent 框架的恢复平面。技术路线分四步：第一步抽象出一个最小非平凡的恢复平面——一次运行按序执行任务 1..N，每个任务带一个非幂等外部效应 $e_t$，其中一个任务 IP 是中断门控的，只有消费了恢复值 $v\in V$ 后效应才触发；完成任务就向持久日志追加 $\langle t, valid\rangle$ 并把持久前沿 $F$ 推到 $\max(F,t)$；崩溃擦除易失状态，恢复选择一个续点作为持久日志的函数。第二步在这抽象接口上陈述六条性质（PC/EO/FD/CV/CO/RD）外加一个协议义务 FI 和一个活性义务。第三步把 Definition 1 和性质 1–6 形式化成一个 251 行的 TLA+ 模块，配六个布尔故障开关，每个开关转录一种部署框架中观察到的违规机制。第四步用一个纯 Python 协议序列的 harness 在五个框架的固定版本上执行探针，崩溃用异常注入或 SIGKILL 屏障同步，效应用进程内计数器和外置 SQLite 账本交叉校验。
核心创新点和已有方法的本质区别有三：(1) 把六条性质陈述在一个抽象的「恢复平面」接口上，而不是绑定到某个具体框架的图步、事件队列、flow 监听器——这让一个契约就能跨不同执行模型适用，且判定只依赖调用者可观察的表面。(2) Proposition 1（无判别器时 FD 与 CO 不可同时满足）是一个不可判定性论证：两条执行在持久状态、线路轨迹、本地调度、环境输入上完全相同，只在线路无法承载的调用者意图上不同；任何确定性响应者对两条都给出同一行为，必违其一；随机响应者也至少在一种意图上以概率 $\ge 1/2$ 出错。这把 FI 协议义务的必要性变成了定理。(3) 用「意图索引」$\iota(w)\in\{\text{FORK},\text{RETRY}\}$ 重新表述 FD 和 CO，使判别器存在时 $\iota$ 可从线路恢复，判别器不存在时意图索引版本严格更强——这正是不可判定性是「信息性的而非实现缺陷」的来源。
方法步骤详情
方法分四阶段。(1) 形式化契约：Definition 1 给出恢复平面（任务按序执行、每任务带非幂等效应 $e_t$、任务 IP 中断门控、消费恢复值 $v\in V$ 后效应才触发），陈述性质 1–6（PC/EO/FD/CV/CO/RD）与 FI 协议义务，Proposition 1 证明无判别器时 FD 与 CO 不可同时满足。(2) TLA+ 机器检查：251 行模块配六故障开关，TLC 在参考配置 87/59 distinct 上六不变式无错误、每单故障深度 4–6 违反目标，R8 放大到 $7.4\times10^6$ distinct 仍无错误；39 单元矩阵得每故障完整违规足迹。(3) 确定性 harness：47 探针分 11 campaign，崩溃用异常注入或 SIGKILL 屏障同步，效应用进程内计数器加独立 SQLite 账本交叉校验。(4) REMIT 修复：在 BaseCheckpointSaver 接口介入，状态是只追加效应账本加按线程全序定序器，恢复核心用 Verus 验证为可执行函数并与出货代码逐行相同。
技术新颖性
技术新颖性四点。(1) 契约在 agent 框架层是新的——Table 11 对比 Durable Functions/Temporal/DBOS，这些引擎要么自拥序列化（CV 无对应）、要么把 EO 委托给调用者幂等键（Temporal activities 是 at-least-once），agent 框架选了更轻的快照式持久化却没继承规约，本文把已有义务在缺失它的接口上重述。(2) 部分独立性是机器检查的——展览完全穷举的有限 witness 而非采样证明非蕴涵，CO-c 用 lost-update 模型 R11 在 127/95 状态、深度 5 违反。(3) 跨进程 CO 失败的剂量–响应测出窗口宽度精确追踪门控节点执行时间（500 ms 门下 0 ms 抖动饱和 1.0、100 ms 跌到 0.40）。(4) 125/134 与 165/v0.1.2 两对干预实验构成「机制是因」证据——写路径绑定分叉键无法修复 FD，读路径 get_tuple 处剥除 __resume__ 待写则修复 #6663，定位了「循环先读再决策最后报告 saver」架构下唯一可执行介入点。
实验结果
五框架被测，无两框架共享一致性画像，违规集中在 FD/CO/CV 授权处。**LangGraph 1.2.9** 三后端全违反 FD(#6663)与 CV(#6491)，EO 按路径分裂——中断 ✓、崩溃 ✗（SIGKILL 后已完成任务重执行，计数 1→2）。**CrewAI 1.15.2** 违反 exactly-once 声明：s2 抛异常后重执行 s1，状态计数 12 而预测 11。其余框架各异：LlamaIndex Workflows 的 wait_for_event 习语按设计重执行前缀（标 D），pydantic-graph 1.107.1 安全性质全过但节点内 SIGKILL 后拒绝恢复持久文件（活性义务反例），AutoGen 0.7.5 唯一对篡改状态大声拒绝。**跨进程 CO 失败**（探针 159/168）：多进程共享 saver 各发 resume，门控效应 10/10 重复，k=16 零抖动 {16:10}，40 单元 36 个饱和 1.0。**REMIT** 修复叉分/CV/跨进程（v0.1.2 门 {1:10}），开销容器内 5%、主机 ±1.7%。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 参考语义模型检验（R0） | TLC 状态数 / 错误数 | 87 生成 / 59 distinct，0 错误 | 无（参考自身） | 在最小可证伪配置下六条性质全部成立 |
| 放大边界模型检验（R8） | TLC 状态数 / 错误数 | $1.47\times10^7$ 生成 / $7.4\times10^6$ distinct，深度 24，0 错误 | R0 的 87/59 | 状态空间大四个数量级，干净单元仍干净，反例只是变深（叉从 5 到 9，双消费从 6 到 13） |
| 单故障反例深度 | counterexample 深度（状态数） | R1 Replay=4、R2 ForkIgnore=5、R3 InvalidPersist=5、R4 NondetRecovery=4、R5 DoubleConsume=6、R9 PrefixReplay=4 | 无 | 每个观察到的违规机制都有 4–6 步最小反例 |
| LangGraph 崩溃路径 EO | 门控效应计数（崩溃前→恢复后） | 1→2（探针 133/137 三点 SIGKILL 矩阵，字节稳定） | exactly-once 预测 1→1 | REMIT 修复后为 1→1 |
| CrewAI CheckpointConfig 恢复 | 状态计数 / s1 效应计数 | 12 / 2（实测） | exactly-once 预测 11 / 1 | 证明文档声称与实测不符，定为 ✗ |
| 跨进程 CO 失败（探针 159/168） | 饱和度（门控触发/k） | k=16 零抖动 {16:10}，40 单元 36 个饱和 1.0，最低 0.933 | exactly-once 预测 1/k | REMIT v0.1.2 opt-in 门修复为 {1:10}（两后端） |
| REMIT 介入开销（探针 139） | 中断协议 p50 延迟相对 stock | 容器内 5% 以内，开发者主机 ±1.7%（−0.34% 到 +0.38%） | stock SqliteSaver 19.4/4.2 ms（容器）、58.7/20.5 ms（主机） | 在两种延迟量级上开销都不可测 |
| 并发压力（探针 157，k=64） | 端到端协议每协议 exactly-once | 6400 次协议执行，每协议 exactly-once 全成立 | stock 在并发下重复 | 吞吐在 k 上平坦、中位延迟近线性，受 GIL 限不是后端限 |
| DBOS 嵌入式引擎同负载（探针 147） | answer-sent → gated-effect-durable p50 | 33.8 ms（容器）/ 92.5 ms（主机），全部被测单元一致 | stock SqliteSaver 6.7/32.0 ms | 语义全过但门答案延迟慢 2.9–5.0×，定价「整体采用持久化执行模型」这条替代路径 |
| 实时复现矩阵（探针 148） | fork 违规 / 中断-审批违规 / 会话恢复违规 | Claude 两模型叉分 40/40（80/80 总，95% Wilson [0.91,1.0]）；gpt 两模型会话恢复 0/40 | 无 | 240 次实时运行、0 harness 错误，证明 LLM 流量既不掩盖也不制造确定性判定 |
局限与改进
作者明确承认三层局限。**形式层**：所有分离论证是边界相对的——在所述常量（如 R0 的 87/59、R8 的 $7.4\times10^6$）上穷举，超出最大边界则沉默；TLAPS 才能把「完全枚举的有限 witness」升级为参数化家族，作者已为相邻工作 [96] 履行部分 TLAPS 义务但本文未完成；属性集最小性、完备性、充分性无定理保证，候选第七条（跨版本迁移有效性、效应可见性排序、丢弃 resume 的大声/小声处置）只作为范围排除列出。**测量层**：五个框架在被测路径上的判定不能推广到生态系统流行率；CO 在 LangGraph 的 ✓ 只对顺序投递成立、跨进程组合失败；PC 的 ✓ 只证其必要推论（状态等价、效应记录完整）而非性质本身——这种不对称是真实、单向的。**机制层**：LangGraphFork.tla 是专家建立的抽象而非机械提取；效应预言机是进程内计数器和外置 SQLite 账本不是真实支付 API；剂量–响应臂只在开发者主机上跑、后端列共享抖动种子是配对而非独立证据、k>16 与更宽抖动未测；跨主机分布只在一种两主机拓扑上测，分区未包含。
独立分析的弱点
独立分析五点。(1) **契约仅陈述线性链，DAG 并发与多检查点 fan-in 刻画不足**——并发 fan-out 在一个 superstep（探针 141）测过，更深嵌套与多检查点竞态是 future work。改进：把 CO-c lost-update 模型扩展为多 racer 谱，引入 Adya 异常 [93] 与 Elle [94] 客户端可观察历史推断。(2) **PC 满足不可判定，只能证必要推论**——harness 观察状态等价与效应记录完整但无法判 provenance。改进：要求框架暴露 provenance 元数据。(3) **REMIT 缺 Verus 模型到编译核心的机械精化关系**（rung 8 缺失）。改进：用 IronFleet/Perennial 精化补。(4) **跨进程门只对同步 saver 单共享 store 序列化**，分区未测。改进：用共识协议把消费记录放进共享 store。(5) **门默认 opt-in**——get_tuple 无 read-intent 判别器。改进：接口加 read-intent 判别器。
未来方向
作者提出方向：(1) TLAPS 精化把边界相对的分离升级为参数化家族，把复合状态机归纳不变式 IndCheck.tla（8610/450926/97800 个不变式状态、三组常量下 TLC 检查无错误）变成机械证明；(2) 把 AG2、OpenAI Agents SDK、Claude Agent SDK、Agno 纳入完整矩阵；(3) 跨版本检查点迁移有效性、效应可见性排序、丢弃 resume 处置三个候选第七属性；(4) 更深并发嵌套、多检查点 fan-in 竞态与跨主机分区拓扑刻画。基于成果可延伸：(5) 推广到 SoundGate [17] 治理的另一半生命周期（stop 是否抑制外部可见效应），合为完整控制平面契约；(6) 用 ACRFence [21] 对抗视角把 EO/CO 从正确性属性升级为安全属性；(7) 把 REMIT 的 read-path 介入模式推广到任何「先读、再决策、最后报告 saver」的执行循环架构；(8) 与 DBOS/Temporal 做生产规模正面比较。
复现评估
复现评估优秀。**(1) 工件完备**：提供 conformance 探针、TLA+ 模型、TLC 配置与 REMIT 设计，配单命令 reproduce.sh 重导每个标题数字；REMIT 包源发表前私有、评审可索取。**(2) 可分发**：REMIT 已在 PyPI 发布，v0.1.2 是所评估精确构建。**(3) 确定性**：harness 不含 LLM、不含定时窗口、不含随机性，判定只随包版本变化、版本被 pin；每探针输出 JSON 并带 manifest。**(4) 跨环境复现**：两独立主机上每个 pilot 判定逐比特复现；持久后端探针在第三个独立容器执行、与 InMemorySaver 路径判定一致；其余探针族、TLC 矩阵、Rust/PyO3 套件、引擎基线全部跨容器与主机复现、零分歧。**(5) 算力门槛低**：参考模型 TLC 数秒级、R8 在 $7.4\times10^6$ 状态量级仍可单机小时级完成。**障碍**：实时单元需 API key；LangGraphFork.tla 是专家建立；端到端精化未声称。
论文图表
纵向把 DART（在原语之上判定回滚可采纳性）置于顶部，本文 RESUME CONTRACT（PC/EO/FD/CV/CO/RD 在框架恢复 API 之上）居中，Crab（OS 级沙箱检查点/恢复）置于底部。两侧注释说明相邻系统都假设框架恢复原语是健全的，而本文指定并测试这一假设。
用一张图厘清本文与两个最强相关工作（Crab、DART）的层关系——两者都把原语语义当给定，本文问原语本身守不守约——这对理解「为什么不能直接用 Crab 或 DART 解决问题」至关重要。
TLA+ 代码片段，展示了 EffectExactlyOnce（\A t : effects[t] <= 1）、ForkDeterminism（分叉结果等于 f(分叉值)）、CheckpointValidity（所有 ckpts[k].valid）、RecoveryDeterminism（相同持久前沿⇒相同决策）四条不变式的逐字形式。
把抽象性质落到可读的一行式代码，让读者看到不变式本身极简（证明负担在六个动作的每个交错里），也为 Table 2/3 的模型检验结果提供可对照的规约文本。
R0 参考配置 87/59 状态、所有六不变式无错误；R1–R5 与 R9 在单故障开关下违反目标不变式，反例深度 4–6；R6 在弱公平下验证活性无错误；LGF-A（as implemented）违反 FD 深度 3、LGF-B（fork-keyed）FD+幂等无错误；R8 放大到 14.7M/7.4M distinct 状态、深度 24 仍无错误；R8-F 多 worker 的 ForkIgnore 仍违反深度 8。
这是机器检查层的核心证据——参考语义在最小与放大两种边界上都通过所有性质，每个单故障都触发可复现反例，LGF-A 与 LGF-B 对比直接证明「叉违规是写路径幂等设计的影子」。