diff --git a/Test.lean b/Test.lean
new file mode 100644
index 0000000..7862fd2
--- /dev/null
+++ b/Test.lean
@@ -0,0 +1,10 @@
+module  -- shake: keep-all --deprecated_module: ignore
+
+public import Test.Bind
+public import Test.Common
+public import Test.Control
+public import Test.Gaps
+public import Test.Instances
+public import Test.IsMarkov
+public import Test.Loops
+public import Test.MonadLaws
diff --git a/Test/Bind.lean b/Test/Bind.lean
new file mode 100644
index 0000000..25ca20c
--- /dev/null
+++ b/Test/Bind.lean
@@ -0,0 +1,84 @@
+module
+
+public import Test.Common
+
+set_option linter.style.header false
+
+/-!
+# `rdo`: binding, sequencing and `return`
+
+`rdo` elaborates to `MeasurableSpacePure.mPure` and `MeasurableSpaceBind.mBind` rather than to
+`pure` and `bind`, so every shape a `do` block can take has to be re-checked here.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+@[expose] public section
+
+namespace Test.Bind
+
+/-- A single bind. -/
+def one (xs : List ℕ) : IdM ℕ := rdo
+  let x ← (xs.headD 0 : IdM ℕ)
+  return x + 1
+
+example : IdM.run (one [4, 5]) = 5 := rfl
+
+/-- A chain of binds. -/
+def chain (a b : ℕ) : IdM ℕ := rdo
+  let x ← (a : IdM ℕ)
+  let y ← (b : IdM ℕ)
+  return x * y
+
+example : IdM.run (chain 6 7) = 42 := rfl
+
+/-- `←` nested inside a larger expression is lifted out of it. -/
+def nested (a b : ℕ) : IdM ℕ := rdo
+  return (← (a : IdM ℕ)) + (← (b : IdM ℕ)) * 2
+
+example : IdM.run (nested 3 4) = 11 := rfl
+
+/-- A pure `let`, and a `have`, alongside the monadic ones. -/
+def mixedLets (a : ℕ) : IdM ℕ := rdo
+  let x ← (a : IdM ℕ)
+  let y := x + 1
+  have : 0 < y + 1 := Nat.succ_pos y
+  return y * 2
+
+example : IdM.run (mixedLets 5) = 12 := rfl
+
+/-- Destructuring a bound pair. -/
+def destructure (p : ℕ × ℕ) : IdM ℕ := rdo
+  let (a, b) ← (p : IdM (ℕ × ℕ))
+  return a + b
+
+example : IdM.run (destructure (3, 4)) = 7 := rfl
+
+/-- A statement in the middle of a block is sequenced, not dropped. -/
+def sequenced (a : ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  (pure () : IdM PUnit)
+  s := s + a
+  return s
+
+example : IdM.run (sequenced 9) = 9 := rfl
+
+/-- `return` in straight-line code drops the rest of the block. -/
+def earlyReturn (a : ℕ) : IdM ℕ := rdo
+  if a = 0 then
+    return 100
+  return a
+
+example : IdM.run (earlyReturn 0) = 100 := rfl
+
+example : IdM.run (earlyReturn 7) = 7 := rfl
+
+/-- The same shapes at `Measure`, where the binds are genuine integrals. -/
+noncomputable def twoCoins : Measure Bool := rdo
+  let x ← fairCoin
+  let y ← fairCoin
+  return x && y
+
+end Test.Bind
+
+end
diff --git a/Test/Common.lean b/Test/Common.lean
new file mode 100644
index 0000000..d3b23f4
--- /dev/null
+++ b/Test/Common.lean
@@ -0,0 +1,40 @@
+module
+
+public import RandomDo
+
+set_option linter.style.header false
+
+/-!
+# Shared scaffolding for the `rdo` test suite
+
+The files in this library exercise the features of `rdo` that are currently implemented. They are
+`module` files, like the library they test.
+
+Where a program reduces, a test states the value it computes rather than only that it elaborates.
+One family does not reduce here: a `for` loop over several collections streams the ones past
+the first through `Std.Stream`, and for an `Array` or a `Vector` that goes through the
+`Array → Subarray` conversion, which core marks `@[no_expose]`. Those are checked by elaborating.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+@[expose] public section
+
+universe u
+
+/-- A deterministic `MeasurableSpaceMonad`. An `rdo` program written at `IdM` denotes a value, so
+the tests can state what a program computes and not merely that it typechecks. -/
+abbrev IdM := Monad.toMeasurableSpaceMonad Id
+
+/-- Read the value out of a deterministic `rdo` program. `IdM α` is definitionally `α` but not
+reducibly so, which is what otherwise stops numerals and `rfl` from seeing through it. -/
+def IdM.run {α : Type u} [MeasurableSpace α] (x : IdM α) : α := x
+
+/-- The fair coin, as a probability measure on `Bool`. -/
+noncomputable def fairCoin : Measure Bool := bernoulliMeasure true false ⟨(1 : ℝ) / 2, by norm_num⟩
+
+instance : IsProbabilityMeasure fairCoin := by
+  unfold fairCoin
+  infer_instance
+
+end
diff --git a/Test/Control.lean b/Test/Control.lean
new file mode 100644
index 0000000..a6b3069
--- /dev/null
+++ b/Test/Control.lean
@@ -0,0 +1,122 @@
+module
+
+public import Test.Common
+
+set_option linter.style.header false
+
+/-!
+# `rdo`: branching
+
+Every branching `do` element goes through core's elaborators, which build the block out of the
+`DoOps` that `rdo` supplies. Each shape is checked here to make sure the substituted `mPure` and
+`mBind` reach it.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+@[expose] public section
+
+namespace Test.Control
+
+/-- `if … then … else`, branching the whole rest of the block. -/
+def branch (n : ℕ) : IdM ℕ := rdo
+  if n = 0 then
+    return 100
+  else
+    return n
+
+example : IdM.run (branch 0) = 100 := rfl
+
+example : IdM.run (branch 5) = 5 := rfl
+
+/-- `if` with no `else`: the block carries on afterwards. -/
+def clampZero (n : ℕ) : IdM ℕ := rdo
+  let mut s := n
+  if n = 0 then
+    s := 100
+  return s
+
+example : IdM.run (clampZero 0) = 100 := rfl
+
+example : IdM.run (clampZero 5) = 5 := rfl
+
+/-- Nested branches. -/
+def nestedIf (a b : ℕ) : IdM ℕ := rdo
+  if a = 0 then
+    if b = 0 then
+      return 0
+    else
+      return 1
+  else
+    return 2
+
+example : IdM.run (nestedIf 0 0) = 0 := rfl
+
+example : IdM.run (nestedIf 0 1) = 1 := rfl
+
+example : IdM.run (nestedIf 1 0) = 2 := rfl
+
+/-- A dependent `if`, whose branch uses the proof it introduces. -/
+def headOr (xs : List ℕ) : IdM ℕ := rdo
+  if h : 0 < xs.length then
+    return xs[0]'h
+  else
+    return 0
+
+example : IdM.run (headOr [7, 8]) = 7 := rfl
+
+example : IdM.run (headOr []) = 0 := rfl
+
+/-- A `match` on a value bound by `←`. -/
+def matchArrow (o : Option ℕ) : IdM ℕ := rdo
+  match ← (o : IdM (Option ℕ)) with
+  | none => return 0
+  | some n => return n + 1
+
+example : IdM.run (matchArrow (some 4)) = 5 := rfl
+
+example : IdM.run (matchArrow none) = 0 := rfl
+
+/-- A pure `match` inside the block. -/
+def matchPure (o : Option ℕ) : IdM ℕ := rdo
+  let v ← (o : IdM (Option ℕ))
+  match v with
+  | none => return 0
+  | some n => return n + 1
+
+example : IdM.run (matchPure (some 4)) = 5 := rfl
+
+/-- `if let`. -/
+def ifLet (o : Option ℕ) : IdM ℕ := rdo
+  let v ← (o : IdM (Option ℕ))
+  if let some n := v then
+    return n + 1
+  else
+    return 0
+
+example : IdM.run (ifLet (some 4)) = 5 := rfl
+
+example : IdM.run (ifLet none) = 0 := rfl
+
+/-- `unless`. -/
+def unlessFlag (b : Bool) : IdM ℕ := rdo
+  let mut s := 0
+  unless b do
+    s := 1
+  return s
+
+example : IdM.run (unlessFlag true) = 0 := rfl
+
+example : IdM.run (unlessFlag false) = 1 := rfl
+
+/-- Branching on a value drawn from a genuine distribution. -/
+noncomputable def fairCoinBranch : Measure ℕ := rdo
+  let b ← fairCoin
+  if b then
+    return 1
+  else
+    return 0
+
+end Test.Control
+
+end
diff --git a/Test/Gaps.lean b/Test/Gaps.lean
new file mode 100644
index 0000000..09b1b72
--- /dev/null
+++ b/Test/Gaps.lean
@@ -0,0 +1,166 @@
+module
+
+public import Test.Common
+
+set_option linter.style.header false
+
+/-!
+# `rdo`: known gaps, with their current behaviour pinned
+
+Each test below is a program `rdo` does *not* handle. The message it currently produces is pinned
+with `#guard_msgs`, so that closing a gap makes the corresponding test fail and forces this file to
+be revisited, rather than letting a gap close unnoticed.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+@[expose] public section
+
+namespace Test.Gaps
+
+/-! ## `for` over several collections
+
+TODO: the expander at `RandomDo/Monad/Notation.lean:141` wraps the loop body in a fresh term-level
+`rdo` block, which severs it from the block around it. Emitting `do $body` instead — a nested
+`doElem`, which is what core's otherwise identical expander does — fixes all three tests below.
+-/
+
+/--
+error: Variable `s` cannot be mutated. Only variables declared using `let mut` can be mutated.
+      If you did not intend to mutate but define `s`, consider using `let s` instead
+-/
+#guard_msgs in
+def zipMut (xs ys : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs, y in ys rdo
+    s := s + x * y
+  return s
+
+/--
+error: Type mismatch
+  some x
+has type
+  Option ℕ
+but is expected to have type
+  Unit
+-/
+#guard_msgs in
+def zipReturn (xs ys : List ℕ) : IdM (Option ℕ) := rdo
+  for x in xs, y in ys rdo
+    if x = y then
+      return some x
+  return none
+
+/-- error: `break` must be nested inside a loop -/
+#guard_msgs in
+def zipThree (xs ys zs : List ℕ) : IdM Bool := rdo
+  for x in xs, y in ys, z in zs rdo
+    if x + y = z then
+      return true
+  return false
+
+/-! ## Nested loops
+
+TODO: register a `ControlInfo` inference handler for `RDo.rdoFor`, mirroring the rule core states
+inline for `doFor` in `Lean/Elab/Do/InferControlInfo.lean`.
+-/
+
+/--
+error: No `ControlInfo` inference handler found for `RDo.rdoFor` in syntax
+  for y in ys rdo
+    s := s + x * y
+Register a handler with `@[doElem_control_info RDo.rdoFor]`.
+-/
+#guard_msgs (whitespace := lax) in
+def nestedLoops (xs ys : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    for y in ys rdo
+      s := s + x * y
+  return s
+
+/-! ## Unbounded and conditional iteration
+
+TODO: `while`, `repeat` and `repeat … until` all expand to `for _ in Loop.mk do …`, which reaches
+core's `doFor` and so asks for a `ForIn` instance. Supporting them needs the macros re-pointed at
+`rdoFor` and, at `Measure`, a denotation for an iteration that need not terminate.
+-/
+
+/--
+error: failed to synthesize instance of type class
+  ForIn IdM Lean.Loop ?α
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+-/
+#guard_msgs in
+def whileLoop : IdM ℕ := rdo
+  let mut i := 0
+  while i < 3 do
+    i := i + 1
+  return i
+
+/-! ## Exceptions
+
+TODO: needs a `MeasurableSpaceMonadExcept` class; `try`/`catch` elaborates against `MonadExcept`.
+-/
+
+/--
+error: failed to synthesize instance of type class
+  MeasurableSpace (Except Bool Bool)
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+-/
+#guard_msgs in
+noncomputable def tryCatch : Measure Bool := rdo
+  try
+    let x ← fairCoin
+    return x
+  catch _ =>
+    return false
+
+/-! ## Collections with no `MeasurableSpaceForIn` instance
+
+TODO: instances exist for `List`, `Array` and `Vector` only. A range is the one most missed, since
+`for i in [0:n]` has to be written `for i in List.range n` today.
+-/
+
+/--
+error: failed to synthesize instance of type class
+  MeasurableSpaceForIn IdM Std.Legacy.Range ?α
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+-/
+#guard_msgs in
+def overRange : IdM ℕ := rdo
+  let mut s := 0
+  for _ in [0:3] rdo
+    s := s + 1
+  return s
+
+/--
+error: failed to synthesize instance of type class
+  MeasurableSpaceForIn IdM (Finset ℕ) ?α
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+-/
+#guard_msgs in
+def overFinset : IdM ℕ := rdo
+  let mut s := 0
+  for _ in Finset.range 3 rdo
+    s := s + 1
+  return s
+
+/-! ## No `Functor`, `Applicative` or `Monad` structure
+
+A measurable-space monad is not a monad on `Type`, which is the whole reason `rdo` exists. The
+consequence inside a block is that core's operators — `<$>`, `<*>`, `<|>` — are unavailable; only
+`<$>ₘ` and `>>=ₘ` are. TODO: an `mMap`-aware notation could recover `<$>`.
+
+This one is not pinned: `Measure` does not even have the arity `Functor` expects, so the message
+is an application type mismatch carrying universe metavariable numbers, which would churn on every
+toolchain bump for no benefit.
+-/
+
+end Test.Gaps
+
+end
diff --git a/Test/Instances.lean b/Test/Instances.lean
new file mode 100644
index 0000000..1105bdb
--- /dev/null
+++ b/Test/Instances.lean
@@ -0,0 +1,83 @@
+module
+
+public import Test.Common
+
+set_option linter.style.header false
+
+/-!
+# `rdo`: the monad instances, and programs polymorphic over them
+
+The point of `MeasurableSpaceMonad` is that one `rdo` program can be read both as a distribution
+and as a sampler. These tests write a program once and interpret it at each instance the library
+provides.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+@[expose] public section
+
+namespace Test.Instances
+
+universe u
+
+/-! ## What `rdo` elaborates to at `Measure` -/
+
+example {α : Type} [MeasurableSpace α] (a : α) :
+    (MeasurableSpacePure.mPure a : Measure α) = Measure.dirac a := rfl
+
+example {α β : Type} [MeasurableSpace α] [MeasurableSpace β]
+    (μ : Measure α) (f : α → Measure β) : μ >>=ₘ f = μ.bind f := rfl
+
+/-- An `rdo` program is the explicit `bind`/`dirac` term one would write by hand. -/
+noncomputable def flip : Measure Bool := rdo
+  let x ← fairCoin
+  return !x
+
+example : flip = fairCoin.bind (fun x ↦ Measure.dirac (!x)) := rfl
+
+/-! ## One program, several interpretations -/
+
+variable {m : (α : Type) → [MeasurableSpace α] → Type u} [MeasurableSpaceMonad m]
+
+/-- A program that draws twice from the same source and adds the results. -/
+def twice (x : m ℕ) : m ℕ := rdo
+  let a ← x
+  let b ← x
+  return a + b
+
+/-- At `IdM` it computes. -/
+example : IdM.run (twice ((3 : ℕ) : IdM ℕ)) = 6 := rfl
+
+/-- At `Measure` it denotes a distribution. -/
+noncomputable def twiceCoin : Measure ℕ := twice (m := Measure) (rdo
+  let b ← fairCoin
+  return (if b then 1 else 0))
+
+/-- At `PseudoRandomM` it is an executable sampler. -/
+def twiceRandom : PseudoRandomM ℕ := twice (m := PseudoRandomM) (rdo
+  let b ← Random.randBool
+  return (if b then 1 else 0))
+
+/-- A polymorphic program containing a loop. -/
+def sumOver (xs : List ℕ) (f : ℕ → m ℕ) : m ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    let y ← f x
+    s := s + y
+  return s
+
+example : IdM.run (sumOver [1, 2, 3] (fun x ↦ ((x * 2 : ℕ) : IdM ℕ))) = 12 := rfl
+
+noncomputable def sumOverMeasure : Measure ℕ :=
+  sumOver (m := Measure) [1, 2, 3] (fun x ↦ rdo
+    let b ← fairCoin
+    return (if b then x else 0))
+
+def sumOverRandom : PseudoRandomM ℕ :=
+  sumOver (m := PseudoRandomM) [1, 2, 3] (fun x ↦ rdo
+    let b ← Random.randBool
+    return (if b then x else 0))
+
+end Test.Instances
+
+end
diff --git a/Test/IsMarkov.lean b/Test/IsMarkov.lean
new file mode 100644
index 0000000..a63e188
--- /dev/null
+++ b/Test/IsMarkov.lean
@@ -0,0 +1,116 @@
+module
+
+public import Test.Common
+
+set_option linter.style.header false
+
+/-!
+# The `is_markov` tactic on `rdo` programs
+
+`is_markov` walks an `rdo` program as a tree of constructs, applying a propagation lemma at each
+node. There is one test here per construct it recognises.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+@[expose] public section
+
+namespace Test.IsMarkov
+
+/-! ## `return` -/
+
+noncomputable def shiftBy (c : ℝ) : Measure ℝ := rdo
+  return c + 1
+
+example : IsMarkov shiftBy := by is_markov
+
+/-! ## `let x ← _` -/
+
+noncomputable def sumTwo : Measure ℝ := rdo
+  let x ← gaussianReal 0 1
+  let y ← gaussianReal 0 1
+  return x + y
+
+example : IsProbabilityMeasure sumTwo := by is_markov
+
+/-- A distribution whose parameter is read off the argument. -/
+noncomputable def centred (c : ℝ) : Measure ℝ := rdo
+  let x ← gaussianReal c 1
+  return x
+
+example : IsMarkov centred := by is_markov
+
+/-! ## Reparametrisation -/
+
+example {κ : ℝ → Measure ℝ} [IsMarkov κ] : IsMarkov fun c ↦ κ (c + 1) := by is_markov
+
+/-! ## A constant family -/
+
+example (μ : Measure ℝ) [IsProbabilityMeasure μ] : IsMarkov fun _ : ℝ ↦ μ := by is_markov
+
+/-! ## `if … then … else` between two families -/
+
+noncomputable def branchOn (c : ℝ) : Measure ℝ := rdo
+  if 0 < c then
+    let x ← gaussianReal c 1
+    return x
+  else
+    let x ← gaussianReal 0 1
+    return x
+
+example : IsMarkov branchOn := by is_markov
+
+/-! ## `for` over a fixed collection -/
+
+noncomputable def sumLoop : Measure ℝ := rdo
+  let mut s : ℝ := 0
+  for _ in List.range 3 rdo
+    let x ← gaussianReal 0 1
+    s := s + x
+  return s
+
+example : IsProbabilityMeasure sumLoop := by is_markov
+
+/-! ## `for` with an early `return`, which goes through `Break.runK` -/
+
+noncomputable def firstPositive : Measure ℝ := rdo
+  for _ in List.range 3 rdo
+    let x ← gaussianReal 0 1
+    if 0 < x then
+      return x
+  return 0
+
+example : IsProbabilityMeasure firstPositive := by is_markov
+
+/-! ## `for` over a collection read off the argument -/
+
+noncomputable def overList (xs : List ℝ) : Measure ℝ := rdo
+  let mut s : ℝ := 0
+  for x in xs rdo
+    let z ← gaussianReal (s + x) 1
+    s := z
+  return s
+
+example : IsMarkov overList := by is_markov
+
+/-! ## Looking through definitions, and the `fuel` argument -/
+
+noncomputable def layerOne : Measure ℝ := sumTwo
+
+noncomputable def layerTwo : Measure ℝ := layerOne
+
+example : IsProbabilityMeasure layerTwo := by is_markov
+
+example : IsProbabilityMeasure layerTwo := by is_markov (fuel := 3)
+
+/-! ## The resulting instance is a `Kernel` -/
+
+instance : IsMarkov centred := by is_markov
+
+noncomputable example : Kernel ℝ ℝ := IsMarkov.toKernel centred
+
+example : IsMarkovKernel (IsMarkov.toKernel centred) := inferInstance
+
+end Test.IsMarkov
+
+end
diff --git a/Test/Loops.lean b/Test/Loops.lean
new file mode 100644
index 0000000..ff77c85
--- /dev/null
+++ b/Test/Loops.lean
@@ -0,0 +1,144 @@
+module
+
+public import Test.Common
+
+set_option linter.style.header false
+
+/-!
+# `rdo`: `for` loops over a single collection
+
+`rdo` has its own `for … rdo …` parser, expander and elaborator, mirroring core's but emitting
+`MeasurableSpaceForIn.forIn`. Instances exist for `List`, `Array` and `Vector`.
+
+There is no test for a loop nested inside another: `rdoFor` has no registered `ControlInfo`
+inference handler, so the outer loop cannot work out what the inner one does to the control flow,
+and such a program is rejected before elaboration.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+@[expose] public section
+
+namespace Test.Loops
+
+/-- A loop over a `List`. -/
+def sumList (xs : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    s := s + x
+  return s
+
+example : IdM.run (sumList [1, 2, 3]) = 6 := rfl
+
+example : IdM.run (sumList []) = 0 := rfl
+
+/-- A loop over an `Array`. -/
+def sumArray (xs : Array ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    s := s + x
+  return s
+
+example : IdM.run (sumArray #[1, 2, 3]) = 6 := rfl
+
+/-- A loop over a `Vector`. -/
+def sumVector (xs : Vector ℕ 3) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    s := s + x
+  return s
+
+example : IdM.run (sumVector #v[1, 2, 3]) = 6 := rfl
+
+/-- `for h : x in xs`, which hands the body a proof that `x` is in the collection. -/
+def sumWithProof (xs : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for h : x in xs rdo
+    have : x ∈ xs := h
+    s := s + x
+  return s
+
+example : IdM.run (sumWithProof [1, 2, 3]) = 6 := rfl
+
+/-- Several mutable variables carried through one loop. -/
+def sumAndCount (xs : List ℕ) : IdM (ℕ × ℕ) := rdo
+  let mut s := 0
+  let mut n := 0
+  for x in xs rdo
+    s := s + x
+    n := n + 1
+  return (s, n)
+
+example : IdM.run (sumAndCount [1, 2, 3]) = (6, 3) := rfl
+
+/-- `break`. -/
+def sumUntilZero (xs : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    if x = 0 then
+      break
+    s := s + x
+  return s
+
+example : IdM.run (sumUntilZero [1, 2, 0, 4]) = 3 := rfl
+
+example : IdM.run (sumUntilZero [1, 2, 3]) = 6 := rfl
+
+/-- `continue`. -/
+def sumSkippingZero (xs : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    if x = 0 then
+      continue
+    s := s + x
+  return s
+
+example : IdM.run (sumSkippingZero [1, 0, 3]) = 4 := rfl
+
+/-- An early `return` out of a loop, which elaborates through `Break.runK`. -/
+def firstNonzero (xs : List ℕ) : IdM (Option ℕ) := rdo
+  for x in xs rdo
+    if x ≠ 0 then
+      return some x
+  return none
+
+example : IdM.run (firstNonzero [0, 0, 3, 4]) = some 3 := rfl
+
+example : IdM.run (firstNonzero [0, 0]) = none := rfl
+
+/-- An early `return` from a loop that also carries mutable state. -/
+def runningSumOver (xs : List ℕ) (limit : ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    s := s + x
+    if s > limit then
+      return s
+  return 0
+
+example : IdM.run (runningSumOver [1, 2, 3, 4] 4) = 6 := rfl
+
+example : IdM.run (runningSumOver [1, 2] 100) = 0 := rfl
+
+/-- A loop with no mutable state, whose only effect is an early return. -/
+def containsZero (xs : List ℕ) : IdM Bool := rdo
+  for x in xs rdo
+    if x = 0 then
+      return true
+  return false
+
+example : IdM.run (containsZero [1, 0]) = true := rfl
+
+example : IdM.run (containsZero [1, 2]) = false := rfl
+
+/-- A loop whose body binds monadically, at `Measure`. -/
+noncomputable def countHeads (n : ℕ) : Measure ℕ := rdo
+  let mut c := 0
+  for _ in List.range n rdo
+    let b ← fairCoin
+    if b then
+      c := c + 1
+  return c
+
+end Test.Loops
+
+end
diff --git a/Test/MonadLaws.lean b/Test/MonadLaws.lean
new file mode 100644
index 0000000..7787395
--- /dev/null
+++ b/Test/MonadLaws.lean
@@ -0,0 +1,57 @@
+module
+
+public import Test.Common
+
+set_option linter.style.header false
+
+/-!
+# The `MeasurableSpaceMonad` laws at `Measure`
+
+`Measure` is the one `LawfulMeasurableSpaceMonad` instance the library provides. Each law is
+guarded by measurability hypotheses, which is what makes the Giry monad fit the class at all, so
+these tests also record the exact shape each law is stated in.
+-/
+
+open MeasureTheory ProbabilityTheory MeasurableSpacePure MeasurableSpaceBind
+  MeasurableSpaceFunctor
+
+@[expose] public section
+
+namespace Test.MonadLaws
+
+variable {α β γ : Type} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
+
+example (a : α) {f : α → Measure β} (hf : Measurable f) : (mPure a : Measure α) >>=ₘ f = f a :=
+  LawfulMeasurableSpaceMonad.mPure_mBind a hf
+
+example (μ : Measure α) : μ >>=ₘ mPure = μ := mBind_mPure μ
+
+example (μ : Measure α) {f : α → Measure β} {g : β → Measure γ}
+    (hf : Measurable f) (hg : Measurable g) :
+    μ >>=ₘ f >>=ₘ g = μ >>=ₘ fun a ↦ f a >>=ₘ g :=
+  LawfulMeasurableSpaceMonad.mBind_assoc μ hf hg
+
+example {f : α → β} (hf : Measurable f) (μ : Measure α) :
+    μ >>=ₘ (fun a ↦ mPure (f a)) = f <$>ₘ μ :=
+  LawfulMeasurableSpaceMonad.mBind_mPure_comp hf μ
+
+example {f : α → β} (hf : Measurable f) (a : α) :
+    f <$>ₘ (mPure a : Measure α) = mPure (f a) := mMap_mPure hf a
+
+example (μ : Measure α) : id <$>ₘ μ = μ := LawfulMeasurableSpaceFunctor.id_mMap μ
+
+example (μ : Measure α) : (fun a ↦ a) <$>ₘ μ = μ := id_mMap' μ
+
+example {f : α → β} (hf : Measurable f) (μ : Measure α) :
+    f <$>ₘ μ = μ >>=ₘ fun a ↦ mPure (f a) := mMap_eq_mPure_mBind hf μ
+
+/-! `mPure` and `mBind` are themselves measurable, which is what lets the laws compose. -/
+
+example : Measurable (mPure : α → Measure α) := LawfulMeasurableSpaceMonad.measurable_mPure
+
+example {f : α → Measure β} (hf : Measurable f) : Measurable fun μ : Measure α ↦ μ >>=ₘ f :=
+  LawfulMeasurableSpaceMonad.measurable_mBind hf
+
+end Test.MonadLaws
+
+end
diff --git a/lakefile.toml b/lakefile.toml
index a820c99..0fdcde8 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,5 +1,5 @@
 name = "RandomDo"
-defaultTargets = ["RandomDo"]
+defaultTargets = ["RandomDo", "Test"]
 lintDriver = "batteries/runLinter"
 
 [leanOptions]
@@ -15,3 +15,6 @@ rev = "main"
 
 [[lean_lib]]
 name = "RandomDo"
+
+[[lean_lib]]
+name = "Test"