재개는 재개를 의미한다: 워크플로우 영속성 계층에서 체크포인트, 인터럽트, 재개 의미론을 위한 기계 검증 적합성 계약

초록

실행 상태를 영속화하여 실행이 중단되거나 충돌을 겪은 뒤에도 계속될 수 있도록 하는 프레임워크는, 이미 발생한 효과에 대해 재개(resume)가 무엇을 의미하는지 결정해야 한다. 널리 배포된 다섯 가지 에이전트 워크플로 프레임워크는 서로 다르게 답하며, 그 어느 것도 기계적으로 검증 가능한 계약을 제공하지 않고, 실제 동작은 이들이 명시한 일부 조항조차 위반한다. RESUME 계약은 영속화 API에 대한 여섯 가지 속성(접두사 연속성, 효과 정확히 한 번, 포크 결정성, 체크포인트 유효성, 소비-한 번, 복구 결정성)과 함께 포크 의도 및 생존성 의무를 규정한다. TLA+ 모델은 참조 의미론을 확장된 경계(740만 상태)에서도 변경 없이 전수적으로 검사한다. 39개 셀 오류 행렬은 독립성을 입증하는 데 필요한 분리 모델들을 제공하며, 소비-한 번은 분리되는데, 그 소비 조항은 다른 여섯 속성 모두와 독립적이다. 결정적이며 LLM을 사용하지 않는 하네스가 고정된 릴리스에서 이들을 측정한다. LangGraph 1.2.9는 두 번째 재개 값을 영속적으로 기록하고 결코 참조하지 않으며, 스키마에 위배되는 상태를 조용히 영속화하고, 실제 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.