diff --git a/Cslib.lean b/Cslib.lean
index b504973c3..113df9364 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -50,6 +50,7 @@ public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
+public import Cslib.Foundations.Control.Monad.Free.WP
 public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
diff --git a/Cslib/Foundations/Control/Monad/Free/Effects.lean b/Cslib/Foundations/Control/Monad/Free/Effects.lean
index 7c58bca5a..11dd9e6f3 100644
--- a/Cslib/Foundations/Control/Monad/Free/Effects.lean
+++ b/Cslib/Foundations/Control/Monad/Free/Effects.lean
@@ -7,6 +7,7 @@ Authors: Tanner Duve
 module
 
 public import Cslib.Foundations.Control.Monad.Free
+public import Cslib.Foundations.Control.Monad.Free.WP
 public import Mathlib.Control.Monad.Cont
 
 /-!
@@ -39,10 +40,14 @@ Free monad, state monad, writer monad, continuation monad
 
 @[expose] public section
 
+set_option mvcgen.warning false
+
 namespace Cslib
 
 namespace FreeM
 
+open Std.Do
+
 universe u v w w' w''
 
 /-! ### State Monad via `FreeM` -/
@@ -157,6 +162,32 @@ lemma run'_bind (x : FreeState σ α) (f : α → FreeState σ β) (s₀ : σ) :
 
 end FreeState
 
+/-- 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
+
 /-! ### Writer Monad via `FreeM` -/
 
 /--
@@ -453,6 +484,26 @@ instance instMonadWithReaderOf : MonadWithReaderOf σ (FreeReader σ) where
 
 end FreeReader
 
+/-- 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/Cslib/Foundations/Control/Monad/Free/WP.lean b/Cslib/Foundations/Control/Monad/Free/WP.lean
new file mode 100644
index 000000000..6e667a6fc
--- /dev/null
+++ b/Cslib/Foundations/Control/Monad/Free/WP.lean
@@ -0,0 +1,127 @@
+/-
+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 (lift op >>= k) = H op >>= fun x => wpH H (k x) := rfl
+
+@[simp] 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 >>= 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] [LawfulMonad 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]
+  | lift_bind op k ih =>
+    simp [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/CslibTests.lean b/CslibTests.lean
index 7b52a3a31..87709d818 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -5,6 +5,7 @@ public import CslibTests.CCS
 public import CslibTests.CLL
 public import CslibTests.DFA
 public import CslibTests.FreeMonad
+public import CslibTests.FreeMonadWP
 public import CslibTests.GrindLint
 public import CslibTests.HML
 public import CslibTests.HasFresh
diff --git a/CslibTests/FreeMonadWP.lean b/CslibTests/FreeMonadWP.lean
new file mode 100644
index 000000000..69324cbf0
--- /dev/null
+++ b/CslibTests/FreeMonadWP.lean
@@ -0,0 +1,230 @@
+/-
+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
+-/
+
+import Cslib.Foundations.Control.Monad.Free.Effects
+import Std.Tactic.Do
+
+/-!
+Examples for WP in `Cslib.Foundations.Control.Monad.Free.WP`: instance resolution,
+a `Triple` on a `FreeState` program discharged by `mvcgen`, and a custom `CounterF` effect with
+its own logical handler.
+-/
+
+set_option mvcgen.warning false
+
+namespace CslibTests.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
+
+end CslibTests.FreeMonadWP