diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc
index 4ef422b..eb16108 100644
--- a/PROOF-NEEDS.adoc
+++ b/PROOF-NEEDS.adoc
@@ -67,6 +67,13 @@ tables must agree.
 | G-3 | The FFI bridge preserves grade 𝟙 (homomorphism) | OPEN | resource-algebra lists homomorphisms OPEN; to file from JNK-01
 | E-1 | An attacker cannot recover obliterated content or use a revoked key | OPEN | `+Types.adversaryCannotKnow+` holds only because `+Knows+` has no Adversary constructor (#145 item 3)
 | X-1 | Hash one-wayness; physical erasure (cryptographic and physical assumptions, external to this repository) | ASSUMED | not theorems of this repo
+| T-1 | Undoing a fully executed transaction's operations in reverse order restores the state it began in, given each step's undo restores its execute (the sequential Theorem 3.4) | PROVEN | `+TransactionAtomicity.rollback-restores+`; `+tests/reject-agda/ForwardRollback.agda+` refused
+| T-2 | begin, add_operation, commit and mark_rolled_back each preserve the log invariant (given a fresh id for begin) and rewrite only the Active transaction, so a completed one is never modified | PROVEN | `+TransactionAtomicity.lifecycle-preserves-good+`; `+tests/reject-agda/CommitWhenIdle.agda+` refused
+| T-3 | At most one transaction is Active, and exactly one when the active pointer is set | PROVEN | `+TransactionAtomicity.at-most-one-active+`
+| T-4 | A rollback that fails part-way can be retried to completion | OPEN | reproduced 2026-10-26 with the real `+jk+`: after one undo error the repaired retry stops at the first, already undone, operation and the transaction stays Active (`+cmd_rollback+`, `+?+` on `+undo+`)
+| T-5 | The transaction log survives an I/O failure or a crash during save without disagreeing with memory or being corrupted | OPEN | by inspection, not reproduced: begin, add_operation and commit mutate the in-memory log before `+save()?+`, and `+save+` is a plain `+fs::write+`
+| T-6 | A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1; single steps are TESTED by `+execute_then_undo_is_identity+`) | ASSUMED | not checked for the failure path
+| T-7 | Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) | ASSUMED | probabilistic, not checked
 |===
 
 Removed, with the reason recorded beside the replacement in source:
@@ -130,7 +137,7 @@ attestations undermine trust
 |Content store integrity |Content-addressed storage never returns wrong
 content |Hash collisions or bugs corrupt stored data
 
-|Transaction atomicity |Delta application is atomic and reversible
+|Transaction atomicity |Delta application is atomic and reversible (the model is proved, T-1 to T-3; the partial-rollback, I/O-failure and id-freshness gaps are T-4 to T-7)
 |Partial transactions corrupt state
 
 |reversible-core |Undo/redo preserves data integrity |Core crate used by
@@ -173,6 +180,9 @@ the status table above.
 |C-4: Replacing an attestation-chain entry by one with a different hash breaks the link |PROVEN |`src/abi/JanusKey/ABI/Proofs.idr::tamperBreaksLink` |`idris2 --typecheck src/abi/januskey-abi.ipkg`
 |C-5: The 32-, 16- and 112-byte ABI structs are 8-byte aligned (divisibility at the literals) |PROVEN |`src/abi/JanusKey/ABI/Layout.idr::oblitAligned` |`idris2 --typecheck src/abi/januskey-abi.ipkg`
 |G-1: Reversibility as a Loss grade: a trace is lossless only if every step is, and an obliterating step absorbs |PROVEN |`verification/proofs/agda/Reversibility.agda::lossless-trace-all` |`bash scripts/check-agda.sh`
+|T-1: Undoing a fully executed transaction's operations in reverse order restores the state it began in, given each step's undo restores its execute |PROVEN |`verification/proofs/agda/TransactionAtomicity.agda::rollback-restores` |`bash scripts/check-agda.sh`
+|T-2: begin, add_operation, commit and mark_rolled_back each preserve the log invariant (given a fresh id for begin) and rewrite only the Active transaction |PROVEN |`verification/proofs/agda/TransactionAtomicity.agda::lifecycle-preserves-good` |`bash scripts/check-agda.sh`
+|T-3: At most one transaction is Active, and exactly one when the active pointer is set |PROVEN |`verification/proofs/agda/TransactionAtomicity.agda::at-most-one-active` |`bash scripts/check-agda.sh`
 |A-3: Idris2 struct sizes, status codes, enums and exported symbols agree with januskey.h and ffi/zig |TESTED |`scripts/check-abi-layout.sh::check-abi-layout` |`bash scripts/check-abi-layout.sh`
 |A-4: A linearly held library handle cannot be closed twice |TESTED |`tests/reject-idris/DoubleClose.idr::DoubleClose` |`bash scripts/check-idris-reject.sh DoubleClose`
 |A-4: A linearly held library handle cannot be forgotten |TESTED |`tests/reject-idris/ForgottenClose.idr::ForgottenClose` |`bash scripts/check-idris-reject.sh ForgottenClose`
@@ -183,6 +193,10 @@ the status table above.
 |G-3: The FFI bridge preserves grade 𝟙 (a homomorphism; resource-algebra lists homomorphisms as OPEN) |OPEN |`verification/proofs/agda/Reversibility.agda` |-
 |E-1: An attacker cannot recover obliterated content or use a revoked key (adversaryCannotKnow holds only by construction of the model) |OPEN |`src/abi/JanusKey/ABI/Types.idr` |-
 |The six security obligations under "What Needs Proving" (obliteration, key derivation, attestation chain, content store, transaction atomicity, reversible-core) are proved |OPEN |`PROOF-NEEDS.adoc` |-
+|T-4: A rollback that fails part-way can be retried to completion (reproduced 2026-10-26: after one undo error the repaired `jk rollback` stops at the first, already undone, operation and the transaction stays Active) |OPEN |`crates/januskey-cli/src/main.rs` |-
+|T-5: The transaction log survives an I/O failure or a crash during save without disagreeing with memory or being corrupted (by inspection: the log is mutated before `save()?`, and `save` is a plain `fs::write`) |OPEN |`crates/reversible-core/src/transaction.rs` |-
+|T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |-
+|T-7: Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) |ASSUMED |`crates/reversible-core/src/transaction.rs` |-
 |Every operation is reversible (MPR), as a theorem linked to the Rust (needs G-2 made mechanical, and G-3) |OPEN |`verification/proofs/agda/Reversibility.agda` |-
 |===
 
@@ -192,8 +206,9 @@ the status table above.
 ABI/runtime layer (ruling 2026-10-12): kernel statements live in
 `+verification/proofs/agda/+` with siblings consumed by pin
 (`+scripts/fetch-siblings.sh+`); the ABI lives in `+src/abi/+`.
-Obliteration completeness, attestation chain integrity and transaction
-atomicity are still to be stated there. The 225 `+unwrap()+` calls should
+Transaction atomicity is stated there for the model
+(`+verification/proofs/agda/TransactionAtomicity.agda+`, rows T-1 to T-3);
+obliteration completeness and attestation chain integrity are still to be stated. The 225 `+unwrap()+` calls should
 be systematically replaced with proven error handling.
 
 === Priority
diff --git a/READINESS.adoc b/READINESS.adoc
index a344e22..505a2db 100644
--- a/READINESS.adoc
+++ b/READINESS.adoc
@@ -9,7 +9,7 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0
 === CRG Grade: D (Alpha — Unstable)
 
 *Justification:* 119 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the
-Idris2 ABI typechecks and 8 proofs are checked (PROVEN ledger rows: ABI and grade lemmas, not the
+Idris2 ABI typechecks and 11 proofs are checked (PROVEN ledger rows: ABI, grade and transaction-model lemmas, not the
 security obligations); benchmarks exist (5 Criterion groups). But: no
 fuzz testing, no mutation testing, 225 unwrap() calls, E2E mostly skips,
 benchmarks measured fake crypto until this session. RSR compliance
@@ -61,11 +61,11 @@ handling
 
 |15 |Compatibility |MISSING |0 |— |No version migration tests
 
-|16 |Proof regression |✓ |8 proofs checked |`+just test-proofs test-proofs-reject test-agda+` |Idris2 0.8.0 typecheck, Agda kernel, expected rejections
+|16 |Proof regression |✓ |11 proofs checked |`+just test-proofs test-proofs-reject test-agda+` |Idris2 0.8.0 typecheck, Agda kernel, expected rejections
 (run by idris-abi.yml, agda-proofs.yml and dashboard-check)
 |===
 
-*Total declared:* 119 tests + 5 benchmark groups; 8 proofs checked (PROVEN ledger rows) *Total
+*Total declared:* 119 tests + 5 benchmark groups; 11 proofs checked (PROVEN ledger rows) *Total
 missing:* Fuzz, mutation, chaos, compatibility
 
 === Aspect Matrix
diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc
index 5733453..469db4b 100644
--- a/TOPOLOGY.adoc
+++ b/TOPOLOGY.adoc
@@ -77,7 +77,7 @@ SECURITY (honest)
 INTERFACES & RESEARCH
   CLI Interface (jk)                ████████░░  ~85%   Full command set; no user testing yet
   MPR Methodology                   ████░░░░░░  ~40%   Design documented; FORMAL PROOFS PENDING
-                                                        (Idris2 ABI typechecks; 8 proofs checked: ABI and grade
+                                                        (Idris2 ABI typechecks; 11 proofs checked: ABI, grade and transaction-model
                                                         lemmas, not the security obligations; MPR not linked to the Rust)
   Testing (READINESS matrix)        ██████░░░░  ~60%   119 tests + 5 benches; missing fuzz, mutation,
                                                         chaos, compatibility (Grade D)
diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh
index 73e9d92..98b9f0d 100755
--- a/scripts/check-agda.sh
+++ b/scripts/check-agda.sh
@@ -11,7 +11,9 @@ prover="${AGDA:-agda}"
 bash scripts/fetch-siblings.sh
 flags=(--safe --without-K --no-libraries --ignore-interfaces --double-check
        -i verification/proofs/agda -i _build/dependencies/resource-algebra/src)
-"$prover" "${flags[@]}" verification/proofs/agda/Reversibility.agda
+for module in Reversibility TransactionAtomicity; do
+  "$prover" "${flags[@]}" "verification/proofs/agda/$module.agda"
+done
 mkdir -p _build/check-logs
 shopt -s nullglob
 rejects=(tests/reject-agda/*.agda)
diff --git a/tests/reject-agda/CommitWhenIdle.agda b/tests/reject-agda/CommitWhenIdle.agda
new file mode 100644
index 0000000..c38ad1f
--- /dev/null
+++ b/tests/reject-agda/CommitWhenIdle.agda
@@ -0,0 +1,19 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+-- Expected rejection: with no active transaction, commit is an error
+-- (NoActiveTransaction in the Rust), not a state change. The claim below
+-- is false and the checker must refuse it; this pins the "refused in the
+-- wrong state" half of the lifecycle model.
+-- expect: nothing != just
+module CommitWhenIdle where
+
+open import Agda.Builtin.List using (List; []; _∷_)
+open import Agda.Builtin.Maybe using (Maybe; nothing; just)
+open import ResourceAlgebra.Prelude
+open import TransactionAtomicity
+
+open Lifecycle
+
+commit-when-idle : commit (log [] nothing) ≡ just (log [] nothing)
+commit-when-idle = refl
diff --git a/tests/reject-agda/ForwardRollback.agda b/tests/reject-agda/ForwardRollback.agda
new file mode 100644
index 0000000..52911db
--- /dev/null
+++ b/tests/reject-agda/ForwardRollback.agda
@@ -0,0 +1,42 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+-- Expected rejection: rollback must undo in reverse execution order. Two
+-- real, individually invertible operations (double, then add one) are
+-- executed from 1 (1 -> 2 -> 3); undoing them in EXECUTION order instead
+-- ends at 0, not 1, so the checker must refuse the claim that it restores 1.
+-- This pins that `rollback-restores` is not vacuous about order.
+-- expect: 0 != 1
+module ForwardRollback where
+
+open import Agda.Builtin.List using (List; []; _∷_)
+open import Agda.Builtin.Maybe using (Maybe; nothing; just)
+open import ResourceAlgebra.Prelude
+open import TransactionAtomicity
+
+open Rollback Nat
+
+half : Nat → Nat
+half zero          = zero
+half (suc zero)    = zero
+half (suc (suc n)) = suc (half n)
+
+half-double : ∀ x → half (x + x) ≡ x
+half-double zero    = refl
+half-double (suc y) rewrite +-suc y y = cong suc (half-double y)
+
+pred : Nat → Nat
+pred zero    = zero
+pred (suc n) = n
+
+doubleOp : Op
+doubleOp = op (λ x → just (x + x)) half
+              (λ {x} e → trans (cong half (sym (just-inj e))) (half-double x))
+
+incOp : Op
+incOp = op (λ x → just (suc x)) pred
+           (λ {x} e → cong pred (sym (just-inj e)))
+
+-- The correct order is a theorem (rollback-restores); the forward order is not.
+forward-restores : rollbackForward (doubleOp ∷ incOp ∷ []) 3 ≡ 1
+forward-restores = refl
diff --git a/verification/proofs/agda/TransactionAtomicity.agda b/verification/proofs/agda/TransactionAtomicity.agda
new file mode 100644
index 0000000..38c9b06
--- /dev/null
+++ b/verification/proofs/agda/TransactionAtomicity.agda
@@ -0,0 +1,364 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- Transaction atomicity, in two parts that match the two places the Rust
+-- keeps it.
+--
+--   Part A (Rollback). `jk rollback` (crates/januskey-cli/src/main.rs,
+--   cmd_rollback) undoes the recorded operations in reverse order
+--   (Theorem 3.4, Sequential Reversibility). Theorem `rollback-restores`:
+--   if every recorded operation executed successfully, and each one's undo
+--   restores the state its execute started from, then undoing the whole
+--   list in reverse order restores the state the transaction began in.
+--   `rollback-restores` is the sequential generalisation of the one-step
+--   premise TESTED as execute_then_undo_is_identity (cf. G-1).
+--
+--   Part B (Lifecycle). `TransactionManager`
+--   (crates/reversible-core/src/transaction.rs) is a log of transactions
+--   plus a pointer to the active one. Invariant `Good`: the pointer is set
+--   exactly when one transaction is Active; every other transaction is
+--   Committed or RolledBack; and the Active one is the first with its id.
+--   It is preserved by begin / add_operation / commit / mark_rolled_back,
+--   and those operations rewrite only the Active transaction, so a
+--   completed transaction is never modified.
+--
+-- What is NOT claimed (the model is hand-transcribed from the Rust, like
+-- G-2, and these are deliberate limits):
+--   * No I/O. The Rust mutates the in-memory log and then calls save()?;
+--     a save failure after the mutation leaves memory and disk disagreeing.
+--     fs::write is not an atomic replace, so a crash mid-write can corrupt
+--     the log. Neither is modelled.
+--   * A failed execute is assumed to leave the state unchanged. Part A only
+--     speaks about operations that executed; nothing here proves the Rust
+--     executor is a no-op on failure.
+--   * Rollback is assumed to succeed on every step. cmd_rollback stops at
+--     the first undo error (`?`) and leaves the transaction Active with the
+--     later operations already undone; a retry then meets "already undone".
+--     Part A does not cover that case; see the OPEN ledger rows.
+--   * Transaction ids are assumed fresh (Fresh below). The Rust draws a
+--     UUID v4; a collision would break Good, and nothing here rules it out.
+--   * Obliterating operations have no undo, so they have no `Op` here
+--     (cf. C-3); a transaction containing one is outside this theorem.
+--   * Concurrency: one process, no locking, is the whole model.
+
+module TransactionAtomicity where
+
+open import Agda.Builtin.List using (List; []; _∷_)
+open import Agda.Builtin.Maybe using (Maybe; nothing; just)
+open import ResourceAlgebra.Prelude
+
+----------------------------------------------------------------------
+-- Small prelude (the kernel pins builtins only; nothing is imported)
+----------------------------------------------------------------------
+
+infixr 5 _++_
+_++_ : {A : Set} → List A → List A → List A
+[]       ++ ys = ys
+(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
+
+data _⊎_ (A B : Set) : Set where
+  inl : A → A ⊎ B
+  inr : B → A ⊎ B
+
+⊥-elim : {A : Set} → ⊥ → A
+⊥-elim ()
+
+just-inj : {A : Set} {a b : A} → just a ≡ just b → a ≡ b
+just-inj refl = refl
+
+nothing≢just : {A : Set} {a : A} → nothing ≡ just a → ⊥
+nothing≢just ()
+
+suc-inj : ∀ {m n} → suc m ≡ suc n → m ≡ n
+suc-inj refl = refl
+
+_≟_ : (m n : Nat) → (m ≡ n) ⊎ (m ≢ n)
+zero  ≟ zero  = inl refl
+zero  ≟ suc n = inr (λ ())
+suc m ≟ zero  = inr (λ ())
+suc m ≟ suc n with m ≟ n
+... | inl p = inl (cong suc p)
+... | inr q = inr (λ r → q (suc-inj r))
+
+data All {A : Set} (P : A → Set) : List A → Set where
+  []  : All P []
+  _∷_ : ∀ {x xs} → P x → All P xs → All P (x ∷ xs)
+
+----------------------------------------------------------------------
+-- Part A. Rollback undoes the recorded operations in reverse order
+----------------------------------------------------------------------
+
+module Rollback (S : Set) where
+
+  -- A recorded operation: `execute` may fail (nothing); `undo`, applied to
+  -- the state a successful execute produced, restores the state it started
+  -- from. In the Rust: OperationExecutor::execute and ::undo
+  -- (crates/januskey-cli/src/operations.rs). `undoes` is the per-step
+  -- premise, TESTED as execute_then_undo_is_identity; it is not proved here.
+  record Op : Set where
+    constructor op
+    field
+      execute : S → Maybe S
+      undo    : S → S
+      undoes  : ∀ {x y} → execute x ≡ just y → undo y ≡ x
+
+  open Op public
+
+  -- The recorded list `os` (execution order) ran successfully from x to z.
+  data Executed : List Op → S → S → Set where
+    done : ∀ {x} → Executed [] x x
+    next : ∀ {o os x y z} → execute o x ≡ just y → Executed os y z → Executed (o ∷ os) x z
+
+  -- cmd_rollback: undo the last recorded operation first, the first last.
+  rollback : List Op → S → S
+  rollback []       z = z
+  rollback (o ∷ os) z = undo o (rollback os z)
+
+  -- Theorem A-1 (rollback-restores). Undoing a fully executed transaction
+  -- in reverse order returns the state it began in.
+  rollback-restores : ∀ {os x z} → Executed os x z → rollback os z ≡ x
+  rollback-restores done           = refl
+  rollback-restores (next {o} e r) =
+    trans (cong (undo o) (rollback-restores r)) (undoes o e)
+
+  -- The order matters. Undoing in execution order instead is NOT a
+  -- theorem; it is here only so that tests/reject-agda/ForwardRollback.agda
+  -- can pin that the checker refuses the claim for it.
+  rollbackForward : List Op → S → S
+  rollbackForward []       z = z
+  rollbackForward (o ∷ os) z = rollbackForward os (undo o z)
+
+----------------------------------------------------------------------
+-- Part B. The TransactionManager lifecycle
+----------------------------------------------------------------------
+
+module Lifecycle where
+
+  data TState : Set where
+    Active Committed RolledBack : TState
+
+  Active≢Committed : Active ≡ Committed → ⊥
+  Active≢Committed ()
+
+  Active≢RolledBack : Active ≡ RolledBack → ⊥
+  Active≢RolledBack ()
+
+  -- id, state, operation ids in execution order.
+  record Tx : Set where
+    constructor tx
+    field
+      txId    : Nat
+      txState : TState
+      txOps   : List Nat
+
+  open Tx public
+
+  -- The log and the pointer to the active transaction.
+  record Log : Set where
+    constructor log
+    field
+      txs      : List Tx
+      activeId : Maybe Nat
+
+  open Log public
+
+  Settled : Tx → Set
+  Settled t = txState t ≢ Active
+
+  addOpTx : Nat → Tx → Tx
+  addOpTx o t = tx (txId t) (txState t) (txOps t ++ o ∷ [])
+
+  settle : TState → Tx → Tx
+  settle s t = tx (txId t) s (txOps t)
+
+  -- `iter_mut().find(|t| t.id == i)` then rewrite: only the FIRST transaction
+  -- with that id changes. nothing = no such transaction.
+  update : Nat → (Tx → Tx) → List Tx → Maybe (List Tx)
+  update i f []       = nothing
+  update i f (t ∷ ts) with txId t ≟ i
+  ... | inl _ = just (f t ∷ ts)
+  ... | inr _ with update i f ts
+  ...   | nothing = nothing
+  ...   | just us = just (t ∷ us)
+
+  -- TransactionManager::begin(name), with the fresh id as an argument.
+  begin : Nat → Log → Maybe Log
+  begin i (log ts (just _)) = nothing
+  begin i (log ts nothing)  = just (log (ts ++ tx i Active [] ∷ []) (just i))
+
+  -- TransactionManager::add_operation.
+  addOp : Nat → Log → Maybe Log
+  addOp o (log ts nothing)  = nothing
+  addOp o (log ts (just i)) with update i (addOpTx o) ts
+  ... | nothing = nothing
+  ... | just us = just (log us (just i))
+
+  -- TransactionManager::commit (s = Committed) and ::mark_rolled_back
+  -- (s = RolledBack).
+  finish : TState → Log → Maybe Log
+  finish s (log ts nothing)  = nothing
+  finish s (log ts (just i)) with update i (settle s) ts
+  ... | nothing = nothing
+  ... | just us = just (log us nothing)
+
+  commit : Log → Maybe Log
+  commit = finish Committed
+
+  markRolledBack : Log → Maybe Log
+  markRolledBack = finish RolledBack
+
+  ----------------------------------------------------------------------
+  -- The invariant
+  ----------------------------------------------------------------------
+
+  data Good : Log → Set where
+    -- No pointer: nothing is Active.
+    idle : ∀ {ts} → All Settled ts → Good (log ts nothing)
+    -- Pointer to t: t is the first with its id, it is the one Active
+    -- transaction, and everything else is Committed or RolledBack.
+    busy : ∀ {pre t post}
+         → All (λ u → txId u ≢ txId t) pre
+         → All Settled pre
+         → txState t ≡ Active
+         → All Settled post
+         → Good (log (pre ++ t ∷ post) (just (txId t)))
+
+  Fresh : Nat → List Tx → Set
+  Fresh i = All (λ u → txId u ≢ i)
+
+  good-empty : Good (log [] nothing)
+  good-empty = idle []
+
+  ----------------------------------------------------------------------
+  -- Only the Active transaction is rewritten (completed ones are frozen)
+  ----------------------------------------------------------------------
+
+  update-active : ∀ f pre t post
+                → All (λ u → txId u ≢ txId t) pre
+                → update (txId t) f (pre ++ t ∷ post) ≡ just (pre ++ f t ∷ post)
+  update-active f []        t post []       with txId t ≟ txId t
+  ... | inl _ = refl
+  ... | inr n = ⊥-elim (n refl)
+  update-active f (u ∷ pre) t post (n ∷ ns) with txId u ≟ txId t
+  ... | inl e = ⊥-elim (n e)
+  ... | inr _ with update (txId t) f (pre ++ t ∷ post) | update-active f pre t post ns
+  ...   | .(just (pre ++ f t ∷ post)) | refl = refl
+
+  ----------------------------------------------------------------------
+  -- Settled transactions append and concatenate without becoming Active
+  ----------------------------------------------------------------------
+
+  all-++ : ∀ {A : Set} {P : A → Set} {xs ys}
+         → All P xs → All P ys → All P (xs ++ ys)
+  all-++ []       qs = qs
+  all-++ (p ∷ ps) qs = p ∷ all-++ ps qs
+
+  ----------------------------------------------------------------------
+  -- Theorem B-1: begin preserves Good (given a fresh id), and is refused
+  -- while a transaction is active.
+  ----------------------------------------------------------------------
+
+  begin-refused-while-active : ∀ i ts j → begin i (log ts (just j)) ≡ nothing
+  begin-refused-while-active i ts j = refl
+
+  begin-good : ∀ {i L L'} → Good L → Fresh i (txs L) → begin i L ≡ just L' → Good L'
+  begin-good (busy _ _ _ _) _ ()
+  begin-good {i} (idle {ts} ss) fr refl =
+    busy {pre = ts} {t = tx i Active []} {post = []} fr ss refl []
+
+  ----------------------------------------------------------------------
+  -- Theorem B-2: add_operation preserves Good, and is refused when idle.
+  ----------------------------------------------------------------------
+
+  addOp-refused-when-idle : ∀ o ts → addOp o (log ts nothing) ≡ nothing
+  addOp-refused-when-idle o ts = refl
+
+  addOp-good : ∀ {o L L'} → Good L → addOp o L ≡ just L' → Good L'
+  addOp-good (idle _) ()
+  addOp-good {o} (busy {pre} {t} {post} np sp act sq) eq
+    with update (txId t) (addOpTx o) (pre ++ t ∷ post) | update-active (addOpTx o) pre t post np
+  ... | .(just (pre ++ addOpTx o t ∷ post)) | refl with eq
+  ... | refl = busy {pre = pre} {t = addOpTx o t} {post = post} np sp act sq
+
+  ----------------------------------------------------------------------
+  -- Theorem B-3: commit and mark_rolled_back preserve Good, land idle,
+  -- and are refused when idle.
+  ----------------------------------------------------------------------
+
+  finish-refused-when-idle : ∀ s ts → finish s (log ts nothing) ≡ nothing
+  finish-refused-when-idle s ts = refl
+
+  finish-good : ∀ {s L L'} → s ≢ Active → Good L → finish s L ≡ just L' → Good L'
+  finish-good _ (idle _) ()
+  finish-good {s} sn (busy {pre} {t} {post} np sp act sq) eq
+    with update (txId t) (settle s) (pre ++ t ∷ post) | update-active (settle s) pre t post np
+  ... | .(just (pre ++ settle s t ∷ post)) | refl with eq
+  ... | refl = idle (all-++ sp ((λ e → sn e) ∷ sq))
+
+  commit-good : ∀ {L L'} → Good L → commit L ≡ just L' → Good L'
+  commit-good = finish-good (λ e → Active≢Committed (sym e))
+
+  markRolledBack-good : ∀ {L L'} → Good L → markRolledBack L ≡ just L' → Good L'
+  markRolledBack-good = finish-good (λ e → Active≢RolledBack (sym e))
+
+  ----------------------------------------------------------------------
+  -- Theorem B-4: at most one transaction is Active, and exactly when the
+  -- pointer is set.
+  ----------------------------------------------------------------------
+
+  countActive : List Tx → Nat
+  countActive []       = 0
+  countActive (t ∷ ts) with txState t
+  ... | Active     = suc (countActive ts)
+  ... | Committed  = countActive ts
+  ... | RolledBack = countActive ts
+
+  expected : Maybe Nat → Nat
+  expected nothing  = 0
+  expected (just _) = 1
+
+  settled-count : ∀ {ts} → All Settled ts → countActive ts ≡ 0
+  settled-count []                  = refl
+  settled-count {t ∷ ts} (s ∷ ss) with txState t | s
+  ... | Active     | s' = ⊥-elim (s' refl)
+  ... | Committed  | _  = settled-count ss
+  ... | RolledBack | _  = settled-count ss
+
+  count-++ : ∀ xs ys → countActive (xs ++ ys) ≡ countActive xs + countActive ys
+  count-++ []       ys = refl
+  count-++ (x ∷ xs) ys with txState x
+  ... | Active     = cong suc (count-++ xs ys)
+  ... | Committed  = count-++ xs ys
+  ... | RolledBack = count-++ xs ys
+
+  at-most-one-active : ∀ {L} → Good L → countActive (txs L) ≡ expected (activeId L)
+  at-most-one-active (idle ss) = settled-count ss
+  at-most-one-active (busy {pre} {t} {post} _ sp act sq)
+    rewrite count-++ pre (t ∷ post) | settled-count sp | act | settled-count sq = refl
+
+  ----------------------------------------------------------------------
+  -- Theorem B-5 (lifecycle-preserves-good): the four transitions together.
+  -- One name for the claims ledger: every transition that succeeds keeps
+  -- Good, begin additionally needs a fresh id, and each transition rewrites
+  -- only the Active transaction, leaving every settled one untouched.
+  ----------------------------------------------------------------------
+
+  record Preserves : Set where
+    field
+      onBegin      : ∀ {i L L'} → Good L → Fresh i (txs L) → begin i L ≡ just L' → Good L'
+      onAddOp      : ∀ {o L L'} → Good L → addOp o L ≡ just L' → Good L'
+      onCommit     : ∀ {L L'} → Good L → commit L ≡ just L' → Good L'
+      onRollback   : ∀ {L L'} → Good L → markRolledBack L ≡ just L' → Good L'
+      onlyActive   : ∀ f pre t post
+                   → All (λ u → txId u ≢ txId t) pre
+                   → update (txId t) f (pre ++ t ∷ post) ≡ just (pre ++ f t ∷ post)
+
+  lifecycle-preserves-good : Preserves
+  lifecycle-preserves-good = record
+    { onBegin    = begin-good
+    ; onAddOp    = addOp-good
+    ; onCommit   = commit-good
+    ; onRollback = markRolledBack-good
+    ; onlyActive = update-active
+    }