Pith. sign in

REVIEW 3 major objections 6 minor 2 cited by

Generated workflow actions are untrusted proposals until a deterministic gate admits them under a declared constraint set, so committed correctness no longer depends on the model that proposed them.

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 →

T0 review · grok-4.5

2026-07-12 09:37 UTC pith:K7CWKOLK

load-bearing objection Solid systems paper: authority separation for untrusted LLM proposals is real, theorems and artifact hold relative to C, residual risk is C-completeness not the gate. the 3 major comments →

arxiv 2607.00269 v2 pith:K7CWKOLK submitted 2026-06-30 cs.AI

Mnemosyne: Agentic Transaction Processing for Validating and Repairing AI-generated Workflows

classification cs.AI
keywords agentic transaction processingLLM agentstransaction processingworkflow validation and repairdata integrityadmission controlevidence-preserving repairbounded reactive repair
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.

Large language models now draft and repair workflows at scale, but a syntactically valid plan can still be stale, infeasible, conflicting, or designed to erase the evidence that justified a repair. This paper introduces Agentic Transaction Processing: every generated action is treated as a proposal that earns committed status only by passing deterministic admission against a declared, executable constraint set and the current effective state. Anything may propose—an LLM, a fired obligation, a runtime driver—but only the runtime admits and commits. When the world produces a disruption no plan foresaw, the system repairs locally within bounds and routes that repair back through the same gate. Relative to the constraint set, committed-state correctness becomes independent of how smart, honest, or well-trained the proposer is. The authors realize the model in an open-source runtime and show, across falsification tests and live LLM pilots, that invalid commits are rejected while valid work still lands.

Core claim

The paper establishes that committed-state correctness for AI-generated workflows can be decoupled from the intelligence layer: under a trusted executable constraint set and a gate-closure assumption, only deterministic admission may append committed truth, so a stronger model improves usefulness while a faulty or adversarial one only produces more rejections—never invalid commits relative to that constraint set.

What carries the argument

Agentic Transaction Processing (ATP): a two-sided authority boundary in which generated actions are proposals, not truth, and a deterministic admission gate under constraint set C, backed by an append-only committed-transition log, effective-state projection, dependency-closed compensation, and non-authoritative active commitment records, is the only path that turns a proposal into durable state; unforeseen disruptions are handled by a bounded local repair protocol whose output re-enters the same gate.

Load-bearing premise

The system must truly prevent every proposer, driver, and wakeup from writing committed truth except by going through the admission gate—an assumption enforced by construction and tests, not by a machine-checked proof that no code path can bypass it.

What would settle it

Run the nine released falsification benchmarks and the live mid-execution repair pilot: if any invalid commit, evidence-destroying repair, unauthorized wakeup mutation, or orphaned effective dependent appears in committed state while the declared constraints are intact, the central authority-separation claim fails.

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

If this is right

  • Workflow engines and multi-agent planners can keep using LLMs for proposal generation without letting model errors become durable domain truth.
  • Repairs that try to succeed by deleting failing tests, suppressing alerts, or hiding violated guards are rejected before commit rather than only audited after the fact.
  • Active obligations may wake and propose mid-execution, but cannot themselves mutate the committed log or effective state.
  • Bounded local repair can absorb a mid-run disruption by editing far fewer operations than a full recompute while still requiring re-admission.
  • Proposer quality then governs how much useful work is admitted, not whether invalid work can commit.

Where Pith is reading between the lines

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

  • Authoring and maintaining a faithful constraint set becomes a first-class data-management skill for agentic systems, comparable to schema design in classical databases.
  • The same admission boundary could sit under non-LLM generators—classical solvers, human operators, or learned policies—without changing the correctness contract.
  • If gate closure were later machine-checked rather than only tested, the safety theorems would become hard guarantees about the implementation, not only about executions that obey the assumption.
  • Evidence-preserving repair suggests a general pattern for any self-modifying agent stack: a fix must not be allowed to discharge its own alarm by destroying the signal that raised it.

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

3 major / 6 minor

Summary. The paper introduces Agentic Transaction Processing (ATP): LLM-generated workflow actions, repairs, and plans are treated as untrusted proposals that become committed truth only after deterministic admission under a declared executable constraint set C. The model is realized in Mnemosyne (append-only CTL, StateView effective-state projection, dependency-closed compensation, Active Commitment Records, and LCRP for bounded reactive repair). Four safety theorems relative to C (authority separation / IDC, serial-equivalent generative admission, evidence-preserving repair, obligation containment) plus bounded-reactive-repair and recursive-recovery reductions are stated and proved by induction under gate closure. Evaluation comprises nine falsification benchmarks with zero targeted violations, a mechanism-level workflow/saga comparator, a cost audit (<6% projection+validation overhead), an LCRP containment study, and bounded live-proposer pilots (80 proposals from four LLMs, zero invalid commits).

Significance. If the results hold as scoped, this is a clear systems contribution: it reframes the agentic-workflow problem as an admission boundary rather than a smarter planner, and cleanly separates proposer usefulness from committed-state correctness relative to C. Evidence-preserving repair and non-authoritative ACR wakeups have no classical analogue and address real failure modes (alarm silencing, ungoverned memory). Strengths that should be credited: open-source artifact with a reproducible nine-test safety suite; explicit relativity of all guarantees to C and gate closure; live heterogeneous LLM pilots scored by an external harness; and a containment study showing order-of-magnitude fewer edits than global recompute. The work complements agent-side discipline (e.g., SagaLLM) from the data-management end and is a natural fit for a systems/DB venue.

major comments (3)
  1. [§3 Guarantees; Conclusion] §3 (Gate closure) and Conclusion: Authority separation (Theorem 1 / IDC) is load-bearing on gate closure, which the paper enforces by construction and regression tests, not by a machine-checked noninterference argument over the Python codebase. The nine falsification tests and live pilots support the tested paths, but residual bypass surface (drivers, ACR continuations, outbox, storage adapters) remains an assumption rather than a closed proof. For the central claim to transfer from the model to the artifact, the manuscript should either (a) state a concrete residual threat model with the regression suite as the evidence, or (b) add a short noninterference/audit argument over the commit path. As written, the theorem is sound under the assumption; the implementation claim is only partially closed.
  2. [§2–§3; Appendix Q; Limitations] §2–§3 and Limitations: All guarantees are relative to an application-authored finite C. Theorem 1 and the Conclusion correctly state that hazards outside C are undetected, but the evaluation only shows that the harness C catches the hazards the authors encoded (stale-world, evidence-destroying repair, orphaning compensation, etc.). There is no measurement of C-completeness, authoring cost, or residual semantic risk (C-valid yet still wrong for the application) under live proposers. This does not break the systems claim as stated, but it is the softest place IDC can be over-read. A short subsection quantifying residual risk (e.g., fraction of live rejections that are safety vs. incompleteness of C; guidance on authoring C from FSMs/schemas as in Appendix Q) would make the practical scope of intelligence-decoupled correctness precise.
  3. [§5.7 RQ6; Table 7] §5.7 RQ6: Containment (edit radius, J) is measured on a companion job-shop harness (MAPLE) that 'implements the same bounded-repair protocol,' not on the Mnemosyne artifact used for RQ1–RQ5. The claim that LCRP edits an order of magnitude fewer operations than global recompute is therefore a protocol-level result, not a Mnemosyne end-to-end result. Either run the same disruption suite through Mnemosyne's reactive path, or clearly reframe RQ6 as a protocol property of LCRP with an explicit equivalence argument to Mnemosyne's admission+ACR loop. Without that, the systems claim for Mnemosyne's reactive half is only partially evidenced.
minor comments (6)
  1. [§5.3 RQ2; Appendix J] §5.3 RQ2: The guardrail comparator is correctly labeled mechanism-level, not a product benchmark of Temporal/Cadence/LangGraph. Consider moving the production-TP coverage audit (Appendix J) into the main RQ2 discussion so the 'not just input validation' claim is harder to miss.
  2. [§5.4 RQ3; Table 5] §5.4 RQ3: Pilots are deliberately bounded (one task family, 40+40 proposals). The text already avoids planning-quality claims; a single sentence on statistical power and planned confirmatory scale would reduce over-reading of the 0.90/0.93 horizon rewards.
  3. [Figure 1; §2.3] Figure 1 and Table 1: The assurance web is helpful; ensure every invariant name in the figure matches the formal invariant list in §2.3 / appendix exactly (e.g., 'no invalid commit' vs. DA wording).
  4. [§3.2; §5.7 Table 7] Free parameters K, δ_max, and cost weights λ in J (§3.2, §5.7) are stated but not sensitivity-analyzed. A brief note that containment conclusions are robust under reasonable λ ranges would strengthen Table 7.
  5. [§6 Related Work; §2.2.2] Related Work: The SagaLLM duality is clear; a one-line contrast with classical integrity constraints / CHECK constraints would further answer the 'is this just input validation?' objection already addressed in §2.2.2.
  6. [References; §5.8] Minor polish: arXiv id 2607.00269 and 2026 dates are consistent with the preprint; ensure camera-ready citation keys for Temporal/Cadence access dates and the Mnemosyne tag match the artifact README.

Circularity Check

0 steps flagged

No significant circularity: safety theorems are architectural guarantees by construction under stated assumptions, not fitted or self-definitional predictions.

full rationale

The paper's load-bearing claims (Authority-Separation / IDC, SEA, EPR, OC, LCRP) are systems-safety theorems proved by induction on the committed-transition log under two explicit assumptions: a trusted executable constraint set C and gate closure. Theorem 1 is intentionally simple once the gate is trusted—if only C-valid transitions append, committed state is C-valid—and the paper states this openly, locating the contribution in the structure of C and the effective-state witness rather than in a non-tautological implication. That is ordinary systems architecture, not a fitted parameter renamed as a prediction. Guarantees are scoped as relative to C; incomplete C is acknowledged as outside the claim. Evaluation is falsification of the implemented gate (permissive baselines commit targeted violations; ATP commits zero) plus bounded live-proposer pilots scored by an external harness—not a derivation that reduces to its own inputs. Self-citations to SagaLLM and REALM-Bench supply complementary prior work and the benchmark substrate; they do not underwrite the inductive proofs or force uniqueness of the model. No uniqueness theorem is imported, no ansatz is smuggled via citation, and no empirical pattern is merely renamed. Residual risk (un-machine-checked gate closure; application-authored C completeness) is scope/assumption risk, not circularity of the derivation chain.

Axiom & Free-Parameter Ledger

3 free parameters · 5 axioms · 4 invented entities

The central claim rests on a trusted executable constraint set C, gate closure of the implementation, and several system objects (CTL, StateView, ACRs, LCRP bounds) that define the admission and repair substrate. No numerical parameters are fitted to scientific data; free parameters are engineering bounds (K, δ_max, cost weights) used in the repair evaluation, not in the safety theorems. Axioms are standard TP assumptions plus domain assumptions that C is decidable and that only admitted appends extend committed truth.

free parameters (3)
  • LCRP iteration cap K
    Engineering bound on revalidation rounds for localized repair; used in Proposition 1 and RQ6, not fitted to prove safety theorems.
  • Displacement budget δ_max
    Edit-radius budget for bounded reactive repair; containment claim depends on this declared bound.
  • Cost weights λ_o, λ_j, λ_w, λ_s in J
    Sensitivity model for RQ6 cost-aware objective (1,5,1,10); chosen by hand for the job-shop containment study.
axioms (5)
  • domain assumption Gate closure: only the admission gate may append domain truth to CTL; proposers emit packages only.
    Stated as assumption for all theorems in §3; enforced by construction and regression tests, not machine-checked noninterference.
  • domain assumption Trusted finite executable constraint set C is decidable for the artifact workloads and is the sole semantic authority.
    All guarantees are relative to C; incomplete C means undetected hazards (§2.3, §3).
  • standard math Append to CTL is atomic; StateView is derived only from effective committed records.
    Standard log/projection assumptions used in Theorems 1–2 and ESS/DCC.
  • domain assumption Conflict-scope contract serializes or rejects overlapping incompatible proposals.
    Required for serial-equivalent generative admission (Theorem 2).
  • domain assumption In-flight repairs remain uncommitted proposals; pending observation set D_k retains all unabsorbed disruptions.
    Premises of Lemma 1 and Proposition 3 on recursive recovery.
invented entities (4)
  • Agentic Transaction Processing (ATP) admission boundary independent evidence
    purpose: Treat generated actions as untrusted proposals until deterministic admission under C.
    Core model contribution; independent evidence via open artifact and falsification tests.
  • Active Commitment Records (ACRs) independent evidence
    purpose: Durable obligations that may wake and propose but never mutate committed truth directly.
    Implements obligation containment; weaker than classical ECA write actions.
  • StateView effective-state projection independent evidence
    purpose: Admission witness excluding compensated/superseded history.
    Mechanism for ESS and stale-world rejection.
  • LCRP (localized cascading repair protocol) independent evidence
    purpose: Bounded reactive repair under edit radius and iteration cap that re-enters admission.
    Reactive half of the two-sided principle; measured on job-shop harness.

pith-pipeline@v1.1.0-grok45 · 40448 in / 3327 out tokens · 29239 ms · 2026-07-12T09:37:47.536439+00:00 · methodology

0 comments
read the original abstract

LLMs increasingly generate workflow actions, repairs, and plans, but a generated action may be syntactically valid yet stale, infeasible, conflicting, or destructive of the evidence that triggered a repair. We introduce Agentic Transaction Processing (ATP), a transaction model that treats generated actions as untrusted proposals until they pass deterministic admission under a declared, executable constraint set C. The governing principle is two-sided: a proposal is not truth, and no proposal foresees every disruption. Anything may propose, but only the runtime admits and commits; when an unforeseen disruption strikes, it repairs reactively within bounds rather than trusting a fresh proposal. Relative to C, committed-state correctness becomes independent of the competence, honesty, or learning of the proposing layer. We realize ATP in Mnemosyne, a runtime with an append-only transition log, effective-state projection, dependency-safe compensation, and active commitment records, and prove four safety properties relative to C (authority separation, serial-equivalent generative admission, evidence-preserving repair, and obligation containment) plus a bounded-reactive-repair guarantee (LCRP). A reproducible artifact rejects the targeted violations across nine falsification tests while still admitting valid work, at under 6% overhead, and local repair edits an order of magnitude fewer operations than global recompute. In live-proposer pilots, 80 static plan-entry and mid-execution repair proposals from four heterogeneous LLMs pass the same admission boundary, scored by an external cross-episode harness with zero invalid commits; the gate admits 24 of 40 live repair proposals and rejects 16, four as explicit safety rejections of over-broad rollback. Mnemosyne is open source: https://github.com/eyuchang/Mnemosyne/tree/mnemosyne-atp-postgres-rerun

Figures

Figures reproduced from arXiv: 2607.00269 by Edward Y. Chang, Emily J. Chang, Longling Geng.

Figure 1
Figure 1. Figure 1: ATP separates proposal generation, validated admission, durable commit, and effective [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 1
Figure 1. Figure 1: The assurance web: each executable invariant (left, checked by the gate on every event) is [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Bounded reactive repair vs. global recompute on a disrupted plan (illustrative; the [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 2
Figure 2. Figure 2: Bounded reactive repair vs. global recompute on a disrupted plan (illustrative; the [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: System architecture. Proposers generate packages; deterministic admission under [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figure 3
Figure 3. Figure 3: System architecture. Proposers generate packages; deterministic admission under [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Violation suppression across the nine benchmarks. Amber bars show the most permissive [PITH_FULL_IMAGE:figures/full_fig_p014_4.png] view at source ↗
Figure 4
Figure 4. Figure 4: Violation suppression across the nine benchmarks. Amber bars show the most permissive [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: RQ3 proposer-quality profile under ATP. Stronger proposers produce more admissi [PITH_FULL_IMAGE:figures/full_fig_p017_5.png] view at source ↗
Figure 5
Figure 5. Figure 5: RQ4 proposer-quality profile under ATP: stronger proposers produce more admissible [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Storage substrate boundary. SQLite is the deterministic default; PostgreSQL and pooled [PITH_FULL_IMAGE:figures/full_fig_p027_6.png] view at source ↗
Figure 6
Figure 6. Figure 6: Storage substrate boundary. PostgreSQL (and pooled PostgreSQL for concurrency) is the [PITH_FULL_IMAGE:figures/full_fig_p030_6.png] view at source ↗

discussion (0)

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

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Looping Is Not Reliability: State-Bound Evidence and Typed Revision Contracts for Agentic Code Repair

    cs.CL 2026-07 conditional novelty 6.0

    Correctness is non-absorbing under forced revision, stale traces harm retained fixes by ~22 points on a 14B coder, and a typed state-bound loop contract makes admission and checkpoints enforceable without proving bett...

  2. TRW: TRACE-RealWorld---An Auditable Consistency Contract for World Models as Materialized Views

    cs.AI 2026-07 conditional novelty 6.0

    TRACE-RealWorld wraps world-model predictions in a consistency contract: refresh and compensation alone cannot eliminate stale commitments, and their composition bounds violations under named, measured assumptions.

Reference graph

Works this paper leans on

29 extracted references · cited by 2 Pith papers

  1. [1]

    Mnemosyne: Agentic Transaction Processing Evaluation Artifact , year =

  2. [2]

    Bernstein and Eric Newcomer , title =

    Philip A. Bernstein and Eric Newcomer , title =

  3. [3]

    Jim Gray and Andreas Reuter , title =

  4. [4]

    Gerhard Weikum and Gottfried Vossen , title =

  5. [5]

    Mohan and Don Haderle and Bruce Lindsay and Hamid Pirahesh and Peter Schwarz , title =

    C. Mohan and Don Haderle and Bruce Lindsay and Hamid Pirahesh and Peter Schwarz , title =. ACM Transactions on Database Systems , volume =. 1992 , doi =

  6. [6]

    Proceedings of the 1987 ACM SIGMOD International Conference on Management of Data , pages =

    Hector Garcia-Molina and Kenneth Salem , title =. Proceedings of the 1987 ACM SIGMOD International Conference on Management of Data , pages =. 1987 , doi =

  7. [7]

    Proceedings of the 8th International Conference on Database Theory (ICDT 2001) , pages =

    Peter Buneman and Sanjeev Khanna and Wang-Chiew Tan , title =. Proceedings of the 8th International Conference on Database Theory (ICDT 2001) , pages =. 2001 , doi =

  8. [8]

    Silva , title =

    Juliana Freire and David Koop and Emanuele Santos and Claudio T. Silva , title =. Computing in Science & Engineering , volume =. 2008 , doi =

  9. [9]

    Simmhan and Beth Plale and Dennis Gannon , title =

    Yogesh L. Simmhan and Beth Plale and Dennis Gannon , title =. SIGMOD Record , volume =. 2005 , doi =

  10. [10]

    Lee and Jing Tao and Yang Zhao , title =

    Bertram Ludäscher and Ilkay Altintas and Chad Berkley and Dan Higgins and Efrat Jaeger and Matthew Jones and Edward A. Lee and Jing Tao and Yang Zhao , title =. Concurrency and Computation: Practice and Experience , volume =. 2006 , doi =

  11. [11]

    Nick Russell and Arthur H. M. ter Hofstede and David Edmond and Wil M. P. van der Aalst , title =. CAiSE 2005 , series =. 2005 , doi =

  12. [12]

    Argo Workflows Documentation , year =

  13. [13]

    Cadence: A Distributed, Scalable, Durable Orchestration Engine , year =

  14. [14]

    Temporal Documentation: Durable Execution , year =

  15. [15]

    2005 , howpublished =

    Martin Fowler , title =. 2005 , howpublished =

  16. [16]

    2011 , howpublished =

    Martin Fowler , title =. 2011 , howpublished =

  17. [17]

    Paton and Oscar Díaz , title =

    Norman W. Paton and Oscar Díaz , title =. ACM Computing Surveys , volume =. 1999 , doi =

  18. [18]

    Chang and Longling Geng , title =

    Edward Y. Chang and Longling Geng , title =. Proceedings of the VLDB Endowment , volume =. 2025 , doi =

  19. [19]

    Chang , title =

    Longling Geng and Edward Y. Chang , title =. Proceedings of the 32nd ACM SIGKDD Conference on Knowledge Discovery and Data Mining , year =

  20. [20]

    O'Brien and Carrie J

    Joon Sung Park and Joseph C. O'Brien and Carrie J. Cai and Meredith Ringel Morris and Percy Liang and Michael S. Bernstein , title =. Proceedings of the 36th Annual ACM Symposium on User Interface Software and Technology , year =

  21. [21]

    2023 , howpublished =

    Noah Shinn and Federico Cassano and Ashwin Gopinath and Karthik Narasimhan and Shunyu Yao , title =. 2023 , howpublished =

  22. [22]

    2023 , howpublished =

    Guanzhi Wang and Yuqi Xie and Yunfan Jiang and Ajay Mandlekar and Chaowei Xiao and Yuke Zhu and Linxi Fan and Anima Anandkumar , title =. 2023 , howpublished =

  23. [23]

    2023 , howpublished =

    Lei Wang and Chen Ma and Xueyang Feng and Zeyu Zhang and Hao Yang and Jingsen Zhang and Zhiyuan Chen and Jiakai Tang and Xu Chen and Yankai Lin and Wayne Xin Zhao and Zhewei Wei and Ji-Rong Wen , title =. 2023 , howpublished =

  24. [24]

    Griffiths and Yuan Cao and Karthik Narasimhan , title =

    Shunyu Yao and Dian Yu and Jeffrey Zhao and Izhak Shafran and Thomas L. Griffiths and Yuan Cao and Karthik Narasimhan , title =. Advances in Neural Information Processing Systems , volume =

  25. [25]

    Proceedings of the 11th International Conference on Learning Representations , year =

    Shunyu Yao and Jeffrey Zhao and Dian Yu and Nan Du and Izhak Shafran and Karthik Narasimhan and Yuan Cao , title =. Proceedings of the 11th International Conference on Learning Representations , year =

  26. [26]

    2023 , howpublished =

    Andy Zhou and Kai Yan and Michal Shlapentokh-Rothman and Haohan Wang and Yu-Xiong Wang , title =. 2023 , howpublished =

  27. [27]

    , title =

    Chang, Edward Y. , title =. 2025 , note =. doi:10.1145/3749421 , isbn =

  28. [28]

    , title =

    Chang, Edward Y. , title =. 2026 , doi =

  29. [29]

    2026 , eprint=

    Trivium: Temporal Regret as a First-Class Objective for Causal-Memory Controllers , author=. 2026 , eprint=