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 →
Mnemosyne: Agentic Transaction Processing for Validating and Repairing AI-generated Workflows
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
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.
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
- 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.
Referee Report
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)
- [§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–§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.
- [§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)
- [§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.
- [§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.
- [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).
- [§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.
- [§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.
- [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
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
free parameters (3)
- LCRP iteration cap K
- Displacement budget δ_max
- Cost weights λ_o, λ_j, λ_w, λ_s in J
axioms (5)
- domain assumption Gate closure: only the admission gate may append domain truth to CTL; proposers emit packages only.
- domain assumption Trusted finite executable constraint set C is decidable for the artifact workloads and is the sole semantic authority.
- standard math Append to CTL is atomic; StateView is derived only from effective committed records.
- domain assumption Conflict-scope contract serializes or rejects overlapping incompatible proposals.
- domain assumption In-flight repairs remain uncommitted proposals; pending observation set D_k retains all unabsorbed disruptions.
invented entities (4)
-
Agentic Transaction Processing (ATP) admission boundary
independent evidence
-
Active Commitment Records (ACRs)
independent evidence
-
StateView effective-state projection
independent evidence
-
LCRP (localized cascading repair protocol)
independent evidence
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
Forward citations
Cited by 2 Pith papers
-
Looping Is Not Reliability: State-Bound Evidence and Typed Revision Contracts for Agentic Code Repair
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...
-
TRW: TRACE-RealWorld---An Auditable Consistency Contract for World Models as Materialized Views
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
-
[1]
Mnemosyne: Agentic Transaction Processing Evaluation Artifact , year =
-
[2]
Bernstein and Eric Newcomer , title =
Philip A. Bernstein and Eric Newcomer , title =
-
[3]
Jim Gray and Andreas Reuter , title =
-
[4]
Gerhard Weikum and Gottfried Vossen , title =
-
[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 =
1992
-
[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 =
1987
-
[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 =
2001
-
[8]
Silva , title =
Juliana Freire and David Koop and Emanuele Santos and Claudio T. Silva , title =. Computing in Science & Engineering , volume =. 2008 , doi =
2008
-
[9]
Simmhan and Beth Plale and Dennis Gannon , title =
Yogesh L. Simmhan and Beth Plale and Dennis Gannon , title =. SIGMOD Record , volume =. 2005 , doi =
2005
-
[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 =
2006
-
[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 =
2005
-
[12]
Argo Workflows Documentation , year =
-
[13]
Cadence: A Distributed, Scalable, Durable Orchestration Engine , year =
-
[14]
Temporal Documentation: Durable Execution , year =
-
[15]
2005 , howpublished =
Martin Fowler , title =. 2005 , howpublished =
2005
-
[16]
2011 , howpublished =
Martin Fowler , title =. 2011 , howpublished =
2011
-
[17]
Paton and Oscar Díaz , title =
Norman W. Paton and Oscar Díaz , title =. ACM Computing Surveys , volume =. 1999 , doi =
1999
-
[18]
Chang and Longling Geng , title =
Edward Y. Chang and Longling Geng , title =. Proceedings of the VLDB Endowment , volume =. 2025 , doi =
2025
-
[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]
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]
2023 , howpublished =
Noah Shinn and Federico Cassano and Ashwin Gopinath and Karthik Narasimhan and Shunyu Yao , title =. 2023 , howpublished =
2023
-
[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 =
2023
-
[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 =
2023
-
[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]
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]
2023 , howpublished =
Andy Zhou and Kai Yan and Michal Shlapentokh-Rothman and Haohan Wang and Yu-Xiong Wang , title =. 2023 , howpublished =
2023
-
[27]
Chang, Edward Y. , title =. 2025 , note =. doi:10.1145/3749421 , isbn =
doi:10.1145/3749421 2025
-
[28]
, title =
Chang, Edward Y. , title =. 2026 , doi =
2026
-
[29]
2026 , eprint=
Trivium: Temporal Regret as a First-Class Objective for Causal-Memory Controllers , author=. 2026 , eprint=
2026
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.