PaperlayerView exact revision on arXiv

Source-linked AI summary

Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers

Sajjad Khan

arXiv:2608.03836v3cs.LGcs.DCcs.LOcs.SE

TL;DR

Workflow persistence frameworks lack a machine-checkable meaning of resume despite handling approvals and non-idempotent effects. This paper defines and verifies the RESUME CONTRACT, then measures pinned framework releases with a deterministic harness, finding incompatible conformance profiles and failures under interrupts, crashes, and concurrent delivery.

  • Problem

    Workflow frameworks document incompatible resume semantics for completed effect-bearing work, without a machine-checkable contract for practitioners to consult.

  • Method

    The paper defines the RESUME CONTRACT, checks reference semantics with TLA+ and TLAPS, and evaluates pinned releases using a deterministic, LLM-free conformance harness.

  • Results

    No two probed frameworks share a conformance profile, with observed violations spanning fork, validity, replay, crash recovery, and concurrent consume-once behavior.

  • Takeaways & Limitations

    The RESUME CONTRACT makes resume semantics explicit and provides a basis for distinguishing framework behavior across interrupts, crashes, and concurrent delivery.

  • Takeaways & Limitations

    The evaluation abstracts effects and crashes, while deeper concurrent nesting and multi-checkpointer fan-in remain outside the current scope.

Abstract

from arXiv · show

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 happened. Five widely deployed agent workflow frameworks answer differently, none exposes a machine-checkable contract, and measured 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), and the reference conjunction is additionally TLAPS-proved unbounded (196 obligations); a 39-cell fault matrix and two companion modules yield the separating models independence requires. 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: an opt-in gate claims consumption in the shared store, serving one racer and refusing the rest before any node executes.

1 INTRODUCTION

This paper argues that agent workflow persistence lacks a machine-checkable contract for interruption, checkpointing, and resume semantics, making continuation of non-idempotent effects a correctness question. It defines the RESUME CONTRACT, verifies a reference model, measures deployed frameworks deterministically, and presents REMIT as a repair path.

  • Motivation: Agent persistence must specify which completed effects may fire again when a run resumes after approval, crash, or preemption.As workflows control non-idempotent effects, “continue” becomes a correctness question rather than merely an availability feature.
  • Problem: None of the evaluated frameworks exposes a machine-checkable contract, and their stated or implied checkpointing disciplines are incompatible.The paper contrasts CrewAI’s no-rerun claim, LlamaIndex’s re-execution guidance, and LangGraph’s completed-task memoization.
  • Contribution: The RESUME CONTRACT defines six properties: prefix continuation, effect exactly-once, fork determinism, checkpoint validity, consume-once, and recovery determinism.These properties govern re-execution, interrupt lifecycle, persistence validity, and whether recovery depends on durable state.
  • Verification: 39 runs map every modeled fault against every property, while TLC verifies the reference configuration and produces depth 4–6 counterexamples for each single-fault configuration.The matrix discovers each fault’s full violation footprint and identifies separating models needed for independence claims.
  • Repair: REMIT provides a reference resume sequencer and append-only effect ledger, with Verus-discharged invariants, a verified recovery-decision core, and conformance checks against the TLA+ relation.Its repair path includes a live validity gate and addresses fork determinism through a matched read-path design.

2 THE RESUME PLANE AND ITS FRAGMENTATION

The resume plane records progress, parks runs for external input, and continues them from durable state after interrupts, crashes, or restores. Its documented semantics fragment across frameworks, with incompatible claims about whether completed work re-executes.

  • Resume plane: The resume plane combines durable checkpoints, interrupt parking, and continuation from durable state after an interrupt, crash, or explicit restore.In LangGraph it is implemented through checkpointers plus interrupt() and Command(resume=...), while other frameworks use distinct persistence mechanisms.
  • Documented fragmentation: LangGraph documentation assigns prior-checkpoint resume two meanings: branch-creating time travel and replay with interrupts re-triggered.The ambiguity arises because both readings are presented for invocation with a prior checkpoint_id.
  • Documented fragmentation: Framework documentation disagrees on completed-work semantics: CrewAI claims skipping completed work, LlamaIndex documents replay, and LangGraph memoizes completed task results.These claims apply to the officially documented mechanisms practitioners would use for durable human-in-the-loop or crash recovery.
  • Release stability: Five LangGraph releases—1.0.5, 1.1.0, 1.1.3, 1.1.10, and 1.2.9—reproduce the fork and silent-persistence violations, indicating stable behavior rather than transient regressions.The probe distinguishes these stable violations from tracker-reported regressions whose current and adjacent versions were clean.
  • Comparability: The study probes each framework’s officially documented recovery mechanism using one abstract workflow: gate a non-idempotent effect on human input and crash after a durable step.This common instantiation makes divergence between matrix rows the hazard inherited by developers porting workflows.

3 THE RESUME CONTRACT

The RESUME CONTRACT defines machine-checkable resume semantics over an abstract persistence interface, covering continuation, effects, forks, validity, authority consumption, recovery, and fork intent. Its formal results show that fork intent is necessary for simultaneously satisfying fork determinism and consume-once, while several core properties are independently separable.

  • Contract scope: The contract states six properties over effects, checkpoints, interrupts, resume values, outcomes, and recovery decisions: PC, EO, FD, CV, CO, and RD.The interface abstracts away framework-specific execution mechanisms, and each property is evaluated from observable behavior.
  • Fork intent: FI requires the resume API to carry fork intent; without a branch discriminator, no responder can satisfy both FD and CO for all admissible traffic.The impossibility construction makes duplicate delivery and caller-requested forking indistinguishable when the wire exposes no discriminator.
  • Fork intent: The impossibility result applies specifically when accepted traffic carries no discriminator, while transport metadata or environments excluding duplicates or same-value forks can make the lemma inapplicable.The probed LangGraph surface lacks the required retry/fork bit, whereas REMIT supplies one through ⟨checkpointId, resumeIndex⟩ keying.
  • Independence: 39 TLC runs provide witness-complete, interface-relative separations, with holding cells exploring 1.0–1.4×10^6 states versus 59–396 in the reference runs.The separation method establishes non-entailment by fully checking a model satisfying the source properties while violating the target.
  • Independence: FD and CV are independently separable from the other five properties, and PC is implied by no single property on non-vacuous witnesses.ForkIgnore separates FD, InvalidPersist separates CV, and the state-rebuild model shows EO does not imply PC.

4 MACHINE-CHECKED MODEL

The section formalizes the RESUME CONTRACT in TLA+ and checks its reference semantics and fault variants with exhaustive model checking. Scaled verification passes the six invariants and TypeOK, while fault matrices and companion modules expose independence, modeling limits, and the separately abstracted LangGraph fork path.

  • Formalization: TLA+ formalizes Definition 1 and Properties 1–6 in ResumeContract.tla, paired with R11_ConsumeCount.tla for the CO-c invariant.The base module contains 251 lines and models program state, effects, checkpoints, interrupts, consumption, forks, crashes, and recovery history.
  • Fault analysis: 39 fault-matrix runs show that replay breaks EO, PC, and CO, while recovery nondeterminism also damages RD and fork or validity faults each break one property.The matrix comprises 36 ResumeContract.tla cells plus the R7 state-rebuild row; clean separating models establish independence among the targeted properties.
  • Exhaustive checking: 7.4×10^6 distinct states pass the six invariants plus TypeOK at scaled bounds, with 1.47×10^7 generated states and depth 24.The scaled run is an exhaustive breadth-first check of the full reachable space at its stated constants.
  • Model scope and limitations: The model excludes crashes while parked, represents fork branches only at the outcome level, and cannot represent CO-c because Consume clears waiting atomically without a consumption counter.Parked behavior is handled empirically and by ResumeContractParked.tla; branch accounting belongs to REMIT’s ledger.
  • LangGraph fork model: LangGraphFork.tla separately abstracts LangGraph’s resume path, while repaired pending-write keying by checkpoint and resume ordinal verifies idempotence and fork determinism together.The mapping is expert-established rather than tool-certified, and probe 134 provides operational evidence for the repair mechanism.

5 CONFORMANCE METHODOLOGY

The conformance methodology uses deterministic, LLM-free probes, timing-free crash injection, and an effect-ledger oracle to measure persistence semantics reproducibly. Forty-seven numbered probes across eleven campaigns emit auditable evidence, with environments pinned to committed lockfiles.

  • LLM-free probes use pure-Python tasks and deterministic values, so verdicts do not depend on sampling, provider state, or prompt behavior.
  • Timing-free crash injection uses exception-based matrix crashes and SIGKILL synchronized by filesystem barriers, eliminating sleep-window races.Probe 160 freezes the durable prefix at exactly the completed-operation count and self-audits each point.
  • The effect-ledger oracle maps side-effect counters and execution traces to exactly-once, consume-once, prefix-continuation, fork-determinism, checkpoint-validity, and recovery-determinism verdicts.On durable-backend and kill probes, the ledger effect is a single autocommitted INSERT durable before task return.
  • RD constructs two legal durable states for crashes between unordered persistence operations, then compares two deterministic resumes rather than racing a kill.
  • 47 numbered probes in 11 campaigns produce raw and stable-view JSON, while the artifact manifest serves as the authoritative inventory.Evidence is stored per campaign, and reported numbers are claimed only from committed evidence whose audit re-derives them.
  • Pilot testing pinned current releases after resolution on 2026-07-16 across Python 3.12.3 and Ubuntu 24.04 containers.The tested frameworks included LangGraph 1.2.9, CrewAI 1.15.2, pydantic-graph 1.107.1, and AutoGen AgentChat 0.7.5.

6 CONFORMANCE RESULTS

The conformance results expose divergent resume semantics: durable interrupt paths generally preserve prefixes and consume responses once, while crash recovery and repeated restoration can replay completed effects or fail to resume at all. LangGraph and CrewAI exhibit concrete contract violations, whereas pydantic-graph fails the documented liveness obligation despite passing probed safety properties.

  • LangGraph: LangGraph 1.2.9 records a second resume value but silently ignores it, violating fork determinism.Resuming the same checkpoint with True and then False returns 1 both times.
  • LangGraph: LangGraph’s crash path re-executes durably recorded work, with effect count 1 at crash and 2 after resume, while interrupt resume preserves exactly-once behavior.The crash replay was replicated on SqliteSaver and PostgresSaver; interrupt-path regressions were fixed.
  • pydantic-graph: pydantic-graph documents interruption and resumption but cannot resume after a crash in the second node, failing liveness despite passing every probed safety property.Its inclusion in the conformance plane is based on the documented FileStatePersistence claim, making “never resumes” a substantive defect rather than vacuity.
  • Crash and interrupt paths: Durable parking is conformant across all three planes: after a parked-run crash, the pending interrupt survives, the prefix effect remains at one, and the gate fires once.By contrast, an exhaustive SIGKILL sweep re-executes completed effect-bearing work at all four incomplete boundaries and recovers at all five kill points.

7 REMIT: A REFERENCE SEQUENCER WITH A VERIFIED MODEL AND CONFORMANCE-TESTED CORE

REMIT is a reference resume sequencer that combines an append-only effect ledger, checkpoint validation, fork-aware sequencing, and deterministic recovery, with repairs demonstrated through verified and conformance-tested components. Its read-path consume-once gate repairs concurrent delivery across shared stores and hosts, while the paper explicitly bounds what remains unverified or unmeasured.

  • Architecture: REMIT interposes at the checkpointer interface, pairing transactional effect-ledger records with sequenced recovery keyed to the contract’s properties.The design maps exactly-once and consume-once to ledger uniqueness, prefix continuation to frontier monotonicity, fork determinism to checkpoint-and-resume indexing, checkpoint validity to write-time schema validation, and recovery determinism to total ordering.
  • Verification: On Verus 0.2026.05.03.8b81855, every positive target discharges with 0 errors, while negative certificates demonstrate that the obligations are non-tautological.The recovery interpretation proves order-independence for the completed #8039 window, and an order-sensitive rule fails the corresponding obligation.
  • Concurrency repair: Read-path gating repairs concurrent consume-once: exactly one racer claims a parked checkpoint before gated execution, succeeding 10/10 times on both SQLite and live Postgres.Both racers load the same checkpoint, while the loser is rejected before the gated effect executes.
  • Concurrency repair: Across two hosts, the stock path duplicates delivery in 10/10 repetitions, whereas the shipped gate rejects the losing racer with RemitConsumeConflict in 10/10 before node execution.The experiment used a networked PostgreSQL server and a 5 s gate; partitions and wider topologies remain unmeasured.
  • Verification: The model-conformance harness independently shadows the TLA+ variables in Rust, rechecks all six invariants after every action, and includes exhaustive verification beyond randomized testing.The randomized arm runs 2×10^4 sequences of up to 48 actions; the exhaustive arm removes the sampling caveat.
  • Scope and limits: The composite state machine is exhaustively checked at both bound sets, but no mechanized refinement connects the Verus model to compiled remit-core and the Python veneer remains unverified.The read-path consumption gate is shipped as an opt-in feature in v0.1.2, and partitions and wider topologies remain outside measurement.

8 RELATED WORK

Prior work addresses recovery layers, rollback attacks, workflow semantics, durable execution, and formal verification, but not uniformly the persistence primitive’s own machine-checkable contract. This paper positions the RESUME CONTRACT as a vertical, interface-level specification and measurement layer for agent frameworks.

  • Recovery layers around the contract: Crab and DART complement the contract at higher layers by restoring agents without replaying completed actions and certifying rollback admissibility, but neither specifies or measures primitive semantics.Crab provides semantics-aware checkpoint/restore for agent sandboxes, while DART operates above persistence primitives.
  • Semantic rollback attacks and approval integrity: ACRFence identifies Action Replay and Authority Resurrection as checkpoint–restore attack classes, whereas this paper specifies the corresponding obligations as a machine-checkable contract.ACRFence records irreversible tool effects with replay-or-fork semantics on restoration, which the paper characterizes as the adversarial face of EO and CO.
  • Testing and verifying agent frameworks: A 998-report study locates dominant bug mass in execution-semantics mechanisms, while LogicHunter and robustness benchmarks test frameworks horizontally; this paper instead supplies a named contract, checked model, verdicts, and implementation.The comparison is explicitly framed as horizontal testing versus vertical conformance analysis.
  • Why not just use Temporal or DBOS: Temporal, DBOS, and related durable-execution systems enforce or construct stronger execution semantics within imposed models, while agent frameworks adopted lighter persistence without the surrounding discipline.Temporal quarantines nondeterminism behind activities and versioning, DBOS ties steps to database transactions, and hosted orchestrators externalize workflow definitions.
  • Formal semantics for durable execution: The contract carries some obligations from mature durable-execution systems to an absent interface, but claims novelty chiefly for the four obligations those systems do not transfer uniformly.PC and RD are described as restatements, while EO is stronger than Temporal’s external-effect guarantee when activities rely on caller-supplied idempotency keys.
  • Isolation anomalies and black-box anomaly inference: The cross-process consume-once failure is a lost update in a non-atomic read–modify–write, connecting the paper’s black-box oracle to established isolation-anomaly definitions and inference methods.Adya et al. provide implementation-independent anomaly definitions, while Elle infers anomalies from client-observable histories.

9 THREATS TO VALIDITY

The validity analysis separates classification, mechanism comparability, oracle scope, replication fidelity, framework breadth, and ecological limits. Claims therefore rest on version-pinned measurements and formal checks while acknowledging documented coverage and abstraction boundaries.

  • Construct validity: The total, symmetric classification rule changes labels rather than measurements, but some claims remain limited by probe scope and required live agents.It labels LlamaIndex prefix replay D, LangGraph fork and CrewAI checkpointing ✗, and CrewAI @persist restore U; the strongest CrewAI task-skipping claim concerns crews and awaits the full matrix.
  • Construct validity: Matrix cells compare properties across each framework’s own mechanism, while documentation determines the EO crash-path classification.For example, LlamaIndex’s fork uses client-side snapshot copies, whereas LangGraph’s concerns a server-side thread fork; maintainer clarification could reclassify documentation status without changing measurement.
  • Ecological validity: Probe 126 found complete agreement between process-local counters and an on-disk external ledger, while probe 142 moved the state holder into a separate OS process.The primary oracle captures non-idempotent re-execution but not production latency or failure modes; replication values are observed frequencies with Wilson intervals.
  • Internal validity: Every pilot verdict replicated bit-identically on a separately provisioned developer host, and cross-environment claims used mechanical guards after a receipt-substitution near miss.The harness has no timing, randomness, or model calls, so verdict changes can arise only from pinned package versions.
  • External validity: The study covers five frameworks on documented paths, while four additional frameworks remain under construction and upstream regressions may already be patched.Accordingly, claims rely on the contract, model, and version-pinned receipts rather than any bug’s persistence.
  • Ecological validity: Neither oracle models a real payment-style API, so end-to-end partition or duplication delivery remains an effect-layer idempotency-key concern.The formal theorem is supported by an inductive invariant generalized from bounded model checking to unbounded sequences, with 196 proof obligations and zero omitted.

10 CONCLUSION

The conclusion finds that LLM-agent resume planes carry approvals and non-idempotent effects without stated semantics, while frameworks document incompatible disciplines and regress across releases. Checkpointing therefore guarantees nothing about completed effects, but the contract and test suite make resume semantics checkable for practitioners and framework authors.

  • Conclusion: LLM-agent resume planes carry human approvals and non-idempotent effects across interrupts, crashes, and restores without stated semantics.Three major frameworks document three incompatible disciplines, and two violate even the semantics they state or imply.
  • Conclusion: The work defers mechanized refinement from the verified model to the compiled core and a corpus-scale prevalence study.It also makes no claim about deeper concurrent nesting.
  • Conclusion: Framework checkpointing licenses nothing about completed effects.The conclusion states this as the immediate implication for practitioners.
  • Conclusion: The contract is checkable and the suite can serve as a CI job, making resume semantics actionable for framework authors.The conclusion frames this as the immediate implication for framework authors.
Loading 2608.03836v3…