レジュメは再開を意味する：ワークフロー永続化レイヤにおけるチェックポイント、割り込み、再開セマンティクスのための機械検証済み適合契約

要旨

実行状態を永続化することで、実行が中断され、クラッシュを生き延びて継続できるようにするフレームワークは、すでに発火したエフェクトに対して再開が何を意味するのかを決定しなければならない。広く導入されている5つのエージェントワークフローフレームワークはそれぞれ異なる答えを返すが、機械検証可能な契約を公開しているものはなく、その挙動は、彼らが明示している断片さえも侵害している。RESUME CONTRACT（再開契約）は、永続化APIに関する6つの性質（プレフィックス継続（prefix continuation）、エフェクトのexactly-once（effect exactly-once）、フォーク決定性（fork determinism）、チェックポイント妥当性（checkpoint validity）、consume-once（一度だけの消費）、回復決定性（recovery determinism））に加えて、フォーク意図（fork-intent）と活性（liveness）の義務を定める。TLA+モデルは、モデルを変更することなく、スケールアップした境界（740万状態）でも参照意味論を網羅的に検証する。39個のセルからなるフォールト行列は、独立性が要求する分離モデルを導出し、consume-onceは分離される。その消費条項は、他の6つすべてから独立している。決定論的でLLMを用いないハーネスが、固定されたリリースにおいてそれらを測定する。LangGraph 1.2.9は、2つ目の再開値を永続的に記録するが、その値を決して参照せず、スキーマに適合しない状態を黙って永続化し、実際のSIGKILL後に、永続化済みの作業を再実行する。つまり、単一のAPI上で、割り込みをまたぐ場合にはexactly-once、クラッシュをまたぐ場合にはat-least-onceとなる。CrewAI 1.15.2は、文書化された主張に反して、完了したエフェクトを伴うメソッドを再実行する。pydantic-graph 1.xは、ノード実行途中のクラッシュ後には再開できない。調査したフレームワークのうち、どの2つも適合プロファイルを共有しない。consume-onceは逐次的には成立するが、並行配送の下では失敗する。k個のプロセスが1つの待機中の割り込みを再開すると、ゲートされたエフェクトがk回発火し、40セル中36セルで飽和度1.0となり、その失敗はホストをまたぐ。REMITは、Verus検証済みのリカバリ中核部が製品版実行可能ファイルと行単位で同一である参照シーケンサであり、フォークセルと妥当性セルを修復する。プロセス間セルは読み出し経路で修復され、その修復は製品に含まれる。オプトインゲートが共有ストア内での消費を主張し、1つの競合プロセスにのみサービスを提供し、残りを、いずれのノードが実行するよりも前に拒否する。

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.