{"id":"22a34b1a-5aba-4ad4-acab-97ee8f3c84f3","arxiv_id":"2608.03836","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper formalizes six resume-semantics properties, machine-checks a reference model, measures five agent workflow frameworks against them, and finds no two frameworks share a conformance profile.","lead":"Five LLM-agent workflow frameworks handle crash and resume differently, and this paper shows none of them has a machine-checkable contract for what resume means for already-completed effects. It defines a formal Resume Contract, verifies a reference model, measures actual violations in LangGraph, CrewAI, and pydantic-graph, and ships a repair.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified.","rationale":"I read the paper in good faith and found no load-bearing concern that would change the reader's CONDITIONAL verdict. The paper's central empirical claims are well-anchored: the effect ledger is external to framework state and autocommitted, so re-execution of a task body necessarily appends a row; probe 163 mechanically verifies the kill-point ordering; and the SIGKILL probes use filesystem barriers rather than timing windows. The 'durably records a second resume value and never consults it' fork claim is corroborated by store dumps, source-line citation, a trace-conformance checker, and four pre-registered out-of-sample predictions that all confirmed. The CrewAI 12-vs-11 arithmetic is a direct ledger-visible duplicate, and the pydantic-graph unrecoverability is a straightforward liveness failure. The reader's weakest_assumption about invisible speculative execution is a stated scope boundary, not a threat to the findings: if a framework fired effects without executing the task body, those effects would lie outside the contract's definition of task effects, and the measured violations would remain valid even if additional unobserved effects existed. The documentation-interpretation fragility for the EO crash-path label is acknowledged in the paper ('a maintainer clarification would reclassify the cell as documented divergence without changing the measurement'), and the pairwise profile separations do not depend on that single cell. The formal model's small-scope checks and finite independence witnesses are honestly described as bound-relative, and the TLAPS proof claims are internally consistent with the stated 196 obligations. The primary reasons for the CONDITIONAL verdict remain the private artifacts and the absent refinement rung, neither of which is a correctness flaw in the argument.","tokens_in":41790,"tokens_out":15191,"duration_ms":135767,"concrete_test":"Run the released artifact's reproduce.sh on a fresh environment, then instrument the LangGraph execution loop (pregel/_algo.py) to log every task-body execution and compare against the SQLite effect ledger for probes 118, 126, and 133. If any ledger entry exists without a corresponding task-body execution, the observable-state boundary could miss hidden effects, warranting re-examination of the ✓ cells; if any headline count differs (e.g., LangGraph crash effect 1→2, CrewAI 12-vs-11, pydantic-graph GraphRuntimeError), the central claims would need revision.","verdict_should_be":"UNCHANGED","load_bearing_attack":"No significant objection identified. The central claims are supported by a multi-layered methodology: pinned framework versions, an external SQLite effect ledger, barrier-synchronized SIGKILL crashes, source-grounded mechanism accounts with out-of-sample predictions, and mutation analysis of both the probes and the harness itself. The weakest point is the reader-noted observable-state boundary (Property 1 and Scope): effects fired outside task-body execution would be invisible to the ledger. However, this is an explicitly stated scope exclusion, not a hidden assumption, and the contract governs task effects as measured by the external ledger. Any such hidden effects would only add violations, never remove the measured ones, so the headline findings (LangGraph crash-path re-execution, CrewAI restore replay, pydantic-graph unrecoverability, cross-process consume-once failure) stand as upper bounds on conformance. No internal inconsistency or unverified load-bearing step was identified.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes the RESUME CONTRACT, a set of six properties (PC, EO, FD, CV, CO, RD) plus fork-intent (FI) and liveness obligations, stated over the checkpoint/interrupt/resume interfaces of agent workflow frameworks. It formalizes the contract in TLA+, verifies a reference semantics and fault models with TLC at two bound sets, proves the reference conjunction with TLAPS (196 obligations), and builds a deterministic, LLM-free conformance harness that measures five frameworks at pinned releases. The empirical study reports that LangGraph violates fork determinism and checkpoint validity, exhibits exactly-once across interrupts but at-least-once across crashes, CrewAI re-executes completed work against its checkpointing claim, pydantic-graph cannot resume after a mid-node crash, and cross-process duplicate delivery breaks consume-once. The paper also presents REMIT, a reference sequencer and shim with a Verus-verified recovery core, which repairs the fork and validity cells, and an opt-in cross-process gate that repairs the consume-once race.","tokens_in":41762,"tokens_out":26167,"duration_ms":215522,"significance":"If the claims hold, this is a substantial contribution. It provides the first machine-checkable contract for resume semantics in the agent-framework ecosystem and combines formal model checking with unusually self-audited empirical conformance testing. The strengths are concrete: exhaustive TLC verification with scaled bounds, a TLAPS proof of the reference conjunction, an external SQLite effect ledger, barrier-synchronized SIGKILL crash injection, cross-host and cross-backend replication, mutation analysis of both probes and harness, and falsifiable out-of-sample predictions from the mechanism model (probe 171). The paper is also exemplary in stating its own limits: observable state is explicitly scoped to the public state-inspection API, fault-footprint completeness is bound-relative, and the absent rung-8 refinement is disclosed. These limitations affect the universal side of the claims, not the upper-bound violation findings; hidden effects could only add violations, never remove the measured ones.","major_comments":[],"minor_comments":[{"comment":"The claim that CO fails on an observed framework path while all other properties hold is contradicted by probe 159, where the same duplicate delivery also violates EO and CO-e; the paper's own model footprint for that cell is {EO, CO-e, CO-c} with PC, FD, CV, RD clean. Please revise the sentence to state the co-occurrence explicitly or to rely on the model-level separation of CO-c in Proposition 1(iv).","section":"Section 3.4, paragraph starting 'The empirical side carries its own weight'"},{"comment":"The sentence 'measured behavior violates even the fragments they state' overstates the results; Table 5 shows LlamaIndex Workflows's wait_for_event idiom is a documented divergence D (behavior matches its stated at-least-once) and AutoGen AgentChat's restore path is conformant. The introduction's more precise statement — 'two of the three do not satisfy even the semantics they themselves state or imply' — should be mirrored in the abstract.","section":"Abstract, first paragraph"},{"comment":"The statement that 'the \"exactly\" is supplied by pairing with the liveness obligation of Sec. 4' is informal; Since EventuallyCompletes only asserts that the run eventually completes, please explain how pairing with it rules out an effect being skipped forever, or reformulate the liveness obligation as an effect-level progress property.","section":"Section 3.2, Property 2 (EO)"},{"comment":"The liveness obligation is not a column in Table 5, yet Section 6.6 and Table 7 use liveness to separate pydantic-graph from other frameworks; consider adding an explicit liveness column or a clear annotation to make the matrix self-contained and to make the pairwise-separation argument easier to verify.","section":"Table 5 and Section 6.6"}],"recommendation":"minor_revision","confidential_remarks":"The manuscript's transparency about its own process — the withdrawn observation, the copied-receipt near miss and its timestamp guard, and the retired Verus lemmas — is commendable, but it makes independent verification of the cross-environment claims important. The artifact and REMIT sources are private and were not inspected in this review; access for reviewers should be confirmed during production. The required changes are localized: correcting the abstract's blanket violation statement and the Section 3.4 sentence about CO's empirical separation. The technical core is sound and the paper fits the journal's scope."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Bottom line: this is the real thing. It specifies a conformance contract for checkpoint/interrupt/resume semantics in LLM-agent workflow frameworks, machine-checks it with TLA+/TLC and a TLAPS proof of the reference conjunction, and then measures five frameworks with a deterministic, LLM-free harness that uses external effect ledgers, SIGKILL barriers, mutation probes, and cross-host replication. The headline findings are strong: LangGraph serves the first resume value twice and ignores the second, persists schema-invalid state silently, and re-executes durably recorded work after a real SIGKILL; CrewAI re-runs completed work against its written exactly-once claim; pydantic-graph cannot resume after a mid-node crash; and no two probed frameworks share a conformance profile. The cross-process consume-once failure is unusually well characterized, including a dose-response window that tracks the gated node's own execution time.\n\nWhat is genuinely new is the assembly. The individual properties are classical (Remark 5 says so), but stating them as a checkable obligation set over the persistence API, proving partial independence with separating models, and then turning the whole thing into a per-release conformance matrix is a real contribution at this layer. The REMIT repair is credible: Verus-verified executable cores, a CI-gated line-identical recovery function, and an honest admission that no mechanized refinement connects the model to the compiled core (rung 8 absent). The paper consistently separates measured behavior from documented semantics and labels undocumented divergence as U rather than overcharging.\n\nSoft spots are real but not undermining. The artifact is private pending publication, so the TLC/TLAPS/Verus receipts and probe implementations cannot be audited from the preprint; that alone justifies the CONDITIONAL verdict. The observable-state boundary (Property 1, Section 3) is explicit, and the stress-test note is right that hidden effects would only add violations, but it does scoped the positive EO/CO verdicts to public-API-visible behavior. The LangGraphFork model is expert-established rather than mechanically extracted, though the committed out-of-sample predictions in probe 171 are a good counterweight. These are minor concerns relative to the central argument.\n\nWho gets value: framework maintainers (a CI conformance suite), practitioners gating payments or approvals behind these APIs, and the formal-methods/systems community. The paper deserves a serious referee. My recommendation: send it to peer review, with artifact access made a condition for reviewers; desk rejection would be a miss.","headline":"A rare and credible combination of a machine-checked resume contract, a deterministic cross-framework conformance study, and a verified repair; the headline findings are robust and the paper deserves serious peer review, conditional on artifact access.","tokens_in":42397,"tokens_out":2293,"would_cite":true,"duration_ms":21703,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Checkpointed agent workflows re-execute completed effects","keywords":["conformance testing","checkpointing","crash recovery","exactly-once semantics","interrupt semantics","model checking","TLA+","workflow persistence"],"falsifier":"Run the artifact's pinned harness, for example probe 159: two OS processes sharing one on-disk SqliteSaver, both resuming the same parked interrupt from a spin-barrier start, with the external ledger as oracle; if the gated effect fires exactly once in even one of ten repetitions, the cross-process consume-once failure does not reproduce. Alternatively, run probe 133 (SIGKILL after the durable write, resume in a fresh interpreter) on LangGraph 1.2.9; if the ledger stays at 1 instead of going 1 to 2, the crash-path exactly-once violation is refuted.","tokens_in":2056,"feed_emoji":"🔁","tokens_out":1976,"duration_ms":86266,"temperature":0.7,"pith_summary":"This paper tries to establish that the checkpoint, interrupt, and resume machinery in LLM-agent workflow frameworks has no reliable common semantics, and that the gap is measurable and fixable. It proposes the RESUME CONTRACT: six properties over the public persistence API (prefix continuation, effect exactly-once, fork determinism, checkpoint validity, consume-once, recovery determinism) plus fork-intent expressibility and a liveness obligation. It checks the contract's reference semantics exhaustively with a TLA+ model, proves the reference conjunction unbounded with TLAPS, and measures five pinned frameworks with a deterministic, LLM-free harness. The measured result is that LangGraph 1.2.9 re-executes durably recorded work after a real SIGKILL while claiming it will not, CrewAI 1.15.2 re-executes completed effect-bearing methods against its written exactly-once claim, and pydantic-graph 1.x cannot resume after a mid-node crash, while no two probed frameworks share a conformance profile. If the paper is right, framework authors can adopt a checkable contract and a CI conformance suite, and practitioners should treat any resume-guarantee claim as unverified until an external effect ledger confirms it.","feed_headline":"Checkpointed agent workflows re-execute completed effects","feed_subtitle":"A machine-checked resume contract shows five frameworks disagree, and even documented exactly-once claims fail under crash and concurrency.","key_machinery":"The RESUME CONTRACT is an abstract property set stated over the resume plane's public persistence interface: prefix continuation (PC), effect exactly-once (EO), fork determinism (FD), checkpoint validity (CV), consume-once (CO), and recovery determinism (RD), plus the fork-intent (FI) protocol obligation and a liveness obligation. The paper formalizes this as a TLA+ module, ResumeContract.tla, with six fault switches that transcribe observed violation mechanisms; TLC exhaustively checks the reference configuration and per-fault matrices, and TLAPS proves the reference conjunction unbounded (196 obligations). On the empirical side, a deterministic, LLM-free harness drives every probe through the framework's own persistence APIs, with a process-local effect counter cross-checked on durable-backend probes by an on-disk SQLite ledger external to framework state; that external ledger is what makes duplicates invisible in framework state measurable, such as CrewAI's restore replay and LangGraph's concurrent delivery. REMIT, the reference resume sequencer, carries the repair: a Verus-verified recovery core line-identical to the shipped executable, branch keying by checkpointId plus resumeIndex, and a read-path consumption gate that claims an interrupt in the shared store before any node executes.","core_discovery":"The central claim is that the resume plane of agent workflow frameworks lacks a machine-checkable conformance contract, and that this is not a benign gap: measured behavior on pinned releases violates even the fragments of semantics the frameworks document. On LangGraph 1.2.9, a second resume value addressed to the same interrupt checkpoint is durably recorded and never consulted, schema-invalid state is persisted silently, and a completed task whose result is durably recorded re-executes after a real SIGKILL, giving exactly-once across interrupts and at-least-once across crashes on one API. CrewAI 1.15.2 re-executes completed effect-bearing methods under CheckpointConfig restore, contradicting its written resume-without-rerunning claim; pydantic-graph 1.x cannot resume after a mid-node crash, so its safety properties hold vacuously while progress is dead. LlamaIndex Workflows documents at-least-once prefix replay, which the contract records as documented divergence rather than violation, and AutoGen AgentChat is the only probed framework that rejects tampered state loudly. No two probed frameworks share a conformance profile, and consume-once holds for sequential re-delivery but fails under concurrent delivery: k processes resuming one parked interrupt fire the gated effect k times, with no observed ceiling below k=16 and the admitting window tracking the gated node's own execution time.","pith_inferences":["If the duplicate-consumption window tracks the gated node's execution time, then inserting a long model call or payment request between reading a human approval and firing its effect widens the window; a testable extension would measure duplicate rates under longer gates on frameworks that do not use REMIT's gate.","The read-path versus write-path finding suggests a general architecture lesson: when an execution loop reads durable state, decides, then reports to its persistence layer, the only enforcement seam at the persistence boundary is the read, and this should transfer to other checkpointer-shaped systems.","Because no two probed frameworks share a conformance profile, porting a side-effecting workflow between frameworks silently changes the reliability regime; a natural next step would be a contract-based portability checker that flags when source and target planes differ on the same path."],"forward_implications":["A documented checkpointing feature says nothing about completed effects; users must verify resume behavior with an external effect ledger rather than trusting framework state.","Crash recovery and interrupt recovery can be different reliability regimes on the same API, so deployments should test the crash path separately from the human-in-the-loop path.","Concurrent delivery of one human approval to one parked interrupt can fire the gated effect once per racing process; sequential inertness does not compose across processes.","The FD-CO impossibility result implies that an API cannot support both forking and inert re-delivery unless it exposes a fork-intent discriminator on the wire, and REMIT's branch keying is one such discriminator.","A conformance suite is practical: the contract can be checked in CI, and the reference sequencer repairs the fork and validity cells at the read path without changing the framework's execution loop."],"supporting_citations":[{"why":"CrewAI checkpointing documentation; supplies the written exactly-once claim that the measured CheckpointConfig replay contradicts.","marker":"[1]"},{"why":"LlamaIndex Workflows context documentation; supplies the at-least-once statement that classifies the workflow's prefix replay as documented divergence.","marker":"[2]"},{"why":"LangGraph persistence and interrupts documentation; supplies the branch-creating time-travel reading and the pending-writes do-not-rerun statement used to classify the FD and EO cells.","marker":"[8]"},{"why":"CopilotKit issue #2315; motivates the double-consume fault class transcribed as the FaultDoubleConsume switch in the model.","marker":"[16]"},{"why":"LangGraph issue #8039; names the ordering hazard that motivates the RD property and that probes 124 and 136 realize.","marker":"[92]"},{"why":"Verus; the verification toolchain used to machine-discharge REMIT's core invariants and the executable recovery core.","marker":"[3]"},{"why":"Durable Functions semantics; supplies the memoized-replay clause of PC that distinguishes conforming replay from CrewAI's rebuild-from-initial restore.","marker":"[13]"}],"fun_headline_variants":["Resume exactly-once claims fail under crash and concurrency","Machine-checked resume contract exposes framework violations","LangGraph re-runs completed work after SIGKILL crash","Five workflow frameworks have inconsistent resume semantics","Documented exactly-once resume fails under concurrent delivery"],"cache_read_input_tokens":44544,"weakest_assumption_plain":"The entire measurement framework defines observable state as exactly what a caller can retrieve through a framework's public state-inspection API, and explicitly excludes invisible speculative execution that never surfaces through that API; if a framework duplicates or re-executes effects through internal paths that never appear in that API, the measured exactly-once and consume-once verdicts could miss the duplication.","fun_headline_variants_meta":{"raw":{"variants":["Resume exactly-once claims fail under crash and concurrency","Machine-checked resume contract exposes framework violations","LangGraph re-runs completed work after SIGKILL crash","Five workflow frameworks have inconsistent resume semantics","Documented exactly-once resume fails under concurrent delivery"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000497,"raw_usage":{"total_tokens":2566,"prompt_tokens":1207,"completion_tokens":1359,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":823,"completion_tokens_details":{"reasoning_tokens":1284}},"tokens_in":823,"tokens_out":1359,"duration_ms":10471,"temperature":1.0,"reasoning_tokens":1284,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T04:14:28.119342+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the artifact's pinned harness, for example probe 159: two OS processes sharing one on-disk SqliteSaver, both resuming the same parked interrupt from a spin-barrier start, with the external ledger as oracle; if the gated effect fires exactly once in even one of ten repetitions, the cross-process consume-once failure does not reproduce. Alternatively, run probe 133 (SIGKILL after the durable write, resume in a fresh interpreter) on LangGraph 1.2.9; if the ledger stays at 1 instead of going 1 to 2, the crash-path exactly-once violation is refuted.","supporting_citations":[{"cited_title":"Unenforced ordering between put_writes and put in synchronous durability,","cited_arxiv_id":null,"evidence_quote":"LangGraph issue #8039; names the ordering hazard that motivates the RD property and that probes 124 and 136 realize."}],"review_version":3}