diff --git a/RandomDo.lean b/RandomDo.lean
index b2d4043..e781baa 100644
--- a/RandomDo.lean
+++ b/RandomDo.lean
@@ -1,11 +1,14 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
 public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Embedding
+public import RandomDo.ForMathlib.MeasureTheory.Measure.GiryMonad
+public import RandomDo.ForMathlib.Probability.Distributions.Bernoulli
 public import RandomDo.Measurable
 public import RandomDo.Monad.ForInInstances
 public import RandomDo.Monad.Instances
 public import RandomDo.Monad.MeasurableSpace
 public import RandomDo.Monad.Notation
+public import RandomDo.Monad.While
 public import RandomDo.NumLean.Binomial
 public import RandomDo.NumLean.Distributions
 public import RandomDo.NumLean.PCG64
@@ -23,3 +26,6 @@ public import RandomDo.Tactic.IsMarkov.Deriving
 public import RandomDo.Tactic.IsMarkov.Elab
 public import RandomDo.Tactic.IsMarkov.ForInStep
 public import RandomDo.Tactic.IsMarkov.Lemmas
+public import RandomDo.Tactic.IsMarkov.While.LoopInvariant
+public import RandomDo.Tactic.IsMarkov.While.Tactic
+public import RandomDo.Tactic.IsMarkov.While.Termination
diff --git a/RandomDo/ForMathlib/MeasureTheory/Measure/GiryMonad.lean b/RandomDo/ForMathlib/MeasureTheory/Measure/GiryMonad.lean
new file mode 100644
index 0000000..e586aa6
--- /dev/null
+++ b/RandomDo/ForMathlib/MeasureTheory/Measure/GiryMonad.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+public import Mathlib.MeasureTheory.Measure.GiryMonad
+
+/-!
+# The bind of a sum of two measures, and of a Dirac mass
+
+-/
+
+@[expose] public section
+
+open MeasureTheory
+
+namespace MeasureTheory.Measure
+
+variable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
+
+theorem bind_add {μ ν : Measure α} {f : α → Measure β} (hf : AEMeasurable f (μ + ν)) :
+    (μ + ν).bind f = μ.bind f + ν.bind f := by
+  obtain ⟨hμ, hν⟩ := aemeasurable_add_measure_iff.1 hf
+  ext s hs
+  rw [add_apply, bind_apply hs hf, bind_apply hs hμ, bind_apply hs hν, lintegral_add_measure]
+
+/-- Binding a Dirac mass at a point of a space whose points are measurable: the continuation needs
+no measurability. -/
+@[simp]
+theorem dirac_bind' [MeasurableSingletonClass α] (a : α) (f : α → Measure β) :
+    (dirac a).bind f = f a := by
+  rw [Measure.bind, map_congr (ae_eq_dirac f)]
+  change (map (fun _ ↦ f a) (dirac a)).join = f a
+  rw [map_const]
+  simp
+
+end MeasureTheory.Measure
diff --git a/RandomDo/ForMathlib/Probability/Distributions/Bernoulli.lean b/RandomDo/ForMathlib/Probability/Distributions/Bernoulli.lean
new file mode 100644
index 0000000..22bd818
--- /dev/null
+++ b/RandomDo/ForMathlib/Probability/Distributions/Bernoulli.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+public import Mathlib.Probability.Distributions.Bernoulli
+public import RandomDo.ForMathlib.MeasureTheory.Measure.GiryMonad
+
+/-!
+# Binding a Bernoulli distribution
+
+-/
+
+@[expose] public section
+
+open MeasureTheory Measure unitInterval
+open scoped ENNReal
+
+namespace ProbabilityTheory
+
+variable {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
+
+/-- Binding a Bernoulli distribution on a space whose points are measurable: the continuation needs
+no measurability, and the two weights are real numbers, so that `simp` can use it and `norm_num`
+can compute with the result. -/
+@[simp]
+lemma bernoulliMeasure_bind [MeasurableSingletonClass X] (x y : X) (p : I) (g : X → Measure Y) :
+    Ber(x, y, p).bind g = ENNReal.ofReal p • g x + ENNReal.ofReal (1 - p) • g y := by
+  have h (q : I) : ((toNNReal q : NNReal) : ℝ≥0∞) = ENNReal.ofReal q := by
+    rw [ENNReal.ofReal, Real.toNNReal_of_nonneg q.2.1]
+    rfl
+  rw [bernoulliMeasure_def, bind_add ((aemeasurable_dirac.smul_measure _).add_measure
+    (aemeasurable_dirac.smul_measure _)), bind_smul, bind_smul, dirac_bind', dirac_bind']
+  change (toNNReal p : ℝ≥0∞) • g x + (toNNReal (σ p) : ℝ≥0∞) • g y = _
+  rw [h, h, coe_symm_eq]
+
+end ProbabilityTheory
diff --git a/RandomDo/Monad/Notation.lean b/RandomDo/Monad/Notation.lean
index 2d2542b..7bd48ec 100644
--- a/RandomDo/Monad/Notation.lean
+++ b/RandomDo/Monad/Notation.lean
@@ -260,6 +260,22 @@ def rdoForDecl := leading_parser
           dec.continueWithUnit
   mkBindApp σ γ forIn rest
 
+/-- parser for `rdo` while loops -/
+@[doElem_parser] def rdoWhile := leading_parser
+  "while " >> withForbidden "rdo" doIfCond >> " rdo " >> doSeq
+
+/-- Define expander for `while` loops in `rdo` notation. As in core, `while c rdo body` is a loop
+over `Loop.mk` that runs `body` while `c` holds and breaks otherwise. -/
+@[macro rdoWhile] def expandRDoWhile : Macro
+  | `(rdoWhile| while%$tk $cond:doIfCond rdo $body) =>
+    `(doElem| for%$tk _ in Lean.Loop.mk rdo if $cond:doIfCond then $body else break)
+  | _ => Macro.throwUnsupported
+
+/-- Infer the `ControlInfo` of an `rdo` loop as that of the core `for` loop with the same body. -/
+@[doElem_control_info rdoFor] def controlInfoRDoFor : ControlInfoHandler := fun stx => do
+  let `(rdoFor| for $_:rdoForDecl,* rdo $body) := stx | throwUnsupportedSyntax
+  inferControlInfoElem (← `(doElem| for _ in #[()] do $body))
+
 end LoopElab
 
 end RDo
diff --git a/RandomDo/Monad/While.lean b/RandomDo/Monad/While.lean
new file mode 100644
index 0000000..e75f67a
--- /dev/null
+++ b/RandomDo/Monad/While.lean
@@ -0,0 +1,290 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+public import RandomDo.Monad.Instances
+public import RandomDo.Tactic.IsMarkov.Defs
+import RandomDo.Monad.Notation
+
+/-!
+# `while` loops
+
+`while c rdo body` runs `body` for as long as `c` holds, each step returning `yield b` to carry on
+from `b` or `done b` to stop there. Such a loop need not terminate, so each monad gives its own
+meaning to it through the class `MeasurableSpaceMonadWhile`: core's loop at a core monad, and at
+`Measure` the least fixed point of "one step, then stop or run the loop again", the sum over `n` of
+the runs that stop at the `n + 1`-th step (`loopExit`). The runs that never stop carry no mass, and
+the loop is a probability measure exactly when the runs still going after `n` steps (`loopRun`) have
+a mass that tends to `0` (`Terminates`).
+
+## Implementation notes
+
+The loop could instead be a field of `MeasurableSpaceMonad`, at the price of asking every measurable
+space monad for its own implementation. It is not defined by `partial_fixpoint`, which needs the
+step to be monotone in the loop over every family `β → Measure β`: this fails for `Measure.bind`,
+which is `0` as soon as its continuation is not measurable.
+
+## References
+
+* Dexter Kozen, *Semantics of probabilistic programs*, 1981.
+-/
+
+@[expose] public section
+
+universe u v
+
+open MeasureTheory MeasurableSpacePure MeasurableSpaceBind
+
+/-- A measurable space monad with an unbounded loop, the one behind `while … rdo`. -/
+class MeasurableSpaceMonadWhile (m : (α : Type u) → [MeasurableSpace α] → Type v) where
+  /-- Run the step `f` from `b`, then from each state it carries on with, until it stops. -/
+  loop {β : Type u} [MeasurableSpace β] (f : β → m (ForInStep β)) (b : β) : m β
+
+namespace MeasurableSpaceMonadWhile
+
+/-- At a core monad, the loop is core's loop over `Lean.Loop`. -/
+instance {m : Type u → Type v} [Monad m] :
+    MeasurableSpaceMonadWhile (Monad.toMeasurableSpaceMonad m) where
+  loop f b := ForIn.forIn (m := m) Lean.Loop.mk b fun _ ↦ f
+
+section Runs
+
+variable {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m]
+  {β : Type u} [MeasurableSpace β] [Zero (m β)]
+
+/-- The runs of the loop whose step is `f` that, from `b`, stop at the `n + 1`-th step. A run that
+does not stop there contributes `0`. -/
+def loopExit (f : β → m (ForInStep β)) : ℕ → β → m β
+  -- One step from `b`: keep the runs that stop there, drop the ones that carry on.
+  | 0, b => f b >>=ₘ fun s ↦ ForInStep.casesOn (motive := fun _ ↦ m β) s mPure fun _ ↦ 0
+  -- One step from `b`: drop the runs that stop there, keep those that stop `n + 1` steps later.
+  | n + 1, b => f b >>=ₘ fun s ↦
+      ForInStep.casesOn (motive := fun _ ↦ m β) s (fun _ ↦ 0) (loopExit f n)
+
+/-- The runs of the loop whose step is `f` that, from `b`, have not stopped after `n` steps, at the
+state they are in. A run that has stopped contributes `0`. -/
+def loopRun (f : β → m (ForInStep β)) : ℕ → β → m β
+  -- No step yet: the run is at `b`.
+  | 0, b => mPure b
+  -- One step from `b`: drop the runs that stop there, keep those still going `n` steps later.
+  | n + 1, b => f b >>=ₘ fun s ↦
+      ForInStep.casesOn (motive := fun _ ↦ m β) s (fun _ ↦ 0) (loopRun f n)
+
+end Runs
+
+/-- At `Measure`, the loop is the least fixed point of "one step, then stop or run the loop again":
+the sum over `n` of the runs that stop at the `n + 1`-th step. -/
+noncomputable instance : MeasurableSpaceMonadWhile Measure where
+  loop f b := Measure.sum fun n ↦ loopExit f n b
+
+/-- The unbounded loop behind `while … rdo` is the loop of the monad. -/
+instance {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonadWhile m] :
+    MeasurableSpaceForIn m Lean.Loop Unit where
+  forIn _ b f := loop (f ()) b
+
+section Measure
+
+open scoped ENNReal Topology
+open Filter
+
+variable {σ : Type u} [MeasurableSpace σ]
+
+private lemma loopExit_zero (f : σ → Measure (ForInStep σ)) (b : σ) :
+    loopExit f 0 b = (f b).bind fun t ↦
+      ForInStep.casesOn (motive := fun _ ↦ Measure σ) t Measure.dirac fun _ ↦ 0 := rfl
+
+private lemma loopExit_succ (f : σ → Measure (ForInStep σ)) (n : ℕ) (b : σ) :
+    loopExit f (n + 1) b = (f b).bind fun t ↦
+      ForInStep.casesOn (motive := fun _ ↦ Measure σ) t (fun _ ↦ 0) (loopExit f n) := rfl
+
+/-- A `while` loop is a sub-probability measure: the runs that stop at the different steps are
+disjoint, so their masses add up to at most `1`. -/
+lemma measure_loop_univ_le_one {f : σ → Measure (ForInStep σ)} (hf : ∀ s, f s Set.univ ≤ 1)
+    (b : σ) : loop f b Set.univ ≤ 1 := by
+  /- The runs that stop at the steps `2, …, n + 1` are one step, followed by the runs that stop at
+  the steps `1, …, n`. -/
+  have tail : ∀ n b, ∑ k ∈ Finset.range n, loopExit f (k + 1) b Set.univ ≤
+      ∫⁻ t, ForInStep.casesOn (motive := fun _ ↦ ℝ≥0∞) t (fun _ ↦ 0)
+        (fun b' ↦ ∑ k ∈ Finset.range n, loopExit f k b' Set.univ) ∂f b := by
+    intro n
+    induction n with
+    | zero => simp
+    | succ n ih =>
+      intro b
+      rw [Finset.sum_range_succ, loopExit_succ]
+      -- Bound each of the two terms by an integral against the first step.
+      refine (add_le_add (ih b) (Measure.bind_apply_le _ MeasurableSet.univ)).trans ?_
+      -- Merge the two integrals.
+      refine (le_lintegral_add _ _).trans (le_of_eq ?_)
+      -- The merged integrand is the one of the statement.
+      refine lintegral_congr fun t ↦ ?_
+      cases t <;> simp [Finset.sum_range_succ]
+  -- The runs that stop within `n` steps have mass at most `1`.
+  have partialSum : ∀ n b, ∑ k ∈ Finset.range n, loopExit f k b Set.univ ≤ 1 := by
+    intro n
+    induction n with
+    | zero => simp
+    | succ n ih =>
+      intro b
+      rw [Finset.sum_range_succ', loopExit_zero]
+      -- Bound each of the two terms by an integral against the first step.
+      refine (add_le_add (tail n b) (Measure.bind_apply_le _ MeasurableSet.univ)).trans ?_
+      -- Merge the two integrals.
+      refine (le_lintegral_add _ _).trans ?_
+      -- The integral of `1` against the first step is its mass, at most `1`.
+      refine le_trans ?_ (lintegral_one.trans_le (hf b))
+      -- The merged integrand is at most `1`.
+      refine lintegral_mono fun t ↦ ?_
+      cases t <;> simp [ih]
+  change Measure.sum (fun n ↦ loopExit f n b) Set.univ ≤ 1
+  rw [Measure.sum_apply _ MeasurableSet.univ, ENNReal.tsum_eq_iSup_nat]
+  exact iSup_le fun n ↦ partialSum n b
+
+private lemma loopRun_zero (f : σ → Measure (ForInStep σ)) (b : σ) :
+    loopRun f 0 b = Measure.dirac b := rfl
+
+private lemma loopRun_succ (f : σ → Measure (ForInStep σ)) (n : ℕ) (b : σ) :
+    loopRun f (n + 1) b = (f b).bind fun t ↦
+      ForInStep.casesOn (motive := fun _ ↦ Measure σ) t (fun _ ↦ 0) (loopRun f n) := rfl
+
+/-- A case analysis on the outcome of a step is measurable as soon as its two branches are. -/
+lemma measurable_casesOn {γ : Type*} [MeasurableSpace γ] {d y : σ → γ}
+    (hd : Measurable d) (hy : Measurable y) :
+    Measurable fun t : ForInStep σ ↦ ForInStep.casesOn (motive := fun _ ↦ γ) t d y :=
+  fun _ hs ↦ ⟨hy hs, hd hs⟩
+
+/-- Binding a case analysis on the outcome of a step, evaluated on the whole space. -/
+private lemma bind_casesOn_apply_univ (μ : Measure (ForInStep σ)) {d y : σ → Measure σ}
+    (hd : Measurable d) (hy : Measurable y) :
+    μ.bind (fun t ↦ ForInStep.casesOn (motive := fun _ ↦ Measure σ) t d y) Set.univ =
+      ∫⁻ t, ForInStep.casesOn (motive := fun _ ↦ ℝ≥0∞) t (fun s ↦ d s Set.univ)
+        (fun s ↦ y s Set.univ) ∂μ := by
+  rw [Measure.bind_apply MeasurableSet.univ (measurable_casesOn hd hy).aemeasurable]
+  exact lintegral_congr fun t ↦ by cases t <;> rfl
+
+private lemma measurable_loopExit {f : σ → Measure (ForInStep σ)} (hf : Measurable f) :
+    ∀ n, Measurable (loopExit f n)
+  | 0 => (Measure.measurable_bind'
+      (measurable_casesOn Measure.measurable_dirac measurable_const)).comp hf
+  | n + 1 => (Measure.measurable_bind'
+      (measurable_casesOn measurable_const (measurable_loopExit hf n))).comp hf
+
+lemma measurable_loopRun {f : σ → Measure (ForInStep σ)} (hf : Measurable f) :
+    ∀ n, Measurable (loopRun f n)
+  | 0 => Measure.measurable_dirac
+  | n + 1 => (Measure.measurable_bind'
+      (measurable_casesOn measurable_const (measurable_loopRun hf n))).comp hf
+
+/-- No step yet: the run is at its starting state, with mass `1`. -/
+@[simp]
+lemma loopRun_zero_apply_univ (f : σ → Measure (ForInStep σ)) (b : σ) :
+    loopRun f 0 b Set.univ = 1 := by
+  simp [loopRun_zero]
+
+/-- The runs still going after `n + 1` steps: one step, then, from the state it carries on with, the
+runs still going after `n` steps. -/
+lemma loopRun_succ_apply_univ {f : σ → Measure (ForInStep σ)} (hf : Measurable f) (n : ℕ)
+    (b : σ) :
+    loopRun f (n + 1) b Set.univ =
+      ∫⁻ t, ForInStep.casesOn (motive := fun _ ↦ ℝ≥0∞) t (fun _ ↦ 0)
+        (fun s ↦ loopRun f n s Set.univ) ∂f b := by
+  rw [loopRun_succ, bind_casesOn_apply_univ _ measurable_const (measurable_loopRun hf n)]
+  simp
+
+/-- The runs still going after `n` steps have mass at most `1`. -/
+lemma loopRun_apply_univ_le_one (f : σ → Measure (ForInStep σ)) [hf : IsMarkov f] (n : ℕ)
+    (b : σ) : loopRun f n b Set.univ ≤ 1 := by
+  induction n generalizing b with
+  | zero => simp [loopRun_zero]
+  | succ n ih =>
+    have := hf.isProbabilityMeasure b
+    rw [loopRun_succ_apply_univ hf.measurable]
+    calc _ ≤ ∫⁻ _, 1 ∂f b := lintegral_mono fun t ↦ by cases t <;> simp [ih]
+      _ = 1 := by simp
+
+/-- The runs still going after `n` steps are those that stop at the next step, and those still going
+after it. -/
+private lemma loopRun_apply_univ (f : σ → Measure (ForInStep σ)) [hf : IsMarkov f] (n : ℕ)
+    (b : σ) :
+    loopRun f n b Set.univ = loopExit f n b Set.univ + loopRun f (n + 1) b Set.univ := by
+  induction n generalizing b with
+  | zero =>
+    have := hf.isProbabilityMeasure b
+    rw [loopExit_zero, loopRun_succ,
+      bind_casesOn_apply_univ _ Measure.measurable_dirac measurable_const,
+      bind_casesOn_apply_univ _ measurable_const (measurable_loopRun hf.measurable 0)]
+    simp only [loopRun_zero, measure_univ, Measure.coe_zero, Pi.zero_apply]
+    -- Merge the two integrals: the integrand is `1` whether the step stops or not.
+    rw [← lintegral_add_left (measurable_casesOn measurable_const measurable_const)]
+    calc (1 : ℝ≥0∞) = ∫⁻ _, 1 ∂f b := by simp
+      _ = _ := lintegral_congr fun t ↦ by cases t <;> simp
+  | succ n ih =>
+    have hExit : Measurable fun s ↦ loopExit f n s Set.univ :=
+      (Measure.measurable_coe MeasurableSet.univ).comp (measurable_loopExit hf.measurable n)
+    rw [loopRun_succ f n b, loopExit_succ, loopRun_succ f (n + 1) b,
+      bind_casesOn_apply_univ _ measurable_const (measurable_loopRun hf.measurable n),
+      bind_casesOn_apply_univ _ measurable_const (measurable_loopExit hf.measurable n),
+      bind_casesOn_apply_univ _ measurable_const
+        (measurable_loopRun hf.measurable (n + 1))]
+    simp only [Measure.coe_zero, Pi.zero_apply]
+    -- Merge the two integrals, and use the statement for `n` from the state the step carries on.
+    rw [← lintegral_add_left (measurable_casesOn measurable_const hExit)]
+    exact lintegral_congr fun t ↦ by cases t <;> simp [ih]
+
+/-- The runs that stop within `n` steps and the runs still going after `n` steps have a total mass
+of `1`. -/
+private lemma sum_loopExit_add_loopRun (f : σ → Measure (ForInStep σ)) [IsMarkov f] (n : ℕ)
+    (b : σ) :
+    ∑ k ∈ Finset.range n, loopExit f k b Set.univ + loopRun f n b Set.univ = 1 := by
+  induction n with
+  | zero => simp [loopRun_zero]
+  | succ n ih => rw [Finset.sum_range_succ, add_assoc, ← loopRun_apply_univ, ih]
+
+/-- The runs still going after `n` steps have a mass that decreases with `n`. -/
+lemma antitone_loopRun_apply_univ (f : σ → Measure (ForInStep σ)) [IsMarkov f] (b : σ) :
+    Antitone fun n ↦ loopRun f n b Set.univ :=
+  antitone_nat_of_succ_le fun n ↦ (loopRun_apply_univ f n b).symm ▸ le_add_self
+
+/-- The loop whose step is `f` stops almost surely from `b`: its runs still going after `n` steps
+have a mass that tends to `0`. -/
+def Terminates (f : σ → Measure (ForInStep σ)) (b : σ) : Prop :=
+  Tendsto (fun n ↦ loopRun f n b Set.univ) atTop (𝓝 0)
+
+/-- The runs still going after `n` steps have a mass that tends to the probability that the loop
+never stops: `1` minus the mass of the loop. -/
+lemma tendsto_loopRun_apply_univ (f : σ → Measure (ForInStep σ)) [IsMarkov f] (b : σ) :
+    Tendsto (fun n ↦ loopRun f n b Set.univ) atTop (𝓝 (1 - loop f b Set.univ)) := by
+  -- The runs that stop within `n` steps have a mass that tends to the mass of the loop.
+  have hExit : Tendsto (fun n ↦ ∑ k ∈ Finset.range n, loopExit f k b Set.univ) atTop
+      (𝓝 (loop f b Set.univ)) := by
+    change Tendsto _ _ (𝓝 (Measure.sum (fun n ↦ loopExit f n b) Set.univ))
+    rw [Measure.sum_apply _ MeasurableSet.univ]
+    exact ENNReal.tendsto_nat_tsum _
+  have h n : loopRun f n b Set.univ = 1 - ∑ k ∈ Finset.range n, loopExit f k b Set.univ := by
+    have hsum := sum_loopExit_add_loopRun f n b
+    refine ENNReal.eq_sub_of_add_eq ?_ ((add_comm _ _).trans hsum)
+    exact ne_top_of_le_ne_top ENNReal.one_ne_top (hsum ▸ le_self_add)
+  simp_rw [h]
+  exact ENNReal.Tendsto.sub tendsto_const_nhds hExit (Or.inl ENNReal.one_ne_top)
+
+/-- A `while` loop whose step is a Markov kernel is a probability measure exactly when it stops
+almost surely. -/
+theorem isProbabilityMeasure_loop_iff (f : σ → Measure (ForInStep σ)) [hf : IsMarkov f]
+    (b : σ) : IsProbabilityMeasure (loop f b) ↔ Terminates f b := by
+  have hRun := tendsto_loopRun_apply_univ f b
+  rw [isProbabilityMeasure_iff, Terminates]
+  constructor
+  · intro h
+    simpa [h] using hRun
+  · intro h
+    refine le_antisymm ?_ (tsub_eq_zero_iff_le.1 (tendsto_nhds_unique hRun h))
+    refine measure_loop_univ_le_one (fun s ↦ ?_) b
+    have := hf.isProbabilityMeasure s
+    simp
+
+end Measure
+
+end MeasurableSpaceMonadWhile
diff --git a/RandomDo/Tactic/IsMarkov/Elab.lean b/RandomDo/Tactic/IsMarkov/Elab.lean
index fa013d8..70f52df 100644
--- a/RandomDo/Tactic/IsMarkov/Elab.lean
+++ b/RandomDo/Tactic/IsMarkov/Elab.lean
@@ -50,6 +50,8 @@ inductive Shape
   along, one for a fixed collection and one for a collection read off the parameter, so that the
   three collections `rdo` supports share a single branch below. -/
   | forIn (fixed varying : Name)
+  /-- `while c rdo body`: a loop over `Lean.Loop`, which need not terminate. -/
+  | forInLoop
   /-- `Break.runK r (fun _ ↦ κ) η`: the case analysis an `rdo` block performs after a loop that
   returns early. -/
   | breakRunK
@@ -68,6 +70,7 @@ instance : ToString Shape where
     | .ite => "ite"
     | .dite .. => "dite"
     | .forIn .. => "forIn"
+    | .forInLoop => "forInLoop"
     | .breakRunK => "breakRunK"
     | .const => "const"
     | .leaf => "leaf"
@@ -104,6 +107,7 @@ def shapeOf (κ : Expr) : MetaM Shape := do
       | .const ``List _ => return .forIn ``IsMarkov.forInList ``IsMarkov.forInList_comp
       | .const ``Array _ => return .forIn ``IsMarkov.forInArray ``IsMarkov.forInArray_comp
       | .const ``Vector _ => return .forIn ``IsMarkov.forInVector ``IsMarkov.forInVector_comp
+      | .const ``Lean.Loop _ => return .forInLoop
       | _ => return .leaf
     else if head.isConstOf ``Break.runK then
       return .breakRunK
@@ -265,6 +269,16 @@ partial def isMarkovCore (g : MVarId) (fuel : Nat) : MetaM (List MVarId) := g.wi
       else
         trace[is_markov] "neither `forIn` lemma applies, handed back"
         return [g]
+    | .forInLoop =>
+      /- `while c rdo body`: a measurability goal for the initial state, an `IsMarkov` goal for the
+      step of the loop, jointly in the parameter and in the state, and the termination of the loop.
+      We recurse into the second, and leave the other two to the user. -/
+      let gs ← g.applyConst ``IsMarkov.forInLoop
+      match gs with
+      | [g_measurable, g_step, g_term] =>
+        return (← isMarkovCore g_step fuel) ++ [g_measurable, g_term]
+      | _ =>
+        throwError "is_markov: expected three goals after the `forInLoop` step, got {gs.length}"
     | .breakRunK =>
       let gs ← g.applyConst ``IsMarkov.breakRunK
       match gs with
diff --git a/RandomDo/Tactic/IsMarkov/ForInStep.lean b/RandomDo/Tactic/IsMarkov/ForInStep.lean
index 6351f45..29c6357 100644
--- a/RandomDo/Tactic/IsMarkov/ForInStep.lean
+++ b/RandomDo/Tactic/IsMarkov/ForInStep.lean
@@ -22,6 +22,7 @@ largest one making both `ForInStep.yield` and `ForInStep.done` measurable.
 ## Main results
 * `measurable_yield`, `measurable_run`, `measurable_isDone`: the maps relating `ForInStep β` to `β`
   and to `Bool` are measurable.
+* The points of `ForInStep β` are measurable as soon as those of `β` are.
 * `measurable_CasesOn`: a case analysis on a `ForInStep`, measurable in each of its two branches, is
   measurable.
 * `IsMarkov.forInStepCasesOn`: the same statement for the Markov property.
@@ -57,6 +58,16 @@ lemma measurable_yield : Measurable (ForInStep.yield : β → ForInStep β) := f
 @[fun_prop]
 lemma measurable_run : Measurable (ForInStep.run : ForInStep β → β) := fun _ hs => ⟨hs, hs⟩
 
+/-- The points of `ForInStep β` are measurable as soon as those of `β` are. -/
+instance [MeasurableSingletonClass β] : MeasurableSingletonClass (ForInStep β) where
+  measurableSet_singleton t := by
+    -- A singleton's preimages under `yield` and `done` are a singleton and the empty set.
+    constructor <;> cases t <;> change MeasurableSet (_ ⁻¹' _) <;> simp [Set.preimage]
+
+instance [Countable β] : Countable (ForInStep β) :=
+  Function.Injective.countable (f := fun t : ForInStep β ↦ (t.isDone, t.run)) <| by
+    rintro (_ | _) (_ | _) h <;> simp_all
+
 @[fun_prop]
 lemma measurable_isDone : Measurable (ForInStep.isDone : ForInStep β → Bool) := by
   intro s _
diff --git a/RandomDo/Tactic/IsMarkov/Lemmas.lean b/RandomDo/Tactic/IsMarkov/Lemmas.lean
index 38cc0d0..2fce5bc 100644
--- a/RandomDo/Tactic/IsMarkov/Lemmas.lean
+++ b/RandomDo/Tactic/IsMarkov/Lemmas.lean
@@ -7,6 +7,7 @@ module
 
 public import RandomDo.Monad.Instances
 public import RandomDo.Monad.ForInInstances
+public import RandomDo.Monad.While
 public import RandomDo.Measurable
 public import RandomDo.Tactic.IsMarkov.ForInStep
 public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
@@ -49,13 +50,16 @@ complex program to the Markov property/measurability of its underlying mathemati
 * `forIn_nil`, `forIn_cons`: A `for` loop over a list, unrolled one element at a time.
 * `breakRunK`: The case analysis a program performs after a loop that returns early, on the `Option`
   slot holding the returned value, is Markovian as soon as both of its branches are.
+* `forInLoop`: A `while` loop, whose initial state depends measurably on the parameter and whose
+  step is Markovian in the parameter and in the state, is measurable in the parameter. It is
+  Markovian as soon as it stops almost surely, which is left as a hypothesis.
 -/
 
 @[expose] public section
 
 open MeasureTheory ProbabilityTheory Function
 open MeasurableSpacePure
-open scoped ENNReal
+open scoped ENNReal Topology
 
 namespace IsMarkov
 
@@ -396,4 +400,41 @@ lemma breakRunK {o : α → Option γ} (ho : Measurable o)
   | none => simpa [Break.runK] using h_break.isProbabilityMeasure a
   | some r => simpa [Break.runK] using h_success.isProbabilityMeasure (a, r)
 
+section While
+
+open MeasurableSpaceMonadWhile
+
+/-- The runs of a `while` loop that stop at the `n + 1`-th step are measurable jointly in the
+parameter and in the starting state, as soon as the step is Markovian in both. -/
+private lemma measurable_loopExit {f : γ → σ → Measure (ForInStep σ)}
+    (hf : IsMarkov fun p : γ × σ ↦ f p.1 p.2) (n : ℕ) :
+    Measurable fun p : γ × σ ↦ loopExit (f p.1) n p.2 := by
+  induction n with
+  | zero =>
+    simp only [loopExit, mBind_def, mPure_def]
+    exact measurable_bind hf (ForInStep.measurable_CasesOn (done := fun _ b ↦ Measure.dirac b)
+      (yield := fun _ _ ↦ 0) (by fun_prop) measurable_const)
+  | succ n ih =>
+    simp only [loopExit, mBind_def]
+    exact measurable_bind hf (ForInStep.measurable_CasesOn (done := fun _ _ ↦ 0)
+      (yield := fun (p : γ × σ) b ↦ loopExit (f p.1) n b) measurable_const
+      (ih.comp (measurable_fst.fst.prodMk measurable_snd)))
+
+lemma forInLoop {b : γ → σ} {f : γ → Unit → σ → Measure (ForInStep σ)} (hb : Measurable b)
+    (hf : IsMarkov fun p : γ × σ ↦ f p.1 () p.2)
+    (hterm : ∀ c, Terminates (f c ()) (b c)) :
+    IsMarkov fun c ↦ MeasurableSpaceForIn.forIn (m := Measure) Lean.Loop.mk (b c) (f c) := by
+  refine ⟨?_, fun c ↦ ?_⟩
+  · change Measurable fun c ↦ Measure.sum fun n ↦ loopExit (f c ()) n (b c)
+    refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_
+    simp_rw [Measure.sum_apply _ hs]
+    exact Measurable.tsum fun n ↦ (Measure.measurable_coe hs).comp
+      ((measurable_loopExit (f := fun c ↦ f c ()) hf n).comp (measurable_id.prodMk hb))
+  -- For a fixed parameter, the step is a Markov kernel in the state.
+  · have : IsMarkov (f c ()) :=
+      hf.comp (g := fun s ↦ (c, s)) (measurable_const.prodMk measurable_id)
+    exact (isProbabilityMeasure_loop_iff (f c ()) (b c)).2 (hterm c)
+
+end While
+
 end IsMarkov
diff --git a/RandomDo/Tactic/IsMarkov/While/LoopInvariant.lean b/RandomDo/Tactic/IsMarkov/While/LoopInvariant.lean
new file mode 100644
index 0000000..0321379
--- /dev/null
+++ b/RandomDo/Tactic/IsMarkov/While/LoopInvariant.lean
@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+public import RandomDo.Monad.While
+
+/-!
+# Invariants of `while` loops
+
+An invariant of a `while` loop is a property of the states it carries on from and one of the states
+it stops at, kept by almost every step of the loop.
+
+## Main definitions
+
+* `LoopInvariant f`: an invariant of the loop whose step is `f`.
+-/
+
+@[expose] public section
+
+open MeasureTheory
+
+namespace MeasurableSpaceMonadWhile
+
+universe u
+
+variable {σ : Type u} [MeasurableSpace σ] {f : σ → Measure (ForInStep σ)}
+
+/-- An invariant of the loop whose step is `f`: a property `running` of the states the loop carries
+on from, and a property `stopped` of the states it stops at, such that from a state satisfying
+`running`, almost every step carries on from a state satisfying `running` or stops at a state
+satisfying `stopped`. -/
+structure LoopInvariant (f : σ → Measure (ForInStep σ)) where
+  /-- The property of the states the loop carries on from. -/
+  running : σ → Prop
+  /-- The property of the states the loop stops at. -/
+  stopped : σ → Prop := fun _ ↦ True
+  /-- Almost every step from a state satisfying `running` stays in the invariant. -/
+  step : ∀ s, running s → ∀ᵐ t ∂f s, ForInStep.casesOn (motive := fun _ ↦ Prop) t stopped running
+
+namespace LoopInvariant
+
+instance : CoeFun (LoopInvariant f) fun _ ↦ ForInStep σ → Prop where
+  coe I t := ForInStep.casesOn t I.stopped I.running
+
+end LoopInvariant
+
+end MeasurableSpaceMonadWhile
diff --git a/RandomDo/Tactic/IsMarkov/While/Tactic.lean b/RandomDo/Tactic/IsMarkov/While/Tactic.lean
new file mode 100644
index 0000000..8672815
--- /dev/null
+++ b/RandomDo/Tactic/IsMarkov/While/Tactic.lean
@@ -0,0 +1,144 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+public import RandomDo.Tactic.IsMarkov.While.Termination
+
+/-!
+# A tactic for the termination of `while` loops
+
+`terminates` proves the goal `Terminates f b` that `is_markov` hands back for a `while` loop, from
+an invariant, a variant and a probability given on the states of the loop. It applies a rule of
+`RandomDo.Tactic.IsMarkov.While.Termination`, unfolds the step of the loop on its successors, and
+leaves the remaining conditions as goals about the states only.
+
+## Main declarations
+
+* `loop_step`: simplifies a goal about one step of a loop into conditions on its successors.
+* `terminates`: proves the termination of a loop by one of the rules.
+-/
+
+public meta section
+
+open Lean
+
+/-- `loop_step [h₁, …]` simplifies a goal about one step of a loop: a property that almost every
+successor of a state satisfies, the probability of a set of successors, or an arithmetic condition.
+It evaluates the step on its successors, with the additional simp lemmas `h₁, …` for the
+definitions of the program, splits on the conditions of the program, and tries to close the
+resulting goals, which only mention the state. -/
+syntax (name := loopStep) "loop_step" (" [" term,* "]")? : tactic
+
+macro_rules
+  | `(tactic| loop_step $[[$ls,*]]?) => do
+    let ls : Array Term := (ls.map (·.getElems)).getD #[]
+    `(tactic| (
+      try intro $(mkIdent `s) $(mkIdent `hs)
+      try simp only at *
+      try simp only [MeasureTheory.ae_iff]
+      try split_ifs
+      all_goals try norm_num [MeasureTheory.Measure.dirac_apply, Set.indicator_apply,
+        ENNReal.toReal_add, ENNReal.toReal_ofReal', ENNReal.mul_eq_top, $[$ls:term],*] at *
+      -- A measure followed by a deterministic successor is its image, and the probability of a set
+      -- under the image is at least the probability of its preimage.
+      all_goals try rw [MeasureTheory.Measure.bind_dirac_eq_map]
+      all_goals try refine le_trans ?_ (ENNReal.toReal_mono (MeasureTheory.measure_ne_top _ _)
+        (MeasureTheory.Measure.le_map_apply ?_ _))
+      all_goals try fun_prop
+      all_goals try simp only [Set.preimage_ofPred_eq] at *
+      all_goals try split_ifs
+      all_goals try norm_num [ENNReal.toReal_add, ENNReal.toReal_ofReal', ENNReal.mul_eq_top] at *
+      all_goals repeat' apply And.intro
+      all_goals try first | done | trivial | assumption | omega | linarith | positivity))
+
+/-- The invariant of `terminates`: the given property of the running states, whose stability is left
+as the goal `step`, or the property that always holds. -/
+def invariant (P? : Option Term) : MacroM Term :=
+  match P? with
+  | some P => `(({ running := $P, step := ?step } : MeasurableSpaceMonadWhile.LoopInvariant _))
+  | none => `(({ running := fun _ ↦ True
+                 step := fun _ _ ↦ Filter.Eventually.of_forall fun t ↦ by cases t <;> trivial } :
+      MeasurableSpaceMonadWhile.LoopInvariant _))
+
+/-- `terminates` proves the termination of a `while` loop, the goal `Terminates f b` that
+`is_markov` hands back (after `intro` of the parameters the loop depends on).
+
+* `terminates (prob := ε)` applies `Terminates.mcIverMorgan_immediateEscape`: every step stops with
+  probability at least `ε > 0`.
+* `terminates (variant := U) (bound := N) (prob := ε)` applies
+  `Terminates.majumdarSathiyanarayana_variantRule`, with a variant `U : σ → ℕ` on the states, at
+  most `N`, decreased with probability at least `ε > 0` by every step that does not stop. Stopping
+  counts as decreasing `U`.
+* `(invariant := P)`, before the other arguments, restricts both to the states satisfying
+  `P : σ → Prop`, which almost every step keeps.
+* `[h₁, …]`, after the other arguments, are simp lemmas for the definitions of the program.
+
+The variant rule takes a variant `U'` on the states `ForInStep σ` of the transition system, with
+`Lo ≤ U' < Hi`, and a probability `> ε` of decreasing it. `terminates` applies it to
+`U' (done s) = 0` and `U' (yield s) = U s + 1`, between `Lo = 0` and `Hi = N + 2`, with `ε / 2`:
+* A step from `yield s` that stops goes to some `done s'`, and counts as decreasing `U'` only if
+  `U' (done s') < U' (yield s)`. As `U` can be `0` on a running state (when the loop is about to
+  stop, as `countdown` at `0`), the terminal states need a value below all the values of `U`:
+  hence the shift of `U` by `1` on the running states, the terminal states taking `0`. A step to
+  `yield s'` still decreases `U'` exactly when it decreases `U`.
+* On the invariant, `U s ≤ N`, so `0 ≤ U' ≤ N + 1`, and the strict upper bound of the rule is
+  `N + 2`: one for the shift, one for passing from `≤` to `<`.
+* `(prob := ε)` asks for a probability at least `ε`, while the rule asks for one greater than its
+  constant: a probability `≥ ε` is `> ε / 2`.
+
+The conditions it cannot prove are left as goals about the states only. -/
+syntax (name := terminatesTac) "terminates" (atomic(" (" &"invariant") " := " term ")")?
+  (atomic(" (" &"variant") " := " term ")")? (atomic(" (" &"bound") " := " term ")")?
+  " (" &"prob" " := " term ")" (" [" term,* "]")? : tactic
+
+macro_rules
+  | `(tactic| terminates $[(invariant := $P?)]? (prob := $ε) $[[$ls,*]]?) => do
+    let ls : Array Term := (ls.map (·.getElems)).getD #[]
+    let I ← invariant P?
+    `(tactic| (
+      intros
+      refine MeasurableSpaceMonadWhile.Terminates.mcIverMorgan_immediateEscape $I $ε ?pos
+        ?init ?stop
+      all_goals try loop_step [$[$ls:term],*]))
+  | `(tactic| terminates $[(invariant := $P?)]? (variant := $U) (bound := $N) (prob := $ε)
+      $[[$ls,*]]?) => do
+    let ls : Array Term := (ls.map (·.getElems)).getD #[]
+    let I ← invariant P?
+    let P ← P?.getDM `(fun _ ↦ True)
+    `(tactic| (
+      intros
+      -- `U` shifted by `1` on the running states, below which the terminal states are `0`: see the
+      -- docstring for the bounds `0` and `N + 2` and for `ε / 2`.
+      refine MeasurableSpaceMonadWhile.Terminates.majumdarSathiyanarayana_variantRule $I
+        (fun t ↦ ForInStep.casesOn (motive := fun _ ↦ ℤ) t (fun _ ↦ 0) fun s ↦ (($U s : ℕ) : ℤ) + 1)
+        0 ((($N : ℕ) : ℤ) + 2) ($ε / 2) (half_pos ?pos) ?init ?bounds
+        (fun $(mkIdent `s) $(mkIdent `hs) ↦ (half_lt_self ?pos).trans_le ?progress) ?measurable
+      -- The bound of the lifted variant, from the bound `U ≤ N` on the states of the invariant.
+      case' bounds =>
+        intro t $(mkIdent `hs)
+        cases t with
+        | done _ => dsimp only; omega
+        | yield $(mkIdent `s) =>
+          replace $(mkIdent `hs) : ($P) $(mkIdent `s) := $(mkIdent `hs)
+          try dsimp only at $(mkIdent `hs):ident ⊢
+          refine (fun h : ($U) $(mkIdent `s) ≤ ($N) ↦ by (try simp only [] at h); omega) ?_
+          try loop_step [$[$ls:term],*]
+      -- The measurability of the lifted variant, from the measurability of `U`.
+      case' measurable => first
+        | exact Measurable.of_discrete
+        | (refine MeasurableSpaceMonadWhile.measurable_casesOn measurable_const
+            (((Measurable.of_discrete (f := fun n : ℕ ↦ (n : ℤ))).comp ?_).add_const 1)
+           first | fun_prop | measurability | skip)
+      try case' step => try loop_step [$[$ls:term],*]
+      try case' init => try loop_step [$[$ls:term],*]
+      try case' pos => try loop_step [$[$ls:term],*]
+      try case' progress => try loop_step [$[$ls:term],*]))
+  | `(tactic| terminates $[(invariant := $_)]? (variant := $_) (prob := $_) $[[$_,*]]?) =>
+    Macro.throwError "terminates: a variant needs a bound, given by `(bound := N)`"
+  | `(tactic| terminates $[(invariant := $_)]? (bound := $_) (prob := $_) $[[$_,*]]?) =>
+    Macro.throwError "terminates: a bound needs a variant, given by `(variant := U)`"
+
+end
diff --git a/RandomDo/Tactic/IsMarkov/While/Termination.lean b/RandomDo/Tactic/IsMarkov/While/Termination.lean
new file mode 100644
index 0000000..1e70659
--- /dev/null
+++ b/RandomDo/Tactic/IsMarkov/While/Termination.lean
@@ -0,0 +1,220 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+public import RandomDo.Tactic.IsMarkov.Elab
+public import RandomDo.Tactic.IsMarkov.While.LoopInvariant
+
+/-!
+# Termination of `while` loops
+
+`is_markov` hands back the termination of a `while` loop as a goal `Terminates f b`. This file
+implements proof rules of the literature for it, each under the name of its authors and with the
+hypotheses of its paper.
+
+## Main results
+
+* `Terminates.mcIverMorgan_zeroOneLaw`: the zero-one law of McIver and Morgan (2005,
+  Lemma 2.6.1).
+* `Terminates.majumdarSathiyanarayana_variantRule`: the variant rule of McIver and Morgan, as
+  presented by Majumdar and Sathiyanarayana (POPL 2025, Proof Rule 3.1), derived from the zero-one
+  law as McIver and Morgan derive their variant rule (2005, Lemma 2.7.1).
+* `Terminates.mcIverMorgan_immediateEscape`: termination when every step stops with probability at
+  least some fixed `ε > 0`, the stronger condition McIver and Morgan remark after their zero-one law
+  (2005, p. 54).
+
+## Implementation notes
+
+The program is a probabilistic transition system whose states are the `ForInStep σ`: the successor
+of `yield s` is drawn from `f s`, and the states `done s` are terminal. Every `rdo` loop is of this
+form. It has no demonic nondeterminism, one step is one iteration of the loop, and "every successor"
+is "almost every successor". The papers state these rules for discrete probabilistic choice; the
+rules here hold for any measurable state space and any Markov kernel, and their measurability
+conditions, which a discrete state space satisfies, have default proofs.
+
+## References
+
+* Annabelle McIver, Carroll Morgan, *Abstraction, Refinement and Proof for Probabilistic Systems*,
+  2005.
+* Rupak Majumdar, V. R. Sathiyanarayana, *Sound and Complete Proof Rules for Probabilistic
+Termination*, POPL 2025.
+-/
+
+@[expose] public section
+
+open MeasureTheory Filter
+open scoped ENNReal Topology
+
+namespace MeasurableSpaceMonadWhile
+
+universe u
+
+variable {σ : Type u} [MeasurableSpace σ] {f : σ → Measure (ForInStep σ)} {b : σ}
+
+namespace Terminates
+
+/-- **Zero-one law** (McIver and Morgan 2005, Lemma 2.6.1, stated informally there; its conditions
+are formalised by (2.12) with `I = [Inv]`, footnote 27).
+
+The program is the transition system whose states are the `ForInStep σ`: the successor of a state
+`yield s` is drawn from `f s`, and the states `done s` are terminal. Let `I` be an invariant, the
+paper's `Inv`, with `I.running b`. If, from every non-terminal state of `I`, the program terminates
+with probability at least some fixed `ε > 0`, then it terminates almost surely from `yield b`. The
+probability of terminating from `s` is the mass of the loop `loop f s`. -/
+theorem mcIverMorgan_zeroOneLaw (I : LoopInvariant f) (ε : ℝ) (hε : 0 < ε) (hb : I.running b)
+    (hterm : ∀ s, I.running s → ε ≤ (loop f s Set.univ).toReal)
+    (hf : IsMarkov f := by is_markov) : Terminates f b := by
+  -- The probability `r s` that the loop never stops from `s`.
+  set r : σ → ℝ≥0∞ := fun s ↦ ⨅ n, loopRun f n s Set.univ
+  have hr s : Tendsto (fun n ↦ loopRun f n s Set.univ) atTop (𝓝 (r s)) :=
+    tendsto_atTop_iInf (antitone_loopRun_apply_univ f s)
+  -- It is `1` minus the probability that the loop stops, so at most `1 - ε` on `I`.
+  have hrInv : ∀ s, I.running s → r s ≤ 1 - ENNReal.ofReal ε := fun s hs ↦ by
+    rw [tendsto_nhds_unique (hr s) (tendsto_loopRun_apply_univ f s)]
+    exact tsub_le_tsub_left (ENNReal.ofReal_le_of_le_toReal (hterm s hs)) 1
+  -- The loop never stops from `s` when one step carries on and it never stops from there.
+  have hstep s : r s = ∫⁻ t, ForInStep.casesOn (motive := fun _ ↦ ℝ≥0∞) t (fun _ ↦ 0) r ∂f s := by
+    have := hf.isProbabilityMeasure s
+    refine tendsto_nhds_unique ((hr s).comp (tendsto_add_atTop_nat 1)) ?_
+    simp_rw [Function.comp_def, loopRun_succ_apply_univ hf.measurable]
+    refine tendsto_lintegral_of_dominated_convergence 1 (fun n ↦ measurable_casesOn
+      measurable_const ((Measure.measurable_coe MeasurableSet.univ).comp
+        (measurable_loopRun hf.measurable n))) (fun n ↦ .of_forall fun t ↦ ?_) (by simp)
+      (.of_forall fun t ↦ ?_)
+    · cases t <;> simp [loopRun_apply_univ_le_one]
+    · cases t with
+      | done _ => exact tendsto_const_nhds
+      | yield s' => exact hr s'
+  -- So the loop never stops with probability at most `(1 - ε)` times that it goes on for `m` steps.
+  have key : ∀ m s, I.running s → r s ≤ (1 - ENNReal.ofReal ε) * loopRun f m s Set.univ := by
+    intro m
+    induction m with
+    | zero => exact fun s hs ↦ by simpa using hrInv s hs
+    | succ m ih =>
+      intro s hs
+      rw [hstep s, loopRun_succ_apply_univ hf.measurable,
+        ← lintegral_const_mul' _ _ (ne_top_of_le_ne_top ENNReal.one_ne_top tsub_le_self)]
+      refine lintegral_mono_ae ?_
+      filter_upwards [I.step s hs] with t ht
+      cases t with
+      | done _ => simp
+      | yield s' => simpa using ih s' ht
+  -- In the limit, `r b ≤ (1 - ε) r b`, so `r b = 0`.
+  have hle : r b ≤ (1 - ENNReal.ofReal ε) * r b := ge_of_tendsto'
+    (ENNReal.Tendsto.const_mul (hr b) (Or.inr (ne_top_of_le_ne_top ENNReal.one_ne_top
+      tsub_le_self))) fun m ↦ key m b hb
+  have hr0 : r b = 0 := by
+    by_contra h
+    have hrb : r b ≠ ∞ := ne_top_of_le_ne_top ENNReal.one_ne_top
+      ((iInf_le _ 0).trans (loopRun_apply_univ_le_one f 0 b))
+    have hlt : 1 - ENNReal.ofReal ε < 1 :=
+      ENNReal.sub_lt_self ENNReal.one_ne_top one_ne_zero (ENNReal.ofReal_pos.2 hε).ne'
+    exact (ENNReal.mul_lt_mul_left h hrb hlt).not_ge (by simpa using hle)
+  simpa [Terminates, hr0] using hr b
+
+/-- **Variant rule for almost-sure termination** (McIver and Morgan 2005, in the form of Majumdar
+and Sathiyanarayana, *Sound and Complete Proof Rules for Probabilistic Termination*, POPL 2025,
+Proof Rule 3.1 and Lemma 3.1).
+
+The program is the transition system of `mcIverMorgan_zeroOneLaw`. To show that it terminates
+almost surely from `yield b`, find
+1. an inductive invariant `Inv` containing `yield b`, here an invariant `I` with `I.running b`;
+2. a variant function `U : Inv → ℤ`;
+3. bounds `Lo` and `Hi` such that `Lo ≤ U < Hi` on `Inv`;
+4. an `ε > 0`,
+
+such that, for each non-terminal state of `Inv`, (4.3) the successors that decrease `U` have a total
+probability `> ε`.
+
+Every non-terminal state is probabilistic, so condition (4.2) on assignment and nondeterministic
+states does not apply, and "every successor" is "almost every successor". Condition (4.1), `U = Lo`
+on the terminal states, is not needed and is dropped: the rule of the paper follows by forgetting
+it. Setting `U = Lo` on the terminal states still makes stopping count as decreasing `U`.
+
+As in McIver and Morgan's proof of their variant rule (Lemma 2.7.1), the program terminates within
+`Hi - Lo` steps with probability at least `ε ^ (Hi - Lo)` from every state of `Inv`, and the
+zero-one law concludes. -/
+theorem majumdarSathiyanarayana_variantRule (I : LoopInvariant f) (U : ForInStep σ → ℤ)
+    (Lo Hi : ℤ) (ε : ℝ) (hε : 0 < ε) (hb : I.running b)
+    (hbounds : ∀ t, I t → Lo ≤ U t ∧ U t < Hi)
+    (hprog : ∀ s, I.running s → ε < (f s {t | U t < U (.yield s)}).toReal)
+    (hU : Measurable U := by fun_prop) (hf : IsMarkov f := by is_markov) : Terminates f b := by
+  have hprog' s (hs : I.running s) : ENNReal.ofReal ε ≤ f s {t | U t < U (.yield s)} :=
+    ENNReal.ofReal_le_of_le_toReal (hprog s hs).le
+  have hε1 s (hs : I.running s) : ENNReal.ofReal ε ≤ 1 := by
+    have := hf.isProbabilityMeasure s
+    exact (hprog' s hs).trans prob_le_one
+  -- From a state of `I` where `U - Lo < n`, the loop goes on for `n` steps with probability at
+  -- most `1 - εⁿ`.
+  have key : ∀ n s, I.running s → (U (.yield s) - Lo).toNat < n →
+      loopRun f n s Set.univ ≤ 1 - ENNReal.ofReal ε ^ n := by
+    intro n
+    induction n with
+    | zero => exact fun s _ hs ↦ absurd hs (Nat.not_lt_zero _)
+    | succ n ih =>
+      intro s hs hUs
+      set S := {t : ForInStep σ | U t < U (.yield s)}
+      have hS : MeasurableSet S := hU measurableSet_Iio
+      have := hf.isProbabilityMeasure s
+      rw [loopRun_succ_apply_univ hf.measurable]
+      calc _ ≤ ∫⁻ t, 1 - S.indicator (fun _ ↦ ENNReal.ofReal ε ^ n) t ∂f s := by
+            refine lintegral_mono_ae ?_
+            filter_upwards [I.step s hs] with t ht
+            cases t with
+            | done _ => simp
+            | yield s' =>
+              by_cases hlt : U (.yield s') < U (.yield s)
+              · have := (hbounds (.yield s') ht).1
+                simpa [S, hlt] using ih s' ht (by omega)
+              · simpa [S, hlt] using loopRun_apply_univ_le_one f n s'
+        _ = 1 - ENNReal.ofReal ε ^ n * f s S := by
+          rw [lintegral_sub (measurable_const.indicator hS), lintegral_indicator_const hS]
+          · simp
+          · rw [lintegral_indicator_const hS]
+            exact ENNReal.mul_ne_top (ENNReal.pow_ne_top ENNReal.ofReal_ne_top) (measure_ne_top _ _)
+          · exact .of_forall fun t ↦
+              Set.indicator_le (fun _ _ ↦ pow_le_one₀ bot_le (hε1 s hs)) t
+        _ ≤ 1 - ENNReal.ofReal ε ^ (n + 1) :=
+          tsub_le_tsub_left (by rw [pow_succ]; gcongr; exact hprog' s hs) 1
+  -- So the loop stops with probability at least `ε ^ (Hi - Lo)` from every state of `I`.
+  refine mcIverMorgan_zeroOneLaw I (ε ^ (Hi - Lo).toNat) (pow_pos hε _) hb
+    (fun s hs ↦ ?_) hf
+  have hloop : loop f s Set.univ ≤ 1 := measure_loop_univ_le_one (fun s ↦ by
+    have := hf.isProbabilityMeasure s
+    exact prob_le_one) s
+  have hlim : 1 - loop f s Set.univ ≤ 1 - ENNReal.ofReal ε ^ (Hi - Lo).toNat := by
+    refine le_of_tendsto (tendsto_loopRun_apply_univ f s) (eventually_atTop.2 ⟨_, fun n hn ↦
+      (antitone_loopRun_apply_univ f s hn).trans (key _ s hs ?_)⟩)
+    have := hbounds (.yield s) hs
+    omega
+  rw [ENNReal.sub_le_sub_iff_left (pow_le_one₀ bot_le (hε1 s hs)) ENNReal.one_ne_top,
+    ← ENNReal.ofReal_pow hε.le] at hlim
+  exact (ENNReal.ofReal_le_iff_le_toReal (ne_top_of_le_ne_top ENNReal.one_ne_top hloop)).1 hlim
+
+/-- **Immediate escape** (McIver and Morgan 2005, p. 54: the stronger condition they remark after
+the zero-one law, Lemma 2.6.1).
+
+If, from every non-terminal state of the invariant `I`, one step stops with probability at least
+some fixed `ε > 0`, then the program terminates almost surely from `yield b`. This is the condition
+of a rejection sampling loop, which stops as soon as its sample satisfies a property of probability
+at least `ε`. It is the variant rule with the variant `1` on the non-terminal states and `0` on the
+terminal ones. -/
+theorem mcIverMorgan_immediateEscape (I : LoopInvariant f) (ε : ℝ) (hε : 0 < ε) (hb : I.running b)
+    (hstop : ∀ s, I.running s → ε ≤ (f s {t | t.isDone}).toReal)
+    (hf : IsMarkov f := by is_markov) : Terminates f b := by
+  refine majumdarSathiyanarayana_variantRule I (fun t ↦ if t.isDone then 0 else 1) 0 2 (ε / 2)
+    (half_pos hε) hb (fun t _ ↦ by split_ifs <;> simp) (fun s hs ↦ ?_)
+    (Measurable.ite (ForInStep.measurable_isDone (measurableSet_singleton true))
+      measurable_const measurable_const) hf
+  -- The successors that decrease the variant are the terminal ones.
+  refine (half_lt_self hε).trans_le ((hstop s hs).trans_eq ?_)
+  congr 2
+  ext t
+  cases t <;> simp
+
+end Terminates
+
+end MeasurableSpaceMonadWhile
diff --git a/Test/Computable.lean b/Test/Computable.lean
index 0b7752b..a1e128c 100644
--- a/Test/Computable.lean
+++ b/Test/Computable.lean
@@ -59,4 +59,17 @@ def ex1 : Measure ℝ := rdo
 
 run_cmd logComputable (ex1Computable)
 
+@[computable]
+noncomputable
+def flipsUntilHeads : Measure ℕ := rdo
+  let mut n := 0
+  while true rdo
+    let heads ← fairCoin
+    n := n + 1
+    if heads then
+      break
+  return n
+
+run_cmd logComputable (flipsUntilHeadsComputable)
+
 end Test.Computable
diff --git a/Test/Gaps.lean b/Test/Gaps.lean
index 39aeb1c..b5a0a6e 100644
--- a/Test/Gaps.lean
+++ b/Test/Gaps.lean
@@ -18,31 +18,10 @@ open MeasureTheory ProbabilityTheory
 
 namespace Test.Gaps
 
-/-! ## 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.
+`while … rdo` is supported. TODO: `repeat` and `repeat … until`, which still expand to core's
+`for _ in Loop.mk do …`, need `rdo` counterparts.
 -/
 
 /--
@@ -52,10 +31,12 @@ error: failed to synthesize instance of type class
 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
+def repeatLoop : IdM ℕ := rdo
   let mut i := 0
-  while i < 3 do
+  repeat
     i := i + 1
+    if 3 ≤ i then
+      break
   return i
 
 /-! ## Exceptions
diff --git a/Test/IsMarkov.lean b/Test/IsMarkov.lean
index a63e188..32d1c16 100644
--- a/Test/IsMarkov.lean
+++ b/Test/IsMarkov.lean
@@ -11,7 +11,8 @@ set_option linter.style.header false
 node. There is one test here per construct it recognises.
 -/
 
-open MeasureTheory ProbabilityTheory
+open scoped ENNReal
+open MeasureTheory ProbabilityTheory MeasurableSpacePure
 
 @[expose] public section
 
@@ -93,6 +94,147 @@ noncomputable def overList (xs : List ℝ) : Measure ℝ := rdo
 
 example : IsMarkov overList := by is_markov
 
+/-! ## `while`, whose termination is handed back
+
+`is_markov` proves that a `while` loop is Markovian up to its termination, which it hands back as a
+goal `Terminates`. Each test closes it with `terminates`, which applies a proof rule of the
+literature from `RandomDo.Tactic.IsMarkov.While.Termination`. -/
+
+noncomputable def untilHeads : Measure ℕ := rdo
+  let mut n := 0
+  while true rdo
+    let heads ← fairCoin
+    n := n + 1
+    if heads then
+      break
+  return n
+
+/-- Immediate escape: every step stops with probability `1 / 2`. -/
+example : IsProbabilityMeasure untilHeads := by
+  is_markov
+  terminates (prob := 1 / 2) [fairCoin]
+
+/-- A `while` loop whose condition reads the parameter. -/
+noncomputable def climbFrom (k : ℕ) : Measure ℕ := rdo
+  let mut n := k
+  while n < k + 3 rdo
+    let heads ← fairCoin
+    if heads then
+      n := n + 1
+  return n
+
+/-- The variant rule: below the invariant bound `k + 3`, the variant `k + 3 - n` decreases with
+probability `1 / 2`. -/
+example : IsMarkov climbFrom := by
+  is_markov
+  intro k
+  terminates (invariant := (· ≤ k + 3)) (variant := (k + 3 - ·)) (bound := k + 3) (prob := 1 / 2)
+    [fairCoin]
+
+/-- A deterministic countdown, whose counter is bounded only by its initial value. -/
+noncomputable def countdown (k : ℕ) : Measure ℕ := rdo
+  let mut i := k
+  while 0 < i rdo
+    i := i - 1
+  return i
+
+/-- The variant rule: below the invariant bound `k`, the counter decreases at every step. -/
+example : IsMarkov countdown := by
+  is_markov
+  intro k
+  terminates (invariant := (· ≤ k)) (variant := id) (bound := k) (prob := 1)
+
+/-- A `while` loop over two mutable variables: the flips until two heads. -/
+noncomputable def untilTwoHeads : Measure ℕ := rdo
+  let mut heads := 0
+  let mut flips := 0
+  while heads < 2 rdo
+    let b ← fairCoin
+    flips := flips + 1
+    if b then
+      heads := heads + 1
+  return flips
+
+/-- The variant rule, on the pairs `(heads, flips)`: below the invariant bound `2` on the heads, the
+variant `2 - heads` decreases with probability `1 / 2`. -/
+example : IsProbabilityMeasure untilTwoHeads := by
+  is_markov
+  terminates (invariant := fun p ↦ p.1 ≤ 2) (variant := fun p ↦ 2 - p.1) (bound := 2)
+    (prob := 1 / 2) [fairCoin]
+
+/-- The flips of a coin of bias `p` until heads. -/
+noncomputable def geometric (p : unitInterval) : Measure ℕ := rdo
+  let mut n := 0
+  while true rdo
+    let b ← bernoulliMeasure true false p
+    n := n + 1
+    if b then
+      break
+  return n
+
+/-- Immediate escape, with a symbolic probability. -/
+example (p : unitInterval) (hp : 0 < (p : ℝ)) : IsProbabilityMeasure (geometric p) := by
+  is_markov
+  terminates (prob := p)
+
+/-- The gambler's ruin: a fair random walk stopped at `0` and at `N`. -/
+noncomputable def ruin (N x : ℕ) : Measure ℕ := rdo
+  let mut y := x
+  while 0 < y ∧ y < N rdo
+    let b ← fairCoin
+    if b then
+      y := y + 1
+    else
+      y := y - 1
+  return y
+
+/-- The variant rule, with the distance to the nearest barrier as the variant. -/
+example (N : ℕ) : IsMarkov (ruin N) := by
+  is_markov
+  terminates (variant := fun y ↦ min y (N - y)) (bound := N) (prob := 1 / 2) [fairCoin]
+
+/-- A die by rejection: three flips give a number below `8`, kept if it is below `6`. -/
+noncomputable def die : Measure ℕ := rdo
+  let mut r := 6
+  while 6 ≤ r rdo
+    let a ← fairCoin
+    let b ← fairCoin
+    let c ← fairCoin
+    r := (if a then 4 else 0) + (if b then 2 else 0) + (if c then 1 else 0)
+  return r
+
+/-- The variant rule, with the variant `1` on the rejected numbers: a step keeps the number it draws
+with probability `3 / 4`. -/
+example : IsProbabilityMeasure die := by
+  is_markov
+  terminates (variant := fun r ↦ if 6 ≤ r then 1 else 0) (bound := 1) (prob := 3 / 4) [fairCoin]
+
+/-- A Gaussian random walk, stopped once it leaves `(-1, 1)`. -/
+noncomputable def gaussianWalk (x : ℝ) : Measure ℝ := rdo
+  let mut y := x
+  while |y| < 1 rdo
+    let z ← gaussianReal 0 1
+    y := y + z
+  return y
+
+/-- The variant rule, with the variant `1` inside `(-1, 1)`: a step leaves it with probability at
+least `P(Z ≥ 2)`. The goals left are about the Gaussian distribution only. -/
+example : IsMarkov gaussianWalk := by
+  is_markov
+  intro x
+  terminates (variant := fun y ↦ if |y| < 1 then 1 else 0) (bound := 1)
+    (prob := (gaussianReal 0 1 (Set.Ici 2)).toReal)
+  · -- From `|s| < 1`, a step of at least `2` leaves `(-1, 1)`.
+    rename_i h
+    refine measure_mono fun a (ha : 2 ≤ a) ↦ ?_
+    have := (abs_lt.1 h).1
+    simp [show ¬|s + a| < 1 from fun h' ↦ by linarith [(abs_lt.1 h').2]]
+  · exact ENNReal.toReal_le_of_le_ofReal zero_le_one (by simp [prob_le_one])
+  · refine ENNReal.toReal_pos (fun h ↦ ?_) (measure_ne_top _ _)
+    simpa using gaussianReal_absolutelyContinuous' 0 one_ne_zero h
+  · exact Measurable.ite (measurableSet_lt (by fun_prop) measurable_const) measurable_const
+      measurable_const
+
 /-! ## Looking through definitions, and the `fuel` argument -/
 
 noncomputable def layerOne : Measure ℝ := sumTwo
diff --git a/Test/Loops.lean b/Test/Loops.lean
index ff77c85..84e6ae9 100644
--- a/Test/Loops.lean
+++ b/Test/Loops.lean
@@ -1,18 +1,22 @@
 module
 
 public import Test.Common
+meta import Test.Common
+public import Std.Tactic.Do
 
 set_option linter.style.header false
+set_option linter.hashCommand false
 
 /-!
-# `rdo`: `for` loops over a single collection
+# `rdo`: `for` and `while` loops
 
 `rdo` has its own `for … rdo …` parser, expander and elaborator, mirroring core's but emitting
-`MeasurableSpaceForIn.forIn`. Instances exist for `List`, `Array` and `Vector`.
+`MeasurableSpaceForIn.forIn`. Instances exist for `List`, `Array` and `Vector`, and for `Lean.Loop`,
+which `while … rdo` loops over.
 
-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.
+A loop can sit under another construct, including another loop: the enclosing one learns what the
+loop does to the control flow from the `ControlInfo` handler of `rdoFor`, which is that of core's
+`for` loop with the same body.
 -/
 
 open MeasureTheory ProbabilityTheory
@@ -139,6 +143,187 @@ noncomputable def countHeads (n : ℕ) : Measure ℕ := rdo
       c := c + 1
   return c
 
+/-! ## Loops under other constructs -/
+
+/-- A loop nested inside another, reassigning a variable of the enclosing block. -/
+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
+
+example : IdM.run (nestedLoops [1, 2] [3, 4]) = 21 := rfl
+
+example : IdM.run (nestedLoops [1, 2] []) = 0 := rfl
+
+/-- `break` in the inner loop leaves the inner loop only. -/
+def innerBreak (xs ys : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    for y in ys rdo
+      if y = 0 then
+        break
+      s := s + x * y
+  return s
+
+example : IdM.run (innerBreak [1, 2] [3, 0, 5]) = 9 := rfl
+
+/-- `continue` in the inner loop skips to the next inner iteration. -/
+def innerContinue (xs ys : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    for y in ys rdo
+      if y = 0 then
+        continue
+      s := s + x * y
+  return s
+
+example : IdM.run (innerContinue [1, 2] [3, 0, 5]) = 24 := rfl
+
+/-- An early `return` in the inner loop leaves the whole program. -/
+def firstProductOver (xs ys : List ℕ) (limit : ℕ) : IdM ℕ := rdo
+  for x in xs rdo
+    for y in ys rdo
+      if x * y > limit then
+        return x * y
+  return 0
+
+example : IdM.run (firstProductOver [1, 2, 3] [1, 2] 3) = 4 := rfl
+
+example : IdM.run (firstProductOver [1, 2] [1, 2] 10) = 0 := rfl
+
+/-- An inner loop over several collections, which the expander rewrites first. -/
+def nestedZip (xs ys zs : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    for y in ys, z in zs rdo
+      s := s + x * y * z
+  return s
+
+example : IdM.run (nestedZip [1, 2] [1, 2] [3, 4]) = 33 := rfl
+
+/-- A loop in a branch of an `if`. -/
+def sumIf (b : Bool) (xs : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  if b then
+    for x in xs rdo
+      s := s + x
+  return s
+
+example : IdM.run (sumIf true [1, 2, 3]) = 6 := rfl
+
+example : IdM.run (sumIf false [1, 2, 3]) = 0 := rfl
+
+/-- A loop in an arm of a `match`. -/
+def sumHead (xss : List (List ℕ)) : IdM ℕ := rdo
+  let mut s := 0
+  match xss with
+  | [] => pure ()
+  | xs :: _ =>
+    for x in xs rdo
+      s := s + x
+  return s
+
+example : IdM.run (sumHead [[1, 2], [10]]) = 3 := rfl
+
+example : IdM.run (sumHead []) = 0 := rfl
+
+/-- Nested loops whose body binds monadically, at `Measure`. -/
+noncomputable def countPairsOfHeads (n : ℕ) : Measure ℕ := rdo
+  let mut c := 0
+  for _ in List.range n rdo
+    for _ in List.range n rdo
+      let b ← fairCoin
+      if b then
+        c := c + 1
+  return c
+
+/-! ## `while` loops -/
+
+/-- A `while` loop, counting down from `n`. -/
+def countdown (n : ℕ) : IdM ℕ := rdo
+  let mut i := n
+  let mut steps := 0
+  while 0 < i rdo
+    i := i - 1
+    steps := steps + 1
+  return steps
+
+#guard IdM.run (countdown 5) = 5
+
+#guard IdM.run (countdown 0) = 0
+
+/-- `break` out of a `while` loop. -/
+def halveUntilOdd (n : ℕ) : IdM ℕ := rdo
+  let mut k := n
+  while 0 < k rdo
+    if k % 2 = 1 then
+      break
+    k := k / 2
+  return k
+
+#guard IdM.run (halveUntilOdd 24) = 3
+
+#guard IdM.run (halveUntilOdd 0) = 0
+
+/-- An early `return` out of a `while` loop. -/
+def firstSquareAbove (n : ℕ) : IdM ℕ := rdo
+  let mut k := 0
+  while true rdo
+    if k * k > n then
+      return k
+    k := k + 1
+  return 0
+
+#guard IdM.run (firstSquareAbove 10) = 4
+
+/-- `while let`, consuming a list one element at a time. -/
+def sumByPopping (xs : List ℕ) : IdM ℕ := rdo
+  let mut rest := xs
+  let mut s := 0
+  while let x :: xs' := rest rdo
+    s := s + x
+    rest := xs'
+  return s
+
+#guard IdM.run (sumByPopping [1, 2, 3]) = 6
+
+/-- `while h : c`, which hands the body a proof of the condition. -/
+def countdownWithProof (n : ℕ) : IdM ℕ := rdo
+  let mut i := n
+  let mut steps := 0
+  while h : 0 < i rdo
+    have : i - 1 < i := Nat.sub_lt h Nat.one_pos
+    i := i - 1
+    steps := steps + 1
+  return steps
+
+#guard IdM.run (countdownWithProof 4) = 4
+
+/-- A `while` loop nested inside a `for` loop. -/
+def sumOfLogs (xs : List ℕ) : IdM ℕ := rdo
+  let mut s := 0
+  for x in xs rdo
+    let mut k := x
+    while 1 < k rdo
+      k := k / 2
+      s := s + 1
+  return s
+
+#guard IdM.run (sumOfLogs [1, 2, 8]) = 4
+
+/-- A `while` loop at `Measure`: flip a fair coin until it lands heads, counting the flips. -/
+noncomputable def flipsUntilHeads : Measure ℕ := rdo
+  let mut n := 0
+  let mut go := true
+  while go rdo
+    let b ← fairCoin
+    n := n + 1
+    if b then
+      go := false
+  return n
+
 end Test.Loops
 
 end
diff --git a/Test/Polymorphic.lean b/Test/Polymorphic.lean
index 566bf7d..4f417ee 100644
--- a/Test/Polymorphic.lean
+++ b/Test/Polymorphic.lean
@@ -10,9 +10,9 @@ set_option linter.style.header false
 # Polymorphic `rdo` programs
 
 The programs of `Test.Computable`, written once over an arbitrary `MeasurableSpaceMonad` `m` and
-drawing through `HasGaussian` and `HasBernoulli`. Read at `m := Measure`, each one is a probability
-measure, checked by `is_markov`, and is the program of `Test.IsMarkov` when there is one. Run at
-`m := RandM`, it samples.
+drawing through `HasGaussian` and `HasBernoulli`. Read at `m := Measure`, each one without a `while`
+loop is a probability measure, checked by `is_markov`, and is the program of `Test.IsMarkov` when
+there is one. Run at `m := RandM`, it samples.
 -/
 
 @[expose] public section
@@ -114,6 +114,17 @@ example : IsProbabilityMeasure (ex1 (m := Measure) (R := ℝ) (V := NNReal)) :=
 
 run_cmd logPolymorphic (ex1 (m := RandM) (R := Float) (V := Float))
 
+def flipsUntilHeads [HasBernoulli m R] [MeasurableSpaceMonadWhile m] : m ℕ := rdo
+  let mut n := 0
+  while true rdo
+    let heads ← coin (m := m) (0.5 : R)
+    n := n + 1
+    if heads then
+      break
+  return n
+
+run_cmd logPolymorphic (flipsUntilHeads (m := RandM) (R := Float))
+
 end Test.Polymorphic
 
 end