恢復即恢復：工作流持久化層中檢查點、中斷與恢復語義的機器檢查符合性契約

摘要

一個框架若要持久化執行狀態，使運行可以中斷、在崩潰後存活並繼續，就必須決定「恢復」對已觸發效應意味著什麼。五個廣泛部署的代理工作流程框架對此給出了不同答案，但沒有一個暴露可機器檢查的契約，且其行為甚至違反了她們所陳述的片段。「恢復契約」規定了持久化 API 上的六個屬性（前綴延續、效應恰好一次、分叉確定性、檢查點有效性、消費一次、恢復確定性），外加分叉意圖與活性義務。一個 TLA+ 模型窮盡檢查了參考語義，在擴展後的邊界（740 萬個狀態）下保持不變；一個 39 格的故障矩陣產生了獨立性所需的分離模型，而消費一次條款被獨立出來，其消費子句與其餘六者皆無關。一個確定性、無 LLM 的測試工具在固定版本上對這些框架進行測量。LangGraph 1.2.9 持久記錄了第二個恢復值但從不查詢它，靜默持久化 schema 無效的狀態，並在真實 SIGKILL 後重新執行已持久記錄的工作：在同一個 API 上，中斷時恰好一次，崩潰時至少一次。CrewAI 1.15.2 違背其書面聲明，重新執行已完成的有效應方法；pydantic-graph 1.x 在節點中途崩潰後無法恢復；沒有任何兩個受測框架共享相同的一致性配置。消費一次在順序執行下成立，但在併發傳遞下失敗：k 個進程恢復一個暫停的中斷，會觸發門控效應 k 次，40 格中 36 格的飽和度為 1.0，且該失敗跨越主機。REMIT 是一個參考序列器，其經 Verus 驗證的恢復核心與發布的可執行檔逐行相同，修復了分叉與有效性格子。跨進程格在讀取路徑上被修復，且該修復已發布：一個選擇加入的閘門在共享儲存中宣告消費，在任一節點執行前服務一個競爭者並拒絕其餘。

English

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 states six properties over the persistence API (prefix continuation, effect exactly-once, fork determinism, checkpoint validity, consume-once, recovery determinism), plus fork-intent and liveness obligations. A TLA+ model checks a reference semantics exhaustively, unchanged at scaled bounds (7.4 million states); a 39-cell fault matrix yields the separating models independence requires, and consume-once splits, its consumption clause independent of all six others. A deterministic, LLM-free harness measures them at pinned releases. LangGraph 1.2.9 durably records a second resume value and never consults it, persists schema-invalid state silently, and re-executes durably recorded work after a real SIGKILL: exactly-once across interrupts, at-least-once across crashes, on one API. CrewAI 1.15.2 re-executes completed effect-bearing methods against its written claim; pydantic-graph 1.x cannot resume after a mid-node crash; no two probed frameworks share a conformance profile. Consume-once holds sequentially and fails under concurrent delivery: k processes resuming one parked interrupt fire the gated effect k times, saturation 1.0 in 36 of 40 cells, and the failure crosses hosts. REMIT, a reference sequencer whose Verus-verified recovery core is line-identical to the shipped executable, repairs the fork and validity cells. The cross-process cell is repaired at the read path, and that repair ships: an opt-in gate claims consumption in the shared store, serving one racer and refusing the rest before any node executes.