diff --git a/dev/bend2/flightsql_transactions/LAWS.bend b/dev/bend2/flightsql_transactions/LAWS.bend
new file mode 100644
index 0000000000..6cb23f6845
--- /dev/null
+++ b/dev/bend2/flightsql_transactions/LAWS.bend
@@ -0,0 +1,340 @@
+# Licensed to the Apache Software Foundation (ASF) under one
+# or more contributor license agreements.  See the NOTICE file
+# distributed with this work for additional information
+# regarding copyright ownership.  The ASF licenses this file
+# to you under the Apache License, Version 2.0 (the
+# "License"); you may not use this file except in compliance
+# with the License.  You may obtain a copy of the License at
+#
+#   http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing,
+# software distributed under the License is distributed on an
+# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
+# KIND, either express or implied.  See the License for the
+# specific language governing permissions and limitations
+# under the License.
+
+# The laws of the transaction and savepoint model. The human states
+# them; PROOF.bend must prove them. Each law quotes the sentence of
+# FlightSql.proto it comes from, or is a sanity check that keeps the
+# others from being satisfied vacuously. Laws are stated over
+# arbitrary server states; the ones that need the id invariant say so
+# with `for w: Inv(...)`, and the two laws at the end show that every
+# reachable state satisfies the invariant.
+
+import Base
+import ./main.bend as TX
+
+# the truth of a Bool as a type: Unit when True, Empty when False
+def T(b: Bool) -> Data:
+  match b:
+    case True{}:
+      Unit
+    case False{}:
+      Empty
+
+# Invariant
+# ---------
+
+# every id in xs is below n and the list is strictly descending, so ids
+# are never reissued and never repeated
+def desc(xs: List<&2, Nat>, +n: Nat) -> Bool:
+  match xs:
+    case Nil{}:
+      True{}
+    case Con{+x, t}:
+      Nat.is_lt(x, n) && desc(t, x)
+
+# the same for savepoint ids
+def desc_sp(sps: List<&2, TX.Sp>, +n: Nat) -> Bool:
+  match sps:
+    case Nil{}:
+      True{}
+    case Con{TX.Sp{+id, tx}, t}:
+      Nat.is_lt(id, n) && desc_sp(t, id)
+
+def Inv(txs: List<&2, Nat>, sps: List<&2, TX.Sp>, +next: Nat) -> Type:
+  T(desc(txs, next)) & T(desc_sp(sps, next))
+
+def Inv_s(s: TX.Server) -> Type:
+  TX.Server{txs, sps, next} = s
+  Inv(txs, sps, next)
+
+# whether request a names t as its transaction_id
+def refers_tx(a: TX.Act, +t: Nat) -> Bool:
+  match a:
+    case TX.ABeginTx{}:
+      False{}
+    case TX.ABeginSp{tx}:
+      Nat.is_eq(t, tx)
+    case TX.AEndTx{tx, how}:
+      Nat.is_eq(t, tx)
+    case TX.AEndSp{sp, how}:
+      False{}
+    case TX.AStmt{TX.SAuto{}}:
+      False{}
+    case TX.AStmt{TX.STx{tx}}:
+      Nat.is_eq(t, tx)
+
+# Ending a transaction
+# --------------------
+
+# LAW: "If the action completes successfully, the transaction handle is
+# invalidated" (ActionEndTransactionRequest). After EndTransaction on
+# t, commit or rollback, every request that names t as its
+# transaction_id (BeginSavepoint, EndTransaction, a statement) is an
+# error. Holds from any state: if t was not live the EndTransaction
+# itself failed and t is still not live.
+law ended_tx_rejected:
+  for  a    : TX.Act
+  for +t    : Nat
+  for  how  : TX.EndTx
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  u    : T(refers_tx(a, t))
+  {TX.resp(TX.step_s(a, TX.state(TX.step(TX.AEndTx{t, how}, txs, sps, next)))) == TX.RErr{} : TX.Resp}
+
+# LAW: "...as are all associated savepoints" (ActionEndTransactionRequest),
+# and "If the associated transaction is committed, rolled back, or
+# times out, then the savepoint is also invalidated"
+# (ActionBeginSavepointResult). After EndTransaction on a live t, any
+# EndSavepoint on a savepoint s that belonged to t is an error. Needs
+# the invariant: without unique ids another transaction could hold a
+# savepoint with the same id.
+law ended_tx_kills_savepoints:
+  for +t    : Nat
+  for +s    : Nat
+  for  how  : TX.EndTx
+  for  how2 : TX.EndSp
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  w    : Inv(txs, sps, next)
+  for  live : T(TX.has(t, txs))
+  for  own  : {Some{t} == TX.owner(s, sps) : Maybe<&2, Nat>}
+  {TX.resp(TX.step_s(TX.AEndSp{s, how2}, TX.state(TX.step(TX.AEndTx{t, how}, txs, sps, next)))) == TX.RErr{} : TX.Resp}
+
+# LAW: the lifecycle does not distinguish commit from rollback: "Commit
+# (COMMIT) or rollback (ROLLBACK) the transaction" lead to the same
+# server state (what happens to the data is outside this model).
+law commit_rollback_same_state:
+  for +t    : Nat
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  {TX.state(TX.step(TX.AEndTx{t, TX.TCommit{}}, txs, sps, next)) == TX.state(TX.step(TX.AEndTx{t, TX.TRollback{}}, txs, sps, next)) : TX.Server}
+
+# Beginning a savepoint
+# ---------------------
+
+# LAW: "Creates a savepoint within a transaction" / "The transaction to
+# which a savepoint belongs" (ActionBeginSavepointRequest). A
+# BeginSavepoint naming a transaction that is not live is an error.
+law savepoint_needs_live_tx:
+  for +t    : Nat
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  dead : {False{} == TX.has(t, txs) : Bool}
+  {TX.resp(TX.step(TX.ABeginSp{t}, txs, sps, next)) == TX.RErr{} : TX.Resp}
+
+# LAW (anti-vacuity): BeginSavepoint on a live transaction succeeds and
+# answers the counter as the savepoint id.
+law savepoint_in_live_tx:
+  for +t    : Nat
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  live : T(TX.has(t, txs))
+  {TX.resp(TX.step(TX.ABeginSp{t}, txs, sps, next)) == TX.RId{next} : TX.Resp}
+
+# LAW: the savepoint id a BeginSavepoint returns is bound to the
+# transaction it was created in: the server records it as owned by t.
+law savepoint_bound_to_tx:
+  for +t    : Nat
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  live : T(TX.has(t, txs))
+  {Some{t} == TX.owner(next, TX.sps_of(TX.state(TX.step(TX.ABeginSp{t}, txs, sps, next)))) : Maybe<&2, Nat>}
+
+# Ending a savepoint
+# ------------------
+
+# LAW: EndSavepoint (release or rollback, on a live savepoint or not)
+# never changes which transactions are live: "Roll back to a savepoint"
+# keeps the transaction open, unlike EndTransaction.
+law end_savepoint_keeps_txs:
+  for +s    : Nat
+  for  how  : TX.EndSp
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  {txs == TX.txs_of(TX.state(TX.step(TX.AEndSp{s, how}, txs, sps, next))) : List<&2, Nat>}
+
+# LAW: "Releasing a savepoint invalidates that savepoint"
+# (ActionEndSavepointRequest). After a release of s, any EndSavepoint
+# on s is an error. Holds from any state, as for ended_tx_rejected.
+law release_kills_savepoint:
+  for +s    : Nat
+  for  how  : TX.EndSp
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  {TX.resp(TX.step_s(TX.AEndSp{s, how}, TX.state(TX.step(TX.AEndSp{s, TX.SRelease{}}, txs, sps, next)))) == TX.RErr{} : TX.Resp}
+
+# LAW (chosen reading): the proto says release "invalidates that
+# savepoint" and nothing about the others, so this model keeps every
+# other live savepoint, including the later ones of the same
+# transaction. (JDBC's releaseSavepoint and PostgreSQL's RELEASE
+# SAVEPOINT also drop the later ones; a server following them would
+# violate this law and satisfy the previous one.)
+law release_keeps_other_savepoints:
+  for +s    : Nat
+  for +s2   : Nat
+  for +t    : Nat
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  ne   : {False{} == Nat.is_eq(s2, s) : Bool}
+  for  own  : {Some{t} == TX.owner(s2, sps) : Maybe<&2, Nat>}
+  {Some{t} == TX.owner(s2, TX.sps_of(TX.state(TX.step(TX.AEndSp{s, TX.SRelease{}}, txs, sps, next)))) : Maybe<&2, Nat>}
+
+# LAW: "Rolling back to a savepoint does not invalidate the savepoint"
+# (ActionEndSavepointRequest). After a rollback to live s, another
+# EndSavepoint on s succeeds.
+law rollback_keeps_savepoint:
+  for +s    : Nat
+  for +t    : Nat
+  for  how  : TX.EndSp
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for +own  : {Some{t} == TX.owner(s, sps) : Maybe<&2, Nat>}
+  {TX.resp(TX.step_s(TX.AEndSp{s, how}, TX.state(TX.step(TX.AEndSp{s, TX.SRollback{}}, txs, sps, next)))) == TX.RDone{} : TX.Resp}
+
+# LAW: "...but invalidates all savepoints created after the current
+# savepoint" (ActionEndSavepointRequest). After a rollback to live s
+# of t, any EndSavepoint on a savepoint s2 of t created after s (a
+# larger id) is an error. Needs the invariant for unique ids.
+law rollback_kills_later_savepoints:
+  for +s    : Nat
+  for +s2   : Nat
+  for +t    : Nat
+  for  how  : TX.EndSp
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  w    : Inv(txs, sps, next)
+  for  own  : {Some{t} == TX.owner(s, sps) : Maybe<&2, Nat>}
+  for  own2 : {Some{t} == TX.owner(s2, sps) : Maybe<&2, Nat>}
+  for  aft  : T(Nat.is_lt(s, s2))
+  {TX.resp(TX.step_s(TX.AEndSp{s2, how}, TX.state(TX.step(TX.AEndSp{s, TX.SRollback{}}, txs, sps, next)))) == TX.RErr{} : TX.Resp}
+
+# LAW: a rollback to s keeps the savepoints of the same transaction
+# created before s (a smaller id).
+law rollback_keeps_earlier_savepoints:
+  for +s    : Nat
+  for +s2   : Nat
+  for +t    : Nat
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  own  : {Some{t} == TX.owner(s, sps) : Maybe<&2, Nat>}
+  for  own2 : {Some{t} == TX.owner(s2, sps) : Maybe<&2, Nat>}
+  for  bef  : T(Nat.is_lt(s2, s))
+  {Some{t} == TX.owner(s2, TX.sps_of(TX.state(TX.step(TX.AEndSp{s, TX.SRollback{}}, txs, sps, next)))) : Maybe<&2, Nat>}
+
+# Statements
+# ----------
+
+# LAW: "Include the query as part of this transaction"
+# (CommandStatementQuery.transaction_id). A statement whose
+# transaction_id is not a live transaction is an error.
+law statement_needs_live_tx:
+  for +t    : Nat
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  dead : {False{} == TX.has(t, txs) : Bool}
+  {TX.resp(TX.step(TX.AStmt{TX.STx{t}}, txs, sps, next)) == TX.RErr{} : TX.Resp}
+
+# LAW: "(if unset, the query is auto-committed)"
+# (CommandStatementQuery.transaction_id). A statement without a
+# transaction_id runs from any state.
+law statement_autocommit:
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  {TX.resp(TX.step(TX.AStmt{TX.SAuto{}}, txs, sps, next)) == TX.RDone{} : TX.Resp}
+
+# LAW (anti-vacuity): a statement inside a live transaction runs.
+law statement_in_live_tx:
+  for +t    : Nat
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  live : T(TX.has(t, txs))
+  {TX.resp(TX.step(TX.AStmt{TX.STx{t}}, txs, sps, next)) == TX.RDone{} : TX.Resp}
+
+# LAW (anti-vacuity): the id a BeginTransaction returns is usable: a
+# statement in it runs, and a savepoint can be created in it.
+law fresh_tx_runs_statement:
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  {TX.resp(TX.step_s(TX.AStmt{TX.STx{next}}, TX.state(TX.step(TX.ABeginTx{}, txs, sps, next)))) == TX.RDone{} : TX.Resp}
+
+law fresh_tx_takes_savepoint:
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  {TX.resp(TX.step_s(TX.ABeginSp{next}, TX.state(TX.step(TX.ABeginTx{}, txs, sps, next)))) == TX.RId{1n+next} : TX.Resp}
+
+# Invariant
+# ---------
+
+# LAW: the initial state satisfies the invariant
+law inv_start:
+  Inv_s(TX.start())
+
+# LAW: every request preserves the invariant, so every reachable state
+# satisfies it and the laws stated `for w: Inv(...)` cover every trace
+law inv_kept:
+  for  a    : TX.Act
+  for +txs  : List<&2, Nat>
+  for +sps  : List<&2, TX.Sp>
+  for +next : Nat
+  for  w    : Inv(txs, sps, next)
+  Inv_s(TX.state(TX.step(a, txs, sps, next)))
+
+# Not modelled
+# ------------
+
+# NOT EXPRESSIBLE: "The transaction can be manipulated with the
+# EndTransaction action, or automatically via server timeout. If the
+# transaction times out, then it is automatically rolled back"
+# (ActionBeginTransactionResult). The model has no clock: a Bend law
+# ranges over pure terms, and a timeout is an event the server raises
+# on its own between requests, not a request. It could be added as an
+# explicit ATimeout{tx} request whose effect equals AEndTx{tx,
+# TRollback{}}, but that would only restate commit_rollback_same_state,
+# not the timing.
+# law timeout_rolls_back:
+#   for +t : Nat
+#   ...
+
+# NOT EXPRESSIBLE: transaction_id and savepoint_id are `bytes` chosen
+# by the server ("Opaque handle for the transaction on the server").
+# The model issues Nats from one counter, so laws about the handle's
+# encoding (length, opacity, that the client does not interpret it)
+# are not stated; Bend has no byte or 64-bit integer type to state
+# them over. inv_kept covers the one property that matters for the
+# lifecycle: an id is never reissued.
+
+# NOT EXPRESSIBLE: "Only supported if FLIGHT_SQL_TRANSACTION is
+# FLIGHT_SQL_TRANSACTION_SUPPORT_SAVEPOINT" (ActionBeginSavepointRequest).
+# Feature negotiation through GetSqlInfo is a separate RPC with its own
+# state; this model assumes a server that supports savepoints.
diff --git a/dev/bend2/flightsql_transactions/PROOF.bend b/dev/bend2/flightsql_transactions/PROOF.bend
new file mode 100644
index 0000000000..136d097342
--- /dev/null
+++ b/dev/bend2/flightsql_transactions/PROOF.bend
@@ -0,0 +1,649 @@
+# Licensed to the Apache Software Foundation (ASF) under one
+# or more contributor license agreements.  See the NOTICE file
+# distributed with this work for additional information
+# regarding copyright ownership.  The ASF licenses this file
+# to you under the Apache License, Version 2.0 (the
+# "License"); you may not use this file except in compliance
+# with the License.  You may obtain a copy of the License at
+#
+#   http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing,
+# software distributed under the License is distributed on an
+# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
+# KIND, either express or implied.  See the License for the
+# specific language governing permissions and limitations
+# under the License.
+
+# The proofs. Imports the model (as TX) and the claims (as Laws) and
+# fills every law they state; `bend PROOF.bend` is the whole check.
+#
+# Conventions, as in dev/bend2/prepared_statement/PROOF.bend: a lemma
+# whose step case matches on a computed Boolean has a `.fin` half that
+# takes the verdict c as a parameter together with an equation about
+# it (the "inspect" idiom); the induction hypothesis arrives as `rec`.
+
+import Base
+import ./main.bend as TX
+import ./LAWS.bend as Laws
+
+# Proof kit
+# ---------
+
+# T(True{}) from an equation
+def true_T(b: Bool, e: {True{} == b : Bool}) -> Laws.T(b):
+  %e : Laws.T(_)
+  Unit{}
+
+# an equation from T(b)
+def T_true(b: Bool, w: Laws.T(b)) -> {True{} == b : Bool}:
+  match b:
+    case True{}:
+      {==}
+    case False{}:
+      Empty.absurd({True{} == False{} : Bool}, w)
+
+def disc(b: Bool) -> Type:
+  match b:
+    case True{}:
+      Unit
+    case False{}:
+      Empty
+
+# True and False clash
+def true_ne_false(e: {True{} == False{} : Bool}) -> Empty:
+  %e : disc(_)
+  Unit{}
+
+# T(c && b) splits into T(c) and T(b); c is a parameter so it can be matched
+def split.fin(c: Bool, -b: Bool, w: Laws.T(c && b), -P: Type, k: Laws.T(c) -> Laws.T(b) -> P) -> P:
+  match c:
+    case True{}:
+      k(Unit{}, w)
+    case False{}:
+      Empty.absurd(P, w)
+
+# T(c) and T(b) join into T(c && b)
+def join.fin(c: Bool, -b: Bool, wc: Laws.T(c), wb: Laws.T(b)) -> Laws.T(c && b):
+  match c:
+    case True{}:
+      wb
+    case False{}:
+      Empty.absurd(Laws.T(False{} && b), wc)
+
+# Some{a} == Some{b} gives a == b
+def some_inj(a: Nat, b: Nat, e: {Some{a} == Some{b} : Maybe<&2, Nat>}) -> {a == b : Nat}:
+  Equal.cong(Maybe<&2, Nat>, Nat, m => Maybe.default(&2, Nat, m, 0n), Some{a}, Some{b}, e)
+
+# Lemmas on Nat
+# -------------
+
+# a nat equals itself
+def eq_refl(n: Nat) -> {True{} == Nat.is_eq(n, n) : Bool}:
+  match n:
+    case 0n:
+      {==}
+    case 1n+p:
+      eq_refl(p)
+
+# a true Nat.is_eq is an equality
+def eq_sound(x: Nat, h: Nat, e: {True{} == Nat.is_eq(x, h) : Bool}) -> {x == h : Nat}:
+  match x h:
+    case 0n 0n:
+      {==}
+    case 0n 1n+q:
+      Empty.absurd({0n == 1n+q : Nat}, true_ne_false(e))
+    case 1n+p 0n:
+      Empty.absurd({1n+p == 0n : Nat}, true_ne_false(e))
+    case 1n+p 1n+q:
+      %eq_sound(p, q, e) : {1n+p == 1n+_ : Nat}
+      {==}
+
+# n < n + 1
+def lt_succ(n: Nat) -> Laws.T(Nat.is_lt(n, 1n+n)):
+  match n:
+    case 0n:
+      Unit{}
+    case 1n+p:
+      lt_succ(p)
+
+# x < n implies x < n + 1
+def lt_mono(x: Nat, n: Nat, w: Laws.T(Nat.is_lt(x, n))) -> Laws.T(Nat.is_lt(x, 1n+n)):
+  match x n:
+    case 0n 0n:
+      Empty.absurd(Laws.T(Nat.is_lt(0n, 1n)), w)
+    case 0n 1n+q:
+      Unit{}
+    case 1n+p 0n:
+      Empty.absurd(Laws.T(Nat.is_lt(1n+p, 1n)), w)
+    case 1n+p 1n+q:
+      lt_mono(p, q, w)
+
+# a < b and b < c give a < c
+def lt_trans(a: Nat, b: Nat, c: Nat, ab: Laws.T(Nat.is_lt(a, b)), bc: Laws.T(Nat.is_lt(b, c))) -> Laws.T(Nat.is_lt(a, c)):
+  match a b c:
+    case 0n 0n c0:
+      Empty.absurd(Laws.T(Nat.is_lt(0n, c0)), ab)
+    case 0n 1n+q 0n:
+      Empty.absurd(Laws.T(Nat.is_lt(0n, 0n)), bc)
+    case 0n 1n+q 1n+r:
+      Unit{}
+    case 1n+p 0n c0:
+      Empty.absurd(Laws.T(Nat.is_lt(1n+p, c0)), ab)
+    case 1n+p 1n+q 0n:
+      Empty.absurd(Laws.T(Nat.is_lt(1n+p, 0n)), bc)
+    case 1n+p 1n+q 1n+r:
+      lt_trans(p, q, r, ab, bc)
+
+# n < n never holds
+def lt_irrefl(n: Nat) -> {False{} == Nat.is_lt(n, n) : Bool}:
+  match n:
+    case 0n:
+      {==}
+    case 1n+p:
+      lt_irrefl(p)
+
+# a < b rules out b < a
+def lt_asym(a: Nat, b: Nat, w: Laws.T(Nat.is_lt(a, b))) -> {False{} == Nat.is_lt(b, a) : Bool}:
+  match a b:
+    case 0n 0n:
+      Empty.absurd({False{} == Nat.is_lt(0n, 0n) : Bool}, w)
+    case 0n 1n+q:
+      {==}
+    case 1n+p 0n:
+      Empty.absurd({False{} == Nat.is_lt(0n, 1n+p) : Bool}, w)
+    case 1n+p 1n+q:
+      lt_asym(p, q, w)
+
+# a < b rules out a == b (in either argument order of is_eq)
+def lt_ne(a: Nat, b: Nat, w: Laws.T(Nat.is_lt(a, b))) -> {False{} == Nat.is_eq(a, b) : Bool}:
+  match a b:
+    case 0n 0n:
+      Empty.absurd({False{} == Nat.is_eq(0n, 0n) : Bool}, w)
+    case 0n 1n+q:
+      {==}
+    case 1n+p 0n:
+      Empty.absurd({False{} == Nat.is_eq(1n+p, 0n) : Bool}, w)
+    case 1n+p 1n+q:
+      lt_ne(p, q, w)
+
+def lt_ne_r(a: Nat, b: Nat, w: Laws.T(Nat.is_lt(a, b))) -> {False{} == Nat.is_eq(b, a) : Bool}:
+  match a b:
+    case 0n 0n:
+      Empty.absurd({False{} == Nat.is_eq(0n, 0n) : Bool}, w)
+    case 0n 1n+q:
+      {==}
+    case 1n+p 0n:
+      Empty.absurd({False{} == Nat.is_eq(0n, 1n+p) : Bool}, w)
+    case 1n+p 1n+q:
+      lt_ne_r(p, q, w)
+
+# Lemmas on has and remove
+# ------------------------
+
+# removing h leaves no h: the step case, over the verdict c of
+# Nat.is_eq(x, h)
+def has_remove.fin(+h: Nat, +x: Nat, -t: List<&2, Nat>,
+  rec: {False{} == TX.has(h, TX.remove(h, t)) : Bool},
+  c: Bool, e: {c == Nat.is_eq(x, h) : Bool})
+  -> {False{} == TX.has(h, TX.put(x, TX.remove(h, t), c)) : Bool}:
+  match c:
+    case True{}:
+      rec
+    case False{}:
+      %e : {False{} == (_ || TX.has(h, TX.remove(h, t))) : Bool}
+      rec
+
+def has_remove(+h: Nat, xs: List<&2, Nat>) -> {False{} == TX.has(h, TX.remove(h, xs)) : Bool}:
+  match xs:
+    case Nil{}:
+      {==}
+    case Con{+x, t}:
+      has_remove.fin(h, x, t, has_remove(h, t), Nat.is_eq(x, h), {==})
+
+# Statements and savepoint creation, from any state
+# -------------------------------------------------
+
+def Laws.statement_autocommit(txs, sps, next):
+  {==}
+
+def Laws.statement_needs_live_tx(t, txs, sps, next, dead):
+  %dead : {TX.resp(TX.stmt(txs, sps, next, _)) == TX.RErr{} : TX.Resp}
+  {==}
+
+def Laws.statement_in_live_tx(t, txs, sps, next, live):
+  %T_true(TX.has(t, txs), live) : {TX.resp(TX.stmt(txs, sps, next, _)) == TX.RDone{} : TX.Resp}
+  {==}
+
+def Laws.savepoint_needs_live_tx(t, txs, sps, next, dead):
+  %dead : {TX.resp(TX.begin_sp(t, txs, sps, next, _)) == TX.RErr{} : TX.Resp}
+  {==}
+
+def Laws.savepoint_in_live_tx(t, txs, sps, next, live):
+  %T_true(TX.has(t, txs), live) : {TX.resp(TX.begin_sp(t, txs, sps, next, _)) == TX.RId{next} : TX.Resp}
+  {==}
+
+def Laws.savepoint_bound_to_tx(t, txs, sps, next, live):
+  %T_true(TX.has(t, txs), live) : {Some{t} == TX.owner(next, TX.sps_of(TX.state(TX.begin_sp(t, txs, sps, next, _)))) : Maybe<&2, Nat>}
+  %eq_refl(next) : {Some{t} == TX.found(t, TX.owner(next, sps), _) : Maybe<&2, Nat>}
+  {==}
+
+def Laws.fresh_tx_runs_statement(txs, sps, next):
+  %eq_refl(next) : {TX.resp(TX.stmt(next <> txs, sps, 1n+next, (_ || TX.has(next, txs)))) == TX.RDone{} : TX.Resp}
+  {==}
+
+def Laws.fresh_tx_takes_savepoint(txs, sps, next):
+  %eq_refl(next) : {TX.resp(TX.begin_sp(next, next <> txs, sps, 1n+next, (_ || TX.has(next, txs)))) == TX.RId{1n+next} : TX.Resp}
+  {==}
+
+def Laws.commit_rollback_same_state(t, txs, sps, next):
+  {==}
+
+# Ended transactions are rejected
+# --------------------------------
+
+# every request naming a transaction that is not live is an error
+def dead_tx_rejected(a: TX.Act, +t: Nat, +txs: List<&2, Nat>, +sps: List<&2, TX.Sp>, +next: Nat,
+  dead: {False{} == TX.has(t, txs) : Bool}, u: Laws.T(Laws.refers_tx(a, t)))
+  -> {TX.resp(TX.step(a, txs, sps, next)) == TX.RErr{} : TX.Resp}:
+  match a:
+    case TX.ABeginTx{}:
+      Empty.absurd({TX.resp(TX.step(TX.ABeginTx{}, txs, sps, next)) == TX.RErr{} : TX.Resp}, u)
+    case TX.ABeginSp{+tx}:
+      %eq_sound(t, tx, T_true(Nat.is_eq(t, tx), u)) : {TX.resp(TX.begin_sp(_, txs, sps, next, TX.has(_, txs))) == TX.RErr{} : TX.Resp}
+      %dead : {TX.resp(TX.begin_sp(t, txs, sps, next, _)) == TX.RErr{} : TX.Resp}
+      {==}
+    case TX.AEndTx{+tx, how}:
+      %eq_sound(t, tx, T_true(Nat.is_eq(t, tx), u)) : {TX.resp(TX.end_tx(_, txs, sps, next, TX.has(_, txs))) == TX.RErr{} : TX.Resp}
+      %dead : {TX.resp(TX.end_tx(t, txs, sps, next, _)) == TX.RErr{} : TX.Resp}
+      {==}
+    case TX.AEndSp{+sp, how}:
+      Empty.absurd({TX.resp(TX.step(TX.AEndSp{sp, how}, txs, sps, next)) == TX.RErr{} : TX.Resp}, u)
+    case TX.AStmt{TX.SAuto{}}:
+      Empty.absurd({TX.resp(TX.step(TX.AStmt{TX.SAuto{}}, txs, sps, next)) == TX.RErr{} : TX.Resp}, u)
+    case TX.AStmt{TX.STx{+tx}}:
+      %eq_sound(t, tx, T_true(Nat.is_eq(t, tx), u)) : {TX.resp(TX.stmt(txs, sps, next, TX.has(_, txs))) == TX.RErr{} : TX.Resp}
+      %dead : {TX.resp(TX.stmt(txs, sps, next, _)) == TX.RErr{} : TX.Resp}
+      {==}
+
+# over the verdict c of has(t, txs): after end_tx, t is not live either way
+def ended.fin(a: TX.Act, +t: Nat, +txs: List<&2, Nat>, +sps: List<&2, TX.Sp>, +next: Nat,
+  c: Bool, e: {c == TX.has(t, txs) : Bool}, u: Laws.T(Laws.refers_tx(a, t)))
+  -> {TX.resp(TX.step_s(a, TX.state(TX.end_tx(t, txs, sps, next, c)))) == TX.RErr{} : TX.Resp}:
+  match c:
+    case True{}:
+      dead_tx_rejected(a, t, TX.remove(t, txs), TX.cut(TX.OfTx{t}, sps), next, has_remove(t, txs), u)
+    case False{}:
+      dead_tx_rejected(a, t, txs, sps, next, e, u)
+
+def Laws.ended_tx_rejected(a, t, how, txs, sps, next, u):
+  ended.fin(a, t, txs, sps, next, TX.has(t, txs), {==}, u)
+
+# EndSavepoint and the transaction list
+# -------------------------------------
+
+# over the lookup verdict o: the transactions are untouched either way
+def keeps_txs.fin(+s: Nat, how: TX.EndSp, +txs: List<&2, Nat>, +sps: List<&2, TX.Sp>, +next: Nat, o: Maybe<&2, Nat>)
+  -> {txs == TX.txs_of(TX.state(TX.end_sp(s, how, txs, sps, next, o))) : List<&2, Nat>}:
+  match o:
+    case None{}:
+      {==}
+    case Some{t}:
+      {==}
+
+def Laws.end_savepoint_keeps_txs(s, how, txs, sps, next):
+  keeps_txs.fin(s, how, txs, sps, next, TX.owner(s, sps))
+
+# Lemmas on owner and cut
+# -----------------------
+
+def disc_m(m: Maybe<&2, Nat>) -> Type:
+  match m:
+    case None{}:
+      Empty
+    case Some{x}:
+      Unit
+
+# None and Some clash
+def none_ne_some(t: Nat, e: {Some{t} == None{} : Maybe<&2, Nat>}) -> Empty:
+  %e : disc_m(_)
+  Unit{}
+
+# cutting the savepoint s itself leaves no s: the step case, over the
+# verdict c of Nat.is_eq(id, s)
+def owner_cut_id.fin(+s: Nat, +id: Nat, +tx: Nat, -t: List<&2, TX.Sp>,
+  rec: {None{} == TX.owner(s, TX.cut(TX.IsId{s}, t)) : Maybe<&2, Nat>},
+  c: Bool, e: {c == Nat.is_eq(id, s) : Bool}, e2: {c == Nat.is_eq(s, id) : Bool})
+  -> {None{} == TX.owner(s, TX.put_sp(TX.Sp{id, tx}, TX.cut(TX.IsId{s}, t), c)) : Maybe<&2, Nat>}:
+  match c:
+    case True{}:
+      rec
+    case False{}:
+      %e2 : {None{} == TX.found(tx, TX.owner(s, TX.cut(TX.IsId{s}, t)), _) : Maybe<&2, Nat>}
+      rec
+
+# Nat.is_eq is symmetric
+def eq_sym(x: Nat, y: Nat) -> {Nat.is_eq(x, y) == Nat.is_eq(y, x) : Bool}:
+  match x y:
+    case 0n 0n:
+      {==}
+    case 0n 1n+q:
+      {==}
+    case 1n+p 0n:
+      {==}
+    case 1n+p 1n+q:
+      eq_sym(p, q)
+
+def owner_cut_id(+s: Nat, sps: List<&2, TX.Sp>) -> {None{} == TX.owner(s, TX.cut(TX.IsId{s}, sps)) : Maybe<&2, Nat>}:
+  match sps:
+    case Nil{}:
+      {==}
+    case Con{TX.Sp{+id, +tx}, t}:
+      owner_cut_id.fin(s, id, tx, t, owner_cut_id(s, t), Nat.is_eq(id, s), {==}, eq_sym(id, s))
+
+# a savepoint not selected by p keeps its owner through cut: the step
+# case, over the verdict c of Nat.is_eq(s, id) and then d of hit(p, id, tx)
+def owner_cut_keep.fin2(+p: TX.Pred, +s: Nat, +t: Nat, +id: Nat, +tx: Nat, -r: List<&2, TX.Sp>,
+  rec: {Some{t} == TX.owner(s, TX.cut(p, r)) : Maybe<&2, Nat>},
+  e: {False{} == Nat.is_eq(s, id) : Bool}, d: Bool)
+  -> {Some{t} == TX.owner(s, TX.put_sp(TX.Sp{id, tx}, TX.cut(p, r), d)) : Maybe<&2, Nat>}:
+  match d:
+    case True{}:
+      rec
+    case False{}:
+      %e : {Some{t} == TX.found(tx, TX.owner(s, TX.cut(p, r)), _) : Maybe<&2, Nat>}
+      rec
+
+# hit(p, s, t) restated for Sp{id, tx} when s == id and t == tx
+def cast_miss(+p: TX.Pred, +s: Nat, +t: Nat, +id: Nat, +tx: Nat, es: {s == id : Nat}, et: {t == tx : Nat},
+  m: {False{} == TX.hit(p, s, t) : Bool}) -> {False{} == TX.hit(p, id, tx) : Bool}:
+  %es : {False{} == TX.hit(p, _, tx) : Bool}
+  %et : {False{} == TX.hit(p, s, _) : Bool}
+  m
+
+def cast_hit(+p: TX.Pred, +s: Nat, +t: Nat, +id: Nat, +tx: Nat, es: {s == id : Nat}, et: {t == tx : Nat},
+  h: Laws.T(TX.hit(p, s, t))) -> Laws.T(TX.hit(p, id, tx)):
+  %es : Laws.T(TX.hit(p, _, tx))
+  %et : Laws.T(TX.hit(p, s, _))
+  h
+
+def owner_cut_keep.fin(+p: TX.Pred, +s: Nat, +t: Nat, +id: Nat, +tx: Nat, -r: List<&2, TX.Sp>,
+  rec: {Some{t} == TX.owner(s, r) : Maybe<&2, Nat>} -> {False{} == TX.hit(p, s, t) : Bool} -> {Some{t} == TX.owner(s, TX.cut(p, r)) : Maybe<&2, Nat>},
+  c: Bool, e: {c == Nat.is_eq(s, id) : Bool},
+  +own: {Some{t} == TX.found(tx, TX.owner(s, r), c) : Maybe<&2, Nat>},
+  miss: {False{} == TX.hit(p, s, t) : Bool})
+  -> {Some{t} == TX.owner(s, TX.put_sp(TX.Sp{id, tx}, TX.cut(p, r), TX.hit(p, id, tx))) : Maybe<&2, Nat>}:
+  match c:
+    case True{}:
+      +es = eq_sound(s, id, e)
+      %Equal.sym(Nat, s, id, es) : {Some{t} == TX.owner(_, TX.put_sp(TX.Sp{id, tx}, TX.cut(p, r), TX.hit(p, id, tx))) : Maybe<&2, Nat>}
+      %cast_miss(p, s, t, id, tx, es, some_inj(t, tx, own), miss) : {Some{t} == TX.owner(id, TX.put_sp(TX.Sp{id, tx}, TX.cut(p, r), _)) : Maybe<&2, Nat>}
+      %eq_refl(id) : {Some{t} == TX.found(tx, TX.owner(id, TX.cut(p, r)), _) : Maybe<&2, Nat>}
+      own
+    case False{}:
+      owner_cut_keep.fin2(p, s, t, id, tx, r, rec(own, miss), e, TX.hit(p, id, tx))
+
+def owner_cut_keep(+p: TX.Pred, +s: Nat, +t: Nat, sps: List<&2, TX.Sp>)
+  -> {Some{t} == TX.owner(s, sps) : Maybe<&2, Nat>} -> {False{} == TX.hit(p, s, t) : Bool} -> {Some{t} == TX.owner(s, TX.cut(p, sps)) : Maybe<&2, Nat>}:
+  match sps:
+    case Nil{}:
+      own => miss => Empty.absurd({Some{t} == TX.owner(s, TX.cut(p, Nil{})) : Maybe<&2, Nat>}, none_ne_some(t, own))
+    case Con{TX.Sp{+id, +tx}, r}:
+      own => miss => owner_cut_keep.fin(p, s, t, id, tx, r, owner_cut_keep(p, s, t, r), Nat.is_eq(s, id), {==}, own, miss)
+
+# Release and rollback keep what they should
+# ------------------------------------------
+
+# over the lookup verdict o of owner(s, sps)
+def release_kills.fin(+s: Nat, how: TX.EndSp, +txs: List<&2, Nat>, +sps: List<&2, TX.Sp>, +next: Nat,
+  o: Maybe<&2, Nat>, e: {o == TX.owner(s, sps) : Maybe<&2, Nat>})
+  -> {TX.resp(TX.step_s(TX.AEndSp{s, how}, TX.state(TX.end_sp(s, TX.SRelease{}, txs, sps, next, o)))) == TX.RErr{} : TX.Resp}:
+  match o:
+    case None{}:
+      %e : {TX.resp(TX.end_sp(s, how, txs, sps, next, _)) == TX.RErr{} : TX.Resp}
+      {==}
+    case Some{t}:
+      %owner_cut_id(s, sps) : {TX.resp(TX.end_sp(s, how, txs, TX.cut(TX.IsId{s}, sps), next, _)) == TX.RErr{} : TX.Resp}
+      {==}
+
+def Laws.release_kills_savepoint(s, how, txs, sps, next):
+  release_kills.fin(s, how, txs, sps, next, TX.owner(s, sps), {==})
+
+# over the lookup verdict o of owner(s, sps); s2 is untouched either way
+def release_keeps.fin(+s: Nat, +s2: Nat, +t: Nat, +txs: List<&2, Nat>, +sps: List<&2, TX.Sp>, +next: Nat,
+  o: Maybe<&2, Nat>, ne: {False{} == Nat.is_eq(s2, s) : Bool}, own: {Some{t} == TX.owner(s2, sps) : Maybe<&2, Nat>})
+  -> {Some{t} == TX.owner(s2, TX.sps_of(TX.state(TX.end_sp(s, TX.SRelease{}, txs, sps, next, o)))) : Maybe<&2, Nat>}:
+  match o:
+    case None{}:
+      own
+    case Some{t2}:
+      owner_cut_keep(TX.IsId{s}, s2, t, sps)(own, ne)
+
+def Laws.release_keeps_other_savepoints(s, s2, t, txs, sps, next, ne, own):
+  release_keeps.fin(s, s2, t, txs, sps, next, TX.owner(s, sps), ne, own)
+
+# a rollback to s does not select s: is_lt(s, s) fails
+def miss_self(+s: Nat, +t: Nat) -> {False{} == (Nat.is_eq(t, t) && Nat.is_lt(s, s)) : Bool}:
+  %eq_refl(t) : {False{} == (_ && Nat.is_lt(s, s)) : Bool}
+  lt_irrefl(s)
+
+# a rollback to s does not select an earlier s2: is_lt(s, s2) fails
+def miss_before(+s: Nat, +s2: Nat, +t: Nat, bef: Laws.T(Nat.is_lt(s2, s))) -> {False{} == (Nat.is_eq(t, t) && Nat.is_lt(s, s2)) : Bool}:
+  %eq_refl(t) : {False{} == (_ && Nat.is_lt(s, s2)) : Bool}
+  lt_asym(s2, s, bef)
+
+def Laws.rollback_keeps_savepoint(s, t, how, txs, sps, next, own):
+  %own : {TX.resp(TX.step_s(TX.AEndSp{s, how}, TX.state(TX.end_sp(s, TX.SRollback{}, txs, sps, next, _)))) == TX.RDone{} : TX.Resp}
+  %owner_cut_keep(TX.AfterIn{s, t}, s, t, sps)(own, miss_self(s, t)) : {TX.resp(TX.end_sp(s, how, txs, TX.cut(TX.AfterIn{s, t}, sps), next, _)) == TX.RDone{} : TX.Resp}
+  {==}
+
+def Laws.rollback_keeps_earlier_savepoints(s, s2, t, txs, sps, next, own, own2, bef):
+  %own : {Some{t} == TX.owner(s2, TX.sps_of(TX.state(TX.end_sp(s, TX.SRollback{}, txs, sps, next, _)))) : Maybe<&2, Nat>}
+  owner_cut_keep(TX.AfterIn{s, t}, s2, t, sps)(own2, miss_before(s, s2, t, bef))
+
+# Lemmas on desc and desc_sp
+# --------------------------
+
+# a bound a is a bound b when a < b
+def weaken(xs: List<&2, Nat>, +a: Nat, +b: Nat, w: Laws.T(Laws.desc(xs, a)), ab: Laws.T(Nat.is_lt(a, b))) -> Laws.T(Laws.desc(xs, b)):
+  match xs:
+    case Nil{}:
+      Unit{}
+    case Con{+x, +t}:
+      split.fin(Nat.is_lt(x, a), Laws.desc(t, x), w, Laws.T(Laws.desc(x <> t, b)),
+        wx => wt => join.fin(Nat.is_lt(x, b), Laws.desc(t, x), lt_trans(x, a, b, wx, ab), wt))
+
+def weaken_sp(sps: List<&2, TX.Sp>, +a: Nat, +b: Nat, w: Laws.T(Laws.desc_sp(sps, a)), ab: Laws.T(Nat.is_lt(a, b))) -> Laws.T(Laws.desc_sp(sps, b)):
+  match sps:
+    case Nil{}:
+      Unit{}
+    case Con{TX.Sp{+id, +tx}, +t}:
+      split.fin(Nat.is_lt(id, a), Laws.desc_sp(t, id), w, Laws.T(Laws.desc_sp(TX.Sp{id, tx} <> t, b)),
+        wx => wt => join.fin(Nat.is_lt(id, b), Laws.desc_sp(t, id), lt_trans(id, a, b, wx, ab), wt))
+
+# a bound below n is a bound below n + 1
+def mono(xs: List<&2, Nat>, +n: Nat, w: Laws.T(Laws.desc(xs, n))) -> Laws.T(Laws.desc(xs, 1n+n)):
+  weaken(xs, n, 1n+n, w, lt_succ(n))
+
+def mono_sp(sps: List<&2, TX.Sp>, +n: Nat, w: Laws.T(Laws.desc_sp(sps, n))) -> Laws.T(Laws.desc_sp(sps, 1n+n)):
+  weaken_sp(sps, n, 1n+n, w, lt_succ(n))
+
+# removing keeps the order: the step case, over the verdict c of the removal
+def desc_remove.fin(c: Bool, +h: Nat, +x: Nat, t: List<&2, Nat>, +n: Nat,
+  wx: Laws.T(Nat.is_lt(x, n)), wr: Laws.T(Laws.desc(TX.remove(h, t), x)))
+  -> Laws.T(Laws.desc(TX.put(x, TX.remove(h, t), c), n)):
+  match c:
+    case True{}:
+      weaken(TX.remove(h, t), x, n, wr, wx)
+    case False{}:
+      join.fin(Nat.is_lt(x, n), Laws.desc(TX.remove(h, t), x), wx, wr)
+
+def desc_remove(+h: Nat, xs: List<&2, Nat>, +n: Nat, w: Laws.T(Laws.desc(xs, n))) -> Laws.T(Laws.desc(TX.remove(h, xs), n)):
+  match xs:
+    case Nil{}:
+      Unit{}
+    case Con{+x, +t}:
+      split.fin(Nat.is_lt(x, n), Laws.desc(t, x), w, Laws.T(Laws.desc(TX.remove(h, x <> t), n)),
+        wx => wt => desc_remove.fin(Nat.is_eq(x, h), h, x, t, n, wx, desc_remove(h, t, x, wt)))
+
+# cutting keeps the order: the step case, over the verdict c of hit
+def desc_cut.fin(c: Bool, +p: TX.Pred, +id: Nat, +tx: Nat, t: List<&2, TX.Sp>, +n: Nat,
+  wx: Laws.T(Nat.is_lt(id, n)), wr: Laws.T(Laws.desc_sp(TX.cut(p, t), id)))
+  -> Laws.T(Laws.desc_sp(TX.put_sp(TX.Sp{id, tx}, TX.cut(p, t), c), n)):
+  match c:
+    case True{}:
+      weaken_sp(TX.cut(p, t), id, n, wr, wx)
+    case False{}:
+      join.fin(Nat.is_lt(id, n), Laws.desc_sp(TX.cut(p, t), id), wx, wr)
+
+def desc_cut(+p: TX.Pred, sps: List<&2, TX.Sp>, +n: Nat, w: Laws.T(Laws.desc_sp(sps, n))) -> Laws.T(Laws.desc_sp(TX.cut(p, sps), n)):
+  match sps:
+    case Nil{}:
+      Unit{}
+    case Con{TX.Sp{+id, +tx}, +t}:
+      split.fin(Nat.is_lt(id, n), Laws.desc_sp(t, id), w, Laws.T(Laws.desc_sp(TX.cut(p, TX.Sp{id, tx} <> t), n)),
+        wx => wt => desc_cut.fin(TX.hit(p, id, tx), p, id, tx, t, n, wx, desc_cut(p, t, id, wt)))
+
+# Invariant laws
+# --------------
+
+def Laws.inv_start():
+  (Unit{}, Unit{})
+
+# the BeginSavepoint arm, over the verdict c of has(t, txs)
+def kept_begin_sp.fin(c: Bool, +t: Nat, +txs: List<&2, Nat>, +sps: List<&2, TX.Sp>, +next: Nat, w: Laws.Inv(txs, sps, next))
+  -> Laws.Inv_s(TX.state(TX.begin_sp(t, txs, sps, next, c))):
+  match c:
+    case True{}:
+      (wt, ws) = w
+      (mono(txs, next, wt), join.fin(Nat.is_lt(next, 1n+next), Laws.desc_sp(sps, next), lt_succ(next), ws))
+    case False{}:
+      w
+
+# the EndTransaction arm, over the verdict c of has(t, txs)
+def kept_end_tx.fin(c: Bool, +t: Nat, +txs: List<&2, Nat>, +sps: List<&2, TX.Sp>, +next: Nat, w: Laws.Inv(txs, sps, next))
+  -> Laws.Inv_s(TX.state(TX.end_tx(t, txs, sps, next, c))):
+  match c:
+    case True{}:
+      (wt, ws) = w
+      (desc_remove(t, txs, next, wt), desc_cut(TX.OfTx{t}, sps, next, ws))
+    case False{}:
+      w
+
+# the EndSavepoint arm, over the lookup verdict o and the action
+def kept_end_sp.fin(o: Maybe<&2, Nat>, how: TX.EndSp, +s: Nat, +txs: List<&2, Nat>, +sps: List<&2, TX.Sp>, +next: Nat, w: Laws.Inv(txs, sps, next))
+  -> Laws.Inv_s(TX.state(TX.end_sp(s, how, txs, sps, next, o))):
+  match o how:
+    case None{} TX.SRelease{}:
+      w
+    case None{} TX.SRollback{}:
+      w
+    case Some{t} TX.SRelease{}:
+      (wt, ws) = w
+      (wt, desc_cut(TX.IsId{s}, sps, next, ws))
+    case Some{t} TX.SRollback{}:
+      (wt, ws) = w
+      (wt, desc_cut(TX.AfterIn{s, t}, sps, next, ws))
+
+# the statement arm: the state is unchanged either way
+def kept_stmt.fin(c: Bool, +txs: List<&2, Nat>, +sps: List<&2, TX.Sp>, +next: Nat, w: Laws.Inv(txs, sps, next))
+  -> Laws.Inv_s(TX.state(TX.stmt(txs, sps, next, c))):
+  match c:
+    case True{}:
+      w
+    case False{}:
+      w
+
+def Laws.inv_kept(a, txs, sps, next, w):
+  match a:
+    case TX.ABeginTx{}:
+      (wt, ws) = w
+      (join.fin(Nat.is_lt(next, 1n+next), Laws.desc(txs, next), lt_succ(next), wt), mono_sp(sps, next, ws))
+    case TX.ABeginSp{+t}:
+      kept_begin_sp.fin(TX.has(t, txs), t, txs, sps, next, w)
+    case TX.AEndTx{+t, how}:
+      kept_end_tx.fin(TX.has(t, txs), t, txs, sps, next, w)
+    case TX.AEndSp{+s, how}:
+      kept_end_sp.fin(TX.owner(s, sps), how, s, txs, sps, next, w)
+    case TX.AStmt{TX.SAuto{}}:
+      w
+    case TX.AStmt{TX.STx{+t}}:
+      kept_stmt.fin(TX.has(t, txs), txs, sps, next, w)
+
+# Unique ids: a cut savepoint is gone
+# -----------------------------------
+
+# below a bound s, no savepoint has id s, before or after a cut: the
+# step case, over the verdict d of hit(p, id, tx)
+def below_none_cut.fin(d: Bool, +p: TX.Pred, +s: Nat, +id: Nat, +tx: Nat, r: List<&2, TX.Sp>,
+  +wx: Laws.T(Nat.is_lt(id, s)), wr: Laws.T(Laws.desc_sp(r, id)),
+  rec: Laws.T(Laws.desc_sp(r, s)) -> {None{} == TX.owner(s, TX.cut(p, r)) : Maybe<&2, Nat>})
+  -> {None{} == TX.owner(s, TX.put_sp(TX.Sp{id, tx}, TX.cut(p, r), d)) : Maybe<&2, Nat>}:
+  match d:
+    case True{}:
+      rec(weaken_sp(r, id, s, wr, wx))
+    case False{}:
+      %lt_ne_r(id, s, wx) : {None{} == TX.found(tx, TX.owner(s, TX.cut(p, r)), _) : Maybe<&2, Nat>}
+      rec(weaken_sp(r, id, s, wr, wx))
+
+def below_none_cut(+p: TX.Pred, +s: Nat, r: List<&2, TX.Sp>) -> Laws.T(Laws.desc_sp(r, s)) -> {None{} == TX.owner(s, TX.cut(p, r)) : Maybe<&2, Nat>}:
+  match r:
+    case Nil{}:
+      w => {==}
+    case Con{TX.Sp{+id, +tx}, +r2}:
+      w => split.fin(Nat.is_lt(id, s), Laws.desc_sp(r2, id), w, {None{} == TX.owner(s, TX.cut(p, TX.Sp{id, tx} <> r2)) : Maybe<&2, Nat>},
+        wx => wr => below_none_cut.fin(TX.hit(p, id, tx), p, s, id, tx, r2, wx, wr, below_none_cut(p, s, r2)))
+
+# then over the verdict d of hit(p, id, tx), when id is not s
+def owner_cut_hit.fin2(+p: TX.Pred, +s: Nat, +t: Nat, +id: Nat, +tx: Nat, -r: List<&2, TX.Sp>,
+  rec: {None{} == TX.owner(s, TX.cut(p, r)) : Maybe<&2, Nat>},
+  e: {False{} == Nat.is_eq(s, id) : Bool}, d: Bool)
+  -> {None{} == TX.owner(s, TX.put_sp(TX.Sp{id, tx}, TX.cut(p, r), d)) : Maybe<&2, Nat>}:
+  match d:
+    case True{}:
+      rec
+    case False{}:
+      %e : {None{} == TX.found(tx, TX.owner(s, TX.cut(p, r)), _) : Maybe<&2, Nat>}
+      rec
+
+# a savepoint selected by p is gone after cut, given unique ids: the
+# step case, over the verdict c of Nat.is_eq(s, id)
+def owner_cut_hit.fin(+p: TX.Pred, +s: Nat, +t: Nat, +id: Nat, +tx: Nat, r: List<&2, TX.Sp>,
+  rec: Laws.T(Laws.desc_sp(r, id)) -> {Some{t} == TX.owner(s, r) : Maybe<&2, Nat>} -> Laws.T(TX.hit(p, s, t)) -> {None{} == TX.owner(s, TX.cut(p, r)) : Maybe<&2, Nat>},
+  c: Bool, e: {c == Nat.is_eq(s, id) : Bool},
+  wr: Laws.T(Laws.desc_sp(r, id)),
+  own: {Some{t} == TX.found(tx, TX.owner(s, r), c) : Maybe<&2, Nat>},
+  h: Laws.T(TX.hit(p, s, t)))
+  -> {None{} == TX.owner(s, TX.put_sp(TX.Sp{id, tx}, TX.cut(p, r), TX.hit(p, id, tx))) : Maybe<&2, Nat>}:
+  match c:
+    case True{}:
+      +es = eq_sound(s, id, e)
+      %Equal.sym(Nat, s, id, es) : {None{} == TX.owner(_, TX.put_sp(TX.Sp{id, tx}, TX.cut(p, r), TX.hit(p, id, tx))) : Maybe<&2, Nat>}
+      %T_true(TX.hit(p, id, tx), cast_hit(p, s, t, id, tx, es, some_inj(t, tx, own), h)) : {None{} == TX.owner(id, TX.put_sp(TX.Sp{id, tx}, TX.cut(p, r), _)) : Maybe<&2, Nat>}
+      below_none_cut(p, id, r)(wr)
+    case False{}:
+      owner_cut_hit.fin2(p, s, t, id, tx, r, rec(wr, own, h), e, TX.hit(p, id, tx))
+
+def owner_cut_hit(+p: TX.Pred, +s: Nat, +t: Nat, sps: List<&2, TX.Sp>, +n: Nat)
+  -> Laws.T(Laws.desc_sp(sps, n)) -> {Some{t} == TX.owner(s, sps) : Maybe<&2, Nat>} -> Laws.T(TX.hit(p, s, t)) -> {None{} == TX.owner(s, TX.cut(p, sps)) : Maybe<&2, Nat>}:
+  match sps:
+    case Nil{}:
+      w => own => h => Empty.absurd({None{} == TX.owner(s, TX.cut(p, Nil{})) : Maybe<&2, Nat>}, none_ne_some(t, own))
+    case Con{TX.Sp{+id, +tx}, +r}:
+      w => own => h => split.fin(Nat.is_lt(id, n), Laws.desc_sp(r, id), w, {None{} == TX.owner(s, TX.cut(p, TX.Sp{id, tx} <> r)) : Maybe<&2, Nat>},
+        wx => wr => owner_cut_hit.fin(p, s, t, id, tx, r, owner_cut_hit(p, s, t, r, id), Nat.is_eq(s, id), {==}, wr, own, h))
+
+# Ended transactions and rollbacks kill savepoints
+# ------------------------------------------------
+
+def Laws.ended_tx_kills_savepoints(t, s, how, how2, txs, sps, next, w, live, own):
+  (wt, ws) = w
+  %T_true(TX.has(t, txs), live) : {TX.resp(TX.step_s(TX.AEndSp{s, how2}, TX.state(TX.end_tx(t, txs, sps, next, _)))) == TX.RErr{} : TX.Resp}
+  %owner_cut_hit(TX.OfTx{t}, s, t, sps, next)(ws, own, true_T(Nat.is_eq(t, t), eq_refl(t))) : {TX.resp(TX.end_sp(s, how2, TX.remove(t, txs), TX.cut(TX.OfTx{t}, sps), next, _)) == TX.RErr{} : TX.Resp}
+  {==}
+
+def Laws.rollback_kills_later_savepoints(s, s2, t, how, txs, sps, next, w, own, own2, aft):
+  (wt, ws) = w
+  %own : {TX.resp(TX.step_s(TX.AEndSp{s2, how}, TX.state(TX.end_sp(s, TX.SRollback{}, txs, sps, next, _)))) == TX.RErr{} : TX.Resp}
+  %owner_cut_hit(TX.AfterIn{s, t}, s2, t, sps, next)(ws, own2, join.fin(Nat.is_eq(t, t), Nat.is_lt(s, s2), true_T(Nat.is_eq(t, t), eq_refl(t)), aft)) : {TX.resp(TX.end_sp(s2, how, txs, TX.cut(TX.AfterIn{s, t}, sps), next, _)) == TX.RErr{} : TX.Resp}
+  {==}
diff --git a/dev/bend2/flightsql_transactions/README.md b/dev/bend2/flightsql_transactions/README.md
new file mode 100644
index 0000000000..48a3948202
--- /dev/null
+++ b/dev/bend2/flightsql_transactions/README.md
@@ -0,0 +1,270 @@
+<!---
+  Licensed to the Apache Software Foundation (ASF) under one
+  or more contributor license agreements.  See the NOTICE file
+  distributed with this work for additional information
+  regarding copyright ownership.  The ASF licenses this file
+  to you under the Apache License, Version 2.0 (the
+  "License"); you may not use this file except in compliance
+  with the License.  You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+  Unless required by applicable law or agreed to in writing,
+  software distributed under the License is distributed on an
+  "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
+  KIND, either express or implied.  See the License for the
+  specific language governing permissions and limitations
+  under the License.
+-->
+
+# Flight SQL transactions and savepoints, as Bend 2 laws
+
+A checked model of the Arrow Flight SQL transaction and savepoint
+lifecycle, written in [Bend 2](https://github.com/bendlang/bend). The
+model (`main.bend`) is an executable state machine for the server side
+of `BeginTransaction`, `BeginSavepoint`, `EndTransaction`,
+`EndSavepoint` and statements that carry an optional `transaction_id`.
+`LAWS.bend` states the sentences of `arrow-format/FlightSql.proto` that
+describe these actions as laws over that machine, and `PROOF.bend`
+proves them. `bend PROOF.bend` refuses to pass while any law is
+unproven or false.
+
+This is a proof of concept for using Bend as a specification tool
+around Arrow. It follows the prepared-statement prototype and the
+research notes in `dev/bend2/README.md` on the
+`claude/bend2-arrow-integration-pgexut` branch of this repository, and
+reuses that prototype's proof helpers (the `T` predicate, `split.fin`
+and `join.fin`, the Nat lemmas, the "inspect" idiom for matching a
+computed Boolean). Checked against Bend 2.0.21, commit `6018e28e` of
+bendlang/bend, on 2026-09-20.
+
+## 1. What is modelled
+
+Sources read: the messages `ActionBeginTransactionRequest`,
+`ActionBeginSavepointRequest`, `ActionBeginTransactionResult`,
+`ActionBeginSavepointResult`, `ActionEndTransactionRequest` (enum
+`EndTransaction`: COMMIT, ROLLBACK), `ActionEndSavepointRequest` (enum
+`EndSavepoint`: RELEASE, ROLLBACK) and the `optional bytes
+transaction_id` of `CommandStatementQuery`, `CommandStatementUpdate` and
+`ActionCreatePreparedStatementRequest` in `arrow-format/FlightSql.proto`;
+`FlightSqlProducer.beginTransaction`, `beginSavepoint`, `endTransaction`,
+`endSavepoint` and `FlightSqlClient.Transaction`, `Savepoint`,
+`beginTransaction`, `beginSavepoint`, `commit`, `rollback`, `release`
+in `flight/flight-sql`; the example servers under
+`flight/flight-sql/src/test/.../example/` (both advertise
+`SQL_SUPPORTED_TRANSACTION_NONE` and implement none of the four
+actions, so they contributed nothing beyond the interface). The format
+document `docs/source/format/FlightSql.rst` in apache/arrow does not
+mention transactions; the proto comments are the whole written spec.
+
+### 1.1 The state machine
+
+```
+type Sp is Data:
+  Sp{id: Nat, tx: Nat}                 # a live savepoint and its transaction
+
+type Server is Data:
+  Server{txs: List<&2, Nat>,           # live transaction ids, newest first
+         sps: List<&2, Sp>,            # live savepoints, newest first
+         next: Nat}                    # the next id to issue
+```
+
+One counter issues both transaction and savepoint ids, so a savepoint
+id can never be mistaken for a transaction id. The "ordered list of
+savepoints of a transaction" is the sub-list of `sps` tagged with that
+transaction; since ids come from a counter, "created after savepoint
+s" is "has an id greater than s".
+
+Requests and responses:
+
+| Request | Proto message | Effect when it succeeds | Error when |
+| --- | --- | --- | --- |
+| `ABeginTx{}` | `ActionBeginTransactionRequest` | adds `next` to `txs`, answers `RId{next}` | never |
+| `ABeginSp{tx}` | `ActionBeginSavepointRequest` | adds `Sp{next, tx}` to `sps`, answers `RId{next}` | `tx` not live |
+| `AEndTx{tx, how}` | `ActionEndTransactionRequest` | removes `tx` and every `Sp{_, tx}`; `how` is COMMIT or ROLLBACK | `tx` not live |
+| `AEndSp{sp, SRelease{}}` | `ActionEndSavepointRequest` RELEASE | removes `Sp{sp, _}` | `sp` not live |
+| `AEndSp{sp, SRollback{}}` | `ActionEndSavepointRequest` ROLLBACK | removes the `Sp{id, t}` of the same transaction `t` with `id > sp`; keeps `sp` | `sp` not live |
+| `AStmt{STx{tx}}` | statement with `transaction_id` | no state change, answers `RDone{}` | `tx` not live |
+| `AStmt{SAuto{}}` | statement without `transaction_id` | no state change, answers `RDone{}` (auto-commit) | never |
+
+`step` is one request against one state, `replay` runs a trace from
+the empty server. `main` prints the responses of a ten-step trace:
+begin transaction 0, savepoints 1 and 2 in it, roll back to 1 (retires
+2), release 2 (error), a statement in 0, commit 0, a statement in 0
+(error), release 1 (error), an auto-commit statement:
+
+```
+[Id(0), Id(1), Id(2), Done, Err, Done, Done, Err, Err, Done]
+```
+
+### 1.2 Readings chosen where the proto is silent
+
+- **Release keeps the other savepoints.** The proto says "Releasing a
+  savepoint invalidates that savepoint" and nothing else. The model
+  removes exactly that savepoint. JDBC's `Connection.releaseSavepoint`
+  and PostgreSQL's `RELEASE SAVEPOINT` also drop the savepoints created
+  after it; a server with that behaviour satisfies
+  `release_kills_savepoint` but violates
+  `release_keeps_other_savepoints`. The law is there so that the choice
+  is explicit and a reviewer can flip it.
+- **Commit and rollback are the same lifecycle transition.** Both
+  retire the transaction and its savepoints ("If the action completes
+  successfully, the transaction handle is invalidated, as are all
+  associated savepoints"). What happens to the data is outside the
+  model, and `commit_rollback_same_state` records that the model does
+  not distinguish them.
+- **Ending a transaction that is not live is an error**, and so is any
+  `EndSavepoint` on an id that is not live. The proto does not say what
+  a server answers to an unknown handle; every Flight SQL producer in
+  practice returns an error status, and the Java client turns a missing
+  result into an exception.
+- **Ids are `Nat`s from one counter**, standing in for the proto's
+  opaque `bytes` handles. The only property of a handle the lifecycle
+  depends on is that it is never reissued, which is the invariant.
+
+## 2. The laws
+
+Every law is stated for arbitrary `txs`, `sps` and `next`. The two
+laws that need unique ids take the invariant `Inv(txs, sps, next)` as
+a hypothesis; `inv_start` and `inv_kept` show every reachable state
+satisfies it. Bend's rewrite direction is the reason every equation is
+written with the constant on the left (`{False{} == has(t, txs)}`).
+
+| Law | Spec sentence (FlightSql.proto) | Statement |
+| --- | --- | --- |
+| `ended_tx_rejected` | "If the action completes successfully, the transaction handle is invalidated" | After `AEndTx{t, how}`, any request that names `t` as its transaction_id (`ABeginSp`, `AEndTx`, `AStmt{STx{t}}`) is `RErr`. Unconditional: if `t` was not live the `EndTransaction` failed and `t` is still not live. |
+| `ended_tx_kills_savepoints` | "...as are all associated savepoints"; "If the associated transaction is committed, rolled back, or times out, then the savepoint is also invalidated" | After `AEndTx{t, how}` on a live `t`, `AEndSp{s, how2}` on any `s` owned by `t` is `RErr`. Needs `Inv`. |
+| `commit_rollback_same_state` | "Commit (COMMIT) or rollback (ROLLBACK) the transaction" | `AEndTx{t, TCommit{}}` and `AEndTx{t, TRollback{}}` produce the same state. |
+| `savepoint_needs_live_tx` | "Creates a savepoint within a transaction"; "The transaction to which a savepoint belongs" | `ABeginSp{t}` with `t` not live is `RErr`. |
+| `savepoint_in_live_tx` | anti-vacuity | `ABeginSp{t}` with `t` live answers `RId{next}`. |
+| `savepoint_bound_to_tx` | "The transaction to which a savepoint belongs" | after `ABeginSp{t}` on live `t`, the server records `next` as owned by `t`. |
+| `end_savepoint_keeps_txs` | "Roll back to a savepoint" (as opposed to the transaction) | any `AEndSp` leaves `txs` unchanged, so the transaction stays live. |
+| `release_kills_savepoint` | "Releasing a savepoint invalidates that savepoint" | after `AEndSp{s, SRelease{}}`, any `AEndSp{s, how}` is `RErr`. Unconditional. |
+| `release_keeps_other_savepoints` | chosen reading, see 1.2 | after `AEndSp{s, SRelease{}}`, every other live savepoint keeps its owner. |
+| `rollback_keeps_savepoint` | "Rolling back to a savepoint does not invalidate the savepoint" | after `AEndSp{s, SRollback{}}` on live `s`, another `AEndSp{s, how}` answers `RDone{}`. |
+| `rollback_kills_later_savepoints` | "...but invalidates all savepoints created after the current savepoint" | after `AEndSp{s, SRollback{}}` on live `s` of `t`, `AEndSp{s2, how}` is `RErr` for every live `s2` of `t` with `s < s2`. Needs `Inv`. |
+| `rollback_keeps_earlier_savepoints` | complement of the sentence above | the savepoints of `t` with `s2 < s` keep their owner. |
+| `statement_needs_live_tx` | "Include the query as part of this transaction" | `AStmt{STx{t}}` with `t` not live is `RErr`. |
+| `statement_autocommit` | "(if unset, the query is auto-committed)" | `AStmt{SAuto{}}` answers `RDone{}` from any state. |
+| `statement_in_live_tx` | anti-vacuity | `AStmt{STx{t}}` with `t` live answers `RDone{}`. |
+| `fresh_tx_runs_statement` | anti-vacuity | the id `ABeginTx{}` returns runs a statement. |
+| `fresh_tx_takes_savepoint` | anti-vacuity | the id `ABeginTx{}` returns takes a savepoint, whose id is `1n+next`. |
+| `inv_start` | freshness | the empty server satisfies `Inv`. |
+| `inv_kept` | freshness | every request preserves `Inv`. |
+
+The invariant is stronger than the prepared-statement prototype's "all
+handles below the counter": `desc(xs, n)` says the list is strictly
+descending with head below `n`. It is what the server naturally
+maintains (new ids go to the front), it implies freshness, and it gives
+uniqueness of ids for free, which `ended_tx_kills_savepoints` and
+`rollback_kills_later_savepoints` need. Without uniqueness a second
+transaction could hold a savepoint with the same id as the one just
+retired, and the later `EndSavepoint` would find it.
+
+### 2.1 Laws kept but not proven
+
+Kept in `LAWS.bend` as comments with the reason above each:
+
+- `NOT EXPRESSIBLE` timeout: "If the transaction times out, then it is
+  automatically rolled back." The model has no clock; a timeout is an
+  event the server raises between requests, not a request. It could be
+  added as an explicit `ATimeout{tx}` request equal to
+  `AEndTx{tx, TRollback{}}`, but that only restates
+  `commit_rollback_same_state`, not the timing.
+- `NOT EXPRESSIBLE` opaque `bytes` handles: nothing about handle
+  encoding is stated; Bend has no byte or 64-bit integer type and the
+  lifecycle depends only on ids not being reissued, which `inv_kept`
+  covers.
+- `NOT EXPRESSIBLE` feature negotiation: "Only supported if
+  FLIGHT_SQL_TRANSACTION is FLIGHT_SQL_TRANSACTION_SUPPORT_SAVEPOINT" is
+  a `GetSqlInfo` property with its own RPC; the model assumes a server
+  that supports savepoints.
+
+Every law that was attempted was proven, so there is no `NOT PROVEN`
+entry.
+
+## 3. How to run
+
+The installer host `bend-lang.com` was blocked in the environment this
+was written in, so the checker ran from a clone with bun, which is
+what the installed binary wraps:
+
+```sh
+git clone --depth 1 https://github.com/bendlang/bend.git /tmp/bend
+BEND="bun /tmp/bend/bend2/main.ts"
+cd dev/bend2/flightsql_transactions
+$BEND PROOF.bend            # All terms check.
+$BEND main.bend             # runs the trace in main
+$BEND main.bend -o out.js   # JavaScript target; node out.js
+$BEND main.bend -o out      # native binary via clang; ./out
+```
+
+## 4. Results
+
+| Item | Value |
+| --- | ---: |
+| `main.bend` | 295 lines |
+| `LAWS.bend` (19 proven laws, 3 not-expressible ones as comments) | 340 lines |
+| `PROOF.bend` | 649 lines |
+| `bend PROOF.bend` wall time | 0.32 s |
+| JavaScript output | 21 KB, runs under node |
+| Native output | 1.1 MB, builds in 4 s with clang 18, runs |
+
+Roughly two lines of proof per line of model, as in the
+prepared-statement prototype. About a third of `PROOF.bend` is the
+generic kit (`T` splitting and joining, `Nat` order lemmas:
+`lt_trans`, `lt_irrefl`, `lt_asym`, `lt_ne`, soundness of `is_eq`,
+injectivity of `Some`). The model-specific part is four lemma
+families: `owner_cut_keep` (a savepoint the cut does not select keeps
+its owner), `owner_cut_hit` (a selected savepoint is gone, given
+unique ids), `below_none_cut` (no savepoint below a bound has that
+bound as id) and the `desc` preservation lemmas for `remove` and `cut`.
+
+### 4.1 Mutation tests
+
+Each mutation was applied to a copy of `main.bend`, `bend PROOF.bend`
+was run, and the copy discarded. The committed files are unmodified.
+
+| # | Mutation of `main.bend` | Spec bug it corresponds to | Law that is false | Where the checker first fails |
+| --- | --- | --- | --- | --- |
+| 1 | `end_tx` keeps `sps` instead of `cut(OfTx{t}, sps)` | commit does not retire the transaction's savepoints | `ended_tx_kills_savepoints` | `ended.fin`: the rewritten state no longer has the `cut` |
+| 2 | `AfterIn` selects `is_le(s, id)` instead of `is_lt(s, id)` | rollback to a savepoint drops the savepoint itself | `rollback_keeps_savepoint` | `Laws.rollback_keeps_savepoint`: `miss_self` proves `is_lt(s, s)` false, the goal now has `is_le(s, s)` |
+| 3 | `stmt` answers `RDone{}` when the transaction is not live | a statement on an ended transaction succeeds | `statement_needs_live_tx`, `ended_tx_rejected` | `Laws.statement_needs_live_tx`: expected `RDone{}`, observed `RErr{}` |
+| 4 | `ABeginTx` does not advance `next` | transaction ids reissued | `fresh_tx_takes_savepoint`, `inv_kept` | `Laws.fresh_tx_runs_statement`: the proof spelled out `1n+next` |
+| 5 | `IsId` selects `is_le(s, id)` (the JDBC reading of release) | release also drops later savepoints | `release_keeps_other_savepoints` | `owner_cut_id`: the verdict passed to `.fin` no longer matches |
+| 6 | `AfterIn` selects nothing (`False{}`) | rollback keeps the later savepoints | `rollback_kills_later_savepoints` | `Laws.rollback_keeps_savepoint`: `miss_self` has the wrong shape |
+| 7 | `end_sp` also removes the owning transaction | ending a savepoint ends the transaction | `end_savepoint_keeps_txs` | `keeps_txs.fin`: expected `txs`, observed `remove(t, txs)` |
+
+All seven are rejected. The last column shows the brittleness noted in
+the research notes: the checker reports the first proof that no longer
+type-checks, which is often a lemma whose statement spelled out the
+old shape of the model, not the law that became false. In rows 1, 2,
+5 and 6 the failing location is a proof step, and the law that is
+genuinely violated is in the column before. Both readings block the
+build, which is what `LAWS.bend` promises; telling "the law is false"
+from "the proof needs updating" is left to the reader.
+
+### 4.2 An observation on the Java client
+
+While reading `FlightSqlClient` for the semantics: `rollback(Savepoint)`
+(documented "Rollback to a savepoint") sets `END_SAVEPOINT_RELEASE` as
+its action, the same value as `release(Savepoint)`. Under this model a
+client calling `rollback(savepoint)` would in fact perform the
+`SRelease{}` transition, so the savepoint would be gone afterwards
+(`release_kills_savepoint`) instead of staying usable
+(`rollback_keeps_savepoint`). This is exactly the kind of mismatch a
+model of the lifecycle makes visible; no Java code was changed in this
+proof of concept.
+
+## 5. What this shows about Bend for Arrow
+
+The lifecycle sentences of the proto, including the ones about
+interaction between actions ("as are all associated savepoints",
+"invalidates all savepoints created after"), fit in a few hundred
+lines of laws and proofs and check in a third of a second. The parts
+that resisted were not the semantics but the language mechanics: the
+rewrite direction forces a convention on how equations are written,
+computed values need a helper to be matched, and a change to the model
+breaks proofs that mention its shape. The parts that Bend cannot say
+are the ones outside a pure request/response machine: time (timeouts),
+bytes (handles), and negotiation state that lives in another RPC.
diff --git a/dev/bend2/flightsql_transactions/main.bend b/dev/bend2/flightsql_transactions/main.bend
new file mode 100644
index 0000000000..3a64f4d529
--- /dev/null
+++ b/dev/bend2/flightsql_transactions/main.bend
@@ -0,0 +1,295 @@
+# Licensed to the Apache Software Foundation (ASF) under one
+# or more contributor license agreements.  See the NOTICE file
+# distributed with this work for additional information
+# regarding copyright ownership.  The ASF licenses this file
+# to you under the Apache License, Version 2.0 (the
+# "License"); you may not use this file except in compliance
+# with the License.  You may obtain a copy of the License at
+#
+#   http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing,
+# software distributed under the License is distributed on an
+# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
+# KIND, either express or implied.  See the License for the
+# specific language governing permissions and limitations
+# under the License.
+
+# A model of the Arrow Flight SQL transaction and savepoint lifecycle
+# (FlightSql.proto: ActionBeginTransaction, ActionBeginSavepoint,
+# ActionEndTransaction, ActionEndSavepoint, and the optional
+# transaction_id on statements), written in Bend 2 so that LAWS.bend
+# can state the spec's sentences about it and PROOF.bend can prove them.
+#
+# Ids for transactions and savepoints are Nats issued by one counter.
+# The server keeps the live transaction ids and the live savepoints,
+# each tagged with the transaction it belongs to; both lists are
+# newest first. The savepoints of one transaction are the entries of
+# `sps` tagged with it, so "created after" is "has a larger id".
+#
+#   bend main.bend         # checks the model and runs the sample trace in main
+#   bend PROOF.bend        # checks LAWS.bend against this model
+
+import Base
+
+# Protocol
+# --------
+
+# ActionEndTransactionRequest.EndTransaction
+type EndTx is Data:
+  TCommit{}
+  TRollback{}
+
+# ActionEndSavepointRequest.EndSavepoint
+type EndSp is Data:
+  SRelease{}
+  SRollback{}
+
+# the optional transaction_id of CommandStatementQuery,
+# CommandStatementUpdate and ActionCreatePreparedStatementRequest
+type TxRef is Data:
+  SAuto{}        # unset: the statement is auto-committed
+  STx{tx: Nat}   # set: the statement runs inside transaction tx
+
+# one client request, by Flight SQL action or command
+type Act is Data:
+  ABeginTx{}                       # DoAction BeginTransaction
+  ABeginSp{tx: Nat}                # DoAction BeginSavepoint{transaction_id}
+  AEndTx{tx: Nat, how: EndTx}      # DoAction EndTransaction{transaction_id, action}
+  AEndSp{sp: Nat, how: EndSp}      # DoAction EndSavepoint{savepoint_id, action}
+  AStmt{ref: TxRef}                # GetFlightInfo / DoPut of a statement
+
+# the server's answer
+type Resp is Data:
+  RId{id: Nat}    # ActionBeginTransactionResult / ActionBeginSavepointResult
+  RDone{}         # completed: no body for End*, a FlightInfo for a statement
+  RErr{}          # an error status
+
+# a live savepoint and the transaction it belongs to
+type Sp is Data:
+  Sp{id: Nat, tx: Nat}
+
+# server state: live transactions, live savepoints, the next id to issue
+type Server is Data:
+  Server{txs: List<&2, Nat>, sps: List<&2, Sp>, next: Nat}
+
+# List helpers on transaction ids
+# -------------------------------
+
+# keep x unless drop
+def put(x: Nat, r: List<&2, Nat>, drop: Bool) -> List<&2, Nat>:
+  match drop:
+    case True{}:
+      r
+    case False{}:
+      x <> r
+
+# xs without every occurrence of h
+def remove(+h: Nat, xs: List<&2, Nat>) -> List<&2, Nat>:
+  match xs:
+    case Nil{}:
+      Nil{}
+    case Con{+x, t}:
+      put(x, remove(h, t), Nat.is_eq(x, h))
+
+# whether h occurs in xs
+def has(+h: Nat, xs: List<&2, Nat>) -> Bool:
+  match xs:
+    case Nil{}:
+      False{}
+    case x <> t:
+      Nat.is_eq(x, h) || has(h, t)
+
+# List helpers on savepoints
+# --------------------------
+
+# which savepoints an EndTransaction or EndSavepoint invalidates
+type Pred is Data:
+  OfTx{tx: Nat}               # every savepoint of transaction tx
+  AfterIn{sp: Nat, tx: Nat}   # the savepoints of tx created after sp
+  IsId{sp: Nat}               # the savepoint sp itself
+
+# whether the savepoint Sp{id, tx} is selected by p
+def hit(p: Pred, +id: Nat, +tx: Nat) -> Bool:
+  match p:
+    case OfTx{t}:
+      Nat.is_eq(tx, t)
+    case AfterIn{s, t}:
+      Nat.is_eq(tx, t) && Nat.is_lt(s, id)
+    case IsId{s}:
+      Nat.is_eq(id, s)
+
+# keep x unless drop
+def put_sp(x: Sp, r: List<&2, Sp>, drop: Bool) -> List<&2, Sp>:
+  match drop:
+    case True{}:
+      r
+    case False{}:
+      x <> r
+
+# sps without the savepoints selected by p
+def cut(+p: Pred, sps: List<&2, Sp>) -> List<&2, Sp>:
+  match sps:
+    case Nil{}:
+      Nil{}
+    case Con{Sp{+id, +tx}, t}:
+      put_sp(Sp{id, tx}, cut(p, t), hit(p, id, tx))
+
+# the first of two candidates when found
+def found(tx: Nat, r: Maybe<&2, Nat>, c: Bool) -> Maybe<&2, Nat>:
+  match c:
+    case True{}:
+      Some{tx}
+    case False{}:
+      r
+
+# the transaction that live savepoint s belongs to, if s is live
+def owner(+s: Nat, sps: List<&2, Sp>) -> Maybe<&2, Nat>:
+  match sps:
+    case Nil{}:
+      None{}
+    case Con{Sp{+id, tx}, t}:
+      found(tx, owner(s, t), Nat.is_eq(s, id))
+
+# Transitions
+# -----------
+
+# BeginSavepoint: inside a live transaction, issue the counter as the
+# savepoint id and record it as the newest savepoint of t; else Err
+def begin_sp(+t: Nat, txs: List<&2, Nat>, sps: List<&2, Sp>, +next: Nat, ok: Bool) -> Server & Resp:
+  match ok:
+    case True{}:
+      (Server{txs, Sp{next, t} <> sps, 1n+next}, RId{next})
+    case False{}:
+      (Server{txs, sps, next}, RErr{})
+
+# EndTransaction: on a live transaction, retire it and every savepoint
+# it owns; commit and rollback are the same transition of the
+# lifecycle (what happens to the data is outside this model); else Err
+def end_tx(+t: Nat, txs: List<&2, Nat>, sps: List<&2, Sp>, next: Nat, ok: Bool) -> Server & Resp:
+  match ok:
+    case True{}:
+      (Server{remove(t, txs), cut(OfTx{t}, sps), next}, RDone{})
+    case False{}:
+      (Server{txs, sps, next}, RErr{})
+
+# what EndSavepoint on savepoint s of transaction t invalidates:
+# release invalidates s itself, rollback invalidates the savepoints of
+# t created after s and keeps s
+def end_sp.go(+s: Nat, how: EndSp, t: Nat, sps: List<&2, Sp>) -> List<&2, Sp>:
+  match how:
+    case SRelease{}:
+      cut(IsId{s}, sps)
+    case SRollback{}:
+      cut(AfterIn{s, t}, sps)
+
+# EndSavepoint: on a live savepoint, apply how to its transaction's
+# savepoints; the transactions are untouched; else Err
+def end_sp(+s: Nat, how: EndSp, txs: List<&2, Nat>, sps: List<&2, Sp>, next: Nat, o: Maybe<&2, Nat>) -> Server & Resp:
+  match o:
+    case None{}:
+      (Server{txs, sps, next}, RErr{})
+    case Some{t}:
+      (Server{txs, end_sp.go(s, how, t, sps), next}, RDone{})
+
+# a statement inside a transaction: runs when the transaction is live
+def stmt(txs: List<&2, Nat>, sps: List<&2, Sp>, next: Nat, ok: Bool) -> Server & Resp:
+  match ok:
+    case True{}:
+      (Server{txs, sps, next}, RDone{})
+    case False{}:
+      (Server{txs, sps, next}, RErr{})
+
+# a statement with or without a transaction_id; auto-commit always runs
+def stmt_ref(ref: TxRef, +txs: List<&2, Nat>, sps: List<&2, Sp>, next: Nat) -> Server & Resp:
+  match ref:
+    case SAuto{}:
+      (Server{txs, sps, next}, RDone{})
+    case STx{+t}:
+      stmt(txs, sps, next, has(t, txs))
+
+# one request against one state
+def step(a: Act, +txs: List<&2, Nat>, +sps: List<&2, Sp>, +next: Nat) -> Server & Resp:
+  match a:
+    case ABeginTx{}:
+      (Server{next <> txs, sps, 1n+next}, RId{next})
+    case ABeginSp{+t}:
+      begin_sp(t, txs, sps, next, has(t, txs))
+    case AEndTx{+t, how}:
+      end_tx(t, txs, sps, next, has(t, txs))
+    case AEndSp{+s, how}:
+      end_sp(s, how, txs, sps, next, owner(s, sps))
+    case AStmt{ref}:
+      stmt_ref(ref, txs, sps, next)
+
+# projections of a step
+def state(sr: Server & Resp) -> Server:
+  (s, r) = sr
+  s
+
+def resp(sr: Server & Resp) -> Resp:
+  (s, r) = sr
+  r
+
+def txs_of(s: Server) -> List<&2, Nat>:
+  Server{txs, sps, next} = s
+  txs
+
+def sps_of(s: Server) -> List<&2, Sp>:
+  Server{txs, sps, next} = s
+  sps
+
+# a request against a whole server
+def step_s(a: Act, s: Server) -> Server & Resp:
+  Server{txs, sps, next} = s
+  step(a, txs, sps, next)
+
+def start() -> Server:
+  Server{Nil{}, Nil{}, 0n}
+
+# a whole trace, collecting every response (newest first); the step
+# result arrives as a parameter, since a computed pair cannot be
+# destructured in place
+def run.go(sr: Server & Resp, acc: List<&2, Resp>, rec: Server -> List<&2, Resp> -> List<&2, Resp>) -> List<&2, Resp>:
+  (s, r) = sr
+  rec(s, r <> acc)
+
+def run(acts: List<Act>) -> Server -> List<&2, Resp> -> List<&2, Resp>:
+  match acts:
+    case Nil{}:
+      s => acc => acc
+    case a <> rest:
+      s => acc => run.go(step_s(a, s), acc, run(rest))
+
+# the responses of a trace from the initial state, in order
+def replay(acts: List<Act>) -> List<&2, Resp>:
+  List.reverse(&2, Resp, run(acts)(start(), Nil{}))
+
+# Show
+# ----
+
+def Resp.show(r: Resp) -> String:
+  match r:
+    case RId{id}:
+      "Id(" ++ Nat.show(id) ++ ")"
+    case RDone{}:
+      "Done"
+    case RErr{}:
+      "Err"
+
+# The trace: begin transaction 0; savepoints 1 and 2 in it; roll back
+# to 1 (retires 2); release 2: Err; a statement in 0: Done; commit 0;
+# a statement in 0: Err; release 1: Err; an auto-commit statement: Done.
+#   [Id(0), Id(1), Id(2), Done, Err, Done, Done, Err, Err, Done]
+def main() -> IO(Unit):
+  IO.print(List.show(~&2, ~Resp, ~Resp.show, replay([
+    ABeginTx{},
+    ABeginSp{0n},
+    ABeginSp{0n},
+    AEndSp{1n, SRollback{}},
+    AEndSp{2n, SRelease{}},
+    AStmt{STx{0n}},
+    AEndTx{0n, TCommit{}},
+    AStmt{STx{0n}},
+    AEndSp{1n, SRelease{}},
+    AStmt{SAuto{}}])))