Pith. sign in

REVIEW 2 major objections 4 minor 96 references

This paper claims that 'resume' in LLM-agent workflow frameworks currently has no coherent semantics: five frameworks give incompatible answers, two violate their own stated guarantees, and one API delivers exactly-once across interrupts bu

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

A six-property resume contract, a TLA+ model, and a deterministic harness show major agent frameworks violate their own checkpoint/resume semantics, with a shipped reference sequencer as repair.

T0 review reviewed 2026-08-05 challenge →

load-bearing objection Serious, self-auditing conformance study of agent-framework resume semantics; the LangGraph crash-path EO headline is an interpretation that needs tightening, but the contract, model, and measurements merit a real referee. the 2 major comments →

arxiv 2608.03836 v1 pith:7ZIUHHDI submitted 2026-08-04 cs.LG cs.DCcs.LOcs.SE

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

Sajjad Khan This is my paper
classification cs.LG cs.DCcs.LOcs.SE
keywords checkpoint/resume semanticsexactly-once effectsfork determinismconsume-oncecrash recoveryTLA+ model checkingconformance testingLLM agent workflows
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

LLM-agent workflow frameworks persist execution state so a run can be interrupted, crash, and continue—but 'continue' has no shared meaning. This paper tries to establish that five widely used frameworks answer the central question (does already-completed work re-execute on resume?) in mutually incompatible ways, and that two of them violate even the guarantees their own documentation states. It names a six-property RESUME CONTRACT over the persistence API, machine-checks a reference semantics in TLA+, and measures the frameworks with a deterministic, LLM-free probe harness. On one framework's single API, interrupt resume is exactly-once while crash resume re-executes durably recorded tasks after a real SIGKILL; another replays completed effect-bearing methods against its written claim; one cannot resume after a mid-node crash; and consume-once holds sequentially but fails when two processes resume one parked interrupt. If the paper is right, 'the framework has checkpointing' licenses nothing about completed effects, and both framework authors and developers need a stated, checkable contract.

Core claim

The paper's central claim is that the resume plane needs an explicit contract and that, measured against it, deployed frameworks are incoherent. The RESUME CONTRACT states six properties—prefix continuation, effect exactly-once, fork determinism, checkpoint validity, consume-once, recovery determinism—plus a fork-intent protocol obligation and a liveness obligation. A TLA+ model checks the reference semantics exhaustively and maps every injected fault's violation footprint; the deterministic harness re-derives conformance at pinned versions. The headline measured finding: a single API delivers exactly-once across interrupts and at-least-once across crashes, the crash path re-executing a task

What carries the argument

RESUME CONTRACT: six checkable properties (plus fork-intent and liveness) stated over effects, checkpoints, interrupts, and resume values—the vocabulary any caller programs against. ResumeContract.tla: a TLA+ module formalizing the contract with six fault switches; TLC exhaustively checks the reference semantics and produces one counterexample per injected violation class, and a 39-cell per-invariant matrix yields the independence witnesses. LangGraphFork.tla: a small derived model whose 'recorded value is always served' rule reproduces the fork violation and predicts out-of-sample outcomes. REMIT: a reference resume sequencer and append-only effect ledger behind the checkpointer interface;

Load-bearing premise

The mechanism account rests on an expert reading of the source rather than a mechanical extraction: if the modeled 'recorded value always wins' rule does not match the real task-preparation precedence, the fork-violation explanation and its out-of-sample predictions would be wrong.

What would settle it

Run the pinned release's SIGKILL crash-resume probe with an on-disk effect ledger: if a task whose result is durably recorded does not re-execute after resume in a fresh process, the paper's headline at-least-once crash-path claim is false.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Porting a side-effecting workflow between frameworks silently changes the resume discipline; no type or signature exposes which regime is in force.
  • Crash-resume re-executes completed work even when the result is durably recorded, so non-idempotent effects (payments, messages) must carry their own idempotency keys or be gated externally.
  • Conformance profiles do not converge with releases; two regressions shipped and were fixed between point releases while the fork and validity violations stayed stable across five versions, so a standing CI conformance suite is the natural fix.
  • The fork repair binds at the durable-state read path, not the persistence write path; any repair that only changes what the saver stores cannot override a decision the execution loop makes from what it loads.
  • The cross-process consume-once failure is a lost update on an unatomic read–modify–write; a compare-and-swap or uniqueness-constrained claim in the shared store eliminates it without slowing the single-process path.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The read-path enforcement lesson likely generalizes beyond the two tested properties: any executor that loads durable state, decides, then reports to a persistence layer has its enforcement seam at loads; the paper demonstrates this for fork determinism and consume-once.
  • The contract's per-property verdicts could be lifted directly into a regression suite run in CI on every release; that would convert the observed drift—user issues as the only specification—into a machine-checked release gate.
  • Because the consume-once window tracks the gated node's own execution time, any long-running model call or payment request widens the race; deployments that route real agents through gates should treat the measured saturation as a floor and add explicit consumption claims rather than relying on row-level locking.
  • The live fork violation's 80/80 replication across models suggests model choice cannot mask this class of read-path defect, so a future prevalence study over more frameworks could quantify ecosystem exposure—something the paper deliberately does not claim.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper proposes the RESUME CONTRACT, a six-property specification (PC, EO, FD, CV, CO, RD) plus fork-intent and liveness obligations for workflow persistence layers, formalizes it in TLA+, and checks a reference semantics and six fault switches with TLC, reporting a 39-cell fault matrix and independence witnesses. A deterministic, LLM-free harness then measures five agent frameworks at pinned releases. The headline results are: LangGraph 1.2.9 exhibits a fork-determinism violation (#6663), silent schema-invalid persistence, and crash-path re-execution of durably recorded work; CrewAI re-executes completed methods against its checkpointing claim; pydantic-graph cannot resume after mid-node crash; consume-once holds sequentially but fails under concurrent delivery; and no two frameworks share a conformance profile. The paper also presents REMIT, a reference sequencer with a Verus-verified recovery core and a shipped LangGraph shim that repairs the fork and validity cells, plus an opt-in cross-process gate for consume-once.

Significance. If the empirical and formal claims hold, this is a valuable and timely contribution. It provides the first explicit, machine-checkable contract for resume semantics at the agent-framework persistence layer, backed by an unusually rigorous evidence package: exhaustive TLC state counts, a per-invariant fault matrix, a deterministic effect-ledger oracle, cross-host replications, mutation studies of both source and harness, out-of-sample model predictions (probe 171), and explicit scoping of verification gaps (Table 10, rung 8 absent). The REMIT artifact, although not fully refinement-proven, is a concrete, shipped repair with machine-discharged core obligations. The main correctness risk is not in the measurements but in the classification of LangGraph's crash-path behavior as a contradiction of its own documented semantics.

major comments (2)
  1. [Section 6.1 / Table 5] The measured crash-path re-execution (probes 118/126/130/133) is not in dispute. What is load-bearing is the classification of that re-execution as a ✗ contradiction of LangGraph's own stated semantics, and the resulting headline that "one API splits exactly-once/at-least-once." The paper quotes the pending-writes sentence that completed nodes' writes are stored so that on resume "you don't re-run the successful nodes," and applies it to a node whose result is durably recorded via put_writes but whose enclosing superstep checkpoint has not advanced. Table 1, however, records LangGraph's stated discipline as "graph-node semantics are checkpoint-granular." Under a checkpoint-granular reading, a node whose superstep did not commit is not a "successful/completed" node; replaying from the last committed checkpoint is exactly the documented recovery model, not a contradiction. The documentatio
  2. [Section 4.3 (LangGraphFork.tla)] The causal claim that #6663 is "the shadow of replay idempotence" rests on the recorded-write rule being an accurate transcription of LangGraph's resume precedence logic. The paper is admirably explicit that this mapping is "expert-established, not tool-certified," and the out-of-sample predictions of probe 171 and the trace conformance of probe 143 are real evidence. But the mapping is not mechanically extracted or refinement-proven; if the real precedence logic in pregel/_algo.py differs at unprobed points, the mechanism account and the 125/134 write-path/read-path localization could be wrong. The conformance verdicts do not depend on this, but Section 4.3's title claim does. Please either (a) provide a mechanical extraction (e.g., a parser/translator from the pinned source to the TLA+ serve rule) or (b) present the "shadow of replay idempotence" finding as a supported hypothesis and m
minor comments (4)
  1. [Section 6.1 / Table 1] Please provide the exact URL or anchor for the "you don't re-run the successful nodes" quotation, and state explicitly whether the crash-path probes use @task-decorated functions or plain graph nodes. Table 1 gives two different documented disciplines (task-body memoization vs. checkpoint-granular graph nodes), and the classification discussion would benefit from knowing which discipline the probe path falls under.
  2. [Table 4 / Section 5.2] The provenance table lists #8039 as "New" and "our own filing"; the text discloses this, but the phrase "with several other developers' reproductions as the independent half" should name or link those reproductions so readers can weigh the independence claim.
  3. [Section 9] The "near miss" about a copied container receipt is important and speaks well of the authors' candor, but the timestamp-inequality audit that prevents recurrence is easy to miss inside the threats section. Consider promoting it to the reproducibility paragraph in Section 5.
  4. [Section 5.4] The environment description says packages were "installed unpinned on 2026-07-16 to test current releases," while the artifact claims to pin releases. Please clarify the relationship between the unpinned installation and the committed lockfiles, and how reproduce.sh verifies that the resolved versions match the pinned ones.

Circularity Check

0 steps flagged

No significant circularity: conformance measurements and out-of-sample model predictions are self-contained; disclosed definitional dependencies and self-citations are non-load-bearing.

full rationale

The paper is a conformance/measurement study, not a derived prediction fitted to data. The RESUME CONTRACT properties are stated over a public persistence surface, and the TLA+ model explicitly checks the reference semantics, not any framework; independence witnesses are finite models exhaustively checked by TLC. The one structural dependence (CO-e is EO restricted to the gated task) is disclosed in the paper itself as 'a fact about the two formulas rather than a discovery' (Sec. 3.4, Prop. 2(iv)), so it is not a hidden derivation. The LangGraphFork model is expert-established rather than mechanically extracted, but the paper does not present it as a proof: it is source-grounded, tested out-of-sample with a registered prediction (probe 171, including a negative control), and interrogated by the 125/134 matched interventional pair. REMIT's verified surface is scoped honestly: no end-to-end refinement is claimed, rung 8 is explicitly absent, and negative Verus certificates establish proof content. Self-citations ([17], [92], [95], [96]) are disclosed and non-load-bearing: the #8039 ordering hazard is re-established by direct probes (118, 124, 128, 136), not by the citation. The main weaknesses flagged in the paper itself — LangGraphFork grounding ('remains expert-established rather than mechanically extracted'), the checkpoint-granular interpretation of the crash-path EO classification, and the absence of mechanized refinement — are correctness/interpretation risks, not circularity. No measured 'prediction' reduces by construction to a fitted parameter or to a self-citation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 1 invented entities

The paper introduces no fitted parameters: the TLA+ constants are dials for exhaustive state exploration, not free parameters tuned to data. The axioms listed are the load-bearing assumptions about model fidelity, oracle correctness, documentation accuracy, and verifier soundness. REMIT is the one new artifact-like entity, and it carries independent evidence through its shipped implementation and machine-checked cores.

axioms (5)
  • domain assumption TLA+ and TLC faithfully model the abstract resume plane of Definition 1
    All formal properties and independence claims are stated over this model; the model's adequacy for real frameworks is supported separately by source-grounded mechanisms and out-of-sample predictions.
  • domain assumption The effect ledger oracle correctly reflects external effects
    The harness relies on process-local counters plus an on-disk SQLite ledger. The paper argues ordering prevents overcounting and that any lost record would undercount, making every duplicate a floor.
  • domain assumption The quoted framework documentation accurately states each framework's intended semantics
    Conformance verdicts (✗, D, U) are defined against these citations. The paper's classification rule is designed so a misquote changes labels but not measurements, and it supplies relabeling recomputations.
  • standard math Verus and TLC verifiers are sound
    Machine-checked proofs and exhaustive finite-state checks are taken as valid evidence. Verus is not one of the proof assistants tracked by this report's formal_verification field, but the paper's own verification claims are treated as weight-bearing.
  • ad hoc to paper The LangGraphFork.tla recorded-write rule matches the pinned source behavior
    Section 4.3 maps the rule to specific source lines at pinned versions. It is expert-established rather than mechanically extracted, and the paper tests it out-of-sample via probe 171, but a mismatch would invalidate the mechanism account of #6663.
invented entities (1)
  • REMIT independent evidence
    purpose: Reference resume sequencer and append-only effect ledger that interposes at LangGraph's BaseCheckpointSaver interface, repairs fork determinism and checkpoint validity, and optionally gates cross-process consumption.
    Ships as remit-contract on PyPI with Verus-verified cores, a decision-free shim, and a claimed CI gate ensuring the recovery core is line-identical to the shipped executable. The artifact is private but the design and verification are described in detail.

reviewed 2026-08-05 · how reviews work

0 comments
Cite this review

Pith. "Pith review of Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers." pith.science (2026). https://pith.science/paper/7ZIUHHDI

@misc{pith2026260803836,
  author       = {Pith},
  title        = {Pith review of: Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7ZIUHHDI}},
  note         = {Machine review of arXiv:2608.03836}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2608.03836 by Sajjad Khan.

Figure 1
Figure 1. Figure 1: Layer positioning. Adjacent systems assume the framework [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

96 extracted references · 68 canonical work pages · 4 internal anchors

  1. [1]

    Checkpointing,

    CrewAI, “Checkpointing,” documentation, https://docs.crewai. com/en/concepts/checkpointing, accessed 2026-07-16

    2026

  2. [2]

    Workflows API reference: Context,

    LlamaIndex, “Workflows API reference: Context,” documen- tation, https://developers.llamaindex.ai/python/workflows-api- reference/context/, accessed 2026-07-16

    2026

  3. [3]

    Verus: Verifying Rust programs using linear ghost types,

    A. Lattuadaet al., “Verus: Verifying Rust programs using linear ghost types,”Proc. ACM Program. Lang., vol. 7, no. OOPSLA1, 2023

    2023

  4. [4]

    Crab: A semantics- aware checkpoint/restore runtime for agent sandboxes,

    T. Wu, C. Chang, L. Cao, W. Gao, and W. Wang, “Crab: A semantics- aware checkpoint/restore runtime for agent sandboxes,”arXiv preprint arXiv:2604.28138, 2026

    Pith/arXiv arXiv 2026

  5. [5]

    DART: Semantic Recoverability for Structured Tool Agents

    K. Yang, P . Li, Z. Wu, K. Xu, H. Huang, and X. Huang, “DART: Semantic recoverability for structured tool agents,”arXiv preprint arXiv:2605.23311, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  6. [6]

    What you approve is what executes: Consent integrity for black-box LLM agents,

    X. Weng, “What you approve is what executes: Consent integrity for black-box LLM agents,”arXiv preprint arXiv:2606.02668, 2026

    Pith/arXiv arXiv 2026

  7. [7]

    LogicHunter: Testing LLM Agent Frameworks with an Agentic Oracle

    M. Longet al., “LogicHunter: Testing LLM agent frameworks with an agentic oracle,”arXiv preprint arXiv:2607.06195, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  8. [8]

    LangGraph persistence and interrupts,

    LangChain, “LangGraph persistence and interrupts,” docu- mentation, https://docs.langchain.com/oss/python/langgraph/ persistence, accessed 2026-07-16

    2026

  9. [9]

    Agent workflows: Human in the loop,

    LlamaIndex, “Agent workflows: Human in the loop,” documenta- tion, https://developers.llamaindex.ai/python/examples/agent/ agent workflow basic/, accessed 2026-07-16

    2026

  10. [10]

    State management in Apache Flink: Consistent stateful distributed stream processing,

    P . Carboneet al., “State management in Apache Flink: Consistent stateful distributed stream processing,”Proc. VLDB Endowment, vol. 10, no. 12, 2017

    2017

  11. [11]

    Life beyond distributed transactions: An apostate’s opinion,

    P . Helland, “Life beyond distributed transactions: An apostate’s opinion,” inProc. CIDR, 2007

    2007

  12. [12]

    Idempotence is not a medical condition,

    P . Helland, “Idempotence is not a medical condition,”ACM Queue, vol. 10, no. 4, 2012

    2012

  13. [13]

    Durable functions: Semantics for stateful serverless,

    S. Burckhardt, C. Gillum, D. Justo, K. Kallas, C. McMahon, and C. S. Meiklejohn, “Durable functions: Semantics for stateful serverless,” Proc. ACM Program. Lang., vol. 5, no. OOPSLA, 2021

    2021

  14. [14]

    Akka Persistence: Event sourcing for stateful actors,

    Lightbend, “Akka Persistence: Event sourcing for stateful actors,” documentation, https://doc.akka.io/, accessed 2026

    2026

  15. [15]

    A survey of rollback-recovery protocols in message-passing systems,

    E. N. Elnozahy, L. Alvisi, Y.-M. Wang, and D. B. Johnson, “A survey of rollback-recovery protocols in message-passing systems,”ACM Computing Surveys, vol. 34, no. 3, pp. 375–408, 2002

    2002

  16. [16]

    Issue #2315: LangGraph interrupt fails due to extra null-state turn between trigger and resume,

    CopilotKit, “Issue #2315: LangGraph interrupt fails due to extra null-state turn between trigger and resume,” https://github.com/ CopilotKit/CopilotKit/issues/2315, 2025

    2025

  17. [17]

    Stop Means Stop: Measuring and Repairing the Enforcement Gap in Agent-Framework Control Primitives

    S. Khan, “Stop means stop: Measuring and repairing the enforce- ment gap in agent-framework control primitives,” arXiv preprint arXiv:2607.14166, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  18. [18]

    Agents SDK: Sessions,

    OpenAI, “Agents SDK: Sessions,” documentation, https://openai. github.io/openai-agents-python/sessions/, accessed 2026-07-16. 25

    2026

  19. [19]

    A critique of ANSI SQL isolation levels,

    H. Berenson, P . Bernstein, J. Gray, J. Melton, E. O’Neil, and P . O’Neil, “A critique of ANSI SQL isolation levels,” inProc. ACM SIGMOD, 1995, pp. 1–10

    1995

  20. [20]

    Anvil: Verifying liveness of cluster management controllers,

    X. Sun, W. Ma, J. T. Gu, Z. Ma, T. Chajed, J. Howell, A. Lattuada, O. Padon, L. Suresh, A. Szekeres, and T. Xu, “Anvil: Verifying liveness of cluster management controllers,” inProc. USENIX OSDI, 2024

    2024

  21. [21]

    ACRFence: Preventing semantic rollback attacks in agent checkpoint-restore,

    Y. Zheng, Y. Yang, W. Zhang, and A. Quinn, “ACRFence: Preventing semantic rollback attacks in agent checkpoint-restore,” arXiv preprint arXiv:2603.20625, CoDAIM Workshop, 2026

    arXiv 2026

  22. [22]

    An empirical study of bugs in modern LLM agent frameworks,

    X. Zhuet al., “An empirical study of bugs in modern LLM agent frameworks,”arXiv preprint arXiv:2602.21806, 2026

    arXiv 2026

  23. [23]

    AgentBench: Evaluating LLMs as agents,

    X. Liuet al., “AgentBench: Evaluating LLMs as agents,” inProc. ICLR, 2024

    2024

  24. [24]

    AgentRFC: Security design principles and conformance testing for agent protocols,

    S. Zheng and Q. Zhang, “AgentRFC: Security design principles and conformance testing for agent protocols,”arXiv preprint arXiv:2603.23801, 2026

    arXiv 2026

  25. [25]

    Pro2Guard: Proactive runtime enforcement of LLM agent safety via probabilistic model checking,

    H. Wang, C. M. Poskitt, J. Sun, and J. Wei, “Pro2Guard: Proactive runtime enforcement of LLM agent safety via probabilistic model checking,”arXiv preprint arXiv:2508.00500, 2025

    Pith/arXiv arXiv 2025

  26. [26]

    VeriGuard: Enhancing LLM agent safety via verified code generation,

    L. Miculicichet al., “VeriGuard: Enhancing LLM agent safety via verified code generation,”arXiv preprint arXiv:2510.05156, 2025

    arXiv 2025

  27. [27]

    Why do multi-agent LLM systems fail?

    M. Cemriet al., “Why do multi-agent LLM systems fail?”arXiv preprint arXiv:2503.13657, 2025

    Pith/arXiv arXiv 2025

  28. [28]

    SagaLLM: Context management, vali- dation, and transaction guarantees for multi-agent LLM planning,

    E. Y. Chang and L. Geng, “SagaLLM: Context management, vali- dation, and transaction guarantees for multi-agent LLM planning,” arXiv preprint arXiv:2503.11951, 2025

    Pith/arXiv arXiv 2025

  29. [29]

    Orleans: Distributed virtual actors for programmability and scalability,

    P . Bernstein, S. Bykov, A. Geller, G. Kliot, and J. Thelin, “Orleans: Distributed virtual actors for programmability and scalability,” Microsoft Research Tech. Rep. MSR-TR-2014-41, 2014

    work page 2014

  30. [30]

    Armstrong,Making Reliable Distributed Systems in the Presence of Software Errors

    J. Armstrong,Making Reliable Distributed Systems in the Presence of Software Errors. PhD thesis, KTH Royal Institute of Technology, 2003

    work page 2003

  31. [31]

    Distributed programming in Argus,

    B. Liskov, “Distributed programming in Argus,”Communications of the ACM, vol. 31, no. 3, pp. 300–312, 1988

    work page 1988

  32. [32]

    Orthogonally persistent object systems,

    M. Atkinson and R. Morrison, “Orthogonally persistent object systems,”The VLDB Journal, vol. 4, no. 3, pp. 319–401, 1995

    work page 1995

  33. [33]

    Linearizability: A correctness condition for concurrent objects,

    M. Herlihy and J. M. Wing, “Linearizability: A correctness condition for concurrent objects,”ACM TOPLAS, vol. 12, no. 3, pp. 463–492, 1990

    work page 1990

  34. [34]

    Workflow determinism and versioning,

    Temporal Technologies, “Workflow determinism and versioning,” documentation, https://docs.temporal.io/workflow-definition, ac- cessed 2026-07-16

    work page 2026

  35. [35]

    DBOS: A DBMS-oriented operating system,

    A. Skiadopouloset al., “DBOS: A DBMS-oriented operating system,” Proc. VLDB Endowment, vol. 15, no. 1, 2022

    work page 2022

  36. [36]

    AWS Step Functions developer guide,

    Amazon Web Services, “AWS Step Functions developer guide,” https://docs.aws.amazon.com/step-functions/, accessed 2026

    work page 2026

  37. [37]

    Realizing the fault-tolerance promise of cloud storage using locks with intent,

    S. Setty, C. Su, J. R. Lorch, L. Zhou, H. Chen, P . Patel, and J. Ren, “Realizing the fault-tolerance promise of cloud storage using locks with intent,” inProc. USENIX OSDI, 2016, pp. 501–516

    work page 2016

  38. [38]

    Automated verification of idempotence for stateful serverless applications,

    H. Ding, Z. Wang, Z. Shen, R. Chen, and H. Chen, “Automated verification of idempotence for stateful serverless applications,” in Proc. USENIX OSDI, 2023, pp. 887–910

    work page 2023

  39. [39]

    Fault- tolerant and transactional stateful serverless workflows,

    H. Zhang, A. Cardoza, P . B. Chen, S. Angel, and V . Liu, “Fault- tolerant and transactional stateful serverless workflows,” inProc. USENIX OSDI, 2020

    work page 2020

  40. [40]

    Netherite: Efficient execution of serverless workflows,

    S. Burckhardt, B. Chandramouli, C. Gillum, D. Justo, K. Kallas, C. McMahon, C. S. Meiklejohn, and X. Zhu, “Netherite: Efficient execution of serverless workflows,”Proc. VLDB Endowment, vol. 15, no. 8, 2022

    work page 2022

  41. [41]

    Boki: Stateful serverless computing with shared logs,

    Z. Jia and E. Witchel, “Boki: Stateful serverless computing with shared logs,” inProc. ACM SOSP, 2021, pp. 691–707

    work page 2021

  42. [42]

    Halfmoon: Log-optimal fault-tolerant stateful serverless computing,

    S. Qi, X. Liu, and X. Jin, “Halfmoon: Log-optimal fault-tolerant stateful serverless computing,” inProc. ACM SOSP, 2023, pp. 314– 330

    work page 2023

  43. [43]

    A.M.B.R.O.S.I.A: Providing performant virtual resiliency for distributed applications,

    J. Goldsteinet al., “A.M.B.R.O.S.I.A: Providing performant virtual resiliency for distributed applications,”Proc. VLDB Endowment, vol. 13, no. 5, 2020

    work page 2020

  44. [44]

    Durable execution and durable promises,

    Restate, “Durable execution and durable promises,” documenta- tion, https://docs.restate.dev/, accessed 2026-07-17

    work page 2026

  45. [45]

    IronFleet: Proving practical distributed systems correct,

    C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. Setty, and B. Zill, “IronFleet: Proving practical distributed systems correct,” inProc. ACM SOSP, 2015, pp. 1–17

    work page 2015

  46. [46]

    Verdi: A framework for implementing and formally verifying distributed systems,

    J. R. Wilcox, D. Woos, P . Panchekha, Z. Tatlock, X. Wang, M. D. Ernst, and T. Anderson, “Verdi: A framework for implementing and formally verifying distributed systems,” inProc. ACM PLDI, 2015, pp. 357–368

    work page 2015

  47. [47]

    Verify- ing concurrent, crash-safe systems with Perennial,

    T. Chajed, J. Tassarotti, M. F. Kaashoek, and N. Zeldovich, “Verify- ing concurrent, crash-safe systems with Perennial,” inProc. ACM SOSP, 2019, pp. 243–258

    work page 2019

  48. [48]

    Using Crash Hoare Logic for certifying the FSCQ file system,

    H. Chen, D. Ziegler, T. Chajed, A. Chlipala, M. F. Kaashoek, and N. Zeldovich, “Using Crash Hoare Logic for certifying the FSCQ file system,” inProc. ACM SOSP, 2015, pp. 18–37

    work page 2015

  49. [49]

    GoJournal: A verified, concurrent, crash-safe journaling system,

    T. Chajed, J. Tassarotti, M. Theng, M. F. Kaashoek, and N. Zeldovich, “GoJournal: A verified, concurrent, crash-safe journaling system,” inProc. USENIX OSDI, 2021, pp. 423–439

    work page 2021

  50. [50]

    Viewstamped replication: A new primary copy method to support highly-available distributed systems,

    B. M. Oki and B. H. Liskov, “Viewstamped replication: A new primary copy method to support highly-available distributed systems,” inProc. ACM PODC, 1988, pp. 8–17

    work page 1988

  51. [51]

    In search of an understandable consensus algorithm,

    D. Ongaro and J. Ousterhout, “In search of an understandable consensus algorithm,” inProc. USENIX ATC, 2014, pp. 305–319

    work page 2014

  52. [52]

    Engineering record and replay for deployability,

    R. O’Callahan, C. Jones, N. Froyd, K. Huey, A. Noll, and N. Partush, “Engineering record and replay for deployability,” inProc. USENIX ATC, 2017, pp. 377–389

    work page 2017

  53. [53]

    DMTCP: Transparent checkpointing for cluster computations and the desktop,

    J. Ansel, K. Arya, and G. Cooperman, “DMTCP: Transparent checkpointing for cluster computations and the desktop,” inProc. IEEE IPDPS, 2009

    work page 2009

  54. [54]

    Berkeley Lab Checkpoint/Restart (BLCR) for Linux clusters,

    P . H. Hargrove and J. C. Duell, “Berkeley Lab Checkpoint/Restart (BLCR) for Linux clusters,”Journal of Physics: Conference Series, vol. 46, pp. 494–499, 2006

    work page 2006

  55. [55]

    Design, modeling, and evaluation of a scalable multi-level check- pointing system,

    A. Moody, G. Bronevetsky, K. Mohror, and B. R. de Supinski, “Design, modeling, and evaluation of a scalable multi-level check- pointing system,” inProc. ACM/IEEE SC, 2010

    work page 2010

  56. [56]

    VeloC: Towards high performance adaptive asynchronous checkpointing at large scale,

    B. Nicolae, A. Moody, E. Gonsiorowski, K. Mohror, and F. Cap- pello, “VeloC: Towards high performance adaptive asynchronous checkpointing at large scale,” inProc. IEEE IPDPS, 2019

    work page 2019

  57. [57]

    Applying ‘design by contract’,

    B. Meyer, “Applying ‘design by contract’,”IEEE Computer, vol. 25, no. 10, pp. 40–51, 1992

    work page 1992

  58. [58]

    Interface automata,

    L. de Alfaro and T. A. Henzinger, “Interface automata,” inProc. ACM ESEC/FSE, 2001, pp. 109–120

    work page 2001

  59. [59]

    Multiparty asynchronous session types,

    K. Honda, N. Yoshida, and M. Carbone, “Multiparty asynchronous session types,” inProc. ACM POPL, 2008, pp. 273–284

    work page 2008

  60. [60]

    Alloy: A lightweight object modelling notation,

    D. Jackson, “Alloy: A lightweight object modelling notation,”ACM Trans. Software Engineering and Methodology, vol. 11, no. 2, pp. 256– 290, 2002

    work page 2002

  61. [61]

    The ConTract model,

    H. W ¨achter and A. Reuter, “The ConTract model,” inDatabase Transaction Models for Advanced Applications, A. K. Elmagarmid, Ed. Morgan Kaufmann, 1992, pp. 219–263

    work page 1992

  62. [62]

    Workflow recovery,

    J. Eder and W. Liebhart, “Workflow recovery,” inProc. IFCIS CoopIS, 1996, pp. 124–134

    work page 1996

  63. [63]

    Workflow patterns,

    W. M. P . van der Aalst, A. H. M. ter Hofstede, B. Kiepuszewski, and A. P . Barros, “Workflow patterns,”Distributed and Parallel Databases, vol. 14, no. 1, pp. 5–51, 2003

    work page 2003

  64. [64]

    Workflow exception patterns,

    N. Russell, W. M. P . van der Aalst, and A. H. M. ter Hofstede, “Workflow exception patterns,” inProc. CAiSE, 2006, pp. 288–302

    work page 2006

  65. [65]

    Garcia-Molina and K

    H. Garcia-Molina and K. Salem, “Sagas,” inProc. ACM SIGMOD, 1987, pp. 249–259

    work page 1987

  66. [66]

    The application of Petri nets to workflow management,

    W. M. P . van der Aalst, “The application of Petri nets to workflow management,”Journal of Circuits, Systems and Computers, vol. 8, no. 1, pp. 21–66, 1998

    work page 1998

  67. [67]

    Semantics and analysis of business process models in BPMN,

    R. M. Dijkman, M. Dumas, and C. Ouyang, “Semantics and analysis of business process models in BPMN,”Information and Software Technology, vol. 50, no. 12, pp. 1281–1294, 2008

    work page 2008

  68. [68]

    Atomic distributed transactions: A RESTful design,

    G. Pardon and C. Pautasso, “Atomic distributed transactions: A RESTful design,” inProc. WWW Companion, 2014, pp. 943–948

    work page 2014

  69. [69]

    Fault tolerance via idempotence,

    G. Ramalingam and K. Vaswani, “Fault tolerance via idempotence,” inProc. ACM POPL, 2013

    work page 2013

  70. [70]

    Implementing remote procedure calls,

    A. D. Birrell and B. J. Nelson, “Implementing remote procedure calls,”ACM Trans. Computer Systems, vol. 2, no. 1, pp. 39–59, 1984

    work page 1984

  71. [71]

    Implementing linearizability at large scale and low latency,

    C. Lee, S. J. Park, A. Kejriwal, S. Matsushita, and J. Ousterhout, “Implementing linearizability at large scale and low latency,” in Proc. ACM SOSP, 2015

    work page 2015

  72. [72]

    The theory and practice of first-class prompts,

    M. Felleisen, “The theory and practice of first-class prompts,” in Proc. ACM POPL, 1988, pp. 180–190

    work page 1988

  73. [73]

    Abstracting control,

    O. Danvy and A. Filinski, “Abstracting control,” inProc. ACM LISP and Functional Programming, 1990, pp. 151–160

    work page 1990

  74. [74]

    Handlers of algebraic effects,

    G. Plotkin and M. Pretnar, “Handlers of algebraic effects,” inProc. ESOP, 2009, pp. 80–94

    work page 2009

  75. [75]

    The influence of browsers on evaluators or, contin- uations to program web servers,

    C. Queinnec, “The influence of browsers on evaluators or, contin- uations to program web servers,” inProc. ACM ICFP, 2000, pp. 23–33

    work page 2000

  76. [76]

    Ray: A distributed framework for emerging AI applications,

    P . Moritz et al., “Ray: A distributed framework for emerging AI applications,” inProc. USENIX OSDI, 2018, pp. 561–577. 26

    work page 2018

  77. [77]

    Apache Airflow: tasks and retries,

    Apache Software Foundation, “Apache Airflow: tasks and retries,” documentation, https://airflow.apache.org/docs/, accessed 2026

    work page 2026

  78. [78]

    Prefect: task caching and retries,

    Prefect Technologies, “Prefect: task caching and retries,” documen- tation, https://docs.prefect.io/, accessed 2026

    work page 2026

  79. [79]

    Consistency and completeness: Rethinking dis- tributed stream processing in Apache Kafka,

    G. Wang et al., “Consistency and completeness: Rethinking dis- tributed stream processing in Apache Kafka,” inProc. ACM SIGMOD, 2021, pp. 2602–2613

    work page 2021

  80. [80]

    Crash-only software,

    G. Candea and A. Fox, “Crash-only software,” inProc. USENIX HotOS, 2003

    work page 2003

Showing first 80 references.

This paper was first reviewed by deepseek-v4-flash on August 5, 2026.