diff --git a/Algolean.lean b/Algolean.lean
index 013a5ba..b4fa103 100644
--- a/Algolean.lean
+++ b/Algolean.lean
@@ -8,9 +8,12 @@ public import Algolean.Algorithms.ListLinearSearch
 public import Algolean.Algorithms.ListOrderedInsert
 public import Algolean.Algorithms.MergeSort
 public import Algolean.Algorithms.NaivePatternSearch
+public import Algolean.Algorithms.VecBubbleSort
 public import Algolean.Algorithms.VecSearch
 public import Algolean.Complexity.Basic
 public import Algolean.Complexity.PolytimeBasicClasses
+public import Algolean.FreeWP.Effects
+public import Algolean.FreeWP.WP
 public import Algolean.LowerBounds.ComparisonSort
 public import Algolean.Models.Circuits
 public import Algolean.Models.Comparison
diff --git a/Algolean/Algorithms/VecBubbleSort.lean b/Algolean/Algorithms/VecBubbleSort.lean
new file mode 100644
index 0000000..19af78b
--- /dev/null
+++ b/Algolean/Algorithms/VecBubbleSort.lean
@@ -0,0 +1,249 @@
+/-
+Copyright (c) 2026 Tanner Duve (Logical Intelligence). All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tanner Duve
+-/
+
+module
+
+public import Algolean.Models.ReadWriteVec
+public import Mathlib.Data.List.Sort
+public import Std.Tactic.Do
+
+/-!
+# Bubble sort in the read/write vector query model
+
+Bubble sort written as a program in the `Vec` query model (`Prog (Vec α)`), using `read` and
+`write` queries against a mutable vector threaded through `for` loops. This is the worked example
+the query-model WP framework is built for: a *non-trivial* `mvcgen` development establishing full
+functional correctness — both that the output is a permutation of the input and that it is sorted.
+
+The algorithm is split into two pieces, each verified with its own single-loop `mvcgen` proof and
+composed through a Hoare-triple spec (`bubblePass_spec`), which is the idiomatic way to keep loop
+reasoning modular:
+
+- `bubblePass` makes one left-to-right sweep over `[0, bound]`, bubbling the largest element of
+  that range up to position `bound`.
+- `bubbleSort` runs `n` such passes with shrinking bounds `n-1, n-2, …`, growing a sorted suffix.
+
+## Main definitions
+
+- `bubblePass` : one bubbling sweep in the `Vec` query model.
+- `bubbleSort` : bubble sort in the `Vec` query model.
+
+## Main results
+
+- `bubbleSort_perm` : `bubbleSort` returns a permutation of its input.
+- `bubbleSort_sorted` : `bubbleSort` returns a sorted vector (for a total, transitive `le`).
+-/
+
+@[expose] public section
+
+namespace Algolean
+
+namespace Algorithms
+
+open Cslib Prog Std.Do
+
+set_option mvcgen.warning false
+
+/--
+One bubbling sweep in the `Vec` query model: for each adjacent pair `v[j], v[j+1]` with
+`j < bound`, read both and, if out of order under `le`, write them back swapped. After the sweep
+the largest element of `[0, bound]` sits at position `bound`.
+-/
+def bubblePass (le : α → α → Bool) (bound : Nat) (hb : bound < n) (v : Vector α n) :
+    Prog (Vec α) (Vector α n) := do
+  let mut v := v
+  for j in List.finRange bound do
+    let a ← (Vec.read v ⟨j, by lia⟩      : Prog (Vec α) α)
+    let b ← (Vec.read v ⟨j + 1, by lia⟩  : Prog (Vec α) α)
+    if !le a b then
+      v ← (Vec.write v ⟨j, by lia⟩     b : Prog (Vec α) (Vector α n))
+      v ← (Vec.write v ⟨j + 1, by lia⟩ a : Prog (Vec α) (Vector α n))
+  return v
+
+/--
+Bubble sort in the `Vec` query model: run `n` bubbling passes with shrinking bounds. After the
+`k`-th pass the last `k` positions hold the `k` largest elements in sorted order.
+-/
+def bubbleSort (le : α → α → Bool) (v : Vector α n) : Prog (Vec α) (Vector α n) := do
+  let mut v := v
+  for i in List.finRange n do
+    v ← bubblePass le (n - 1 - i) (by lia) v
+  return v
+
+/-! ### Invariants and pointwise lemmas
+
+`MaxAt le w m` says `w[m]` dominates the prefix `[0, m]`; `SortedFrom le w b` says positions
+`[b, n)` are sorted and dominated by the whole prefix. These are the loop invariants, with the
+pointwise lemmas below feeding `mvcgen`'s verification conditions. -/
+
+variable {α : Type} {n : Nat}
+
+/-- `w[m]` is `≥` everything in the prefix `[0, m]`. -/
+def MaxAt (le : α → α → Bool) (w : Vector α n) (m : Nat) : Prop :=
+  ∀ p q : Fin n, (p : Nat) ≤ m → (q : Nat) = m → le w[p] w[q] = true
+
+/-- Positions `[b, n)` are sorted and dominated by the whole prefix. -/
+def SortedFrom (le : α → α → Bool) (w : Vector α n) (b : Nat) : Prop :=
+  ∀ p q : Fin n, (p : Nat) ≤ (q : Nat) → b ≤ (q : Nat) → le w[p] w[q] = true
+
+/-- In a `finRange` split, the cursor element sits at the prefix length. -/
+private theorem fin_cur_eq {pref suff : List (Fin n)} {cur : Fin n}
+    (h : List.finRange n = pref ++ cur :: suff) : (cur : Nat) = pref.length := by
+  have hlt : pref.length < n := by have := congrArg List.length h; simp at this; lia
+  have h2 := congrArg (fun l => l[pref.length]?) h
+  simp only [List.getElem?_append_right (Nat.le_refl pref.length), Nat.sub_self,
+    List.getElem?_cons_zero, List.getElem_finRange,
+    List.getElem?_eq_getElem (show pref.length < (List.finRange n).length by simpa using hlt)] at h2
+  exact (congrArg Fin.val (Option.some.inj h2)).symm
+
+/-- Swapping two entries permutes the underlying list. -/
+private lemma set_set_toList_perm (w : Vector α n) (i j : Nat) (hi : i < n) (hj : j < n) :
+    ((w.set i (w[j]'hj) hi).set j (w[i]'hi) hj).toList.Perm w.toList := by
+  simpa [Vector.toList_set, Vector.getElem_toList] using
+    List.set_set_perm (as := w.toList) (by simpa using hi) (by simpa using hj)
+
+/-- After swapping out-of-order `w[m], w[m+1]`, the prefix maximum moves to `m+1`. -/
+private lemma maxAt_swap (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true)
+    (w : Vector α n) (m : Nat) (hm : m + 1 < n) (hmax : MaxAt le w m)
+    (hsw : le (w[m]'(by lia)) (w[m + 1]'hm) = false) :
+    MaxAt le ((w.set m (w[m + 1]'hm) (by lia)).set (m + 1) (w[m]'(by lia)) hm) (m + 1) := by
+  intro p q hp hq
+  have hcmp := (htot (w[m]'(by lia)) (w[m + 1]'hm)).resolve_left (by simp [hsw])
+  have key : ∀ r : Fin n, (r : Nat) ≤ m → le w[r] (w[m]'(by lia)) = true :=
+    fun r hr => hmax r ⟨m, by lia⟩ hr rfl
+  grind
+
+/-- When the pair is already in order, the prefix maximum still extends to `m+1`. -/
+private lemma maxAt_noswap (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true)
+    (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true)
+    (w : Vector α n) (m : Nat) (hm : m + 1 < n) (hmax : MaxAt le w m)
+    (hns : le (w[m]'(by lia)) (w[m + 1]'hm) = true) : MaxAt le w (m + 1) := by
+  intro p q hp hq
+  have key : ∀ r : Fin n, (r : Nat) ≤ m → le w[r] (w[m]'(by lia)) = true :=
+    fun r hr => hmax r ⟨m, by lia⟩ hr rfl
+  grind
+
+/-- A swap strictly below the boundary `b` preserves the sorted suffix `[b, n)`. -/
+private lemma sortedFrom_swap (le : α → α → Bool) (w : Vector α n) (m b : Nat)
+    (hm : m + 1 < n) (hmb : m + 1 < b) (hsort : SortedFrom le w b) :
+    SortedFrom le ((w.set m (w[m + 1]'hm) (by lia)).set (m + 1) (w[m]'(by lia)) hm) b := by
+  intro p q hp hq
+  have e_m := hsort ⟨m, by lia⟩ q (show m ≤ (q : Nat) by lia) hq
+  have e_m1 := hsort ⟨m + 1, hm⟩ q (show m + 1 ≤ (q : Nat) by lia) hq
+  have hpq := hsort p q hp hq
+  grind
+
+/-- The prefix maximum at `k` extends a sorted suffix `[k+1, n)` to `[k, n)`. -/
+private lemma sortedFrom_of_maxAt (le : α → α → Bool) (w : Vector α n) (k : Nat)
+    (hmax : MaxAt le w k) (hsort : SortedFrom le w (k + 1)) : SortedFrom le w k := by
+  intro p q hp hq
+  rcases Nat.lt_or_ge (q : Nat) (k + 1) with h | h
+  · exact hmax p q (by lia) (by lia)
+  · exact hsort p q hp h
+
+/-- The prefix maximum at `0` is trivial: `w[0] ≥ w[0]`. -/
+private lemma maxAt_zero (le : α → α → Bool) (hrefl : ∀ a, le a a = true) (w : Vector α n) :
+    MaxAt le w 0 := by
+  intro p q hp hq
+  obtain rfl : p = q := by ext; lia
+  exact hrefl _
+
+/-- `SortedFrom le w 0` is exactly sortedness of the underlying list. -/
+private lemma sortedFrom_zero_pairwise {le : α → α → Bool} {w : Vector α n}
+    (h : SortedFrom le w 0) : w.toList.Pairwise (fun a b => le a b = true) := by
+  rw [List.pairwise_iff_getElem]
+  intro i j hi hj _
+  simpa [Vector.getElem_toList] using
+    h ⟨i, by simpa using hi⟩ ⟨j, by simpa using hj⟩ (by simp; lia) (Nat.zero_le _)
+
+private lemma sub_one_sub_add (k : Nat) (h : k < n) : n - 1 - k + 1 = n - k := by lia
+private lemma sub_succ (k : Nat) : n - (k + 1) = n - 1 - k := by lia
+
+/-! ### Hoare specs via `mvcgen`
+
+The two single-loop proofs that carry the work: each calls `mvcgen` with one hand-supplied loop
+invariant, then discharges the (concrete, `grind`-friendly) verification conditions. -/
+
+set_option mvcgen.warning false in
+/-- One pass deposits the maximum of `[0, bound]` at `bound`, preserves the sorted suffix above,
+and permutes the vector. -/
+theorem bubblePass_spec (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)]
+    [IsTrans α (fun a b => le a b = true)]
+    (bound : Nat) (hb : bound < n) (v : Vector α n) (hpre : SortedFrom le v (bound + 1)) :
+    ⦃⌜True⌝⦄ bubblePass le bound hb v
+      ⦃⇓w => ⌜MaxAt le w bound ∧ SortedFrom le w (bound + 1) ∧ w.toList.Perm v.toList⌝⦄ := by
+  mvcgen [bubblePass] invariants
+    · ⇓⟨xs, w⟩ => ⌜MaxAt le w xs.prefix.length ∧ SortedFrom le w (bound + 1)
+        ∧ w.toList.Perm v.toList⌝
+  case vc3.pre =>
+    simp only [List.length_nil]
+    exact ⟨maxAt_zero le (Std.Refl.refl (r := fun a b : α => le a b = true)) v,
+      hpre, List.Perm.refl _⟩
+  case vc4.post.success =>
+    obtain ⟨h1, h2, h3⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _›
+    rw [List.length_finRange] at h1
+    exact ⟨h1, h2, h3⟩
+  case vc1.step.isTrue =>
+    obtain ⟨hmax, hsort, hperm⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _›
+    have hc := fin_cur_eq ‹List.finRange bound = _ ++ _ :: _›
+    have hcb := (‹Fin bound› : Fin bound).isLt
+    have hcmp := ‹(!le _ _) = true›
+    simp only [Vec.hasModel_model, Bool.not_eq_true',
+      List.length_append, List.length_cons, List.length_nil, ← hc] at hmax hcmp hcb ⊢
+    exact ⟨maxAt_swap le Std.Total.total _ _ (by grind) hmax hcmp,
+      sortedFrom_swap le _ _ _ (by grind) (by grind) hsort,
+      (set_set_toList_perm _ _ _ (by grind) (by grind)).trans hperm⟩
+  case vc2.step.isFalse =>
+    obtain ⟨hmax, hsort, hperm⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _›
+    have hc := fin_cur_eq ‹List.finRange bound = _ ++ _ :: _›
+    have hcb := (‹Fin bound› : Fin bound).isLt
+    have hns := ‹¬(!le _ _) = true›
+    simp only [Vec.hasModel_model, Bool.not_eq_true,
+      Bool.not_eq_false', List.length_append, List.length_cons, List.length_nil, ← hc]
+      at hmax hns hcb ⊢
+    exact ⟨maxAt_noswap le Std.Total.total IsTrans.trans _ _ (by lia) hmax hns, hsort, hperm⟩
+
+set_option mvcgen.warning false in
+/-- `bubbleSort` is correct: it sorts and permutes its input (for a total, transitive `le`). -/
+theorem bubbleSort_spec (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)]
+    [IsTrans α (fun a b => le a b = true)] (v : Vector α n) :
+    ⦃⌜True⌝⦄ bubbleSort le v ⦃⇓w => ⌜SortedFrom le w 0 ∧ w.toList.Perm v.toList⌝⦄ := by
+  mvcgen [bubbleSort, bubblePass_spec] invariants
+    · ⇓⟨xs, w⟩ => ⌜SortedFrom le w (n - xs.prefix.length) ∧ w.toList.Perm v.toList⌝
+  case vc1.hpre =>
+    have hsort := (‹SortedFrom le _ _ ∧ List.Perm _ _›).1
+    have hcb := (‹Fin n› : Fin n).isLt
+    rw [fin_cur_eq ‹List.finRange n = _ ++ _ :: _›] at hcb ⊢
+    rwa [sub_one_sub_add _ hcb]
+  case vc2.step.success =>
+    obtain ⟨hmax, hsort, hperm⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _›
+    have hperm0 := (‹SortedFrom le _ _ ∧ List.Perm _ _›).2
+    have key := sortedFrom_of_maxAt le _ _ hmax hsort
+    rw [fin_cur_eq ‹List.finRange n = _ ++ _ :: _›] at key
+    exact ⟨by simp only [List.length_append, List.length_cons, List.length_nil]; rwa [sub_succ],
+      hperm.trans hperm0⟩
+  case vc3.pre =>
+    exact ⟨fun p q _ hq => absurd (by simpa using hq) (by have := q.isLt; lia), List.Perm.refl _⟩
+  case vc4.post.success =>
+    obtain ⟨h1, h2⟩ := ‹SortedFrom le _ _ ∧ List.Perm _ _›
+    rw [List.length_finRange, Nat.sub_self] at h1
+    exact ⟨h1, h2⟩
+
+/-- `bubbleSort` returns a permutation of its input. -/
+theorem bubbleSort_perm (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)]
+    [IsTrans α (fun a b => le a b = true)] (v : Vector α n) :
+    ((bubbleSort le v).eval Vec.natCost).toList.Perm v.toList :=
+  (eval_of_triple (bubbleSort_spec le v)).2
+
+/-- `bubbleSort` returns a sorted vector, for a total and transitive `le`. -/
+theorem bubbleSort_sorted (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)]
+    [IsTrans α (fun a b => le a b = true)] (v : Vector α n) :
+    ((bubbleSort le v).eval Vec.natCost).toList.Pairwise (fun a b => le a b = true) :=
+  sortedFrom_zero_pairwise (eval_of_triple (bubbleSort_spec le v)).1
+
+end Algorithms
+
+end Algolean
diff --git a/Algolean/FreeWP/Effects.lean b/Algolean/FreeWP/Effects.lean
new file mode 100644
index 0000000..38a21c6
--- /dev/null
+++ b/Algolean/FreeWP/Effects.lean
@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2025 Tanner Duve (Logical Intelligence). All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tanner Duve
+-/
+
+module
+
+public import Cslib.Foundations.Control.Monad.Free.Effects
+public import Algolean.FreeWP.WP
+
+/-!
+# Logical handlers for the standard `FreeM` effects
+
+Logical handlers and `HasHandler` instances for the state and reader effects from
+`Cslib.Foundations.Control.Monad.Free.Effects`, each induced by the canonical interpreter
+into the corresponding Lean monad (`StateM`, `ReaderM`) via `Std.Do`'s `WP` instances.
+Adequacy theorems relate the `FreeM`-level WP to the WP of the interpretation, and `@[spec]`
+Hoare triples for the primitive operations enable `mvcgen` reasoning.
+-/
+
+@[expose] public section
+
+set_option mvcgen.warning false
+
+namespace Cslib
+
+namespace FreeM
+
+open Std.Do
+
+universe u
+
+/-! ### State -/
+
+/-- Logical handler for the state effect, induced by `Std.Do`'s `WP (StateM σ)`. -/
+def StateF.handler {σ : Type u} : LHandler (StateF σ) (.arg σ .pure) :=
+  LHandler.ofInterp (m := StateM σ) (fun _ op => FreeState.stateInterp op)
+
+instance StateF.instHasHandler {σ : Type u} :
+    HasHandler (StateF σ) (.arg σ .pure) where
+  handler := StateF.handler
+
+/-- WP of a `FreeState` program matches WP of its `StateM` interpretation. -/
+theorem StateF.wp_FreeState_eq_wp_toStateM {σ α : Type u} (comp : FreeState σ α) :
+    wp comp = wp (FreeState.toStateM comp) :=
+  wpH_ofInterp_eq_wp_liftM (m := StateM σ)
+    (fun _ op => FreeState.stateInterp op) comp
+
+/-- Hoare spec for `get` on `FreeState`. -/
+@[spec]
+theorem Spec.get_FreeState {σ : Type u} {Q : PostCond σ (.arg σ .pure)} :
+    Triple (MonadStateOf.get : FreeState σ σ) (spred(fun s => Q.1 s s)) Q := by
+  mvcgen
+
+/-- Hoare spec for `set` on `FreeState`. -/
+@[spec]
+theorem Spec.set_FreeState {σ : Type u} (s : σ) {Q : PostCond PUnit (.arg σ .pure)} :
+    Triple (MonadStateOf.set s : FreeState σ PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) Q := by
+  mvcgen
+
+/-! ### Reader -/
+
+/-- Logical handler for the reader effect, induced by `Std.Do`'s `WP (ReaderM σ)`. -/
+def ReaderF.handler {σ : Type u} : LHandler (ReaderF σ) (.arg σ .pure) :=
+  LHandler.ofInterp (m := ReaderM σ) (fun _ op => FreeReader.readInterp op)
+
+instance ReaderF.instHasHandler {σ : Type u} :
+    HasHandler (ReaderF σ) (.arg σ .pure) where
+  handler := ReaderF.handler
+
+/-- WP of a `FreeReader` program matches WP of its `ReaderM` interpretation. -/
+theorem ReaderF.wp_FreeReader_eq_wp_toReaderM {σ α : Type u} (comp : FreeReader σ α) :
+    wp comp = wp (FreeReader.toReaderM comp) :=
+  wpH_ofInterp_eq_wp_liftM (m := ReaderM σ)
+    (fun _ op => FreeReader.readInterp op) comp
+
+/-- Hoare spec for `read` on `FreeReader`. -/
+@[spec]
+theorem Spec.read_FreeReader {ρ : Type u} {Q : PostCond ρ (.arg ρ .pure)} :
+    Triple (MonadReaderOf.read : FreeReader ρ ρ) (spred(fun r => Q.1 r r)) Q := by
+  mvcgen
+
+end FreeM
+
+end Cslib
diff --git a/Algolean/FreeWP/WP.lean b/Algolean/FreeWP/WP.lean
new file mode 100644
index 0000000..7782f65
--- /dev/null
+++ b/Algolean/FreeWP/WP.lean
@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2025 Tanner Duve (Logical Intelligence). All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tanner Duve
+-/
+
+module
+
+public import Cslib.Foundations.Control.Monad.Free
+public import Std.Do.PredTrans
+public import Std.Do.WP.Basic
+public import Std.Do.WP.Monad
+public import Std.Do.Triple
+
+/-!
+# Weakest preconditions for `FreeM` programs
+
+Weakest-precondition interpretation of `FreeM F` programs through `Std.Do`'s
+predicate-transformer monad `PredTrans ps`. The universal property of `FreeM` lifts any
+effect handler `F ι → PredTrans ps ι` to a unique monad morphism `wpH H = liftM H`,
+so weakest preconditions are compositional in `FreeM`'s monadic structure. A
+`[HasHandler F ps]` instance plugs `FreeM F` into `Std.Do`'s `WP`/`WPMonad`/`Triple`
+infrastructure.
+
+The WP's structural rules (`wpH_pure`, `wpH_bind`, …) are immediate from `liftM` being a monad
+morphism; the adequacy theorem `wpH_ofInterp_eq_wp_liftM` — that WP-via-handler agrees with
+`Std.Do`'s WP of the `liftM` interpretation — is the same statement of uniqueness.
+
+The design follows [Vistrup, Sammler, Jung. *Program Logics à la Carte.* POPL 2025], adapted
+from coinductive ITrees to inductive `FreeM` and from Iris to `Std.Do`.
+-/
+
+@[expose] public section
+
+set_option mvcgen.warning false
+
+namespace Cslib
+
+open Std.Do
+
+namespace FreeM
+
+universe u v w
+
+variable {F G : Type u → Type v} {ps : PostShape.{u}} {α β : Type u}
+
+/-- A logical handler: an effect handler from `F` into the predicate-transformer monad
+`PredTrans ps`. -/
+abbrev LHandler (F : Type u → Type v) (ps : PostShape.{u}) : Type (max (u + 1) v) :=
+  ∀ {ι : Type u}, F ι → PredTrans ps ι
+
+namespace LHandler
+
+/-- Sum of handlers; the counterpart of the paper's `H₁ ⊕ H₂`. -/
+def sum (H₁ : LHandler F ps) (H₂ : LHandler G ps) :
+    LHandler (fun α => F α ⊕ G α) ps :=
+  fun op => Sum.elim H₁ H₂ op
+
+@[simp] theorem sum_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps)
+    {ι : Type u} (x : F ι) :
+    LHandler.sum H₁ H₂ (Sum.inl x : F ι ⊕ G ι) = H₁ x := rfl
+
+@[simp] theorem sum_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps)
+    {ι : Type u} (y : G ι) :
+    LHandler.sum H₁ H₂ (Sum.inr y : F ι ⊕ G ι) = H₂ y := rfl
+
+/-- Derive a logical handler from an effect handler into any `[WP m ps]` monad, by composing
+with `m`'s WP. -/
+def ofInterp {m : Type u → Type w} [WP m ps]
+    (interp : ∀ ι : Type u, F ι → m ι) : LHandler F ps :=
+  fun {ι} op => wp (interp ι op)
+
+@[simp] theorem ofInterp_apply {m : Type u → Type w} [WP m ps]
+    (interp : ∀ ι : Type u, F ι → m ι) {ι : Type u} (op : F ι) :
+    LHandler.ofInterp interp op = wp (interp ι op) := rfl
+
+end LHandler
+
+/-- Weakest-precondition interpretation of a `FreeM F α` program against a logical handler `H`.
+Defined as `FreeM.liftM` instantiated at `PredTrans ps`, the unique monad morphism
+`FreeM F → PredTrans ps` extending `H` per the universal property of `FreeM`. -/
+def wpH (H : LHandler F ps) (x : FreeM F α) : PredTrans ps α :=
+  x.liftM H
+
+@[simp] theorem wpH_pure (H : LHandler F ps) (a : α) :
+    wpH H (.pure a : FreeM F α) = Pure.pure a := rfl
+
+@[simp] theorem wpH_liftBind (H : LHandler F ps) {ι : Type u}
+    (op : F ι) (k : ι → FreeM F α) :
+    wpH H (liftBind op k) = H op >>= fun x => wpH H (k x) := rfl
+
+theorem wpH_lift (H : LHandler F ps) {ι : Type u} (op : F ι) :
+    wpH H (lift op : FreeM F ι) = H op :=
+  liftM_lift _ op
+
+@[simp] theorem wpH_bind (H : LHandler F ps) (x : FreeM F α) (f : α → FreeM F β) :
+    wpH H (x.bind f) = wpH H x >>= fun a => wpH H (f a) :=
+  liftM_bind _ x f
+
+/-- Adequacy theorem: WP via `FreeM` against an `ofInterp`-derived handler agrees with
+`Std.Do`'s WP of the `liftM` interpretation. Equivalently, two monad morphisms
+`FreeM F → PredTrans ps` extending the same handler are equal. -/
+theorem wpH_ofInterp_eq_wp_liftM
+    {m : Type u → Type w} [Monad m] [WPMonad m ps]
+    (interp : ∀ ι : Type u, F ι → m ι) (x : FreeM F α) :
+    wpH (LHandler.ofInterp interp) x = wp (x.liftM (fun {_} => interp _)) := by
+  induction x with
+  | pure a => simp [wpH, FreeM.liftM, WPMonad.wp_pure]
+  | liftBind op k ih =>
+    simp only [wpH] at ih ⊢
+    simp [liftM_liftBind, WPMonad.wp_bind, ih]
+
+/-- Records a default logical handler for `F` at shape `ps`, enabling the global
+`WP (FreeM F) ps` instance and any `Triple`/`mvcgen` reasoning over `FreeM F`. -/
+class HasHandler (F : Type u → Type v) (ps : outParam (PostShape.{u})) where
+  /-- The default logical handler for `F`. -/
+  handler {ι : Type u} : F ι → PredTrans ps ι
+
+instance instWPFreeM [HasHandler F ps] : WP (FreeM F) ps where
+  wp := wpH HasHandler.handler
+
+instance instWPMonadFreeM [HasHandler F ps] : WPMonad (FreeM F) ps where
+  wp_pure _ := rfl
+  wp_bind x f := wpH_bind _ x f
+
+end FreeM
+
+end Cslib
diff --git a/Algolean/Models/ReadOnlyVec.lean b/Algolean/Models/ReadOnlyVec.lean
index be911d8..3684da7 100644
--- a/Algolean/Models/ReadOnlyVec.lean
+++ b/Algolean/Models/ReadOnlyVec.lean
@@ -44,6 +44,12 @@ def ReadOnlyVec.natCost : Model (ReadOnlyVec α) ℕ where
     | .read a i => a[i]
   cost _ := 1
 
+/-- Register `natCost` as the default model for `ReadOnlyVec`, so the global
+`WP (Prog (ReadOnlyVec α)) .pure` / `HasHandler` instances fire and `Triple`/`mvcgen` reasoning
+works on read-only-vector programs out of the box. -/
+instance : HasModel (ReadOnlyVec α) ℕ where
+  model := ReadOnlyVec.natCost
+
 end Algorithms
 
 end Algolean
diff --git a/Algolean/Models/ReadWriteVec.lean b/Algolean/Models/ReadWriteVec.lean
index 007b81e..ad2e431 100644
--- a/Algolean/Models/ReadWriteVec.lean
+++ b/Algolean/Models/ReadWriteVec.lean
@@ -49,6 +49,17 @@ def Vec.natCost : Model (Vec α) ℕ where
     | .write a i x => a.set i x
   cost _ := 1
 
+/-- Register `natCost` as the default model for `Vec`, so the global
+`WP (Prog (Vec α)) .pure` / `HasHandler` instances fire and `Triple`/`mvcgen` reasoning works on
+read/write-vector programs out of the box. Both `Vec` cost models share the same `evalQuery`, so
+this choice fixes only the functional semantics used by the weakest-precondition handler. -/
+instance : HasModel (Vec α) ℕ where
+  model := Vec.natCost
+
+/-- The default `Vec` model unfolds to `natCost`; lets `mvcgen` reduce `evalQuery` on `Vec`
+programs to concrete `read`/`write` semantics. -/
+@[simp] theorem Vec.hasModel_model : (HasModel.model : Model (Vec α) ℕ) = Vec.natCost := rfl
+
 
 section VecModel
 
diff --git a/Algolean/QueryModel.lean b/Algolean/QueryModel.lean
index 991563b..b307b07 100644
--- a/Algolean/QueryModel.lean
+++ b/Algolean/QueryModel.lean
@@ -9,6 +9,7 @@ module
 public import Cslib
 public import Cslib.Foundations.Control.Monad.Free
 public import Algolean.AddWriter.Basic
+public import Algolean.FreeWP.WP
 
 @[expose] public section
 
@@ -206,6 +207,74 @@ theorem FreeM.bind_eq_bind {α β : Type w}
 
 end FreeMExtras
 
+section WeakestPrecondition
+/-!
+## Weakest preconditions for query programs
+
+A `Prog Q α` is by definition a `FreeM Q α`, so the weakest-precondition framework of
+`Algolean.FreeWP.WP` applies to query-model algorithms verbatim. The bridge is a *logical handler*
+read off a model: a `Model Q Cost` already carries an interpreter `evalQuery : Q ι → ι`, and viewing
+that as an interpreter into `Id` produces a handler at the pure post-shape `.pure`, against which
+we can state Hoare triples about the *result value* a program computes under the model.
+
+The cost field plays no role here — `.pure` tracks only the returned value — so the construction
+works for a model over *any* cost type, with no algebraic structure required. To register a query
+type's canonical model as the default for `mvcgen`/`Triple` reasoning, provide a `HasModel`
+instance; the global `WP (Prog Q) .pure` instance then fires automatically.
+-/
+
+open Cslib Cslib.FreeM Std.Do
+
+variable {Q : Type u → Type v} {Cost : Type w} {ι α : Type u}
+
+/-- The logical handler induced by a model `M : Model Q Cost`: interpret each query through
+`M.evalQuery` into `Id` (where `pure` is the identity), then take its weakest precondition at the
+pure post-shape. This is the bridge that turns a query model into a `Std.Do` effect, so
+`mvcgen`/`Triple` reasoning works on any `Prog Q α`. -/
+def Model.handler (M : Model Q Cost) : LHandler Q .pure :=
+  LHandler.ofInterp (m := Id) (fun _ q => M.evalQuery q)
+
+/-- A query type equipped with a designated default cost model. Registering an instance lets the
+generic `HasHandler`/`WP (Prog Q) .pure` instances fire, so query programs plug into
+`Std.Do`'s `Triple`/`mvcgen` infrastructure with no per-type boilerplate. -/
+class HasModel (Q : Type u → Type v) (Cost : outParam (Type w)) where
+  /-- The designated default model for `Q`. -/
+  model : Model Q Cost
+
+/-- Generic handler instance: every query type with a default `HasModel` gets the WP framework at
+the pure post-shape, induced by that model. This is the single instance that "generates" a handler
+for an arbitrary model. -/
+instance instHasHandlerOfModel [HasModel Q Cost] : HasHandler Q .pure where
+  handler := (HasModel.model (Cost := Cost)).handler
+
+/-- Adequacy for the query model: the WP of a query program against a model's handler agrees with
+`Std.Do`'s WP of its `Id`-interpretation under that model — i.e. with what the program
+`eval`uates to. -/
+theorem Model.wp_eq_wp_interp (M : Model Q Cost) (P : Prog Q α) :
+    wpH M.handler P = wp (P.liftM (fun {_} q => (M.evalQuery q : Id _))) :=
+  wpH_ofInterp_eq_wp_liftM (m := Id) (fun _ q => M.evalQuery q) P
+
+/-- The single-query Hoare spec, generic over any registered model: to establish postcondition `Q'`
+after running a query `q`, it suffices that `Q'` holds of the value `HasModel.model.evalQuery q`
+that the model returns. Tagged `@[spec]` so `mvcgen` discharges every lifted query automatically. -/
+@[spec]
+theorem Spec.query [HasModel Q Cost] (q : Q ι) {Q' : PostCond ι .pure} :
+    Triple (FreeM.lift q : Prog Q ι)
+      (Q'.1 ((HasModel.model : Model Q Cost).evalQuery q)) Q' :=
+  Triple.iff.mpr SPred.entails.rfl
+
+/-- Adequacy bridge: a pure-shape Hoare triple with trivial precondition yields a fact about the
+value the program `eval`uates to under the registered model. This turns an `mvcgen` proof about a
+`Prog Q` program directly into a statement about `Prog.eval`. -/
+theorem eval_of_triple [HasModel Q Cost] {prog : Prog Q α} {φ : α → Prop}
+    (h : ⦃⌜True⌝⦄ prog ⦃⇓r => ⌜φ r⌝⦄) :
+    φ (prog.eval (HasModel.model : Model Q Cost)) :=
+  Id.of_wp_run_eq
+    (prog := prog.liftM (fun {_} q => ((HasModel.model : Model Q Cost).evalQuery q : Id _)))
+    rfl φ (by rw [← (HasModel.model : Model Q Cost).wp_eq_wp_interp prog]; exact h)
+
+end WeakestPrecondition
+
 end Algorithms
 
 end Algolean
diff --git a/AlgoleanTests.lean b/AlgoleanTests.lean
index 87c80c8..523359e 100644
--- a/AlgoleanTests.lean
+++ b/AlgoleanTests.lean
@@ -1,6 +1,7 @@
 module  -- shake: keep-all
 
 public import AlgoleanTests.CircuitExamples
+public import AlgoleanTests.FreeMonadWP
 public import AlgoleanTests.KMPExamples
 public import AlgoleanTests.NaivePatternSearchExamples
 public import AlgoleanTests.ProgExamples
diff --git a/AlgoleanTests/FreeMonadWP.lean b/AlgoleanTests/FreeMonadWP.lean
new file mode 100644
index 0000000..7ea6364
--- /dev/null
+++ b/AlgoleanTests/FreeMonadWP.lean
@@ -0,0 +1,284 @@
+/-
+Copyright (c) 2025 Tanner Duve (Logical Intelligence). All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tanner Duve
+-/
+
+module
+
+public import Algolean.FreeWP.Effects
+public import Algolean.Models.ReadOnlyVec
+public import Std.Tactic.Do
+
+/-!
+Examples for WP in `Algolean.FreeWP.WP`: instance resolution,
+a `Triple` on a `FreeState` program discharged by `mvcgen`, a custom `CounterF` effect with
+its own logical handler, sum/failure/demonic effects, and — connecting the WP framework to this
+repository's query model — Hoare triples about query-model programs `Prog Q α` against a handler
+derived from a `Model Q Cost` (illustrated on `ReadOnlyVec`).
+-/
+
+@[expose] public section
+
+set_option mvcgen.warning false
+
+namespace AlgoleanTests.FreeMonadWP
+
+open Cslib Cslib.FreeM Std.Do
+
+example : WP (FreeState Nat) (.arg Nat .pure) := inferInstance
+example : WPMonad (FreeState Nat) (.arg Nat .pure) := inferInstance
+example : WP (FreeReader Nat) (.arg Nat .pure) := inferInstance
+example : HasHandler (StateF Nat) (.arg Nat .pure) := inferInstance
+
+/-- Increment the natural-number state by 1. -/
+def incr : FreeState Nat Unit := do
+  let n ← MonadStateOf.get
+  MonadStateOf.set (n + 1)
+
+example : wp incr = wp (FreeState.toStateM incr) :=
+  StateF.wp_FreeState_eq_wp_toStateM incr
+
+/-- Starting in state `n`, `incr` ends in state `n + 1`. `mvcgen` picks up the `@[spec]` lemmas
+for `MonadStateOf.get`/`set` on `FreeState` and discharges the resulting arithmetic VC. -/
+example (n : Nat) :
+    ⦃fun s => ⌜s = n⌝⦄ (incr : FreeState Nat Unit) ⦃⇓ _ s' => ⌜s' = n + 1⌝⦄ := by
+  mvcgen
+  intro s heq
+  subst heq
+  rfl
+
+/-- A counter effect with two operations. -/
+inductive CounterF : Type → Type where
+  /-- Increment the counter by one. -/
+  | tick : CounterF Unit
+  /-- Read the counter's value. -/
+  | read : CounterF Nat
+
+/-- Counter programs built from `CounterF`. -/
+abbrev FreeCounter := FreeM CounterF
+
+namespace CounterF
+
+/-- Effect handler for `CounterF` into `StateM Nat`, used to seed both the executable
+semantics and the logical handler. -/
+def interp : ∀ ι : Type, CounterF ι → StateM Nat ι
+  | _, .tick => modify (· + 1)
+  | _, .read => MonadStateOf.get
+
+/-- Logical handler for `CounterF` induced by `interp` and `Std.Do`'s `WP (StateM Nat)`
+instance. -/
+def handler : LHandler CounterF (.arg Nat .pure) :=
+  LHandler.ofInterp CounterF.interp
+
+instance : HasHandler CounterF (.arg Nat .pure) where
+  handler := CounterF.handler
+
+/-- Interpret counter programs as `StateM Nat` programs. -/
+abbrev toStateM {α : Type} (comp : FreeCounter α) : StateM Nat α :=
+  comp.liftM (fun {ι} => CounterF.interp ι)
+
+/-- Adequacy theorem specialized to `CounterF`. -/
+theorem wp_FreeCounter_eq_wp_toStateM {α : Type} (comp : FreeCounter α) :
+    wp comp = wp (CounterF.toStateM comp) :=
+  wpH_ofInterp_eq_wp_liftM (m := StateM Nat) CounterF.interp comp
+
+end CounterF
+
+/-- Smart constructor: tick the counter as a `FreeCounter` action. -/
+abbrev tick : FreeCounter Unit := lift CounterF.tick
+
+/-- Smart constructor: read the counter as a `FreeCounter` action. -/
+abbrev readCounter : FreeCounter Nat := lift CounterF.read
+
+/-- Tick three times, then read out the counter. -/
+def threeTicks : FreeCounter Nat := do
+  tick; tick; tick
+  readCounter
+
+/--
+Triple about the counter program: starting at `0`, the final value is `3` and the final state
+is `3`. Proven by the same bridge-then-`mvcgen` pattern as `incr`.
+-/
+example :
+    ⦃fun s => ⌜s = 0⌝⦄ threeTicks ⦃⇓ v s => ⌜v = 3 ∧ s = 3⌝⦄ := by
+  mvcgen
+  intro s seq0
+  subst seq0
+  exact ⟨rfl, rfl⟩
+
+/-- A failure effect with one operation `fail` of empty answer type. -/
+inductive FailF : Type → Type where
+  /-- Abort the computation. -/
+  | fail : FailF PEmpty.{1}
+
+/-- Logical handler for `FailF`: `fail` has precondition `⌜False⌝`, so it is only provable in
+unreachable branches. -/
+def FailF.handler {ps : PostShape} : LHandler FailF ps :=
+  fun op => match op with
+    | .fail => PredTrans.const spred(⌜False⌝)
+
+/-- A combined state + failure signature, sequencing `StateF Nat` with `FailF`. -/
+abbrev StateFail := fun α => StateF Nat α ⊕ FailF α
+
+/-- Handler for the combined signature: the sum of the component handlers — the paper's
+`H₁ ⊕ H₂` composition. -/
+instance : HasHandler StateFail (.arg Nat .pure) where
+  handler := StateF.handler.sum FailF.handler
+
+/-- Smart constructor for state-read in the combined signature. -/
+abbrev sfGet : FreeM StateFail Nat := lift (Sum.inl StateF.get)
+
+/-- Smart constructor for state-write in the combined signature. -/
+abbrev sfSet (n : Nat) : FreeM StateFail PUnit := lift (Sum.inl (StateF.set n))
+
+/-- Smart constructor for failure in the combined signature, eliminated to any return type via
+`PEmpty.elim`. -/
+abbrev sfFail {α : Type} : FreeM StateFail α :=
+  lift (Sum.inr FailF.fail) >>= PEmpty.elim
+
+/-- Hoare spec for the sum-lifted state-read. -/
+@[spec]
+theorem Spec.sfGet {Q : PostCond Nat (.arg Nat .pure)} :
+    Triple sfGet (spred(fun s => Q.1 s s)) Q := by
+  mvcgen
+
+/-- Hoare spec for the sum-lifted state-write. -/
+@[spec]
+theorem Spec.sfSet (n : Nat) {Q : PostCond PUnit (.arg Nat .pure)} :
+    Triple (sfSet n) (spred(fun _ => Q.1 ⟨⟩ n)) Q := by
+  mvcgen
+
+/-- Hoare spec for sum-lifted failure: requires `False` to verify. -/
+@[spec]
+theorem Spec.sfFail {α : Type} {Q : PostCond α (.arg Nat .pure)} :
+    Triple (sfFail : FreeM StateFail α) (spred(⌜False⌝)) Q := by
+  mvcgen
+
+/-- A non-branching program in the combined signature: read the state, then write
+`state + 1`. Shows that the sum handler composes the StateF and FailF specs cleanly. -/
+def getAndBump : FreeM StateFail Unit := do
+  let n ← sfGet
+  sfSet (n + 1)
+
+/-- `getAndBump` advances the state by 1, proven through the sum handler. -/
+example (n : Nat) :
+    ⦃fun s => ⌜s = n⌝⦄ (getAndBump : FreeM StateFail Unit)
+      ⦃⇓ _ s => ⌜s = n + 1⌝⦄ := by
+  mvcgen
+  intro s a
+  subst a
+  rfl
+
+/-- Increment the state if it's strictly below `limit`, otherwise fail. Branches on the state's
+value and uses `sfFail` in the else branch. -/
+def bumpUnder (limit : Nat) : FreeM StateFail Unit := do
+  let n ← sfGet
+  if n < limit then sfSet (n + 1) else sfFail
+
+/-- Starting in a state below `limit`, `bumpUnder` increments without failing — the failure
+branch is unreachable because the precondition rules it out. -/
+example (limit n : Nat) (hlt : n < limit) :
+    ⦃fun s => ⌜s = n⌝⦄ (bumpUnder limit : FreeM StateFail Unit)
+      ⦃⇓ _ s => ⌜s = n + 1⌝⦄ := by
+  unfold bumpUnder
+  mvcgen <;> aesop
+
+/-- Demonic non-determinism: a single operation `choice α` that abstractly returns an arbitrary
+`a : α`. Verification must consider all possible values of `a`. -/
+inductive DemonicF : Type → Type 1 where
+  /-- Choose an element of `α`. -/
+  | choice (α : Type) : DemonicF α
+
+/-- Logical handler for `DemonicF`: the predicate transformer for `choice α` is universal
+quantification over `α`. Conjunctivity of `∀` (i.e. `∀ a, P a ∧ Q a ⊣⊢ (∀ a, P a) ∧ (∀ a, Q a)`)
+is what makes this admissible in `PredTrans`. -/
+def DemonicF.handler {ps : PostShape} : LHandler DemonicF ps :=
+  fun op => match op with
+    | .choice _ =>
+      { trans := fun Q => SPred.forall (fun a => Q.1 a)
+        conjunctiveRaw := by
+          intro Q₁ Q₂
+          apply SPred.bientails.iff.mpr
+          refine ⟨?_, ?_⟩
+          · apply SPred.and_intro
+            · apply SPred.forall_intro
+              intro a
+              exact (SPred.forall_elim a).trans SPred.and_elim_l
+            · apply SPred.forall_intro
+              intro a
+              exact (SPred.forall_elim a).trans SPred.and_elim_r
+          · apply SPred.forall_intro
+            intro a
+            apply SPred.and_intro
+            · exact SPred.and_elim_l.trans (SPred.forall_elim a)
+            · exact SPred.and_elim_r.trans (SPred.forall_elim a) }
+
+instance : HasHandler DemonicF .pure where
+  handler := DemonicF.handler
+
+/-- Smart constructor for demonic choice over `α`. -/
+abbrev demonic (α : Type) : FreeM DemonicF α := lift (DemonicF.choice α)
+
+/-- Triple for `demonic α`: the precondition must imply the postcondition for *every* `a : α`. -/
+@[spec]
+theorem Spec.demonic {α : Type} {Q : PostCond α .pure} :
+    Triple (demonic α) (SPred.forall (fun a : α => Q.1 a)) Q :=
+  Triple.iff.mpr SPred.entails.rfl
+
+/-- A demonic Bool: the precondition must hold for both `true` and `false`. -/
+example {Q : PostCond Bool .pure} :
+    Triple (demonic Bool) (SPred.and (Q.1 true) (Q.1 false)) Q :=
+    fun ⟨ht, hf⟩ b =>
+    match b with
+    | true => ht
+    | false => hf
+
+/-! ### Query-model programs
+
+The repository's query model defines `Prog Q α := FreeM Q α`, and `Algolean.QueryModel` wires every
+query model into this WP framework: `Model.handler` reads a logical handler off a model's
+`evalQuery` at the pure post-shape, a `HasModel` instance registers a query type's default model,
+and the generic `Spec.query` discharges single queries under `mvcgen`. So Hoare triples about the
+*result value* a query program computes are available with no per-example setup.
+
+We illustrate with `ReadOnlyVec`, whose `HasModel (ReadOnlyVec α) ℕ` instance (via
+`ReadOnlyVec.natCost`, in `Algolean.Models.ReadOnlyVec`) makes the global
+`WP (Prog (ReadOnlyVec α)) .pure` instance fire automatically. -/
+
+open Algolean Algolean.Algorithms
+
+/-- The WP framework is available on query programs with no local setup — the handler instance is
+generated from the registered model. -/
+example {α : Type} : WP (Prog (ReadOnlyVec α)) .pure := inferInstance
+
+/-- Adequacy, specialized to `ReadOnlyVec` from the generic `Model.wp_eq_wp_interp`: the WP of a
+program agrees with the WP of its `Id`-interpretation under `natCost`, i.e. with what the program
+actually `eval`uates to. -/
+example {α β : Type} (P : Prog (ReadOnlyVec α) β) :
+    wp P = wp (P.liftM (fun {_} q => (ReadOnlyVec.natCost.evalQuery q : Id _))) :=
+  ReadOnlyVec.natCost.wp_eq_wp_interp P
+
+/-- Read indices `i` then `j` of a vector and return the pair of values. Queries lift into `Prog`
+automatically through the `CoeOut` coercion, so no explicit `lift` is needed. -/
+def readTwo {α : Type} {n : Nat} (a : Vector α n) (i j : Fin n) :
+    Prog (ReadOnlyVec α) (α × α) := do
+  let x ← ReadOnlyVec.read a i
+  let y ← ReadOnlyVec.read a j
+  pure (x, y)
+
+/-- Functional correctness of `readTwo`: it returns exactly `(a[i], a[j])`. The two `read`
+specs compose through the `bind` rule, and `mvcgen` discharges the program. -/
+example {α : Type} {n : Nat} (a : Vector α n) (i j : Fin n) :
+    ⦃⌜True⌝⦄ (readTwo a i j) ⦃⇓ r => ⌜r = (a[i], a[j])⌝⦄ := by
+  mvcgen
+
+/-- A read program whose result depends on the data: read index `i`, and if the value equals
+`x`, the answer is `true`. The triple shows the verifier sees the concrete element `a[i]`. -/
+example {n : Nat} (a : Vector Nat n) (i : Fin n) (x : Nat) :
+    ⦃⌜True⌝⦄
+      (do let v ← ReadOnlyVec.read a i; pure (v == x) : Prog (ReadOnlyVec Nat) Bool)
+    ⦃⇓ r => ⌜r = (a[i] == x)⌝⦄ := by
+  mvcgen
+
+end AlgoleanTests.FreeMonadWP