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

• URL: http://arxiv.org/abs/2608.03836v3
• Date: Sat, 08 Aug 2026 12:41:44 GMT
• Title: Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
• Abstract summary: 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.<n>Five widely deployed agent workflow frameworks answer differently, none exposes a machine-checkable contract.<n>LangGraph 1.2.9 records a second resume value and never consults it, persists-invalid state silently, and re-executes durably recorded work after a real SIGKILL.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• ReDraft, Don't Just Distill: Reference-Driven Revision for Continual VLLM Post-Training [66.72708893922605]
  Post-training of large multimodal models should add new capabilities while preserving those from pre-training.<n>SFT gives explicit target supervision that learns a task from near-zero accuracy, but its off-policy targets move the model far enough to cause forgetting.<n>We introduce ReDraft, which obtains both from the model's own failures.
  arXiv  Detail & Related papers  (2026-09-15T04:59:03Z)
• Calibration is the Bottleneck: An Action-Class Diagnostic of Multi-Turn Tool-Calling [65.03665015319457]
  We propose an action-class-oriented diagnostic framework that decomposes multi-turn failures into two modes: action-class miscalibration and action-execution failure.<n>We validate it on a panel of tool-calling models across multiple multi-turn benchmarks.
  arXiv  Detail & Related papers  (2026-09-01T09:08:15Z)
• AGM: Achievement-Grounded Memory for Closed-Loop Agents with Frozen VLA Policies [17.09836507714724]
  We propose Achievement-Grounded Memory (AGM) for frozen vision-language-action (VLA) policies.<n>AGM represents a task as a subgoal sequence with a progress pointer and advances this memory only after the current subgoal is verified by physical evidence.<n>On the RoboMME Counting benchmark, AGM reaches on PickXTimes and on BinFill, surpassing the strongest memory-augmented baseline by points on average.
  arXiv  Detail & Related papers  (2026-08-30T03:50:49Z)
• Independent Patch Verification for Coding Agents with a Bidirectional Reconstruct-and-Verify Framework [49.16055123488827]
  coding agents powered by large language models can now generate code patches directly from bug reports.<n>No mechanism independently verifies whether it truly resolves the reported problem.<n>We propose RETRACE, a training-free post-generation verification framework.
  arXiv  Detail & Related papers  (2026-08-09T22:59:13Z)
• TraceCompiler: Skill-Guided Mining and Compilation of LLM Agent Traces into Mostly Deterministic Workflows [2.435006380732194]
  We present TraceCompiler, a skill-guided system that compiles noisy traces into trajectories.<n>Every hard edge carries an auditable evidence, and ambiguous relations are marked suspected.<n>We measure call reduction but not offline compilation cost, so we claim no net efficiency result.
  arXiv  Detail & Related papers  (2026-08-03T01:05:06Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• Stop Means Stop: Measuring and Repairing the Enforcement Gap in Agent-Framework Control Primitives [0.0]
  This contract holds on none of six widely used open-source frameworks.<n>Model-free differential probes isolate a recurring sibling leak.<n>SoundGATE is an environment-external Rust gate through which every side effect must be admitted.
  arXiv  Detail & Related papers  (2026-07-15T05:55:38Z)
• MemOps: Benchmarking Lifecycle Memory Operations in Long-Horizon Conversations [50.24315431387575]
  We introduce MemOps, a benchmark that reformulates conversational memory as a sequence of lifecycle operations.<n>MemOps represents each memory event with a structured trace specifying its trigger, target, scope, state transition, and supporting evidence.<n>Across long-context, retrieval-based, parametric and managed-memory systems, MemOps disentangles failure modes that final-answer accuracy alone conceals.
  arXiv  Detail & Related papers  (2026-07-14T15:33:44Z)
• Lingering Authority: Revocable Resource-and-Effect Capabilities for Coding Agents [0.0]
  PORTICO is a reference monitor for capabilities exposed to the planner.<n>It compiles an explicit task contract into initial capabilities, grant rules, trusted closure predicates, and global deny rules.
  arXiv  Detail & Related papers  (2026-06-21T13:52:37Z)
• Getting Better at Working With You: Compiling User Corrections into Runtime Enforcement for Coding Agents [99.67681154381803]
  Test-time Rule Acquisition and Compiled Enforcement (TRACE) is a skill-layer pipeline for coding-agent runtimes.<n>Unlike runtime checks written ahead of time by developers, TRACE skills come from the user's own chat corrections.
  arXiv  Detail & Related papers  (2026-06-11T10:43:40Z)
• Regimes: An Auditable, Held-Out-Gated Improvement Loop Demonstrated on LongMemEval with ActiveGraph [0.0]
  We show that an event-sourced agent runtime turns controlled improvement into a first-class workflow.<n>When the agent's state is a deterministic projection of an append-only event log, failures are recorded, a run replays exactly from its log, and candidate patches scope to typed pipeline seams, gates are auditable.<n>We demonstrate this with Regimes, a loop on the ActiveGraph runtime that diagnoses failed evaluations, proposes a repair at a pipeline point, and promotes it only after static checks, sandbox execution, in-sample evaluation, and held-out validation.
  arXiv  Detail & Related papers  (2026-06-08T23:04:35Z)
• Overeager Coding Agents: Measuring Out-of-Scope Actions on Benign Tasks [40.270213696031625]
  OverEager-Gen is a benchmark dedicated to overeager behavior on benign tasks.<n>On Claude Code, stripping the consent declaration alone raises the overeager rate from 0.0% to 17.1%.<n>OverEager-Gen therefore certifies each scenario's discriminative power before admission.
  arXiv  Detail & Related papers  (2026-05-18T16:00:41Z)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  Safety-aligned large language models (LLMs) are increasingly deployed in real-world pipelines.<n> adversaries can distribute backdoored checkpoints that behave normally under standard evaluation but jailbreak when a hidden trigger is present.<n>Recent post-hoc weight-editing methods offer an efficient approach to injecting such backdoors.
  arXiv  Detail & Related papers  (2026-04-14T06:48:33Z)
• AgentSys: Secure and Dynamic LLM Agents Through Explicit Hierarchical Memory Management [47.49917373646469]
  Existing defenses treat bloated memory as given and focus on remaining resilient.<n>We present AgentSys, a framework that defends against indirect prompt injection through explicit memory management.
  arXiv  Detail & Related papers  (2026-02-07T06:28:51Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.