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

# Mnemosyne: Agentic Transaction Processing for Validating and Repairing AI-generated Workflows
Source: [https://arxiv.org/html/2607.00269](https://arxiv.org/html/2607.00269)
###### Abstract

LLMs, solvers, and agent teams 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𝒞\\mathcal\{C\}\. The 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, and when an unforeseen disruption strikes it repairs reactively within bounds rather than trusting a fresh proposal\. Relative to𝒞\\mathcal\{C\}, committed\-state correctness becomes independent of the competence, honesty, or learning of the proposing layer\. We realizeATPinMnemosyne, 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𝒞\\mathcal\{C\}\(authority separation, serial\-equivalent generative admission, evidence\-preserving repair, and obligation containment\) together with a bounded\-reactive\-repair guarantee for its localized repair protocol \(LCRP\)\. A reproducible artifact rejects the targeted violations across nine falsification tests while still admitting valid work, at under6%6\\%projection\-and\-validation overhead, and bounded local repair edits an order of magnitude fewer operations than global recompute\.Mnemosyneis open source:https://github\.com/eyuchang/Mnemosyne/tree/arxiv\-atp\-rq1\-rq9b\-r8\-v2\.

## 1Introduction

Database systems have long separated logical correctness from physical execution through transactions, recovery, isolation, logging, and integrity constraintsGray and Reuter \([1993](https://arxiv.org/html/2607.00269#bib.bib3)\); Bernstein and Newcomer \([2009](https://arxiv.org/html/2607.00269#bib.bib2)\); Weikum and Vossen \([2001](https://arxiv.org/html/2607.00269#bib.bib4)\); Mohanet al\.\([1992](https://arxiv.org/html/2607.00269#bib.bib5)\)\. Workflow systems extend these ideas to long\-running activities with retries, timeouts, idempotency, and compensationGarcia\-Molina and Salem \([1987](https://arxiv.org/html/2607.00269#bib.bib6)\); Ludäscheret al\.\([2006](https://arxiv.org/html/2607.00269#bib.bib10)\); Russellet al\.\([2005](https://arxiv.org/html/2607.00269#bib.bib11)\)\. Both families, however, usually assume that the submitted unit of work is meaningful enough to be treated as a transaction request: it may conflict, fail, or abort, but it is not itself a hallucinated, stale, or semantically invalid proposal produced by an untrusted reasoning process\.

Agentic workflows violate this assumption\. The candidate transaction may be generated by a language model, an optimization solver, or a team of agents, including prior multi\-agent planning systems that add validation and transaction\-style guaranteesChang and Geng \([2025](https://arxiv.org/html/2607.00269#bib.bib19)\); Yaoet al\.\([2023b](https://arxiv.org/html/2607.00269#bib.bib26),[a](https://arxiv.org/html/2607.00269#bib.bib25)\); Shinnet al\.\([2023](https://arxiv.org/html/2607.00269#bib.bib22)\); Wanget al\.\([2023a](https://arxiv.org/html/2607.00269#bib.bib23)\); Parket al\.\([2023](https://arxiv.org/html/2607.00269#bib.bib21)\); Wanget al\.\([2023b](https://arxiv.org/html/2607.00269#bib.bib24)\); Chang \([2025](https://arxiv.org/html/2607.00269#bib.bib28)\)\. Yet a well\-formed proposal can still be wrong in ways a syntactic check accepts\.

Consider a concrete case from multi\-agent planningChang and Geng \([2025](https://arxiv.org/html/2607.00269#bib.bib19)\)\. In a family’s Thanksgiving plan, the father lands in Boston and picks up Grandma on the way home so dinner can start on time\. His flight is delayed, so an LLM agent reactively replans the afternoon’s pickups and drives\. The new schedule parses as valid, yet two faults slip through\. It reuses the off\-peak drive time from the original 3 pm plan, ignoring that the delayed pickup now lands in rush\-hour traffic, so the rescheduled pickup is physically impossible\. And after reshuffling the drivers, it silently drops Grandma’s pickup, leaving her stranded so dinner never starts\.

A conventional transaction layer would commit this well\-formed schedule and inherit both faults\.ATPinstead routes each revised assignment through a deterministic gate against the declared constraint set𝒞\\mathcal\{C\}over the current effective state \(theStateView\)\. The infeasible pickup is rejected because its travel time violates𝒞\\mathcal\{C\}; the replan is rejected for dropping Grandma’s pickup, since a committed obligation cannot silently disappear\. Feasible reassignments commit; the rest are rejected with a recorded reason\. The durable guarantee thus comes from outside the model: a stronger planner gets more of the day right, but none can erase a standing commitment or commit a physically impossible plan\.

Admission stops bad proposals, but some failures are not proposals at all\. Suppose the gate has committed a feasible afternoon and execution begins, and then an*unforeseen*disruption strikes that no policy anticipated: a highway closure makes the committed airport leg infeasible in mid\-execution\. No pre\-registered compensation covers it\. HereATPdoes not merely reject; it*reacts*\. The affected commitment wakes and launches a*bounded local repair*that re\-times only the disrupted leg and its dependents, leaving the rest of the day untouched, and the repair it produces re\-enters the same admission gate\. A wrong reactive repair is caught exactly like any other proposal, while the blast radius stays contained to the affected region instead of forcing a full re\-plan\. Static admission and bounded reactive repair are thus two halves of one boundary: nothing becomes truth, whether first proposed or repaired, without passing the gate\.

The failure boundary is no longer only the commit protocol\. It is the transition from generated intent to durable truth\. For agentic workflows, the first transaction question is not merely “can this transaction commit?” but:*should this generated proposal be admitted as a transaction at all?*

This paper introduces*Agentic Transaction Processing*\(ATP\), a transaction model for generated workflows\.111We use*workflow*and*transaction*in their classical senses, not as synonyms\. A workflow is a*sequence*of actions and state transitions enacted to accomplish a task; a transaction is a*unit of work*executed with atomicity, isolation, consistency, and durability guarantees, so “transactional” names a property of how a unit of work commits, not the action sequence itself\. A generated workflow step becomes a transaction only when the data layer admits and commits it under these guarantees, andATPgoverns precisely that boundary\.What is new is not the failure but the proposer\. Capable AI now drafts and repairs workflows at a speed and scale no human author matches, and that is genuinely useful: an LLM or agent can react to a disruption no designer anticipated and propose a fix in seconds\. But the same models hallucinate, and they are*sycophantic*\(asked to validate their own plan, they tend to endorse it\), so the proposer cannot be its own judge\. Speed, autonomy, and reactivity are exactly what we want from AI, and exactly what makes an unguarded transaction layer dangerous: we can neither simply trust the proposer nor surrender the automation\.ATPkeeps both\. It admits AI, solver, agent, and trigger output as*untrusted proposals*that only a deterministic gate may turn into committed truth, so the system stays smart and reactive where it proposes while remaining correct where it commits\. The central rule is:

*A proposal is not truth, and no proposal foresees every disruption\.*

Generated actions may propose\. Active workflow obligations may wake\. Solvers may repair\. Runtime drivers may orchestrate\. But only the transaction layer may admit and commit\. And the first clause is not the whole story: no proposal, however well admitted, foresees every future disruption, soATPdoes not stop at the gate\.

This yields a separation that classical transaction processing never needed\. Because every generated action, repair, and learned policy is a proposal that only the gate may admit,*committed\-state correctness is decoupled from the intelligence layer*\. Relative to a declared constraint set𝒞\\mathcal\{C\}, a more capable model produces better proposals, while a faulty or adversarial one produces more rejected work, but neither can write committed truth that violates𝒞\\mathcal\{C\}\. Intelligence governs usefulness; the transaction layer governs correctness, and building that layer is a data\-management problem: it lives in a committed transition log, an effective\-state projection, and a deterministic admission gate, not in the prompt\.

This boundary is the complement of agent\-side approaches\. Where SagaLLMChang and Geng \([2025](https://arxiv.org/html/2607.00269#bib.bib19)\)brings transactional discipline*to*the LLM planner, ATP opens the transaction layer*to*untrusted planners: one disciplines the proposer, the other governs the committer, and together they bracket the same goal from both ends\.

#### Why this is not input validation\.

For decades the unit of work submitted to a transaction system was authored by a person or a trusted application and reviewed before submission, so the system could assume the submitter held the authority to transact; classical input validation and integrity constraints then checked only*data quality*\(does this command satisfy fixed predicates\), never the submitter’s right to commit\. A generative proposer breaks that assumption, and that is what is new\.ATPgoverns the prior question \(whether an untrusted,*generated*proposal may become a transaction request at all\), so what it enforces is an*authority contract*over committed state, not a richer predicate on a trusted command: a proposal is validated against the effective\-state witness \(StateView\), a repair may not destroy the evidence that justified it, an active commitment may wake but never write, and concurrent proposals are admitted as if serial\. The hardest of these, evidence\-preserving repair, has no analogue in classical validation, which never had to distrust the author of the command\.

#### The second half: reactive local repair\.

Admission decides which proposals may commit, but it cannot, by itself, handle a disruption that strikes*after*commit and that no registered compensation covers: a breakdown, a closure, a late arrival\. For these,ATPadds a second mechanism: a*localized cascading repair protocol*\(LCRP\)\. When such a failure fires, the affected obligation wakes and LCRP edits only the affected region of the committed plan, under a bounded edit radius and iteration cap, propagating along effective dependencies and escalating to rollback if it cannot contain the damage\. The repair LCRP produces is itself a proposal that re\-enters the same admission gate, so reactive recovery inherits the same guarantee: a wrong repair cannot commit\. Admission keeps a bad proposal out; LCRP keeps an unforeseen disruption from forcing an unbounded, unguarded re\-plan, the proposal\-time and runtime faces of a single authority rule \(§[3\.2](https://arxiv.org/html/2607.00269#S3.SS2)\)\.

#### Contributions\.

1. 1\.A new database\-systems problem\.Agentic transaction processing: a generated action must earn transaction authority before it becomes committed truth \(§[2](https://arxiv.org/html/2607.00269#S2)\)\.
2. 2\.TheATPmodel\.A transaction model that decouples committed\-state correctness from the intelligence layer by treating every LLM, solver, and agent output as a proposal, with*active commitment records*\(ACRs\), transaction\-log\-resident obligations whose wakeups are themselves proposals \(§[2\.2](https://arxiv.org/html/2607.00269#S2.SS2)\)\.
3. 3\.Four safety theorems\.Authority separation, serial\-equivalent generative admission, evidence\-preserving repair, and obligation containment, proved relative to a constraint set𝒞\\mathcal\{C\}\(§[2\.3](https://arxiv.org/html/2607.00269#S2.SS3), §[3](https://arxiv.org/html/2607.00269#S3)\)\.
4. 4\.Reactive local repair\.A bounded localized repair protocol \(LCRP\) whose output re\-enters admission, with a bounded\-recovery contract and a reduction of recursive recovery to sequential recovery \(§[3\.2](https://arxiv.org/html/2607.00269#S3.SS2)\)\.
5. 5\.TheMnemosyneruntime\.An executable ATP substrate over a committed\-transition log, effective\-state projection, deterministic admission, dependency\-safe compensation, and PostgreSQL\-backed concurrency \(§[4](https://arxiv.org/html/2607.00269#S4)\)\.
6. 6\.Evaluation\.Nine falsification\-style safety experiments, a cost audit, a disruption\-containment study \(LCRP edits an order of magnitude fewer operations than global recompute\), and a recovery\-during\-recovery analysis \(§[5](https://arxiv.org/html/2607.00269#S5)\)\.

## 2Agentic Transaction Processing

Generated workflow actions fail in ways ACID does not address: an invalid transition, a compensation that orphans effective dependents, conflicting or stale\-world proposals, or a repair that destroys the evidence that triggered it\. ACID governs a transaction*after*the system accepts itGray and Reuter \([1993](https://arxiv.org/html/2607.00269#bib.bib3)\); Bernstein and Newcomer \([2009](https://arxiv.org/html/2607.00269#bib.bib2)\); Weikum and Vossen \([2001](https://arxiv.org/html/2607.00269#bib.bib4)\);ATPgoverns whether a generated proposal should be admitted as a transaction at all\. This section presents the failure model \(§[2\.1](https://arxiv.org/html/2607.00269#S2.SS1)\), the transaction model \(§[2\.2](https://arxiv.org/html/2607.00269#S2.SS2)\), the properties it adds beyond ACID \(§[2\.3](https://arxiv.org/html/2607.00269#S2.SS3)\), and the invariants the runtime enforces \(§[2\.4](https://arxiv.org/html/2607.00269#S2.SS4)\)\.

### 2\.1Failure Model

Mnemosyne addresses failure modes that ACID does not govern, because ACID constrains a unit of work only after it is admitted\. We describe the principal modes below; Table[1](https://arxiv.org/html/2607.00269#S2.T1)pairs each with the mechanism that rejects or contains it\.

Invalid generated transition\.An LLM proposes a workflow transition that violates a finite\-state constraint\. A conventional workflow engine may persist the action unless application code rejects it\. ATP requires a deterministic validator to reject it before commit\.

Compensation with effective dependents\.A record is compensated after downstream records have depended on it\. Raw log history still contains the record, but it is no longer effective\. ATP disallows compensation that would orphan currently effective dependents or break the effective\-state chain\.

Conflicting proposals\.Two agents propose different plans for the same tenant and entity\. Both may be individually feasible\. ATP rejects the active proposal set before commit because the proposals conflict over the same admission scope\.

Stale\-world proposal\.A solver proposes a route assuming a deadline of 17:00, but an observed world snapshot reports the deadline is now 11:00\. ATP rejects the proposal before commit because its assumptions no longer match observed facts\.

Evidence\-destroying repair\.A coding agent observes that continuous integration is red and proposes to “repair” the repository by deleting the failing tests\. A periodic checker may see the next CI run turn green and conclude the violation is gone, but the defect has not been repaired: the evidence has been destroyed\. ATP requires admission to preserve the evidence that triggered repair unless the validator accepts that the repair addresses the underlying condition rather than suppressing its observable signal\.

Table 1:Generated\-workflow failures and ATP mechanisms\.FailureATP mechanismInvalid transitiondeterministic admissionUnsafe compensationdependency\-closed compensationConflicting proposalsscoped proposal\-conflict rejectionStale assumptionsstale\-world rejectionEvidence\-destroying repairevidence\-preserving admissionUnbounded live obligationactive commitment lifecycleDuplicate concurrent repairidempotent recovery\-event admission
### 2\.2The Agentic Transaction Model

###### Definition 1\(Proposal\)\.

A proposalppis an uncommitted candidate action generated by an LLM, solver, agent, active commitment, or external tool\. It may include a target tenant, workflow, entity, operation, dependency set, world assumptions, and optional solver certificate\.

###### Definition 2\(Committed transition\)\.

A committed transition is a proposal that has passed admission and has been durably written to the committed\-transition log\.

###### Definition 3\(Committed\-transition log\)\.

The committed\-transition log \(CTL\) is the append\-only record of admitted transitions, active commitment lifecycle events, and durable recovery events\. It is the source of committed truth\.

###### Definition 4\(Effective state\)\.

The effective state of an entity is the state obtained by replaying committed transitions while excluding records that have been compensated, superseded, or otherwise made ineffective\.

###### Definition 5\(Admission\)\.

Admission is the deterministic pre\-commit procedure that checks a proposal against current effective state, structural constraints, dependency safety, conflict scope, policy, and observed world facts\. Only admitted proposals may commit\.

###### Definition 6\(Conflict scope\)\.

A conflict scope is the tenant, entity, or recovery region over which two proposals may not both become effective without revalidation\. ATP requires every proposal to declare a conflict scope, and the admission gate serializes or rejects proposals with overlapping incompatible scopes\.

###### Definition 7\(Active commitment record\)\.

An active commitment record \(ACR\) is a durable obligation stored inCTLand created by an admitted workflow step\. It records a commitment or assumption together with a trigger, dependency scope, continuation pointer, guard, admission policy, compensation handler, expiry condition, and failure signature\. When its trigger fires, the runtime may resume the continuation to produce a repair proposal; the record itself cannot mutate committed state\.

We model anACRas:

r=⟨\\displaystyle r=\\langleid,txn,commitment,scope,trigger,\\displaystyle\\text\{id\},\\text\{txn\},\\text\{commitment\},\\text\{scope\},\\text\{trigger\},continuation,guard,validator,compensation,\\displaystyle\\text\{continuation\},\\text\{guard\},\\text\{validator\},\\text\{compensation\},expiry,failure\-key,status⟩\.\\displaystyle\\text\{expiry\},\\text\{failure\-key\},\\text\{status\}\\rangle\.Typical status values arelive,fired,proposed,admitted,rejected,compensated,expired, anddischarged\.

LLM / Solver/ ACRValidatedadmissionCTLcommit logStateViewOutboxeffective\-state read

Figure 1:ATP separates proposal generation, validated admission, durable commit, and effective\-state projection\.Figure[1](https://arxiv.org/html/2607.00269#S2.F1)shows the core ATP path\. The proposal is not committed directly\. It passes through admission\. The commit log is the source of committed truth, whileStateViewexposes current effective state\.

Algorithm 1: ATP admission under constraint set𝒞\\mathcal\{C\}\.1Parsepp; check tenant, idempotency and operation keys, and the declared conflict scope\.2Read effectiveStateViewand retained evidence, never speculative or rejected history\.3Apply𝒞\\mathcal\{C\}\(finite\-state, stale\-world, dependency closure, compensation safety\); ifppis a repair, require its triggering evidence to stay effective and queryable\.4Serialize or reject overlapping conflict scopes; anACRwakeup may only*propose*, never mutateCTLorStateView\.5Atomically append and project toStateView, else record a queryable rejection reason\.Algorithm[2\.2](https://arxiv.org/html/2607.00269#S2.SS2)gives the executable contract used by the implementation and by the RQ1–RQ5 experiments\. The details of𝒞\\mathcal\{C\}are application\-specific, but the authority pattern is fixed: proposal generation can vary, while admission and commit remain deterministic runtime operations\.

### 2\.3Properties Beyond ACID

ACID is necessary but insufficient for agentic workflows\. Atomicity, consistency, isolation, and durability protect a transaction once the system has accepted itGray and Reuter \([1993](https://arxiv.org/html/2607.00269#bib.bib3)\); Bernstein and Newcomer \([2009](https://arxiv.org/html/2607.00269#bib.bib2)\); Weikum and Vossen \([2001](https://arxiv.org/html/2607.00269#bib.bib4)\); Mohanet al\.\([1992](https://arxiv.org/html/2607.00269#bib.bib5)\)\. They do not decide whether a generated action should have been accepted as a transaction in the first place\. ATP adds an admissibility layer in front of commit:*ACID*protects committed transactions, while*ATP*protects the authority boundary before a generated action becomes a transaction\. The properties below make the ATP layer precise, and Section[3](https://arxiv.org/html/2607.00269#S3)proves the four that matter most\.

###### Property 1\(Proposal Non\-Authority,PNA\)\.

LLMs, solvers, agents, benchmark adapters, runtime drivers, learned repair policies, and active commitments may propose or orchestrate, but none may directly create committed truth\.

###### Property 2\(Intelligence\-Decoupled Correctness,IDC\)\.

Relative to a declared constraint set𝒞\\mathcal\{C\}, the correctness of committed state is independent of the competence, honesty, or learning behavior of the proposing intelligence layer\.

###### Property 3\(Deterministic Admission under𝒞\\mathcal\{C\},DA\)\.

Every generated proposal must pass a deterministic validator enforcing𝒞\\mathcal\{C\}before commit\. Admission depends on effective state, policy, dependency safety, conflict scope, and observed world facts, not on the proposer\.

###### Property 4\(Effective\-State Soundness,ESS\)\.

StateViewis derived only from effective committed records, excluding records that have been compensated, superseded, or invalidated\.

###### Property 5\(Evidence\-Preserving Repair,EPR\)\.

An admitted repair may not discharge its own trigger by deleting, compensating, or obscuring the evidence that justified it, unless admission verifies that the triggering condition is actually resolved under𝒞\\mathcal\{C\}\.

###### Property 6\(Dependency\-Closed Compensation,DCC\)\.

A compensation is inadmissible if it would orphan effective dependents or break the effective chain for an entity\.

###### Property 7\(Obligation Containment,OC\)\.

Active commitments can wake and emit proposals, but cannot mutate committed truth directly\.

###### Property 8\(Serial\-Equivalent Generative Admission,SEA\)\.

Concurrent generative proposers are admitted as if in some serial order over their declared conflict scopes, so committed state never reflects two conflicting proposals or a duplicate of one\.

###### Property 9\(Audit and Traceability,AET\)\.

Rejections, wakeups, proposal packages, repairs, admitted records, and compensations remain queryable as historical evidence\. Traceability supports the guarantees above; it is not itself the primary guarantee\.

Table[2](https://arxiv.org/html/2607.00269#S2.T2)aligns each classical guarantee or mechanism with the ATP property that governs it once the writer is an untrusted generator\. Most rows extend a familiar guarantee to generated proposals; the last names a concern ACID never had\.

Table 2:Each classical guarantee or mechanism, and the ATP property that governs it once writers are untrusted generators\.Classical guarantee or mechanismATP propertyAtomicityProposal Non\-Authority \(PNA\)ConsistencyDeterministic Admission under𝒞\\mathcal\{C\}\(DA\)IsolationSerial\-Equivalent Generative Admission \(SEA\)DurabilityCTLwith Audit and Traceability \(AET\)Saga compensationDependency\-Closed Compensation \(DCC\)Active triggersObligation Containment \(OC\)Generated\-repair integrity \(new\)Evidence\-Preserving Repair \(EPR\)
### 2\.4Safety Invariants

We state the core safety conditions as invariants here; the properties that follow are proved as theorems in §[3](https://arxiv.org/html/2607.00269#S3), with full proofs in the extended version\. The results are relative systems\-safety claims rather than complexity\-theoretic claims\. Throughout the section, fix a*trusted constraint set*𝒞\\mathcal\{C\}consisting of the deterministic admission validator, application finite\-state constraints, dependency and compensation rules, stale\-world checks, evidence\-preservation rules, and conflict\-scope rules\. A committed transition is*𝒞\\mathcal\{C\}\-valid*if the admission gate accepts it under this constraint set and current effective state\. All guarantees below are relative to𝒞\\mathcal\{C\}; if𝒞\\mathcal\{C\}omits a hazard, ATP does not claim to detect it\.

#### Bounded executable constraint set\.

ATP does not assume an oracle for semantic correctness\. In the implementation and experiments,𝒞\\mathcal\{C\}is a finite executable constraint set over proposal structure, tenant/entity scope, operation and idempotency keys, currentStateView, dependency edges, retained evidence handles, declared world facts, and application validators\. Thus𝒞\\mathcal\{C\}is decidable for the artifact workloads\. In richer deployments, constructing a faithful𝒞\\mathcal\{C\}is part of the application engineering problem rather than something ATP solves by itself\. Appendix[H](https://arxiv.org/html/2607.00269#A8)gives a taxonomy and grammar of𝒞\\mathcal\{C\}, showing that most rules are derived structurally or declared as predicates rather than hand\-coded per case\.

#### Gate closure\.

The theorems assume gate closure: proposer, solver, runtime\-driver, benchmark, andACR\-wakeup code can emit proposal packages but cannot append domain truth toCTLexcept through admission\. Mnemosyne’s reference implementation is organized around this boundary and includes regression tests for non\-authoritative wakeups, rejected proposals, and commit\-boundary behavior, but this paper does not claim a machine\-checked noninterference proof of the entire Python codebase\. The formal claims therefore apply to executions that satisfy this gate\-closure assumption\.

#### Where the difficulty lives\.

Theorem[1](https://arxiv.org/html/2607.00269#Thmtheorem1)is deliberately simple once the gate is trusted: if only𝒞\\mathcal\{C\}\-valid transitions are appended, committed state is𝒞\\mathcal\{C\}\-valid\. The systems contribution is not that implication but the*structure*of𝒞\\mathcal\{C\}and the*witness*the gate reads\. A classical validator checks a submitted command against static predicates; ATP’s gate instead reads the effective\-state projection rather than raw history, enforces dependency\-closed compensation, rejects stale\-world and conflicting proposals, and, hardest of all, refuses a repair that would discharge its own trigger by destroying evidence\. We therefore lead the development conceptually with evidence\-preserving repair \(Theorem[3](https://arxiv.org/html/2607.00269#Thmtheorem3)\), the guarantee with no classical analogue, and read authority separation \(Theorem[1](https://arxiv.org/html/2607.00269#Thmtheorem1)\) as the umbrella it instantiates\.

###### Invariant 1\(No invalid commit\)\.

A proposal with a non\-empty validation violation set must not be written toCTL\.

###### Invariant 2\(Effective\-state separation\)\.

Full history preserves all committed records, while effective history excludes records that have been compensated, superseded, or otherwise made ineffective\.

###### Invariant 3\(No orphaned effective dependents\)\.

A compensation is rejected if it would leave an effective record depending on an ineffective record\.

###### Invariant 4\(Proposal conflict rejection\)\.

Two active proposals that target the same tenant/entity scope with incompatible effects are rejected or serialized before commit\.

###### Invariant 5\(Stale\-world rejection\)\.

A proposal whose world assumptions disagree with observed world facts is rejected before commit\.

###### Invariant 6\(Non\-authoritative wakeup\)\.

A firedACRcannot directly mutateCTLorStateView\. It can only resume a continuation that emits a proposal subject to ordinary admission\.

###### Invariant 7\(Evidence preservation\)\.

A memory\-initiated repair must not remove, overwrite, compensate, or invalidate the evidence that caused the trigger unless the admission gate accepts, under retained evidence and validator rules, that the proposed repair addresses the triggering condition rather than merely suppressing its observable signal\.

###### Invariant 8\(Effective\-chain preservation\)\.

A compensation is rejected if it would break the effective chain for an entity\.

###### Invariant 9\(Admitted commitment creation\)\.

Creating anACRis itself an admitted transition\. The record must have bounded dependency scope, a discharge or expiry condition, a guard, a validator, and an idempotent creation key\.

###### Invariant 10\(Scoped repair\)\.

A proposal generated by anACRmay touch only the dependency scope recorded by thatACR, unless a wider scope is explicitly admitted as an escalation\.

###### Invariant 11\(Cross\-episode traceability\)\.

Rejected or compensatedACRproposals with matching failure signatures remain queryable as historical evidence for future proposal ranking, guard strengthening, or external causal\-learning modules\.

## 3ATP Theorems

We prove the invariants of §[2\.4](https://arxiv.org/html/2607.00269#S2.SS4)as safety theorems: first for the admission of generated proposals, then for reactive repair under unforeseen disruptions \(§[3\.2](https://arxiv.org/html/2607.00269#S3.SS2)\)\.

### 3\.1Admission Safety

###### Theorem 1\(Authority\-Separation Theorem\)\.

Let𝒞\\mathcal\{C\}be the trusted admission constraint set\. Let the intelligence layer consist of arbitrary LLMs, solvers, agents, active\-commitment wakeups, learned repair policies, and benchmark adapters\. Assume: \(i\) the intelligence layer can only emit proposals; \(ii\) the only operation that extendsCTLis append of an admitted transition; and \(iii\) the admission gate appends only proposals accepted under𝒞\\mathcal\{C\}and current effective state\. Then committed\-state correctness with respect to𝒞\\mathcal\{C\}is independent of the correctness, competence, honesty, or learning behavior of the intelligence layer\.

###### Authority Separation, Theorem[1](https://arxiv.org/html/2607.00269#Thmtheorem1)\.

We prove the claim by induction on the length ofCTL\. Initially,CTLis empty or contains only trusted initial records, so every committed transition is𝒞\\mathcal\{C\}\-valid\. Assume afterkkappends that every transition inCTLk\\textsf\{CTL\}\_\{k\}is𝒞\\mathcal\{C\}\-valid\. Consider the\(k\+1\)\(k\+1\)\-st committed transition\. By assumption, no LLM, solver, agent,ACRwakeup, learned policy, or adapter can append toCTLdirectly; such components can only emit a proposalpp\. Since the only operation that extendsCTLis the append of an admitted transition,ppcan become the next committed transition only if the gate admits it under𝒞\\mathcal\{C\}and the current effective state\. By the soundness of the gate with respect to𝒞\\mathcal\{C\}, the appended transition is𝒞\\mathcal\{C\}\-valid\. Thus every transition inCTLk\+1\\textsf\{CTL\}\_\{k\+1\}is𝒞\\mathcal\{C\}\-valid\. By induction, all committed transitions are𝒞\\mathcal\{C\}\-valid\. The argument never assumes that the intelligence layer is accurate, rational, complete, honest, or improving; therefore committed\-state correctness is decoupled from that layer\. ∎

The intelligence layer may make the system more or less useful; it cannot make committed state incorrect with respect to𝒞\\mathcal\{C\}unless it is granted authority to bypass or weaken the admission boundary\. This is the central systems claim: the model can hallucinate, the solver can be wrong, the agent can be adversarial, and a learned policy can be bad, yet none can corrupt committed truth unless𝒞\\mathcal\{C\}itself admits the transition\.

###### Corollary 1\(Solver Non\-Authority\)\.

A solver certificate proves only that a solver produced a plan under its own assumptions\. It does not make the plan admissible\. The plan remains a proposal until ATP admission accepts it under𝒞\\mathcal\{C\}\.

###### Corollary 2\(Effective\-State Soundness\)\.

IfStateViewis derived only from non\-compensated, non\-superseded, dependency\-valid committed records, then everyStateViewfact corresponds to an effective committed chain, and no compensated or superseded record appears as current truth\.

###### Corollary 3\(Dependency\-Closed Compensation Safety\)\.

If compensation is admitted only when it preserves dependency closure and effective\-chain continuity, then no admitted compensation can leave an effective dependent orphaned or produce an effective state lacking a valid committed chain\.

###### Theorem 2\(Serial\-Equivalent Generative Admission\)\.

By the conflict\-scope contract \(Definition[6](https://arxiv.org/html/2607.00269#Thmdefinition6)\), proposals with overlapping incompatible scopes are serialized or rejected at admission\. Assume in addition that append toCTLis atomic and that every dependent recovery proposal reads only committed effective state after its dependencies have committed\. Then concurrent generative proposers are observationally equivalent to some serial admission order over committed transitions\. Moreover, cascading recovery is memoryless with respect to speculative proposal history: later recovery depends only on committed history and effective state, not on rejected, in\-flight, or superseded proposal attempts\.

###### Serial\-Equivalent Generative Admission, Theorem[2](https://arxiv.org/html/2607.00269#Thmtheorem2)\.

For each conflict scope, admission imposes a total order on accepted proposals: if two proposals contend for the same scope, the gate admits at most one before the other observes the updated effective state or is rejected as conflicting\. Because append is atomic, each admitted proposal contributes one indivisible committed transition\. Interleavings across disjoint scopes commute with respect to the observations made throughStateView, so the global committed history is equivalent to an interleaving of the per\-scope serial orders\. A dependent recovery proposal is evaluated only after its dependencies appear inCTLand afterStateViewreflects the effective projection of committed records\. Rejected or in\-flight proposals never appear in this projection\. Thus each recovery step can be explained by a serial prefix of committed history, and recovery decisions are independent of speculative attempts that never committed\. ∎

###### Corollary 4\(Storage\-Level Idempotency Boundary\)\.

In the PostgreSQL substrate, tenant\-scoped uniqueness over event identifier, idempotency key, and recovery sequence position implements the concrete idempotency and conflict boundary used by Theorem[2](https://arxiv.org/html/2607.00269#Thmtheorem2): concurrent duplicate proposals either converge to one canonical committed event or reject conflicting losers without producing duplicate committed truth\.

###### Theorem 3\(Evidence\-Preserving Repair Safety\)\.

Let a repair proposal be triggered by evidenceEEof a failure conditionFF\. If admission requires that eitherFFis resolved under𝒞\\mathcal\{C\}, orEEremains effective and queryable after the repair, then no admitted repair can discharge its own trigger merely by deleting, compensating, or obscuring the evidence that justified it\.

###### Evidence\-Preserving Repair Safety, Theorem[3](https://arxiv.org/html/2607.00269#Thmtheorem3)\.

The trigger is evaluated over committed evidence inCTLand effective evidence inStateView\. Suppose a repairrris admitted and discharges the trigger\. IfrrleavesEEeffective and queryable, then the trigger has not been discharged by destroying evidence\. Otherwise,rrdeletes, compensates, or obscuresEE\. By the evidence\-preservation invariant, such a repair is admissible only when the gate verifies that the underlying failure conditionFFis resolved under𝒞\\mathcal\{C\}\. Hence no admitted repair can succeed solely by removing the observable signal ofFF: it either preserves the evidence or resolves the condition\. SinceCTLis append\-only, the evidence and the gate decision remain auditable after the fact\. ∎

This theorem is stronger than audit traceability\. Traceability says the alarm can be found later; evidence\-preserving repair says the alarm cannot be silenced by the repair\.

#### Decidability caveat for repair\.

Theorem[3](https://arxiv.org/html/2607.00269#Thmtheorem3)does not decide whether an arbitrary real\-world failure has truly been fixed\. That question can be open\-ended or outside the information available to the runtime\. ATP requires either an executable validator in𝒞\\mathcal\{C\}that accepts the repair as resolving the triggering condition, or continued retention of the triggering evidence\. If neither condition can be established, the safe behavior is rejection or escalation rather than admission\.

###### Theorem 4\(Obligation Containment\)\.

If everyACRis itself created by an admitted committed transition, and every firedACRcan only emit a proposal package, then no active commitment can mutate domain truth except through the same admission boundary as any other proposal\.

###### Obligation Containment, Theorem[4](https://arxiv.org/html/2607.00269#Thmtheorem4)\.

Creation of anACRis already a committed transition, so its existence is governed by ordinary admission\. Firing anACRis not a commit operation; it resumes a continuation that constructs a proposal package\. By assumption, that package must pass ordinary admission before any domain transition can be appended\. Therefore anACRhas no direct mutation path toCTLorStateView\. It can influence committed truth only by generating a proposal that the same gate admits for every other proposer\. A future obligation can wake, but it cannot corrupt\. ∎

###### Corollary 5\(Learning Non\-Authority\)\.

If learned artifacts can affect only proposal generation and ranking, and cannot weaken𝒞\\mathcal\{C\}except through an explicitly admitted governance transition, then learning cannot directly compromise committed\-state correctness\. By Theorem[1](https://arxiv.org/html/2607.00269#Thmtheorem1), any domain effect of learning must pass the admission gate, so its worst outcome is over\-rejection, delayed repair, or selection among admissible but suboptimal proposals, never an invalid commit\. Whether learning improves remedies, reduces repeated failures, or lowers regret is outside the scope of this paper and is deferred to future work \(see the*Limitations*section\)\.

#### What these guarantees do and do not claim\.

All ATP guarantees are relative to the declared trusted constraint set𝒞\\mathcal\{C\}\. If𝒞\\mathcal\{C\}is incomplete, ATP cannot reject violations outside𝒞\\mathcal\{C\}\. The theorems do not prove convergence, optimality, monotonic improvement, unlimited liveness, or full\-code bypass freedom\. They prove a narrower systems property: intelligence, learning, and recovery memory remain non\-authoritative\. They may propose, rank, delay, or over\-reject, but they cannot commit domain truth except through admission under𝒞\\mathcal\{C\}\.

### 3\.2Reactive Repair for the Unforeseen

Admission decides whether a*generated*proposal may become truth\. But not every threat to committed state is a proposal: the world also produces failures no proposal anticipated: a delayed flight, a machine breakdown, a road closure mid\-execution\. A generated plan can be perfectly admitted and still be overtaken by an event it never modeled\.ATPtherefore pairs admission with a second mechanism\.*A proposal is not truth, and no proposal foresees every disruption*: the first clause is enforced by the gate, the second by*reactive local repair*\.

ATPdistinguishes two failure modes\.*Anticipated*failures have a recovery path the designer registered in advance \(a cancelled booking that triggers a declared compensation\), and are handled by the evidence\-preserving, dependency\-closed compensation of Theorems[3](https://arxiv.org/html/2607.00269#Thmtheorem3)and[4](https://arxiv.org/html/2607.00269#Thmtheorem4)\.*Unforeseen*failures have none: the committed log reaches a state no compensation addresses\. Here a firedACRhands the disrupted region to a*localized cascading repair protocol*\(LCRP\) rather than recomputing the whole plan\.

#### The reactive loop\.

The runtime runs one loop per event \(propose, admit, commit, monitor, repair\), and on disruption LCRP applies*bounded edits*instead of a global recompute\. It edits only the disrupted region under an iteration capKKand a displacement budgetδmax\\delta\_\{\\max\}, where the*edit radius*counts the transitions \(operations or jobs\) touched\. Each iteration revalidates feasibility against𝒞\\mathcal\{C\}and propagates effects only along the*effective dependencies*of the disrupted region, so a change ripples to a successor only if that successor actually depends on the changed record in the currentStateView\. The runtime, not the proposal, computes the reversibility class of each candidate edit, so a repair cannot self\-certify as safe; one that would cross an irreversible boundary is vetoed\. Crucially, the repair LCRP produces is itself a*proposal*that re\-enters the admission gate, so a wrong reactive repair is caught exactly like any other proposal and can never become committed truth\.

#### Repair phases\.

A single repair round proceeds in three phases over the disrupted region\.*\(I\) Status update*records the disruption as a new world fact \(marking the affected committed records ineffective and retaining the disruption as evidence\), so the repair is computed against the true post\-disruptionStateView, not the stale plan\.*\(II\) Effect propagation*pushes the consequences \(delays, freed resources, violated guards\) forward along effective dependencies, computing the minimal set of downstream transitions that must change\.*\(III\) Bounded reassignment*re\-times or re\-assigns only those transitions, underδmax\\delta\_\{\\max\}andKK, and emits the result as a proposal package\. Each phase is contained to the dependency closure of the disruption, which is what keeps the edit radius small; the package then passes ordinary admission before any of it commits\.

###### Proposition 1\(Bounded Reactive Repair\)\.

Under LCRP with iteration capKKand displacement budgetδmax\\delta\_\{\\max\}, repair time satisfiesTrepair∈𝒪​\(K​\(J​M\+J​Omax\)\)T\_\{\\mathrm\{repair\}\}\\in\\mathcal\{O\}\\\!\\big\(K\(JM\+JO\_\{\\max\}\)\\big\)and the cumulative displacement satisfiesΔ​\(σ∗\)≤δmax\\Delta\(\\sigma^\{\\ast\}\)\\leq\\delta\_\{\\max\}, whereJJis the number of affected entities,MMthe number of resources, andOmaxO\_\{\\max\}the maximum transitions per entity\. Repair terminates withinKKrevalidation rounds; if either bound is exceeded, the runtime escalates deterministically by rolling back to the most recent restore point\. No transition commits while its violation set against𝒞\\mathcal\{C\}is non\-empty\.

###### Proof\.

Each repair round validates the affected region in𝒪​\(J​M\)\\mathcal\{O\}\(JM\)and propagates effects along effective dependencies in𝒪​\(J​Omax\)\\mathcal\{O\}\(JO\_\{\\max\}\); rounds are capped atKK, giving the time bound\. The displacement budget is checked each round and escalation triggers as soon as it is exceeded, so cumulative displacement never passesδmax\\delta\_\{\\max\}\. Commit occurs only on an empty violation set \(admission\), so no infeasible transition is appended; if no in\-budget repair is found withinKKrounds, rollback restores the last validated state\. ∎

###### Proposition 2\(Transactional Rollback Safety\)\.

LetSjS\_\{j\}be the most recent restore point\. Rollback guarantees that \(i\) no infeasible state remains committed, \(ii\) all effects afterSjS\_\{j\}are logically undone through dependency\-closed compensation, and \(iii\) replay fromSjS\_\{j\}is deterministic\.

###### Proof\.

Restore points are created only after admission \(empty violation set\), and committed\-transition\-log entries are immutable; superseded branches are excluded from the effectiveStateViewbut retained for audit\. Compensation handlers keyed by idempotency keys logically undo effects afterSjS\_\{j\}under the dependency\-closure rule, so rollback returns to a previously admitted,𝒞\\mathcal\{C\}\-feasible state from which replay is deterministic\. ∎

These guarantees are relative to𝒞\\mathcal\{C\}and the runtime’s effective\-state model; they do not assert that the proposer finds a globally optimal repair, nor that𝒞\\mathcal\{C\}is semantically complete\.

LCRPt1t\_\{1\}t2t\_\{2\}t3t\_\{3\}t4t\_\{4\}t5t\_\{5\}t6t\_\{6\}t7t\_\{7\}breakdownedit radius≤δmax\\leq\\delta\_\{\\max\}\(effective\-dependency closure\)Recomputeentire plan re\-timed

Figure 2:Bounded reactive repair vs\. global recompute on a disrupted plan \(illustrative; the5×35\\times 3job\-shop instance of §[5\.6](https://arxiv.org/html/2607.00269#S5.SS6)moves from makespan1919to2222\)\. A breakdown att3t\_\{3\}confines LCRP to the effective\-dependency closure\{t3,t4,t5\}\\\{t\_\{3\},t\_\{4\},t\_\{5\}\\\}\(amber\) within the displacement budgetδmax\\delta\_\{\\max\}, leaving the rest committed \(green\); global recompute re\-times every transition\. RQ5 \(§[5\.6](https://arxiv.org/html/2607.00269#S5.SS6)\) measures this edit\-radius gap\.
#### Recovery during recovery\.

A repair is itself an execution, so a failure can strike*while a repair is in flight*: a second disruption arrives before the first is absorbed, or a compensation itself fails\. This recursive recovery appears to demand a recovery stack whose depth must be tracked and bounded\. It does not, but the reason must be stated carefully, because a disruption is a new fact about the world and must never be dropped\. After the most recent committed restore pointSkS\_\{k\}, the runtime maintains a*pending observation set*DkD\_\{k\}: the disruptions observed sinceSkS\_\{k\}that no admitted repair has yet absorbed\. Every repair candidate is validated againstSkS\_\{k\},𝒞\\mathcal\{C\}, and*all*ofDkD\_\{k\}, so it must account for every outstanding failure, not only the latest\.

###### Lemma 1\(Memorylessness with respect to recovery history\)\.

Because admission reads only the latest committed restore pointSkS\_\{k\}, the constraint set𝒞\\mathcal\{C\}, and the accumulated observation setDkD\_\{k\}, a repair candidate is a functionR​\(Sk,𝒞,Dk\)R\(S\_\{k\},\\mathcal\{C\},D\_\{k\}\)\. It is memoryless with respect to*recovery history*\(independent of whether earlier repair attempts were in progress, aborted, or superseded\), but*not*with respect to world observations, sinceDkD\_\{k\}retains every disruption not yet absorbed into an admitted repair\.

###### Proposition 3\(Recursive recovery reduces to sequential recovery\)\.

If every in\-flight repair remains an uncommitted proposal and every admitted repair is validated againstSkS\_\{k\},𝒞\\mathcal\{C\}, and the full pending setDkD\_\{k\}, then a failure arriving mid\-repair is equivalent to appending it toDkD\_\{k\}and restarting single\-shot recovery fromSkS\_\{k\}\. Recursive recovery is therefore exactly sequential recovery over the accumulated observations: nesting introduces no new case, every committed transition is𝒞\\mathcal\{C\}\-feasible at any nesting depth and failure timing, and a sequence ofFFfailures terminates in at mostF​KFKrounds before success or escalation\.

###### Proof\.

By Lemma[1](https://arxiv.org/html/2607.00269#Thmlemma1)a candidate depends only on\(Sk,𝒞,Dk\)\(S\_\{k\},\\mathcal\{C\},D\_\{k\}\), not on the in\-flight repair it interrupts; since in\-flight repairs are uncommitted, interrupting one changes no committed state\. Appending the new disruption toDkD\_\{k\}thus yields the same problem instance as a fresh single\-shot recovery fromSkS\_\{k\}against the enlargedDkD\_\{k\}\. Safety and termination follow from Proposition[1](https://arxiv.org/html/2607.00269#Thmproposition1)applied to each single\-shot recovery, and theF​KFKbound from at mostFFsuch recoveries, each capped atKKrounds\. ∎

#### Why reactive repair is the hard half\.

Reactive repair is where admission stops being a predicate check\. A generated repair runs over*effective*state, must preserve the very evidence that triggered it, must close its own dependencies and conflict scope, and may be interrupted by a fresh disruption, yetATPkeeps every committed transition feasible and loses no observation, with edit radius and recovery depth both bounded\. This is the systems content behind the second clause of the principle: because no proposal foresees every disruption, the transaction layer must*react*safely, not merely admit\. Reactive planning is thus fully in scope; only*preemptive*guard synthesis \(anticipating disruptions before they occur\) is deferred to future work \(Limitations\)\.

## 4Mnemosyne Architecture and System Specification

Mnemosyneis the executable substrate for ATP\. Its design objective is not to make the proposer smarter; it is to make proposal authority explicit\. The architecture therefore separates four planes: the*proposal plane*, where LLMs, solvers, benchmark adapters, learned policies, and active commitments generate candidates; the*admission plane*, where deterministic validators decide whether a candidate may become truth; the*commit plane*, where admitted transitions are durably appended; and the*projection plane*, where current effective state is materialized for future admission\. Runtime engines sit outside these planes as orchestrators\. They schedule work, retry steps, and wake obligations, but they do not own committed truth\. Figure[3](https://arxiv.org/html/2607.00269#S4.F3)shows these planes, the proposers that feed them, and the durable stores that only admitted transitions may extend\.

LLMs / AgentsSolvers / ToolsACR wakeupsBenchmarks / eventsProposalpackageAdmission gate𝒞\\mathcal\{C\}\+ StateViewauthority boundaryCTL commit logRecovery\-event logInbox / outboxStateViewACR indexProposal planeAdmissionCommit planeProjectioneffective stateACR wakeup→\\rightarrownew proposal

Figure 3:System architecture\. Proposers generate packages; deterministic admission under𝒞\\mathcal\{C\}and current effective state is the only authority boundary; only admitted transitions cross it into the durable logs that feedStateViewand the active\-commitment index\. Runtime drivers \(not shown\) orchestrate but never own committed truth\.Durable substrate\.The committed\-transition log \(CTL\) is the source of committed truth: tenant\-scoped, versioned, and logically append\-only, it stores admitted transitions, compensation and supersession records, andACRlifecycle records, so later transitions may supersede earlier ones without erasing the fact that they were admitted\.StateViewprojects*current*truth fromCTLby replaying only effective records \(not compensated, superseded, or invalidated, with dependency chains intact\); admission readsStateView, never raw history, which is the mechanism behind effective\-state soundness\. A recovery\-event log records the fine\-grained events of repair and obligation execution, and in the PostgreSQL substrate tenant\-scoped uniqueness over event identifiers, idempotency keys, and recovery sequence positions is the concrete idempotency boundary of Theorem[2](https://arxiv.org/html/2607.00269#Thmtheorem2)\.

Concurrency and contention\.The serialization unit is the conflict scope, not the whole log: proposals over disjoint scopes \(distinct tenant, entity, or resource\) commit concurrently, so throughput scales with scope\-level parallelism rather than a single global lock\. Within one hot scope, the PostgreSQL substrate orders contenders through row\-level locking and a unique constraint over \(tenant, scope, idempotency key, recovery sequence position\), so concurrent proposals either converge to one canonical committed transition or reject the conflicting losers, exactly the boundary of Theorem[2](https://arxiv.org/html/2607.00269#Thmtheorem2); MVCC snapshot isolation lets theStateViewprojection read effective state without blocking admission\. A large disruption that wakes many obligations therefore degrades to serialized admission*on the affected scopes only*, trading latency for serial equivalence rather than risking an invalid interleaving, and rejected contenders retry against the updatedStateViewunder the memoryless repair model \(§[3\.2](https://arxiv.org/html/2607.00269#S3.SS2)\)\. Cross\-scope independence is what keeps dense conflict\-scope collisions from becoming a global bottleneck\.

Authority boundary\.The admission gate is the only authority boundary\. A proposal package carries a candidate transition, declared scope, proposer identity, an optional solver certificate, world assumptions, and evidence; the gate checks finite\-state validity, idempotency, scope, dependency closure, compensation safety, stale\-world conditions, conflicts, and evidence preservation, treats a solver certificate or LLM rationale as evidence rather than authority, and returns an admitted transition, a reasoned rejection, or an escalation\.ACRs are durable obligations in the same substrate, recording guards, triggers, continuations, compensation hooks, scopes, and validators; on firing, anACRmay resume a continuation that constructs a repair proposal, which still passes ordinary admission, so memory is active but non\-authoritative\.

Boundaries and drivers\.External events enter through an inbox deduplication boundary, and external effects leave through an outbox that stages provider calls with idempotency keys, so a domain commit never silently becomes an external effect and duplicate observations never create duplicate commits\. Runtime drivers, including durable engines such as Temporal and CadenceTemporal Technologies \([2026](https://arxiv.org/html/2607.00269#bib.bib14)\); Cadence Workflow Authors \([2026](https://arxiv.org/html/2607.00269#bib.bib13)\), orchestrate execution, timers, retries, and wakeups but remain non\-authoritative: a driver may detect a readyACR, call a provider, and submit a package, yet may not mutate domain truth, so the deployment substrate can change without changing ATP’s correctness\. Table[3](https://arxiv.org/html/2607.00269#S4.T3)states each component’s authority contract: what it owns, what it does not own, and the failure that results if its boundary is bypassed\.

Table 3:Component authority contract\. Each component owns one boundary; bypassing it produces the named failure\.ComponentOwnsDoes not ownFailure if bypassedLLM / solver / agentProposal generationCommitted truthHallucinated commitAdmission gateAuthority boundary under𝒞\\mathcal\{C\}Proposal generationInvalid commitCTLDurable historyEffective truth aloneLost audit and replayStateViewCurrent effective truthFull historyStale or compensated state usedACRDurable obligationMutation authorityTrigger corrupts truthStore substrateAtomic and idempotencySemantic validationDuplicate or conflict anomalyThe full proposal\-and\-obligation lifecycle \(propose→\\rightarrowadmit→\\rightarrowcommit→\\rightarrowproject, with an obligation’screate→\\rightarrowwatch→\\rightarrowwake→\\rightarrowresumerejoining the same proposal\-admission path\) together with the six\-point functional contract, the storage substrate \(SQLite default and optional gated PostgreSQL\), and the deployable service boundary, is specified in Appendices[D](https://arxiv.org/html/2607.00269#A4)–[I](https://arxiv.org/html/2607.00269#A9); Appendix[J](https://arxiv.org/html/2607.00269#A10)gives concrete JSON\-level proposal examples, and Appendix[K](https://arxiv.org/html/2607.00269#A11)traces one transaction end to end\. The invariant they enforce is the one already proved here: anACRwakeup is not a commit; it only returns the system to ordinary proposal admission, so no component receives a privileged commit path because it is a solver, a learned guard, or an active commitment\.

## 5Evaluation

This paper evaluates ATP as a data\-management system, not as an LLM planning method\. The experiments validate the assumptions behind the theorems and the correctness of the implementation; they make no claim about learning, regret, or preemptive planning, which are future work\. Planning and recovery workloads are derived from the REALM\-Bench planning benchmark and instantiated here as the J1–J4 benchmark harnessGeng and Chang \([2026](https://arxiv.org/html/2607.00269#bib.bib20)\)\. We reserve the name P1–P10 for broader readiness suites that are tracked as a separate artifact and are not certified in this draft\. The evaluation is organized around five research questions\. RQ1 asks whether the authority boundary holds across hazard classes and end\-to\-end; RQ2 compares against workflow/saga guardrails; RQ3 separates proposer usefulness from committed\-state correctness; RQ4 audits artifact\-level cost; and RQ5 examines reactive repair: how contained a bounded repair is, and whether recovery during recovery stays safe\. RQ1–RQ4 are completed in the releasedMnemosyneartifact\. RQ5’s containment \(edit radius\) is reported on a companion job\-shop scheduling harness that implements the same bounded\-repair protocol, where blast radius is directly measurable and the claim is a systems property \(bounded edit radius at equal feasibility\), not planning quality; recovery during recovery is validated by construction \(Proposition[3](https://arxiv.org/html/2607.00269#Thmproposition3)\), with broader empirical study in progress\.

### 5\.1Overview and Scoreboard

The current implementation covers the falsification\-oriented empirical spine of the released artifact: six theorem\- and property\-validation benchmarks, two end\-to\-end usefulness benchmarks, one mechanism\-level workflow/saga comparator, and one infrastructure\-cost audit\. The six safety benchmarks check, respectively, that generated proposals stay non\-authoritative until admitted \(AuthorityBench\); that concurrent proposals commit to a serial\-equivalent history \(SerialAdmissionBench\); that a repair cannot discharge its own trigger by destroying evidence \(EvidenceRepairBench\); that commitment wakeups resume recovery without mutating domain truth \(ObligationBench\); that compensation and supersession preserve effective\-state projection \(CompensationProjectionBench\); and that storage\-level uniqueness, idempotency, and transactional projection reject duplicate or malformed attempts without corruptingStateView\(StorageSubstrateBench\)\.J1J4EndToEndBenchdrives planning and recovery cases through the boundary,ProposerQualityBenchvaries proposer quality while tracking usefulness and the invalid\-commit invariant, andGuardrailComparatorBenchcompares ATP with a workflow/saga guardrail stack \(schema validation, finite\-state checks, idempotency keys, timers, local saga compensation, proposer self\-checking\) that lacks ATP\-specific evidence, effective\-state, obligation, compensation\-closure, and conflict\-scope admission\.

These benchmarks are falsification\-oriented systems tests rather than stochastic model\-quality experiments\. The deliberately permissive baselines expose each targeted failure mode by giving generated actions, repairs, wakeups, or storage writes more authority than ATP permits\. The guardrail comparator \(RQ2\) then reduces the strawman\-baseline concern by comparing ATP with a mechanism\-level workflow/saga guardrail stack\. A result is meaningful only when the comparator commits the specified violation, while ATP commits zero such violations and still admits valid operations\. Figure[4](https://arxiv.org/html/2607.00269#S5.F4)summarizes the safety evidence across every hazard class and the comparator; the cost audit \(RQ4\) is reported separately because it measures infrastructure overhead rather than violation suppression\.

055101015152020252530303535404045455050555560606565707075758080AuthoritySerialEvidenceObligationProjectionStorageEndToEndProposerComparator353548482020161677646433373766000000000Targeted violations committed \(lower is safer\)unsafe baselineATP /MnemosyneFigure 4:Violation suppression across the nine benchmarks\. Amber bars show the most permissive unsafe baseline for each hazard class and the workflow/saga guardrail comparator; green bars showATP\. Lower is safer;ATPcommits zero targeted violations in every class\.Table 4:Aggregate safety scoreboard across the nine benchmarks: each permissive baseline commits the targeted violation, whileATPcommits zero and still admits valid operations\.ClassBenchmarkBaseline violationsATP violationsAuthorityAuthorityBench35 invalid generated commits0 invalid generated commitsSerialSerialAdmissionBench48 invalid commits and capacity underflow0 invalid commits; serial\-equivalent historyEvidenceEvidenceRepairBench20 evidence\-destroying repairs0 evidence\-destroying repairsObligationObligationBench16 unauthorized wakeup mutations0 unauthorized wakeup mutationsProjectionCompensationProjectionBench7StateViewmismatches0StateViewmismatchesStorageStorageSubstrateBench64 invalid storage commits and 1StateViewmismatch0 invalid commits and 0StateViewmismatchesEnd\-to\-endJ1J4EndToEndBench3 invalid commits and 3StateViewmismatches0 invalid commits, 0 mismatches, 4 completed casesProposerProposerQualityBench37 invalid direct commits0 invalid commits across six proposer classesComparatorGuardrailComparator6 ATP\-specific hazards missed by workflow/saga guardrails0 invalid commits; 4 valid commits admittedTogether, Table[4](https://arxiv.org/html/2607.00269#S5.T4)and Figure[4](https://arxiv.org/html/2607.00269#S5.F4)are the scoreboard: the permissive baselines expose the targeted failure mode, the comparator adds a mechanism\-level workflow/saga guardrail comparison, and ATP suppresses the failure mode without turning into a reject\-all system\.

### 5\.2RQ1: Does the Authority Boundary Hold Across Hazard Classes and End\-to\-End?

The first and primary question is whether the admission boundary actually holds: across every hazard class ATP is designed to stop, does committed state stay𝒞\\mathcal\{C\}\-valid even when generated proposals, repairs, wakeups, or storage writes are given more authority than ATP permits? We answer it with six falsification benchmarks, one per hazard class, each comparing ATP against deliberately permissive baselines\. Figure[4](https://arxiv.org/html/2607.00269#S5.F4)is the scoreboard: in every class the permissive baseline commits the targeted violation, while ATP commits zero such violations and still admits the valid operations\. Per\-class designs and full result tables are in Appendix[A](https://arxiv.org/html/2607.00269#A1); we summarize the six classes here\.

AuthorityBench\(Theorem[1](https://arxiv.org/html/2607.00269#Thmtheorem1)\) gives five proposer classes direct or self\-validated commit authority: both baselines commit3535invalid transitions, while ATP commits zero and still admits the five valid ones\.SerialAdmissionBench\(Theorem[2](https://arxiv.org/html/2607.00269#Thmtheorem2)\) runs8080concurrent proposals over a shared capacity object; the unserialized and weak\-lock baselines commit invalid proposals and underflow capacity, while ATP commits only the3232valid proposals through a serialized boundary and yields a serial\-equivalent history\.ObligationBench\(Theorem[4](https://arxiv.org/html/2607.00269#Thmtheorem4)\) fires active commitment records under four continuation sources; the baselines let wakeups mutate domain state directly \(1212and1616unauthorized mutations\), while ATP routes every wakeup through ordinary admission and commits zero\.CompensationProjectionBenchstresses compensation, supersession, and replay across seven dependency scenarios; the projection baselines admit invalid compensations and project ineffective history as current truth \(sevenStateViewmismatches\), while ATP keepsStateViewthe projection of effective committed records only, with zero mismatches\.StorageSubstrateBenchexercises duplicate, stale, and malformed storage attempts; the unconstrained log commits6464invalid attempts and mis\-projects the total, while the ATP storage path \(SQLite default, optional gated PostgreSQL\) rejects all6464and preserves projection\.

The distinctive case isEvidenceRepairBench\(Theorem[3](https://arxiv.org/html/2607.00269#Thmtheorem3)\), which has no classical analogue\. It constructs repairs that discharge their own trigger by deleting a failing test, suppressing an alert, compensating a diagnostic record, or hiding a violated guard\. A naive repair agent and a workflow baseline without an evidence\-preservation rule each commit2020such evidence\-destroying repairs; ATP commits zero, rejecting every repair that would succeed merely by removing the signal that justified it, while still admitting the eight genuinely valid repairs\. This is the property that separates ATP from audit logging: the alarm cannot be silenced by the repair\.

Across all six classes the pattern is identical: the permissive baseline commits the targeted violation, while ATP commits zero and still admits valid work\. This is the operational content of the four theorems of Section[3](https://arxiv.org/html/2607.00269#S3), relative to the declared constraint set𝒞\\mathcal\{C\}\. Because the boundary is enforced by construction, these results are best read as evidence that the implemented gate is wired and unbypassed on the tested hazards, not as a competitive comparison; the comparison against state\-of\-practice mechanisms is RQ2\.

End\-to\-end\.Beyond the unit hazards, real planning\-and\-recovery cases must run end\-to\-end through the same boundary\. J1–J4 instantiate four REALM\-Bench planning and disruption\-recovery casesGeng and Chang \([2026](https://arxiv.org/html/2607.00269#bib.bib20)\), each emitting valid and invalid packages \(six valid, three invalid\) along benchmark case→\\rightarrowproposal→\\rightarrowadmission→\\rightarrowCTL→\\rightarrowStateView, measured against a direct\-workflow baseline that commits every package\. Table[5](https://arxiv.org/html/2607.00269#S5.T5)shows the result: ATP admits the six valid packages, rejects the three invalid ones, completes all four cases with zero invalid commits and a consistentStateView, while the baseline commits all nine and leaves threeStateViewmismatches\. These cases also exercise the reactive\-repair path of §[3\.2](https://arxiv.org/html/2607.00269#S3.SS2): when a disruption fires, the affected obligation wakes and proposes a bounded local repair that re\-enters admission, so end\-to\-end safety already covers reactive recovery; RQ5 then quantifies how*contained*that repair is\.

Table 5:RQ1 end\-to\-end execution on J1–J4\. The unsafe baseline commits invalid case proposals and corruptsStateView; ATP completes all four cases while rejecting invalid packages before commit\.SystemPkgs\.Admit\.RejectInvalidDoneMismatchDirect workflow990343ATP /Mnemosyne963040
### 5\.3RQ2: Does ATP Catch Hazards Workflow/Saga Guardrails Miss?

Does ATP catch hazards that common workflow, saga, or guardrail mechanisms would miss? The safety benchmarks \(RQ1\) use falsification baselines to isolate each hazard class\. RQ2 strengthens the comparison withGuardrailComparatorBench, which models mechanisms commonly available in durable workflow engines and guarded agent stacks: schema validation, finite\-state checks, idempotency keys, retry and timer execution, local saga compensation, and proposer self\-checking\. This comparator is not a product benchmark of Temporal, Cadence, Argo, LangGraph, or any specific framework; it is a semantic baseline for mechanisms those systems commonly provide and hazards they typically leave to application\-level logic\. Consequently, RQ2 should be read as a mechanism\-level baseline rather than a third\-party product comparison; adding a live Temporal, LangGraph, or saga\-library baseline is future empirical work\.

The benchmark contains fourteen cases: four valid operations, four classical guardrail hazards, and six ATP\-specific hazards\. The classical hazards are a malformed proposal, a finite\-state violation, a duplicate operation key, and a failed proposer self\-check\. The ATP\-specific hazards are a stale\-world plan, an evidence\-destroying repair, a direct obligation mutation, an orphaning compensation, an ineffective\-record projection error, and a conflict\-scope violation\. The workflow/saga guardrail stack rejects the classical hazards but does not implement ATP\-specific admission over effectiveStateView, evidence preservation, obligation containment, dependency\-closed compensation, or conflict\-scoped generative admission\.

Table 6:RQ2 mechanism\-level workflow/saga guardrail comparator\. A workflow/saga guardrail stack rejects classical validation hazards, but still commits ATP\-specific hazards\. ATP rejects all invalid cases while admitting all valid cases\.SystemCasesAcceptedRejectedInvalidClassical rej\.Missed ATP hazardsRaw generated write141401006Workflow/saga guardrails14104646ATP /Mnemosyne14410040Table[6](https://arxiv.org/html/2607.00269#S5.T6)shows the completed mechanism\-level comparator run\. The raw generated write baseline commits all fourteen cases, including ten invalid cases\. The workflow/saga guardrail stack improves on that baseline by rejecting all four classical guardrail hazards, but it still commits the six ATP\-specific hazards\. ATP admits the four valid cases, rejects all ten invalid cases, commits zero invalid cases, and misses zero ATP\-specific hazards\. This is the artifact\-level answer to the input\-validation objection: ATP is not merely a predicate checker before commit\. It makes effective state, retained evidence, active obligations, compensation closure, and generative conflict scopes part of the transaction authority boundary\. Appendix[B](https://arxiv.org/html/2607.00269#A2)extends this comparison to a production transaction\-processing substrate, auditing which layer owns each enforcement responsibility\.

### 5\.4RQ3: Does Proposer Quality Affect Usefulness but Not Correctness?

How does proposer competence affect utility while ATP holds committed\-state correctness fixed? We evaluate this usingProposerQualityBench\. The benchmark emits 60 proposals from six proposer classes: no\-intelligence, random, rule\-based, solver\-like, LLM\-like, and adversarial proposers\. Proposal quality controls how many attempts are valid under𝒞\\mathcal\{C\}and how much utility an admitted attempt contributes\. We compare ATP with a direct\-commit baseline that commits every attempt\.

Table 7:RQ3 system\-level result\. Direct commit preserves all generated attempts, including invalid ones; ATP rejects invalid attempts while preserving the same valid utility mass\.SystemAttemptsCommitRejectInvalidUtilityDirect commit6060037131ATP /Mnemosyne6023370131Table[7](https://arxiv.org/html/2607.00269#S5.T7)shows the safety invariant\. The direct\-commit baseline commits all 60 attempts, including 37 invalid attempts\. ATP admits 23 valid attempts, rejects 37 invalid attempts, and commits zero invalid attempts\. The total valid utility is the same because invalid proposals carry zero utility; therefore the usefulness signal appears in the proposer\-level acceptance and utility profile, not in the unsafe direct\-commit row\. The proposer classes in this artifact are deterministic adapters rather than live calls to a frontier LLM, chosen so the safety result is reproducible; the failure modes they inject are exactly those that live models such as Claude 3\.7 and GPT\-4o produce in multi\-agent planningChang and Geng \([2025](https://arxiv.org/html/2607.00269#bib.bib19)\)\. Because admission is evaluated against𝒞\\mathcal\{C\}and the effectiveStateView, the authority\-boundary claim is independent of how a proposal is generated: a live\-model proposer changes which proposals are*useful*, not whether an invalid one can commit\.

01010202030304040505060607070AdversarialNo intel\.RandomRuleLLM\-likeSolver\-like111144252536366464Admitted utility under ATPFigure 5:RQ3 proposer\-quality profile under ATP\. Stronger proposers produce more admissible utility, while every proposer class has zero invalid commits because all attempts remain non\-authoritative until admission\.Table 8:RQ3 proposer\-level result under ATP\. Proposer quality changes acceptance rate, utility, and first\-admission delay; invalid commits remain zero for every proposer class\.ProposerAttemptsAdmittedRejectedAccept\. rateUtilityFirst admissionNo intelligence10190\.1018Random10280\.2045Rule\-based10550\.50252LLM\-like10640\.60362Solver\-like10820\.80641Adversarial10190\.10110The per\-proposer profile \(Figure[5](https://arxiv.org/html/2607.00269#S5.F5)and Table[8](https://arxiv.org/html/2607.00269#S5.T8)\) shows that proposer quality affects usefulness and admission efficiency\. The solver\-like proposer has the highest acceptance rate and admitted utility; the no\-intelligence and adversarial proposers are mostly rejected\. Yet every proposer class has zero invalid commits under ATP\. This supports the paper’s central separation: intelligence governs usefulness, while the transaction layer governs committed\-state correctness relative to𝒞\\mathcal\{C\}\. This is not a learning experiment; it makes no cross\-episode improvement, regret, or preemptive\-planning claim\.

### 5\.5RQ4: What Does the Safety Boundary Cost?

RQ2 establishes that ATP rejects the ATP\-specific hazards in the mechanism\-level workflow/saga comparator; RQ4 audits the cost visible in the implemented ATP infrastructure paths\. We do not time the RQ2 oracle comparator as though it were the ATP runtime, and we do not claim a production load test\. Instead, we run a repository infrastructure workload covering kernel admission, runtime admission, commit\-boundary enforcement, effective\-state projection, validation, compensation, active recovery, and Temporal activity\-boundary validation\. Each repeat executes 20 ATP infrastructure paths, and we measure 30 repeats at worker counts11,44, and88\. The workflow/saga semantic comparator is still executed to preserve the RQ2 baseline, but its single semantic test is not treated as a throughput competitor for the 20\-path ATP infrastructure workload\.

Table 9:RQ4 artifact\-level infrastructure\-cost audit for ATP’s implemented safety paths\. Each run executes 20 real repository paths covering admission, commit\-boundary enforcement, effective\-state projection, validation, compensation, active recovery, and Temporal activity\-boundary validation\. Latencies arep50/p95p\_\{50\}/p\_\{95\}in milliseconds; throughput is infrastructure\-test units per minute\. All settings use 30 repeats\.WorkersPassE2EmsAdmissionmsCommitmsProjectionmsValidationmsPVoverheadThroughputunits/min130/305192\.7 / 5266\.50\.040 / 17\.2352\.574 / 8\.6200\.023 / 1\.7310\.001 / 0\.0575\.98%230\.56430/306356\.6 / 6740\.50\.051 / 22\.8772\.997 / 9\.2940\.025 / 2\.0240\.001 / 0\.0675\.63%709\.10830/3011929\.3 / 12172\.00\.100 / 36\.7315\.120 / 12\.9790\.030 / 3\.6010\.001 / 0\.0944\.96%804\.43Table[9](https://arxiv.org/html/2607.00269#S5.T9)reports the real\-infrastructure result\. All ATP infrastructure runs pass at all three worker counts\. At one worker, the 20\-path workload requires5192\.7/5266\.55192\.7/5266\.5ms end\-to\-endp50/p95p\_\{50\}/p\_\{95\}, with admission latency0\.040/17\.2350\.040/17\.235ms and commit latency2\.574/8\.6202\.574/8\.620ms\. At four workers, measured throughput rises to709\.10709\.10infrastructure units per minute, with projection plus validation accounting for5\.63%5\.63\\%of end\-to\-end runtime\. At eight workers, measured throughput reaches804\.43804\.43infrastructure units per minute; admission and commit tail latency increase, as expected under concurrent pytest execution, but projection plus validation remains bounded at4\.96%4\.96\\%of end\-to\-end runtime\. Thus ATP safety is not free, but the artifact exposes where its implemented infrastructure cost appears\. Together, RQ2 and RQ4 report the safety result and the local artifact overhead audit; they do not establish production\-scale throughput or a product\-level comparison against a deployed workflow engine\.

### 5\.6RQ5: Is Reactive Repair Contained, and Safe Under Recovery\-During\-Recovery?

RQ1 shows reactive repair stays*safe*end\-to\-end; here we ask how*contained*it is, then whether recovery*during*recovery stays safe\. The Bounded Reactive Repair guarantee \(Proposition[1](https://arxiv.org/html/2607.00269#Thmproposition1)\) promises a repair confined to a bounded edit radius, and containment is only meaningful on a workload where a single disruption can ripple across many dependent operations\. We therefore measure it on the job\-shop instances of REALM\-BenchGeng and Chang \([2026](https://arxiv.org/html/2607.00269#bib.bib20)\)using a companion scheduling harness \(MAPLE\) that implements the same bounded\-repair protocol asMnemosyne’s reactive\-repair path\. After computing a feasible baseline schedule, we inject a single machine breakdown and recover it two ways under the same disruption and seeds:*LCRP*, the bounded localized repair, edits only the affected region under the displacement budgetδmax\\delta\_\{\\max\}and iteration capKK;*global recompute*re\-solves the instance from the disruption point with no localization\. Both must end feasible\. Because raw makespan alone rewards a global reset that is physically expensive on a shop floor, we score repair under a cost\-aware objective that also charges for disturbance,

J=Δ​Cmax\+λo​Nops\+λj​Njobs\+λw​Nwip\+λs​Nsetup⏟H,J=\\Delta C\_\{\\max\}\+\\underbrace\{\\lambda\_\{o\}N\_\{\\mathrm\{ops\}\}\+\\lambda\_\{j\}N\_\{\\mathrm\{jobs\}\}\+\\lambda\_\{w\}N\_\{\\mathrm\{wip\}\}\+\\lambda\_\{s\}N\_\{\\mathrm\{setup\}\}\}\_\{H\},counting edited operations, touched jobs, work\-in\-progress moves, and machine\-sequence \(setup\) changes, withλo=1,λj=5,λw=1,λs=10\\lambda\_\{o\}\{=\}1,\\ \\lambda\_\{j\}\{=\}5,\\ \\lambda\_\{w\}\{=\}1,\\ \\lambda\_\{s\}\{=\}10as a sensitivity model that weights job and setup disturbance above a single operation shift\.

Table 10:RQ5 disruption containment: bounded local repair \(LCRP\) vs\. global recompute under a single machine breakdown, mean and median over six job\-shop instances \(both feasible6/66/6; sourcemaple\_lcrp\_containment\_raw\.csv\)\. Global recompute improves makespan by rebuilding unfinished work but edits an order of magnitude more of the schedule; LCRP contains the disruption at far lower disturbance costJJ\.MethodΔ​Cmax\\Delta C\_\{\\max\}OpsJobsWIPSetupHHJJLCRP \(mean\)9\.509\.507\.177\.171\.831\.837\.177\.172\.502\.5048\.5048\.5058\.00\\mathbf\{58\.00\}LCRP \(median\)0\.000\.003\.003\.001\.501\.503\.003\.003\.503\.5053\.5053\.5053\.50\\mathbf\{53\.50\}Recompute \(mean\)−606\.17\-606\.1759\.8359\.838\.008\.0059\.8359\.8360\.8360\.83768\.00768\.00161\.83161\.83Recompute \(median\)−654\.00\-654\.0071\.0071\.008\.008\.0071\.0071\.0079\.0079\.00974\.50974\.50125\.00125\.00Table[10](https://arxiv.org/html/2607.00269#S5.T10)reports medians and means over six instances; both policies recover feasibility \(6/66/6\)\. The contrast is the containment story behind Proposition[1](https://arxiv.org/html/2607.00269#Thmproposition1)\.*Global recompute wins on raw makespan*\(it is free to rebuild unfinished work, soΔ​Cmax\\Delta C\_\{\\max\}is large and negative\),*but it disturbs the whole shop*to do so, editing59\.859\.8operations on average against LCRP’s7\.27\.2\(12\.0%12\.0\\%as many, and about4%4\\%at the median\), touching all88jobs against LCRP’s1\.81\.8, and moving59\.859\.8in\-progress operations against LCRP’s7\.27\.2\. LCRP holds the median makespan exactly \(Δ​Cmax=0\\Delta C\_\{\\max\}=0\) while keeping edit radius and WIP disturbance an order of magnitude smaller, and its cost\-aware objectiveJJis lower in both the mean \(58\.058\.0vs\.161\.8161\.8\) and the median \(53\.553\.5vs\.125\.0125\.0\)\. This is the empirical face of bounded reactive repair: a disruption is contained to its neighborhood instead of triggering a global reset, at equal feasibility and equal\-or\-better makespan where it matters\. When the extra makespan headroom is genuinely worth the disturbance, the runtime can still escalate to a global recompute; the point is that ATP does not pay that cost by default\.

Recovery during recovery\.The hardest reactive case is a failure that arrives*while a repair is still in flight*, and we ask whether nesting introduces any new way to corrupt committed truth\. By construction it cannot\. ATP keeps no recovery stack: after the most recent restore pointSkS\_\{k\}it maintains a pending\-observation setDkD\_\{k\}of unabsorbed disruptions and validates every repair candidate againstSkS\_\{k\},𝒞\\mathcal\{C\}, and all ofDkD\_\{k\}, so a failure arriving mid\-repair is simply appended toDkD\_\{k\}and recovery restarts single\-shot fromSkS\_\{k\}\. Proposition[3](https://arxiv.org/html/2607.00269#Thmproposition3)states the consequence: recursive recovery is exactly sequential recovery over the accumulated observations, every committed transition stays𝒞\\mathcal\{C\}\-feasible at any nesting depth and failure timing, and a sequence ofFFfailures terminates in at mostF​KFKrounds before success or escalation\. Empirically, the only way a mid\-repair failure could commit invalid state is an in\-flight repair that mutates outside admission, and that path is already covered by RQ1: every repair, nested or not, is an ordinary proposal subject toAuthorityBenchandObligationBench, so a wrong or interrupted repair is rejected exactly like any other proposal\. We therefore report recovery\-during\-recovery as validated by construction and by the existing safety suite, and flag a dedicated stress harness \(injecting failures at controlled depths and measuring realized round counts against theF​KFKbound and the escalation frequency\) as in\-progress empirical work\.

### 5\.7Artifact Availability and Reproducibility

The executable artifact is a tagged GitHub snapshotMnemosyne \([2026](https://arxiv.org/html/2607.00269#bib.bib1)\):https://github\.com/eyuchang/Mnemosyne/tree/arxiv\-atp\-rq1\-rq9b\-r8\-v2\. The default reproducibility path is PostgreSQL\-free and runs the safety experiment files withpytest\(expected result9 passed\)\. Full validation commands, the RQ4 infrastructure\-cost benchmark, and the optional environment\-gated PostgreSQL path \(MNEMOSYNE\_POSTGRES\_DATABASE\_URL\) are described in the artifact README\.

## 6Related Work

Transactions, recovery, and input validation\.A classical transaction provides the ACID guarantees \(atomicity, consistency, isolation, and durability\) over a submitted unit of work, together with concurrency control, logging, and recovery, with ARIES the canonical write\-ahead\-logging designGray and Reuter \([1993](https://arxiv.org/html/2607.00269#bib.bib3)\); Bernstein and Newcomer \([2009](https://arxiv.org/html/2607.00269#bib.bib2)\); Weikum and Vossen \([2001](https://arxiv.org/html/2607.00269#bib.bib4)\); Mohanet al\.\([1992](https://arxiv.org/html/2607.00269#bib.bib5)\)\. ATP is complementary: ACID governs how an admitted unit of work commits, whereas ATP governs whether an untrusted generated action should be admitted as a transaction at all\. Schema checks and integrity constraints reject malformed*commands*from a trusted application, whereas ATP distrusts the*generator*itself and adds the effective\-state witness, evidence preservation, obligation containment, and serial\-equivalent generative concurrency, none of which a per\-command predicate expresses\.

Compensation and event sourcing\.Sagas decompose long\-running transactions into compensatable subtransactionsGarcia\-Molina and Salem \([1987](https://arxiv.org/html/2607.00269#bib.bib6)\), and event sourcing and CQRS separate an append\-only history from read\-side projectionsFowler \([2005](https://arxiv.org/html/2607.00269#bib.bib16),[2011](https://arxiv.org/html/2607.00269#bib.bib17)\)\. Mnemosyne adopts both separations but adds constraints they do not: compensation must be dependency\-closed over effective state and must itself pass admission, andStateViewis the effective\-state witness the gate reads rather than a mere read model, because ATP targets generated proposals that may be hallucinated, stale, or adversarial rather than commands already granted authority\.

Active databases and provenance\.Active database systems attach event\-condition\-action rules to database eventsPaton and Díaz \([1999](https://arxiv.org/html/2607.00269#bib.bib18)\);ACRs are deliberately weaker, waking a continuation and constructing a proposal but unable to mutate committed truth, which is the basis of obligation containment\. Provenance and scientific\-workflow systems record lineage for auditBunemanet al\.\([2001](https://arxiv.org/html/2607.00269#bib.bib7)\); Simmhanet al\.\([2005](https://arxiv.org/html/2607.00269#bib.bib9)\); Ludäscheret al\.\([2006](https://arxiv.org/html/2607.00269#bib.bib10)\); Freireet al\.\([2008](https://arxiv.org/html/2607.00269#bib.bib8)\); ATP uses provenance\-like evidence for a stronger admission condition, since a repair cannot discharge its own trigger by destroying the evidence that justified it, making evidence part of the safety contract rather than only explanatory metadata\.

Workflow engines and LLM agents\.Workflow engines provide retries, timers, task graphs, and durable executionRussellet al\.\([2005](https://arxiv.org/html/2607.00269#bib.bib11)\); Argo Project \([2025](https://arxiv.org/html/2607.00269#bib.bib12)\); Temporal Technologies \([2026](https://arxiv.org/html/2607.00269#bib.bib14)\); Cadence Workflow Authors \([2026](https://arxiv.org/html/2607.00269#bib.bib13)\); LangChain \([2024](https://arxiv.org/html/2607.00269#bib.bib15)\), and LLM\-agent research improves generation, tool use, reflection, memory, and multi\-agent simulationYaoet al\.\([2023b](https://arxiv.org/html/2607.00269#bib.bib26),[a](https://arxiv.org/html/2607.00269#bib.bib25)\); Shinnet al\.\([2023](https://arxiv.org/html/2607.00269#bib.bib22)\); Zhouet al\.\([2023](https://arxiv.org/html/2607.00269#bib.bib27)\); Wanget al\.\([2023a](https://arxiv.org/html/2607.00269#bib.bib23)\); Parket al\.\([2023](https://arxiv.org/html/2607.00269#bib.bib21)\); Wanget al\.\([2023b](https://arxiv.org/html/2607.00269#bib.bib24)\)\. ATP treats both as proposers or drivers: engines may schedule, retry, and wake, and an agent’s reasoning trace, tool call, or memory retrieval is evidence, but neither owns committed truth, which changes only through admission\.

Relationship to SagaLLM\.SagaLLMChang and Geng \([2025](https://arxiv.org/html/2607.00269#bib.bib19)\)and ATP pursue trustworthy multi\-agent LLM execution from opposite ends\. SagaLLM brings transactional discipline*to the agent*, wrapping multi\-agent planning in the saga pattern with persistent memory, validation agents, and compensating transactions\. ATP works from the*data\-management end*: a generated action holds no authority until a deterministic gate admits it, and committed\-state correctness is provably independent of the proposing layer \(Theorems[1](https://arxiv.org/html/2607.00269#Thmtheorem1)–[4](https://arxiv.org/html/2607.00269#Thmtheorem4)\)\. The two are complementary: one disciplines the proposer, the other lets the transaction layer accept untrusted proposers under one admission boundary\. On the failures SagaLLM documents, the contrast is concrete: a canceled flight that leaves a hotel active is a*dependency\-closed compensation*the gate refuses if it would orphan an effective dependent; a replan that drops a satisfied constraint is a*stale\-world*rejection against the effective\-state witness; and a repair that hides the violated constraint is blocked by*evidence\-preserving repair*\. Beyond this duality, ATP contributes the effective\-state projection, the safety theorems at the transaction layer, and a complete runtime; preventive or self\-improving recovery is left to future work\.

## 7Conclusion

Agentic workflows need transaction systems that do not trust generated actions: an LLM, solver, or agent may propose, but a generated proposal is not committed truth\. Our central claim is authority separation: relative to a declared executable constraint set𝒞\\mathcal\{C\}and a gate\-closure assumption, proposer behavior affects proposal usefulness, not the ability to append committed truth\. We formalize four safety properties of this boundary \(authority separation, serial\-equivalent generative admission, evidence\-preserving repair, and obligation containment\), add reactive local repair whose proposals re\-enter the same gate, and implement them inMnemosyne\. The reproducible artifact exercises nine safety tests, a cost audit, and a disruption\-containment study in which bounded local repair edits an order of magnitude fewer operations than global recompute: ATP rejects the specified violations while still admitting valid work, at modest overhead\. Production deployment, a live\-LLM quality study, a third\-party workflow benchmark, and cross\-episode learning, regret, and preemptive planning remain future workChang \([2026a](https://arxiv.org/html/2607.00269#bib.bib29),[b](https://arxiv.org/html/2607.00269#bib.bib30)\)\. ACID protects admitted transactions; ATP protects admission into committed truth\.

## Limitations

ATP’s guarantees are relative to𝒞\\mathcal\{C\}: hazards outside𝒞\\mathcal\{C\}are undetected, and writing a faithful𝒞\\mathcal\{C\}is itself work\. RQ2’s guardrail comparator is implemented in the artifact, not benchmarked against a deployed workflow engine; the proposer\-quality experiments use deterministic adapters that replay live\-model failure modes, so results are reproducible while authority separation holds for any proposer\. The artifact does not statically verify that no path bypasses admission, and RQ4’s overhead is a local audit, not a production load test\.

Distributed execution\.The evaluation runs against a single durable store, which is the linearization point for committed truth: each tenant and conflict scope has one authoritativeCTL, so the authority boundary is well defined within a store even when proposers, solvers, and orchestrators are distributed\. External orchestration engines such as Temporal drive execution but never hold commit authority \(Appendix[I](https://arxiv.org/html/2607.00269#A9)\); under network partitions or worker\-node failure they re\-drive activities at least once, and the operation idempotency key together with the outbox deduplication boundary make replays converge to a single committed transition and a single external effect rather than duplicating either\. What we do not yet evaluate is multi\-region or sharded operation, where committed truth would span several stores: maintaining serial\-equivalent admission and outbox idempotency across asynchronous cross\-region updates would require partitioning conflict scopes across stores or a shared consensus log, which, with production\-scale load testing, we leave to future work\.

## References

- Argo Project \(2025\)Argo workflows documentation\.Note:https://argo\-workflows\.readthedocs\.io/en/latest/CNCF graduated project; authoritative docs\.Cited by:[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- P\. A\. Bernstein and E\. Newcomer \(2009\)Principles of transaction processing\.2 edition,Morgan Kaufmann\.Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p1.1),[§2\.3](https://arxiv.org/html/2607.00269#S2.SS3.p1.1),[§2](https://arxiv.org/html/2607.00269#S2.p1.1),[§6](https://arxiv.org/html/2607.00269#S6.p1.1)\.
- P\. Buneman, S\. Khanna, and W\. Tan \(2001\)Why and where: a characterization of data provenance\.InProceedings of the 8th International Conference on Database Theory \(ICDT 2001\),pp\. 316–330\.External Links:[Document](https://dx.doi.org/10.1007/3-540-44503-X%5F20)Cited by:[§6](https://arxiv.org/html/2607.00269#S6.p3.1)\.
- Cadence Workflow Authors \(2026\)Cadence: a distributed, scalable, durable orchestration engine\.Note:https://github\.com/cadence\-workflow/cadenceAccessed 2026\-06\-28\.Cited by:[§4](https://arxiv.org/html/2607.00269#S4.p5.1),[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- E\. Y\. Chang and L\. Geng \(2025\)SagaLLM: context management, validation, and transaction guarantees for multi\-agent llm planning\.Proceedings of the VLDB Endowment18\(12\),pp\. 4874–4886\.External Links:[Document](https://dx.doi.org/10.14778/3750601.3750611)Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p2.1),[§1](https://arxiv.org/html/2607.00269#S1.p3.1),[§1](https://arxiv.org/html/2607.00269#S1.p9.1),[§5\.4](https://arxiv.org/html/2607.00269#S5.SS4.p2.1),[§6](https://arxiv.org/html/2607.00269#S6.p5.1)\.
- E\. Y\. Chang \(2025\)Multi\-LLM agent collaborative intelligence; the path to artificial general intelligence, volume i\.ACM Books\.Note:\(First Amazon edition published in March 2024\)External Links:[Document](https://dx.doi.org/10.1145/3749421),ISBN 979\-8\-4007\-3197\-6Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p2.1)\.
- E\. Y\. Chang \(2026a\)System\-2 reasoning: from semantic anchoring to causal intelligence: the path to artificial general intelligence, volume ii\.ACM Books\.External Links:[Document](https://dx.doi.org/10.1145/3822380),ISBN 979\-8\-4007\-2804\-4Cited by:[§7](https://arxiv.org/html/2607.00269#S7.p1.1)\.
- E\. Y\. Chang \(2026b\)Trivium: temporal regret as a first\-class objective for causal\-memory controllers\.External Links:2606\.04421,[Link](https://arxiv.org/abs/2606.04421)Cited by:[§7](https://arxiv.org/html/2607.00269#S7.p1.1)\.
- M\. Fowler \(2005\)Event sourcing\.Note:https://martinfowler\.com/eaaDev/EventSourcing\.htmlAccessed 2026\-06\-28\.Cited by:[§6](https://arxiv.org/html/2607.00269#S6.p2.1)\.
- M\. Fowler \(2011\)CQRS\.Note:https://martinfowler\.com/bliki/CQRS\.htmlAccessed 2026\-06\-28\.Cited by:[§6](https://arxiv.org/html/2607.00269#S6.p2.1)\.
- J\. Freire, D\. Koop, E\. Santos, and C\. T\. Silva \(2008\)Provenance for computational tasks: a survey\.Computing in Science & Engineering10\(3\),pp\. 11–21\.External Links:[Document](https://dx.doi.org/10.1109/MCSE.2008.79)Cited by:[§6](https://arxiv.org/html/2607.00269#S6.p3.1)\.
- H\. Garcia\-Molina and K\. Salem \(1987\)Sagas\.InProceedings of the 1987 ACM SIGMOD International Conference on Management of Data,pp\. 249–259\.External Links:[Document](https://dx.doi.org/10.1145/38713.38742)Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p1.1),[§6](https://arxiv.org/html/2607.00269#S6.p2.1)\.
- L\. Geng and E\. Y\. Chang \(2026\)REALM\-bench: a real\-world multi\-agent planning and scheduling benchmark\.InProceedings of the 32nd ACM SIGKDD Conference on Knowledge Discovery and Data Mining,Cited by:[§5\.2](https://arxiv.org/html/2607.00269#S5.SS2.p5.4),[§5\.6](https://arxiv.org/html/2607.00269#S5.SS6.p1.2),[§5](https://arxiv.org/html/2607.00269#S5.p1.1)\.
- J\. Gray and A\. Reuter \(1993\)Transaction processing: concepts and techniques\.Morgan Kaufmann\.Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p1.1),[§2\.3](https://arxiv.org/html/2607.00269#S2.SS3.p1.1),[§2](https://arxiv.org/html/2607.00269#S2.p1.1),[§6](https://arxiv.org/html/2607.00269#S6.p1.1)\.
- LangChain \(2024\)LangGraph\.Note:https://github\.com/langchain\-ai/langgraphAccessed 2026\-06\-28\.Cited by:[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- B\. Ludäscher, I\. Altintas, C\. Berkley, D\. Higgins, E\. Jaeger, M\. Jones, E\. A\. Lee, J\. Tao, and Y\. Zhao \(2006\)Scientific workflow management and the kepler system\.Concurrency and Computation: Practice and Experience18\(10\),pp\. 1039–1065\.External Links:[Document](https://dx.doi.org/10.1002/cpe.994)Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p1.1),[§6](https://arxiv.org/html/2607.00269#S6.p3.1)\.
- Mnemosyne \(2026\)Mnemosyne: agentic transaction processing evaluation artifact\.Note:https://github\.com/eyuchang/Mnemosyne/tree/arxiv\-atp\-rq1\-rq9b\-r8\-v2Executable artifact and artifact\-evaluation instructions for reproducing the ATP/Mnemosyne safety, comparator, proposer\-quality, infrastructure\-cost, and deployment\-boundary results\.Cited by:[§5\.7](https://arxiv.org/html/2607.00269#S5.SS7.p1.1)\.
- C\. Mohan, D\. Haderle, B\. Lindsay, H\. Pirahesh, and P\. Schwarz \(1992\)ARIES: a transaction recovery method supporting fine\-granularity locking and partial rollbacks using write\-ahead logging\.ACM Transactions on Database Systems17\(1\),pp\. 94–162\.External Links:[Document](https://dx.doi.org/10.1145/128765.128770)Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p1.1),[§2\.3](https://arxiv.org/html/2607.00269#S2.SS3.p1.1),[§6](https://arxiv.org/html/2607.00269#S6.p1.1)\.
- J\. S\. Park, J\. C\. O’Brien, C\. J\. Cai, M\. R\. Morris, P\. Liang, and M\. S\. Bernstein \(2023\)Generative agents: interactive simulacra of human behavior\.InProceedings of the 36th Annual ACM Symposium on User Interface Software and Technology,External Links:[Document](https://dx.doi.org/10.1145/3586183.3606763)Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p2.1),[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- N\. W\. Paton and O\. Díaz \(1999\)Active database systems\.ACM Computing Surveys31\(1\),pp\. 63–103\.External Links:[Document](https://dx.doi.org/10.1145/311531.311623)Cited by:[§6](https://arxiv.org/html/2607.00269#S6.p3.1)\.
- N\. Russell, A\. H\. M\. ter Hofstede, D\. Edmond, and W\. M\. P\. van der Aalst \(2005\)Workflow resource patterns: identification, representation and tool support\.InCAiSE 2005,Lecture Notes in Computer Science, Vol\.3520,pp\. 216–232\.External Links:[Document](https://dx.doi.org/10.1007/11431855%5F16)Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p1.1),[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- N\. Shinn, F\. Cassano, A\. Gopinath, K\. Narasimhan, and S\. Ma \(2023\)Reflexion: language agents with verbal reinforcement learning\.Note:arXiv preprint arXiv:2303\.11366Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p2.1),[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- Y\. L\. Simmhan, B\. Plale, and D\. Gannon \(2005\)A survey of data provenance in e\-science\.SIGMOD Record34\(3\),pp\. 31–36\.External Links:[Document](https://dx.doi.org/10.1145/1084805.1084812)Cited by:[§6](https://arxiv.org/html/2607.00269#S6.p3.1)\.
- Temporal Technologies \(2026\)Temporal documentation: durable execution\.Note:https://docs\.temporal\.io/Accessed 2026\-06\-28\.Cited by:[§4](https://arxiv.org/html/2607.00269#S4.p5.1),[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- G\. Wang, Y\. Xie, Y\. Jiang, A\. Mandlekar, C\. Xiao, Y\. Zhu, L\. Fan, and A\. Anandkumar \(2023a\)Voyager: an open\-ended embodied agent with large language models\.Note:arXiv preprint arXiv:2305\.16291Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p2.1),[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- L\. Wang, C\. Ma, X\. Feng, Z\. Zhang, H\. Yang, J\. Zhang, Z\. Chen, J\. Tang, X\. Chen, Y\. Lin, W\. X\. Zhao, Z\. Wei, and J\. Wen \(2023b\)A survey on large language model based autonomous agents\.Note:arXiv preprint arXiv:2308\.11432Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p2.1),[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- G\. Weikum and G\. Vossen \(2001\)Transactional information systems: theory, algorithms, and the practice of concurrency control and recovery\.Morgan Kaufmann\.Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p1.1),[§2\.3](https://arxiv.org/html/2607.00269#S2.SS3.p1.1),[§2](https://arxiv.org/html/2607.00269#S2.p1.1),[§6](https://arxiv.org/html/2607.00269#S6.p1.1)\.
- S\. Yao, D\. Yu, J\. Zhao, I\. Shafran, T\. L\. Griffiths, Y\. Cao, and K\. Narasimhan \(2023a\)Tree of thoughts: deliberate problem solving with large language models\.InAdvances in Neural Information Processing Systems,Vol\.36\.Cited by:[§1](https://arxiv.org/html/2607.00269#S1.p2.1),[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- S\. Yao, J\. Zhao, D\. Yu, N\. Du, I\. Shafran, K\. Narasimhan, and Y\. Cao \(2023b\)ReAct: synergizing reasoning and acting in language models\.InProceedings of the 11th International Conference on Learning Representations,Note:https://openreview\.net/forum?id=PNv7R5eOoGCited by:[§1](https://arxiv.org/html/2607.00269#S1.p2.1),[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.
- A\. Zhou, K\. Yan, M\. Shlapentokh\-Rothman, H\. Wang, and Y\. Wang \(2023\)Language agent tree search unifies reasoning, acting, and planning in language models\.Note:Preprint, arXiv:2310\.04406Cited by:[§6](https://arxiv.org/html/2607.00269#S6.p4.1)\.

## Appendix APer\-Property Safety Results

This appendix gives the full per\-class result tables for the six safety hazard classes summarized in RQ1 \(Section[5\.2](https://arxiv.org/html/2607.00269#S5.SS2)\) and visualized in Figure[4](https://arxiv.org/html/2607.00269#S5.F4); each comparesMnemosyneagainst the deliberately permissive baseline\(s\) for that class\. Table[11](https://arxiv.org/html/2607.00269#A1.T11)reportsAuthorityBench: a raw\-append baseline and a self\-validation baseline each commit3535invalid generated transitions, whileATPcommits zero and still admits the five valid proposals\. Table[12](https://arxiv.org/html/2607.00269#A1.T12)reportsSerialAdmissionBench: under8080concurrent proposals over a shared capacity object, the unserialized and weak\-lock baselines commit invalid proposals and underflow capacity, whileATPcommits only the3232valid proposals through a serialized boundary and yields a serial\-equivalent history\. Table[13](https://arxiv.org/html/2607.00269#A1.T13)reportsEvidenceRepairBench: the naive\-repair and no\-rule workflow baselines each commit2020evidence\-destroying repairs, whileATPcommits zero and still admits the eight valid repairs\. Table[14](https://arxiv.org/html/2607.00269#A1.T14)reportsObligationBench: the trigger\-direct and timer\-direct baselines commit1212and1616unauthorized wakeup mutations, whileATProutes every wakeup through ordinary admission and commits zero\. Table[15](https://arxiv.org/html/2607.00269#A1.T15)reportsCompensationProjectionBench: the projection baselines admit five invalid compensations and produce sevenStateViewmismatches, whileATPproduces zero and still commits the two valid compensations\. Table[16](https://arxiv.org/html/2607.00269#A1.T16)reportsStorageSubstrateBench: the unconstrained log commits6464invalid storage attempts and oneStateViewmismatch, while theATPstorage path rejects all6464with zero mismatches\.

Table 11:Authority separation\. Unsafe baselines commit invalid generated proposals; ATP rejects all invalid proposals while still admitting valid ones\.SystemInvalidcommitsRejectedinvalidValidcommitsRaw append3505Self\-validation3505ATP /Mnemosyne0355Table 12:Serial\-equivalent admission under concurrency\. Unsafe baselines commit invalid concurrent proposals and produce non\-serial\-equivalent state; ATP admits only valid proposals through a serialized transaction boundary\. Column SEA denotes serial equivalence\.SystemCommittedRejectedInvalidUnderflowSEAUnserial\. writes800481noWeak lock6812361noATP /Mnemosyne324800yesTable 13:Evidence\-preserving repair\. Unsafe baselines admit repairs that hide trigger evidence while leaving the underlying failure unresolved; ATP rejects all such repairs and still admits valid repairs\.SystemEvidence\-destroyingRejectedevid\.\-dest\.ValidrepairsNaive repair2004Workflow w/o rule2008ATP /Mnemosyne0208Table 14:Obligation containment\. Unsafe baselines allow wakeups to mutate committed domain state without ordinary admission; ATP allows wakeups to emit proposal packages but rejects unauthorized mutations before commit\.SystemUnauthorizedmutationsProposalpackagesAdmittedRejectedTrigger direct12000Timer direct write16000ATP /Mnemosyne024420Table 15:Effective\-state and compensation safety\. Unsafe projection baselines admit invalid compensations and project ineffective history as current truth; ATP rejects invalid compensations and preservesStateViewas the projection of effective committed records only\.SystemInvalidadmittedOrphaneddeps\.BrokenchainsStateViewmismatchesValidUnsafe projection baselines52572ATP /Mnemosyne00002Table 16:Storage\-substrate correctness\. The unconstrained log baseline commits duplicate or malformed storage attempts; the ATP storage path rejects invalid attempts and preserves effective\-state projection\. The PostgreSQL\-backed store is implemented and exercised by environment\-gated live conformance tests; the default artifact path is PostgreSQL\-free\.SystemSubs\.CommittedRejectedInvalidMismatchUnconstr\. logmem1280641ATP storageSQLite646400
## Appendix BCoverage Audit: ATP and a Production Transaction\-Processing Substrate

This appendix extends the RQ2 comparator \(Table[6](https://arxiv.org/html/2607.00269#S5.T6)\) with a third layer: a production transaction\-processing \(TP\) substrate such as PostgreSQL\. ATP is not a replacement for production TP\. PostgreSQL\-style systems provide the durable substrate, with atomicity, isolation, durability, uniqueness, foreign keys, checks, triggers, and serializable execution\. ATP is complementary: it governs whether a generated proposal should receive transaction authority before it becomes an ordinary transaction\. The distinction matters because several agentic hazards are not storage\-level violations unless application developers manually encode ATP\-specific semantics\.

Table[17](https://arxiv.org/html/2607.00269#A2.T17)is an analytical coverage audit, not a throughput benchmark: each entry is a by\-design assessment of which layer naturally owns the corresponding check\. “App\-only” means the TP substrate can enforce the property only if the application explicitly encodes the ATP\-specific rule; “partial” means the mechanism catches one implementation of the hazard but not its general ATP form\.

Table 17:Coverage audit: a production TP substrate versus workflow/saga guardrails versus ATP\. Entries are by\-design assessments of which layer owns each check, not measured throughput\.HazardPostgreSQL\-style TPWorkflow/sagaATP/MnemosynePrimary\-key / unique duplicatecaughtcaughtcaughtMissing foreign\-key dependencycaughtcaughtcaughtFinite\-state invalid transitionapp\-onlycaughtcaughtStale\-world proposalmissedmissedcaughtOrphaning compensation over effective stateapp\-onlypartialcaughtEvidence\-destroying repairmissedmissedcaughtACRdirect domain mutationmissedmissedcaughtGenerative conflict\-scope collisionapp\-onlypartialcaughtDuplicate side\-effect intentpartialpartialcaught \(staged, then rejected\)The audit identifies a layer boundary rather than a weakness in PostgreSQL or other TP systems\. Production TP systems are strong commit substrates, but they do not by themselves define which generated proposal should be granted transaction authority\. ATP addsStateView\-based admission, retained\-evidence checks, dependency\-closed compensation, non\-authoritativeACRwakeups, and generative conflict scopes before a proposal becomes a transaction; once a proposal is admitted, ATP relies on a production TP substrate for atomic commit, durability, uniqueness, and isolation\.

An executable version of this audit \(ProductionTPComparatorBench\) is future work\. It would run the same cases through \(i\) a PostgreSQL\-style TP substrate with keys, foreign keys, checks, triggers, and serializable transactions; \(ii\) a workflow/saga guardrail layer; and \(iii\) ATP/Mnemosyneover the same durable store\. The expected systems claim is not that production TP is weak, but that ATP supplies the missing authority semantics for generated proposals\.

## Appendix CR8 Deployment Smoke\-Load Variability

R8 implements a deployableMnemosyneservice boundary with health, proposal\-submission,StateView, and metrics endpoints\. The purpose of the R8 smoke\-load audit is not to claim production\-scale throughput, but to check that the deployment service preserves ATP’s authority\-separation rule under concurrent HTTP proposal submission: clients may submit proposals, but invalid proposals and explicit bypass attempts must not become committed truth\.

Table[18](https://arxiv.org/html/2607.00269#A3.T18)reports two consecutive local runs of the same deployment load script\. Each worker setting submits 200 HTTP proposal requests\. The workload contains 120 valid proposals and 80 invalid or bypass proposals\. In both runs, every worker setting admits exactly 120 proposals, rejects exactly 80 proposals, and produces zero invalid commits\. Thus the safety result is stable across repeated local runs\.

The throughput measurements are intentionally treated as diagnostic rather than production evidence\. The 16\-worker setting shows substantial run\-to\-run throughput variability despite similarp50/p95p\_\{50\}/p\_\{95\}request latency, indicating sensitivity to local client scheduling, socket backlog, and short\-run wall\-clock effects\. We therefore use R8 only as deployment\-boundary evidence: concurrent HTTP submission preserves the ATP admission boundary, while production load testing over durable PostgreSQL storage, Kubernetes workers, networked workflow services, and pool saturation remains future work\.

Table 18:R8 local deployment smoke\-load variability across two consecutive runs\. Each setting submits 200 HTTP proposal requests to the R8 service\. The stable result is safety: invalid commits remain zero in every run and worker setting\. Throughput is local diagnostic evidence, not a production load\-test claim\.RunWorkersAccepted /RejectedInvalidcommitsLatencyp50/p95p\_\{50\}/p\_\{95\}msThroughput/min11120 / 8000\.281 / 0\.381119,717\.9614120 / 8000\.871 / 1\.515243,307\.1518120 / 8001\.744 / 2\.892245,481\.60116120 / 8003\.398 / 6\.226245,801\.7421120 / 8000\.250 / 0\.380173,746\.8524120 / 8000\.822 / 1\.307271,099\.3928120 / 8001\.743 / 3\.136257,312\.64216120 / 8003\.047 / 5\.39611,784\.96
## Appendix DMnemosyne Architecture and Runtime Data Structures

Store protocolSQLitedefault CIPostgreSQLoptionalPooled PGoptionalScalability / Kubernetes port

Figure 6:Storage substrate boundary\. SQLite is the deterministic default; PostgreSQL and pooled PostgreSQL are optional live\-validation paths\. The scalability and Kubernetes deployment phase changes deployment scale, not ATP correctness semantics\.This appendix specifies the runtime data structures that realize the architecture of Section[4](https://arxiv.org/html/2607.00269#S4)at the level of record fields\. The intent is to make the authority boundary inspectable: every object below is either committed truth, a projection of committed truth, a durable obligation, or an external boundary, and no proposer\-side object can become truth except by passing admission\.

#### Object taxonomy\.

Mnemosynekeeps four kinds of object apart, and logs only the last\. An*event*is an immutable observed fact \(for example, a provider confirmation or a disruption notice\)\. A*candidate*is a proposed finite\-state transition that an admitted commit may or may not produce\. A*constraint evaluation*is a predicate that the admission validator checks\. A*committed transition*is the durable record of an admitted transition: aCTLrecord\. Events, constraints, and finite\-state structure live outside theCTL; only an admitted, committed transition is aCTLrecord\. A vetoed or rejected proposal leaves a queryable rejection or escalation entry, never a committed transition\.

#### The committed\-transition log record\.

ACTLrecord is the unit of committed truth\. Its identity and ordering fields are fixed; its recovery metadata and domain evidence are carried in two typed side\-channels, the metadata mapMMand the typed extensionXX, so that recovery and provenance fields can evolve without changing a transition’s identity\. Table[19](https://arxiv.org/html/2607.00269#A4.T19)lists the fields\.

Table 19:CTLrecord fields\. The identity and ordering fields fix committed truth;MMandXXare typed side\-channels for recovery metadata and domain or causal evidence\. The record is logically append\-only: later transitions may compensate or supersede it, but never erase it\.FieldSymbolRoleridrrUnique record identifier \(primary key\); the idempotency key when client\-supplied\.op\_idOptional client idempotency key, used whenridis server\-assigned\.tx\_group\_idSaga group: the records that compensate together \(indexed, not unique\)\.workflow\_idSession or instance identity \(for example, a ride or trip\)\.binding\_idRole\-binding identity \(an abstract role bound to entities\)\.eidIndividual entity whose state changed\.fsmFinite\-state machine to which the edge belongs\.versionvvMonotonic version per\(eid, fsm\); one ordered history per entity\.state\_befores−s^\{\-\}Pre\-state; the reversal target for compensation\.state\_afters\+s^\{\+\}Post\-state of the committed transition\.action\_typeaaNamed action \(for example, pickup, reroute, compensate\); disambiguates self\-loops\.triggersUUProximate causes \(event identifiers in the recovery\-event log\)\.dependenciesDDRequired preconditions:rids that must be committed and still effective\.metadataMMVerdict, compensation policy, restore flag, status, supersession or compensation links, provenance\.extensionXXSchema\-validated domain and causal\-audit evidence plus temporal\-spatial attributes\.schema\_id/
schema\_versionSchema identity for safe replay across schema evolution\.timestampttCommit time;log\_position\(below\) provides ordering\.The storage layer enforces two uniqueness constraints that carry the safety load:ridis the primary key, so a retried commit cannot double\-apply, and\(eid, fsm, version\)is unique, so each entity has exactly one ordered history\. The saga grouptx\_group\_idis indexed but deliberately*not*unique, so one saga spans many records\. The metadata mapMMcarries the recovery and audit fields, includingstatus\(one ofactive,compensated, orsuperseded\),restore\(whether the record is a clean restore point\), and thecompensatesorsupersedeslinks naming therids a record reverses or replaces\. The typed extensionXXcarries domain attributes \(location, ETA, deadline, route, assignment\) and causal\-audit evidence;XXis schema\-validated rather than free\-form\.

#### Identity and log position\.

Mnemosynekeeps three identities distinct rather than collapsing them into one: the individual entityeid, the role\-bindingbinding\_id, and the session or instanceworkflow\_id\. Conflating them breaks repeated participation \(one entity acting twice\), multi\-party instances \(one session with several participants\), and reassignment \(a resource re\-bound to a new role\)\. Independently of the wall\-clocktimestamp, the store assigns a monotoniclog\_positionthat provides total append ordering for replay and recovery; replay can proceed by per\-entityversionor by globallog\_position\. The recovery\-event log records the fine\-grained events of repair and obligation execution \(packages created, idempotency keys observed, sequence positions assigned, conflicts detected, outcomes accepted or rejected\)\. In the PostgreSQL substrate, tenant\-scoped uniqueness over event identifiers, idempotency keys, and recovery sequence positions provides the concrete concurrent\-idempotency boundary\.

#### StateView: the effective\-state projection\.

StateViewexposes current operational truth\. It is reconstructed from theCTLby replaying only*effective*records: records that have not been compensated, superseded, or invalidated and whose dependency chains remain effective\. Current state is derived, never stored\. Beyond the bare finite\-state value, aStateViewfor an\(eid, fsm\)pair folds theXXattribute deltas forward \(location, ETA, deadline, route, assignment\) and carries the set of effective records that support it, so that admission and the reactive loop read where each entity currently is, not a static plan\. The projection is materialized per\(eid, fsm\)and is a cache: replay from theCTLremains the source of truth\. A cross\-entity correction must re\-project*every*affected entity, because refreshing only the issuing entity could leave a now\-ineffective record lingering as current truth elsewhere\.

#### Active commitment records\.

AnACRis a durable workflow obligation stored in the same committed substrate as ordinary transitions\. It is created by an admitted step, and creating it is itself an admitted transition\. AnACRrecords an assumption or commitment together with the fields in Table[20](https://arxiv.org/html/2607.00269#A4.T20)\. When its trigger fires, the runtime may resume the continuation to construct a repair proposal, but theACRitself cannot mutate committed state: its wakeup re\-enters the ordinary admission gate\.ACRstatus moves through values such aslive,fired,proposed,admitted,rejected,compensated,expired, anddischarged\.

Table 20:ACRfields\. AnACRis a durable obligation in theCTL; its wakeup is a non\-authoritative proposal that re\-enters admission\.FieldRoleidIdentifier of the obligation record\.txnAdmitted transition that created the obligation\.commitmentThe recorded commitment or assumption\.scopeBounded dependency scope the resumed proposal may touch\.triggerCondition whose firing makes the obligation ready\.continuationPointer to the continuation resumed on firing\.guardPredicate gating whether a fired trigger may resume\.validatorAdmission validator applied to the resulting proposal\.compensationCompensation handler for the obligation\.expiryExpiry or discharge condition\.failure\-keyFailure signature for cross\-episode traceability\.statusLifecycle state \(live…\\ldotsdischarged\)\.
#### Inbox and outbox boundaries\.

External events enter through an inbox deduplication boundary; external side effects leave through an outbox boundary that stages provider calls with idempotency keys\. The outbox is an intent log: provider execution remains outside committed truth until its result is observed and admitted as a subsequent transition\. This prevents a domain commit from silently becoming an external effect, and prevents a duplicate external observation from creating a duplicate commit\. Both boundaries sit on the commit side of the authority line but neither owns truth: the inbox only deduplicates inbound observations, and the outbox only stages outbound intent\.

## Appendix EAdmission, Commit, Logging, and Replay

This appendix gives the deterministic admission contract under𝒞\\mathcal\{C\}and the commit, logging, and replay sequence at the mechanism level\. The contract is independent of proposer identity: an LLM, solver, runtime driver, benchmark adapter, orACRwakeup may change the proposal package, but only the ordered admission steps can create committed truth\.

#### The admission contract\.

Admission is the deterministic pre\-commit procedure that decides whether a proposal may become a committed transition\. It reads current effective state fromStateViewand retained evidence, never speculative or rejected proposal history, and applies the ordered checks below\. Steps 1–8 are the executable contract used by the implementation and the RQ1–RQ5 experiments\.

1. 1\.Parse the proposal package and reject malformed packages before commit processing begins\.
2. 2\.Check tenant, entity, idempotency key, operation key, and declared conflict scope\.
3. 3\.Read currentStateViewand retained evidence; do not validate against speculative or rejected proposal history\.
4. 4\.Apply the deterministic constraints in𝒞\\mathcal\{C\}: finite\-state rules, policy rules, stale\-world checks, dependency closure, and compensation safety\.
5. 5\.If the proposal is a repair, require that the underlying failure is resolved under𝒞\\mathcal\{C\}, or that the trigger evidence remains effective and queryable after the repair\.
6. 6\.If the proposal is anACRwakeup, require a proposal package and forbid direct mutation of theCTLorStateView\.
7. 7\.Serialize or reject overlapping incompatible conflict scopes; admit only if the resulting transition is valid over current effective state\.
8. 8\.Atomically append the admitted transition and recovery metadata to durable storage and updateStateView; otherwise record a queryable rejection reason\.

A solver certificate or LLM rationale is treated as evidence supplied to these checks, not as authority\. The validator reads log\-grounded effective state only: a finite\-state edge is checked for legality withaction\_typedisambiguating self\-loops; each dependency is required to be committed*and*still effective \(existence alone is insufficient\); and application constraints are keyed by\(fsm, action\_type\)so that, for example, a pickup may be required to follow the driver’s arrival as read from the driver’s effective state\. The gate returns an admitted transition, a rejected proposal with structured reasons, or an escalation request for a wider scope\.

#### Commit, logging, and projection\.

An admitted proposal commits through a single atomic step that also produces the projection update\. The commit batch is the unit of multi\-entity atomicity\. In one transaction it: locks the affected entities in sorted key order, verifies the expected monotonicversionfor each\(eid, fsm\), re\-checks that every dependency inDDis committed and effective, appends allCTLrows, updates the synchronousStateViewprojection for every affected key, and stages any outbox intents\. Three guarantees hold exactly at the write: idempotency \(theridprimary key, withop\_idas the client key whenridis server\-assigned\), ordering \(the monotonic per\-entityversion\), and dependency effectiveness \(DDcommitted and not since compensated or superseded\)\. Only after this step does a row exist; a rejected proposal yields a queryable rejection, not a row\.

#### Idempotency and retry safety\.

Because durable runtime drivers execute steps at least once, the commit path must be idempotent under retry\. Theridprimary key \(orop\_idwhenridis server\-assigned\) makes a retried commit return the existing committed record rather than duplicate domain truth\. This is why the idempotency key is part of the proposal package and is checked at Step 2 before any state mutation: a retried submission after a crash or timeout resolves to the same committed transition, so the commit batch is safe to re\-drive\.

#### Replay\.

TheCTLis the source of committed truth, and current state is recovered by replay rather than read from a stored cursor\. Replay of an\(eid, fsm\)history proceeds in order and self\-checks consistency: each record’sstate\_beforemust equal the prior record’sstate\_after, and a mismatch is a replay error that signals log corruption\. The bare replay yields the finite\-state value; the full reconstruction is theStateViewthat additionally folds theXXattribute deltas forward and retains the effective records supporting the state\. Because compensation and supersession are themselves later admitted transitions, effective\-state replay reproduces current truth without deleting history or moving a cursor: the effective index marks which records still count, and the projection excludes the rest\.

## Appendix FDisruption, Recovery, and Compensation

This appendix specifies recovery at the mechanism level\. The central property is that recovery does not bypass admission: a disruption, a fired obligation, or a crash\-recovery action produces a proposal that passes through the same gate as any generated action\. Recovery decisions are made in the proposal and policy layers; the substrate supplies only the mechanism and the invariants\.

#### Obligation wakeups do not bypass admission\.

When anACRtrigger fires, the runtime may resume its continuation and construct a repair proposal, but the wakeup carries no write authority\. The resumed proposal declares theACR’s bounded dependencyscopeand re\-enters the ordinary admission gate, where Step 6 requires that anACRwakeup supply a proposal package and forbids direct mutation of theCTLorStateView\. A proposal generated by anACRmay touch only the dependency scope recorded by thatACR, unless a wider scope is explicitly admitted as an escalation\. Thus a fired obligation can only return the system to the proposal\-admission path; it cannot install committed truth on its own\. Rejected or compensatedACRproposals with matching failure signatures remain queryable as historical evidence for future ranking or guard strengthening, which is how memory becomes active without becoming authoritative\.

#### Three recovery moves\.

The class of an action against the full governed\-invariant set, re\-checked at commit time, selects the recovery move; the substrate supplies the mechanism and the policy layer supplies the timing\. Table[21](https://arxiv.org/html/2607.00269#A6.T21)states the three moves\. A restore \(return to a clean checkpoint\) is the bulk form of an undo: it resets state but, unlike an exact undo, does not reverse external effects, so it is paired with compensation\.

Table 21:Recovery moves\. The action’s class against the current governed\-invariant set selects the move; the substrate supplies the mechanism\.MoveWhenMechanismundoAn exact inverse exists \(reversible\)\.Apply the inverse; the entity returns tos−s^\{\-\}\.compensateNo inverse, but governed invariants are restorable within a validity window \(compensable\)\.Append a compensating transition; history is preserved\.escalateNeither holds, or local repair cannot contract \(irreversible\)\.Veto, or hand to a human task; no committed transition is written\.
#### Dependency\-closed compensation and supersession\.

Compensation is represented as a new admitted transition, never as physical deletion, and the whole saga group identified bytx\_group\_idunwinds together\. The group is compensated in reverse topological order over the group’s dependency subgraph, not merely reverse insertion order, so a leg is never compensated before the legs that depend on it\. Admission enforces dependency\-closed compensation through the recovery invariants: a compensation is rejected if it would leave an effective record depending on an ineffective record \(no orphaned effective dependents\), and a compensation is rejected if it would break the effective chain for an entity \(effective\-chain preservation\)\. Supersession is the related operation by which a later admitted transition replaces an earlier one through thesupersedeslink inMM; like compensation, it changes effectiveness without erasing history\.

#### Effective\-chain preservation under cross\-entity correction\.

Compensation and supersession never delete history; they only change which records are effective\. Because the projection is materialized per\(eid, fsm\), a correction that touches several entities must drop the corrected record from current truth on*every*entity it touches, not only the entity that issued the correction\. Refreshing only the issuing entity would let a now\-ineffective record linger as current truth elsewhere\. Replay from theCTLtherefore remains the source of truth, and the per\-entity projection is rebuilt for all affected keys after a correction\.

#### Evidence\-preserving repair\.

A memory\-initiated repair must not discharge its own trigger by deleting, overwriting, compensating, or obscuring the evidence that justified it\. Admission permits a repair to alter trigger evidence only if it verifies, under the retained evidence and validator rules, that the proposed repair addresses the triggering condition rather than merely suppressing its observable signal \(Step 5\)\. Concretely: let a repair proposal be triggered by evidenceEEof a failure conditionFF\. Admission admits the repair only if eitherFFis resolved under𝒞\\mathcal\{C\}, orEEremains effective and queryable after the repair\. As a result, no admitted repair can clear its own trigger by destroying the evidence that caused it, and a repeated failure remains visible through its failure signature for later analysis\.

#### Crash recovery as invariants in reverse\.

A transactional fault, such as a crash mid\-leg, is handled with the same mechanisms\. Recovery locates the most recent record marked as a clean restore point, appends compensating transitions for the saga groups committed after it in reverse topological order \(marking themcompensated\), and resumes the reactive loop from the resulting effective state\. Nothing is deleted and no cursor moves: the original records remain for audit, and effective\-state replay yields current truth because each compensation is itself a later committed transition\. Recovery is thus the ordinary commit invariants \(idempotency, monotonic versions, dependency effectiveness\) run in reverse under a policy\.

## Appendix GStaged Implementation \(R0–R8\) and Reproducibility

This appendix records the staged build ofMnemosyneand the reproducibility path\. The build follows a small\-to\-large discipline: a visible, auditable correctness kernel is established before scale\-out infrastructure is connected, so that the authority boundary \(the central claim\) is not obscured by an external engine or solver\. Table[22](https://arxiv.org/html/2607.00269#A7.T22)lists stages R0 through R8 and their status\. The deployment service boundary \(R8\) is now complete: a deployable service with health, proposal\-submission,StateView, and metrics endpoints is implemented and audited for authority separation under concurrent HTTP submission \(Appendix[C](https://arxiv.org/html/2607.00269#A3)\)\.

Table 22:Staged implementation R0–R8\. Each stage is independently runnable and testable\. The correctness kernel and its safety boundary are completed before deployment scale\-out; R8 changes deployment scale, not the semantics proved in the main text\.StageDeliversDetailStatusR0Substrate kernelCTLschema, append\-only commit, monotonic per\-entity versioning, SQLite store,log\_positionordering\.CompleteR1Effective\-state projectionStateViewreconstruction from effective records; full and effective entity histories\.CompleteR2Deterministic admission under𝒞\\mathcal\{C\}Isolated validator: finite\-state legality, dependency effectiveness, conflict scope, stale\-world checks; structured rejection reasons\.CompleteR3Compensation and recoveryDependency\-closed compensation, supersession, restore points, fail\-closed compensation invariants; recovery\-event log\.CompleteR4Idempotency and boundariesop\_idlogical idempotency, inbox deduplication, outbox intent boundary, multi\-entity atomic commit batch\.CompleteR5Active commitment recordsACRcreation as an admitted transition, non\-authoritative wakeups, scoped repair, failure signatures\.CompleteR6Benchmark and proposer integrationJ1–J4 end\-to\-end harness; proposer\-quality safety\-invariance path; mechanism\-level workflow/saga guardrail comparator\.CompleteR7Storage substrate and cost auditOptional environment\-gated PostgreSQL and pooled\-PostgreSQL paths behind the store protocol; RQ4 infrastructure\-cost audit\.CompleteR8Deployable service boundaryHTTP service with health, proposal\-submission,StateView, and metrics endpoints; authority separation audited under concurrent submission\.Complete#### Default reproducibility path\.

The default reproducibility path is PostgreSQL\-free and deterministic\. It runs the nine executable safety experiment files directly withpytest; the expected result is9 passed\. These nine experiments correspond to the safety properties evaluated in RQ1–RQ4 and the mechanism\-level comparator: authority separation, serial\-equivalent admission, evidence\-preserving repair, obligation containment, effective\-state and compensation safety, storage\-substrate correctness, the J1–J4 end\-to\-end execution, proposer\-quality safety invariance, and the workflow/saga guardrail comparison\. A broader safe command additionally runstests/core,tests/apps, andtests/benchmarks\. Reviewers should not run all oftests/experimentsas a blanket command, because older exploratory imports outside theATPartifact path are intentionally excluded from the reproducibility suite\.

#### Infrastructure\-cost benchmark \(RQ4\)\.

The cost audit is run as a separate infrastructure\-cost benchmark over selected real infrastructure tests rather than as a violation\-suppression experiment\. It reports end\-to\-end, admission, and commit latency, projection\-plus\-validation overhead, and throughput at one, four, and eight workers; projection plus validation remains bounded at under6%6\\%of end\-to\-end runtime\. The benchmark script that generates the RQ4 table is included in the artifact alongsideARTIFACT\_EVALUATION\.md, which lists the exact safety validation command and expected reports\.

#### Optional live PostgreSQL path\.

The live PostgreSQL path for the storage\-substrate experiment is optional and environment\-gated by theMNEMOSYNE\_POSTGRES\_DATABASE\_URLvariable, with an optional connection\-pool dependency\. When supplied, it validates recovery\-event append and list operations, canonical duplicate\-idempotency behavior, clean sequence\-conflict handling, and pooled connection use\. The artifact claim does not require a live database: default CI remains PostgreSQL\-free and pool\-dependency\-free, so the9 passedresult reproduces without any database setup\.

## Appendix HStructure and Scalability of the Constraint Set𝒞\\mathcal\{C\}

A natural objection is that ATP merely moves the correctness burden from the agent prompt into the validator: if every semantic rule must be hand\-coded,𝒞\\mathcal\{C\}does not scale\. In the implementation most of𝒞\\mathcal\{C\}is not hand\-coded per case\. Its rules fall into three classes \(Table[23](https://arxiv.org/html/2607.00269#A8.T23)\)\.

1. 1\.Structurally derived\.Generated mechanically from declarations the application already maintains\. Finite\-state legality is derived from the per\-entity transition table keyed byaction\_type; dependency effectiveness and compensation closure are derived from the effective\-chain overCTL; idempotency and conflict scope are derived from the record’s identity triad\. No per\-rule code is written\.
2. 2\.Declarative predicates\.Declared once as data, not procedures, and checked by a generic evaluator: schema and type constraints, required\-evidence handles, world\-fact freshness keys, and conflict\-scope keys\.
3. 3\.Application validators\.The only genuinely hand\-written part: domain semantics that cannot be derived or declared \(for example, a capacity rule specific to one operation\)\. In the artifact these are a small minority of the constraint surface\.

Table 23:Taxonomy of the constraint set𝒞\\mathcal\{C\}: most rules are derived or declared, not hand\-coded per case\.ClassHow declaredExamplesStructurally derivedgenerated from FSM table, effective\-chain, identity triadfinite\-state legality, dependency effectiveness, compensation closure, idempotency, conflict scopeDeclarative predicatesdeclared as data, evaluated genericallyschema and type, required evidence, world\-fact freshnessApplication validatorshand\-written per operationdomain capacity and business rulesA proposal package is admissible when it satisfies the conjunction of all applicable constraints, which in grammar form is:

```
admit(p)       := structural(p) AND declarative(p) AND validators(p)
structural(p)  := fsm_legal(p) AND deps_effective(p)
                  AND compensation_closed(p) AND idempotent(p)
                  AND scope_consistent(p)
declarative(p) := schema_ok(p) AND evidence_present(p)
                  AND world_fresh(p)
validators(p)  := conjunction of application-declared predicates
```

Because the structural and declarative classes are generated from declarations the application already keeps \(entity FSMs, the dependency model, the schema\), adding a new operation typically extends𝒞\\mathcal\{C\}by declaration rather than by new validator code\. That is what keeps the admission boundary scalable as an application grows, and it bounds the hand\-written surface to genuine domain semantics\.

## Appendix IWorkflow\-Engine and Storage\-Substrate Selection

This appendix records the substrate selection and its rationale\. The governing principle is that the substrate is non\-authoritative: a workflow engine or storage backend may change deployment scale, availability, or throughput, but it must preserve theATPauthority boundary\. Committed truth is produced only by admitted transitions, regardless of which engine orchestrates the work or which store persists the log\.

#### Why the substrate is non\-authoritative\.

Mnemosyneseparates orchestration from authority\. Runtime drivers schedule work, fire timers, retry steps, and wake obligations, but they do not own committed truth: a driver may detect that anACRis ready, call a proposal provider, submit a package, and record a deterministic summary, yet it may not directly mutate domain truth\. Keeping the source of truth in theCTLrather than in engine\-internal state is a deliberate design fork\. Letting the engine own state would tie the design to one engine and weaken the validator’s evidence story, because admission reads the effective\-state projection rather than engine\-private execution history\. Holding the authority boundary in the admission gate is what lets a deployment substrate change without changing the correctness semantics\.

#### Two\-tier, PostgreSQL\-anchored recommendation\.

The deciding requirement is a true ACID store with snapshot isolation, which PostgreSQL provides natively through MVCC\. The recommendation is therefore a PostgreSQL\-anchored two\-tier substrate: a Postgres\-backed durable\-execution and transaction core that hosts theCTL, the effective\-state projection, and the recovery\-event log in one store, with a compute fan\-out tier layered beneath it for concurrent proposal and probe execution\. The durable tier supplies transactional bookkeeping and a measurable commit\-failure rate; the compute tier supplies node\-count scale\. In the reference implementation the store protocol admits SQLite as the deterministic default for local development and CI and PostgreSQL \(and pooled PostgreSQL\) as optional, environment\-gated live\-validation paths \(Figure[6](https://arxiv.org/html/2607.00269#A4.F6)\)\. The scalability and Kubernetes deployment phase is a deployment concern that may add containerized services, durable\-workflow workers, orchestration, observability, and load tests; it changes deployment scale, notATPcorrectness semantics\.

#### Durable\-execution survey: interop targets, not authority\.

The 2025–2026 durable\-execution category provides persistence, retries, and exactly\-once or ACID semantics as infrastructure, andMnemosynebuilds theCTLand theATPlayer on top of such an engine rather than reimplementing logging or recovery primitives\. Table[24](https://arxiv.org/html/2607.00269#A9.T24)summarizes the engines considered\. They are treated as interoperability or deployment targets behind an engine\-agnostic interface, not as the authority for committed truth: durable workflow engines such as Temporal and Cadence orchestrate execution but are non\-authoritative, and Argo Workflows is retained as a Kubernetes deployment and export target rather than a transaction engine\. Checkpoint\-persistence agent frameworks are explicitly excluded as the transactional substrate, because checkpoint persistence is not durable execution with exactly\-once or ACID guarantees; they may serve only as optional agent\-authoring layers above a real durable engine\.

Table 24:Durable\-execution and orchestration engines considered\. Each is an interoperability or deployment target behind an engine\-agnostic interface; none owns theATPauthority boundary, which remains in the admission gate\.EngineModelRole forMnemosynePostgreSQLACID store with MVCC snapshot isolationAnchor substrate: hostsCTL,projection, recovery log\.SQLiteEmbedded ACID storeDeterministic default for local development and CI\.TemporalDurable execution, code\-defined sagasOrchestration and scale escape hatch; non\-authoritative\.CadenceDurable execution \(Temporal predecessor\)Orchestration interop target; non\-authoritative\.Argo WorkflowsKubernetes DAG executionDeployment and export target, not a transaction engine\.
#### Engine portability\.

The durable\-execution core sits behind an engine\-agnostic interface so that the choice of orchestrator is a contained substitution\. The Temporal\-style boundary makes the contract concrete: the workflow layer is deterministic and side\-effect free \(timers, timeouts, retries, signals\), while the activity layer performs the side effects \(validate the commit batch, build theCTLrecords, commit, reprojectStateView, stage outbox\)\. The workflow orchestrates and the activity commits, but the store andCTLown truth\. Because activities execute at least once under a retry policy, theop\_ididempotency key makes a retried activity return the existing committed record rather than duplicate domain truth\. This portability is why the same authority boundary holds whether the orchestrator is a local driver or a durable workflow engine, and why a change of engine does not change the safety properties proved in the main text\.

## Appendix JWorked Proposal Examples

This appendix makes the*proposal is not truth*boundary concrete\. The examples use compact JSON\-like records to show what crosses the proposal boundary and what the admission gate does before anything becomes committed truth\. They are illustrative but match the implementation contract used throughout the artifact: a proposal package carries a tenant, entity, operation, dependency set, world assumptions, conflict scope, evidence handles, and an idempotency key\. Admission evaluates the package against the current effectiveStateView, retained evidence, and the declared constraint set𝒞\\mathcal\{C\}\. Two axes matter independently: whether the proposal is*well formed*, and whether the committed*output*it would produce is𝒞\\mathcal\{C\}\-valid\.

### J\.1Valid Proposal

A valid proposal may come from an LLM, solver, workflow driver, or active commitment wakeup\. The proposer supplies a candidate action, but the candidate stays non\-authoritative until admission accepts it\.

```
{
  "proposal_id": "p_valid_hotel_001",
  "tenant": "t1",
  "entity": "trip_17",
  "operation": "book_hotel",
  "depends_on": ["flight_f1"],
  "world_assumptions": {"flight_f1_status": "confirmed"},
  "conflict_scope": "t1/trip_17/lodging",
  "evidence": ["user_request_e1"],
  "idempotency_key": "book_hotel_trip17_once"
}
```

Admission result\.Accepted\. The referenced flight remains effective inStateView, the world assumption is current, no incompatible proposal occupies the lodging conflict scope, and the idempotency key is fresh\.

Committed effect\.The admitted hotel\-booking transition is appended to the committed\-transition log \(CTL\);StateViewprojects the booking as effective current truth; a confirmation message may be staged in the outbox under its own idempotency key\.

### J\.2Invalid Proposal

The next proposal is syntactically well formed but semantically stale\. A classical parser would accept the record; ATP rejects it before commit because its assumptions disagree with observed effective state\.

```
{
  "proposal_id": "p_stale_hotel_002",
  "tenant": "t1",
  "entity": "trip_17",
  "operation": "book_hotel",
  "depends_on": ["flight_f2"],
  "world_assumptions": {"flight_f2_status": "confirmed"},
  "observed_world": {"flight_f2_status": "cancelled"},
  "conflict_scope": "t1/trip_17/lodging",
  "evidence": ["user_request_e1"],
  "idempotency_key": "book_hotel_trip17_once"
}
```

Admission result\.Rejected\. The proposal depends on a flight that is no longer effective under the observed world facts\. The rejection is recorded with a durable reason, but no domain transition is appended\.

Committed effect\.CTLis unchanged with respect to domain truth,StateViewis unchanged, and no external side effect is staged\.

### J\.3Valid Output After a Valid Proposal

A valid admitted proposal may create a valid outbox intent\. The outbox record is not the external effect itself; it is an admitted intent to perform the effect under an idempotency key\.

```
{
  "proposal_id": "p_notify_after_booking_003",
  "tenant": "t1",
  "entity": "trip_17",
  "operation": "stage_outbox_notification",
  "depends_on": ["hotel_booking_b1"],
  "message_type": "booking_confirmation",
  "recipient": "user_u1",
  "conflict_scope": "t1/trip_17/notification",
  "idempotency_key": "notify_trip17_booking_once"
}
```

Admission result\.Accepted\. The booking dependency is an effective committed fact, the outbox idempotency key has not been consumed, and no incompatible notification intent exists for the same scope\.

Committed effect\.CTLrecords the admitted outbox intent;StateViewexposes the notification as staged; the provider call stays outside committed truth until its result is observed and admitted as a later transition\.

### J\.4Invalid Output After a Valid Proposal

Even after a valid domain proposal, a later output proposal can be invalid\. Here an agent tries to charge a card twice by changing only the provider\-level idempotency key while targeting the same committed payment obligation\.

```
{
  "proposal_id": "p_duplicate_charge_004",
  "tenant": "t1",
  "entity": "trip_17",
  "operation": "stage_outbox_payment",
  "depends_on": ["hotel_booking_b1"],
  "payment_obligation": "hotel_booking_b1/deposit",
  "amount": "250.00",
  "conflict_scope": "t1/trip_17/payment/deposit",
  "idempotency_key": "pay_deposit_trip17_b1_once",
  "provider_idempotency_key": "new_key_but_same_obligation"
}
```

Admission result\.Rejected \(or escalated for reconciliation\)\. The proposal targets an already staged or satisfied payment obligation under the same semantic conflict scope and obligation idempotency key\. A changed*provider*key is evidence, not authority to create a duplicate external effect\.

Committed effect\.No duplicate outbox payment intent becomes current truth, and the rejected package remains queryable as evidence for audit or guard strengthening\. Only the first and third proposals commit; the second and fourth are rejected with a durable reason, so committed\-state correctness is independent of how the proposal was generated\.

## Appendix KAn End\-to\-End Transaction Trace

This appendix traces one disruption\-recovery path through ATP, separating five objects that agentic systems often conflate: input observation, proposal package, admission decision, committed log record, and external side\-effect intent\. It continues the trip scenario of Appendix[J](https://arxiv.org/html/2607.00269#A10)\.

### K\.1Input Observation

```
flight_cancelled(flight_f1)
source_event_id = flight_provider_event_e123
observed_at     = 2026-06-30T10:15:00Z
```

The input observation is evidence\. It is not, by itself, a domain repair, and it grants no write authority to the proposer or the runtime driver\.

### K\.2Proposal Package

A planner or active commitment wakeup proposes a repair package:

```
{
  "proposal_id": "p_repair_trip_017",
  "tenant": "t1",
  "entity": "trip_17",
  "operation": "repair_trip_after_flight_cancellation",
  "depends_on": ["flight_f1", "hotel_h1"],
  "evidence": ["flight_provider_event_e123"],
  "conflict_scope": "t1/trip_17",
  "proposed_steps": [
    "compensate_hotel(hotel_h1)",
    "search_alternate_flight(trip_17)",
    "notify_user(user_u1)"
  ],
  "idempotency_key": "repair_trip17_after_flight_f1_once"
}
```

The proposal is not committed truth; it is a candidate package supplied to the admission gate\.

### K\.3Admission

Admission evaluates the package against𝒞\\mathcal\{C\}and the current effective state:

```
checks:
  dependency closure:    hotel_h1 depends on flight_f1
  stale-world facts:     flight_f1 is observed cancelled
  compensation safety:   no effective downstream record is orphaned
  evidence preservation: flight_provider_event_e123 stays queryable
  conflict scope:        no active repair owns t1/trip_17
  idempotency:           repair_trip17_after_flight_f1_once is fresh
```

If all checks pass, the proposal is admitted; if any fails, the rejection and its reason remain durable, but the proposed repair does not become domain truth\.

### K\.4Committed\-Transition Log

An admitted repair appends records such as:

```
CTL append:
  compensation_requested(hotel_h1)
  repair_proposal_admitted(trip_17)
  ACR_updated(trip_repair_obligation)
  recovery_metadata(...)
```

CTLis the source of committed truth\. Compensation is logical: the earlier hotel record is not erased; it becomes ineffective only through admitted compensating transitions and effective\-state projection\.

### K\.5StateView

StateViewprojects current effective truth fromCTL:

```
StateView:
  flight_f1              = cancelled
  hotel_h1               = compensation_pending
  trip_17                = repair_in_progress
  trip_repair_obligation = live
```

StateViewis not raw history: it excludes compensated, superseded, or otherwise ineffective records while preserving fullCTLhistory for audit\.

### K\.6Outbox

External actions are staged rather than executed as hidden side effects of the planner:

```
outbox:
  notify_user(user_u1)
  idempotency_key = notify_trip17_repair_once
  status          = staged
```

An outbox intent is not the external effect itself\. The provider call and its result stay outside committed truth until observed and admitted as later evidence, which prevents a generated proposal from silently turning into an irreversible external mutation\.

### K\.7Boundary Summary

> Input observation is evidence, not committed repair\. A proposal is candidate intent, not truth\. An outbox intent is a staged effect, not external truth\. Only admittedCTLrecords define committed truth, andStateViewis the effective projection used for future admission\.