Pith. sign in

REVIEW 4 minor 96 references

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

T0 review · 0 major / 4 minor · reviewed 2026-08-11 · deepseek-v4-flash

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

Pith's one-line read Checkpointed agent workflows re-execute completed effects

desk verdict 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. read the letter →

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

Sajjad Khan This is my paper · ORCID
classification cs.LGcs.DCcs.LOcs.SE
keywords conformancetestingcheckpointingcrashrecoveryexactly-oncesemanticsinterruptmodelcheckingTLA+workflowpersistence
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

0 major / 4 minor

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.

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.

minor comments (4)
  1. [Section 3.4, paragraph starting 'The empirical side carries its own weight'] 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).
  2. [Abstract, first paragraph] 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.
  3. [Section 3.2, Property 2 (EO)] 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.
  4. [Table 5 and Section 6.6] 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.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: the conformance verdicts rest on pinned external measurements and machine-checked models; only minor author self-citation in the RD provenance is present, and it is not load-bearing.

full rationale

The derivation chain is self-contained at every load-bearing step. The RESUME CONTRACT is stated over the persistence API (Section 3), and each property is evaluated by deterministic probes with an external SQLite effect ledger, not by the contract itself. The TLA+ model's fault switches are transcribed from observed mechanisms, and the paper explicitly addresses the circularity objection by showing the per-invariant matrix has off-diagonal footprints (Table 3); the clean rows are finite witnesses for the independence claims, and TLC exhaustively enumerates their reachable state spaces at stated bounds. The LangGraphFork module is source-grounded and the paper honestly labels it expert-established rather than mechanically extracted; probe 171 supplies pre-registered out-of-sample predictions that were confirmed, which is the opposite of a fitted input being called a prediction. REMIT's Verus verification is explicitly scoped to REMIT's own model and to executable cores, with rung 8 (refinement to the compiled core) named absent, so no unverified self-support is smuggled in. The only self-referential elements are the author's own issue #8039 used to motivate RD and the author's prior SoundGate paper [17] cited for provenance and methodology; neither is load-bearing because RD's conformance cells are decided by probes 118/128/136 that construct both legal durable states and measure recovery decisions independently, and the formal proof of the reference conjunction is TLAPS-discharged. The stated observable-state boundary (Property 1 and Scope) is an explicit scope exclusion, not a hidden assumption, and any effects invisible to the ledger would only add violations, never remove measured ones. Consequently the paper earns a low score; the 2 reflects the minor self-citation in the RD motivation, not any reduction of a central claim to its inputs.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The central claims rest on the abstraction boundary of Definition 1 (the resume plane), the small-scope adequacy of the TLA+ configuration, and the visibility restriction to the public state API. The paper states most of these assumptions explicitly; the invisible-speculative-execution boundary is the one that could, if violated by a real framework, make the measured EO and CO verdicts incomplete. No free parameters are fitted to data; the TLA+ bound constants are chosen model-checking scopes, not fitted values.

assumptions (6)
  • domain assumption Definition 1's abstract resume plane faithfully captures the persistence APIs of the probed frameworks.
    Section 2 and 3.1. The behavior of checkpoints, interrupts, and resume values in LangGraph, CrewAI, and the other frameworks is mapped to this interface; if the mapping fails, the verdicts do not transfer.
  • domain assumption Observable state is exactly what is retrievable through the public state-inspection API; invisible speculative execution is outside the contract.
    Property 1 and Section 3 Scope. The EO and CO verdicts depend on this visibility boundary.
  • domain assumption Fault switches in ResumeContract.tla transcribe observed deployment mechanisms rather than negations of target properties.
    Section 4.1. The discovered violation footprints and the independence witnesses rely on this grounding.
  • domain assumption Three tasks with the interrupt at task 2 realize every phase relationship the transition relation admits; the scaled configuration corroborates beyond the bound.
    Section 4.2. This small-scope argument underlies the exhaustiveness claims for the reference and fault models.
  • standard math The TLA+, TLAPS, and Verus toolchains are sound as used.
    Sections 4 and 7. The formal results inherit standard trust in these tools and their semantics.
  • domain assumption The probed workflows are representative of each framework's documented resume mechanism; no prevalence claims are made.
    Section 5 and 9 Threats. The study measures probed paths only, as stated repeatedly in the paper.

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}
}
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 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.

Figures

Figures reproduced from arXiv: 2608.03836 by the authors.

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

Review history (3 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

96 extracted references · 2 canonical work pages

  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

    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

    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

    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

    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

Show all 96 references
  1. [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

  2. [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

  3. [11]

    Life beyond distributed transactions: An apostate’s opinion,

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

    2007

  4. [12]

    Idempotence is not a medical condition,

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

    2012

  5. [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

  6. [14]

    Akka Persistence: Event sourcing for stateful actors,

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

    2026

  7. [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

  8. [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

  9. [17]

    Stop means stop: Measuring and repairing the enforce- ment 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

    2026 arXiv

  10. [18]

    Agents SDK: Sessions,

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

    2026

  11. [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

  12. [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

  13. [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

    2026

  14. [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

    2026 arXiv

  15. [23]

    AgentBench: Evaluating LLMs as agents,

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

    2024

  16. [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

    2026

  17. [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

    2025 arXiv

  18. [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. 24

    2025

  19. [27]

    Why do multi-agent LLM systems fail?

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

    2025 arXiv

  20. [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

    2025 arXiv

  21. [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

    2014

  22. [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

    2003

  23. [31]

    Distributed programming in Argus,

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

    1988

  24. [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

    1995

  25. [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

    1990

  26. [34]

    Workflow determinism and versioning,

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

    2026

  27. [35]

    DBOS: A DBMS-oriented operating system,

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

    2022

  28. [36]

    AWS Step Functions developer guide,

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

    2026

  29. [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

    2016

  30. [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

    2023

  31. [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

    2020

  32. [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

    2022

  33. [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

    2021

  34. [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

    2023

  35. [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

    2020

  36. [44]

    Durable execution and durable promises,

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

    2026

  37. [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

    2015

  38. [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

    2015

  39. [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

    2019

  40. [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

    2015

  41. [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

    2021

  42. [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

    1988

  43. [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

    2014

  44. [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

    2017

  45. [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

    2009

  46. [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

    2006

  47. [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

    2010

  48. [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

    2019

  49. [57]

    Applying ‘design by contract’,

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

    1992

  50. [58]

    Interface automata,

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

    2001

  51. [59]

    Multiparty asynchronous session types,

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

    2008

  52. [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

    2002

  53. [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

    1992

  54. [62]

    Workflow recovery,

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

    1996

  55. [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

    2003

  56. [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

    2006

  57. [65]

    Garcia-Molina and K

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

    1987

  58. [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

    1998

  59. [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

    2008

  60. [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

    2014

  61. [69]

    Fault tolerance via idempotence,

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

    2013

  62. [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

    1984

  63. [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

    2015

  64. [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

    1988

  65. [73]

    Abstracting control,

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

    1990

  66. [74]

    Handlers of algebraic effects,

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

    2009

  67. [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

    2000

  68. [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

    2018

  69. [77]

    Apache Airflow: tasks and retries,

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

    2026

  70. [78]

    Prefect: task caching and retries,

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

    2026

  71. [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

    2021

  72. [80]

    Crash-only software,

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

    2003

  73. [81]

    Distributed snapshots: Determin- ing global states of distributed systems,

    K. M. Chandy and L. Lamport, “Distributed snapshots: Determin- ing global states of distributed systems,”ACM Trans. Computer Systems, vol. 3, no. 1, pp. 63–75, 1985

    1985

  74. [82]

    MillWheel: Fault-tolerant stream processing at internet scale,

    T. Akidau, A. Balikov, K. Bekiro ˘glu, S. Chernyak, J. Haberman, R. Lax, S. McVeety, D. Mills, P . Nordstrom, and S. Whittle, “MillWheel: Fault-tolerant stream processing at internet scale,”Proc. VLDB Endowment, vol. 6, no. 11, pp. 1033–1044, 2013

    2013

  75. [83]

    ARIES: A transaction recovery method supporting fine-granularity locking and partial rollbacks using write-ahead logging,

    C. Mohan, D. Haderle, B. Lindsay, H. Pirahesh, and P . Schwarz, “ARIES: A transaction recovery method supporting fine-granularity locking and partial rollbacks using write-ahead logging,”ACM Trans. Database Systems, vol. 17, no. 1, pp. 94–162, 1992. 25

    1992

  76. [84]

    All file systems are not created equal: On the complexity of crafting crash-consistent applications,

    T. S. Pillaiet al., “All file systems are not created equal: On the complexity of crafting crash-consistent applications,” inProc. USENIX OSDI, 2014

    2014

  77. [85]

    Finding crash-consistency bugs with bounded black-box crash testing,

    J. Mohan, A. Martinez, S. Ponnapalli, P . Raju, and V . Chidambaram, “Finding crash-consistency bugs with bounded black-box crash testing,” inProc. USENIX OSDI, 2018

    2018

  78. [86]

    Jepsen: Distributed systems safety research,

    K. Kingsbury, “Jepsen: Distributed systems safety research,” https: //jepsen.io, accessed 2026

    2026

  79. [87]

    Model based testing with labelled transition systems,

    J. Tretmans, “Model based testing with labelled transition systems,” inFormal Methods and Testing, LNCS 4949. Springer, 2008, pp. 1–38

    2008

  80. [88]

    How Amazon Web Services uses formal methods,

    C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, “How Amazon Web Services uses formal methods,” Communications of the ACM, vol. 58, no. 4, pp. 66–73, 2015

    2015

  81. [89]

    Lamport,Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers

    L. Lamport,Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002

    2002

  82. [90]

    Using model checking to generate tests from specifications,

    P . Ammann, P . E. Black, and W. Majurski, “Using model checking to generate tests from specifications,” inProc. IEEE ICFEM, 1998, pp. 46–54

    1998

  83. [91]

    Lineage-driven fault injection,

    P . Alvaro, J. Rosen, and J. M. Hellerstein, “Lineage-driven fault injection,” inProc. ACM SIGMOD, 2015, pp. 331–346

    2015

  84. [92]

    Unenforced ordering between put_writes and put in synchronous durability,

    LangGraph issue #8039, “Unenforced ordering between put_writes and put in synchronous durability,” https://github. com/langchain-ai/langgraph/issues/8039, 2026

    2026

  85. [93]

    Generalized isolation level definitions,

    A. Adya, B. Liskov, and P . O’Neil, “Generalized isolation level definitions,” inProc. IEEE ICDE, 2000, pp. 67–78

    2000

  86. [94]

    Elle: Inferring isolation anomalies from experimental observations,

    K. Kingsbury and P . Alvaro, “Elle: Inferring isolation anomalies from experimental observations,”Proc. VLDB Endowment, vol. 14, no. 3, 2020

    2020

  87. [95]

    Token budgets: An empirical catalog of budget-overrun incidents in LLM-agent frameworks,

    S. Khan, “Token budgets: An empirical catalog of budget-overrun incidents in LLM-agent frameworks,” manuscript under review, Empirical Software Engineering (EMSE-D-26-00583); preprint arXiv:2606.04056, 2026

    2026 arXiv

  88. [96]

    A consistency lattice for multi-agent memory: Specifi- cation, mechanized proof, and runtime enforcement,

    S. Khan, “A consistency lattice for multi-agent memory: Specifi- cation, mechanized proof, and runtime enforcement,” manuscript under review; preprint arXiv:2606.17182, 2026

    2026 arXiv

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.