diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index b4db1342d4..8fcb1e7dc2 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -2100,6 +2100,68 @@ introductions in sequence.
 macro (name := mintroMacro) (priority:=low) "mintro" : tactic =>
   Macro.throwError "to use `mintro`, please include `import Std.Tactic.Do`"
 
+/--
+`mspec` is an `apply`-like tactic that applies a Hoare triple specification to the target of the
+stateful goal.
+
+Given a stateful goal `H ⊢ₛ wp⟦prog⟧.apply Q'`, `mspec foo_spec` will instantiate
+`foo_spec : ... → ⦃P⦄ foo ⦃Q⦄`, match `foo` against `prog` and produce subgoals for
+the verification conditions `?pre : H ⊢ₛ P` and `?post : Q ⊢ₚ Q'`.
+
+* If `prog = x >>= f`, then `mspec Specs.bind` is tried first so that `foo` is matched against `x`
+  instead. Tactic `mspec_no_bind` does not attempt to do this decomposition.
+* If `?pre` or `?post` follow by `.rfl`, then they are discharged automatically.
+* `?post` is automatically simplified into constituent `⊢ₛ` entailments on
+  success and failure continuations.
+* `?pre` and `?post.*` goals introduce their stateful hypothesis as `h`.
+* Any uninstantiated MVar arising from instantiation of `foo_spec` becomes a new subgoal.
+* If the goal looks like `fun s => _ ⊢ₛ _` then `mspec` will first `mintro ∀s`.
+* If `P` has schematic variables that can be instantiated by doing `mintro ∀s`, for example
+  `foo_spec : ∀(n:Nat), ⦃⌜n = ‹Nat›ₛ⌝⦄ foo ⦃Q⦄`, then `mspec` will do `mintro ∀s` first to
+  instantiate `n = s`.
+* Right before applying the spec, the `mframe` tactic is used, which has the following effect:
+  Any hypothesis `Hᵢ` in the goal `h₁:H₁, h₂:H₂, ..., hₙ:Hₙ ⊢ₛ T` that is
+  pure (i.e., equivalent to some `⌜φᵢ⌝`) will be moved into the pure context as `hᵢ:φᵢ`.
+
+Additionally, `mspec` can be used without arguments or with a term argument:
+
+* `mspec` without argument will try and look up a spec for `x` registered with `@[spec]`.
+* `mspec (foo_spec blah ?bleh)` will elaborate its argument as a term with expected type
+  `⦃?P⦄ x ⦃?Q⦄` and introduce `?bleh` as a subgoal.
+  This is useful to pass an invariant to e.g., `Specs.forIn_list` and leave the inductive step
+  as a hole.
+-/
+macro (name := mspecMacro) (priority:=low) "mspec" : tactic =>
+  Macro.throwError "to use `mspec`, please include `import Std.Tactic.Do`"
+
+/--
+`mvcgen` will break down a Hoare triple proof goal like `⦃P⦄ prog ⦃Q⦄` into verification conditions,
+provided that all functions used in `prog` have specifications registered with `@[spec]`.
+
+A verification condition is an entailment in the stateful logic of `Std.Do.SPred`
+in which the original program `prog` no longer occurs.
+Verification conditions are introduced by the `mspec` tactic; see the `mspec` tactic for what they
+look like.
+When there's no applicable `mspec` spec, `mvcgen` will try and rewrite an application
+`prog = f a b c` with the simp set registered via `@[spec]`.
+
+When used like `mvcgen +noLetElim [foo_spec, bar_def, instBEqFloat]`, `mvcgen` will additionally
+
+* add a Hoare triple specification `foo_spec : ... → ⦃P⦄ foo ... ⦃Q⦄` to `spec` set for a
+  function `foo` occurring in `prog`,
+* unfold a definition `def bar_def ... := ...` in `prog`,
+* unfold any method of the `instBEqFloat : BEq Float` instance in `prog`.
+* it will no longer substitute away `let`-expressions that occur at most once in `P`, `Q` or `prog`.
+
+Furthermore, `mvcgen` tries to close trivial verification conditions by `SPred.entails.rfl` or
+the tactic sequence `try (mpure_intro; trivial)`. The variant `mvcgen_no_trivial` does not do this.
+
+For debugging purposes there is also `mvcgen_step 42` which will do at most 42 VC generation
+steps. This is useful for bisecting issues with the generated VCs.
+-/
+macro (name := mvcgenMacro) (priority:=low) "mvcgen" : tactic =>
+  Macro.throwError "to use `mvcgen`, please include `import Std.Tactic.Do`"
+
 end Tactic
 
 namespace Attr
diff --git a/src/Lean/Elab/Tactic/Do.lean b/src/Lean/Elab/Tactic/Do.lean
index 620d690d8e..277e516a93 100644
--- a/src/Lean/Elab/Tactic/Do.lean
+++ b/src/Lean/Elab/Tactic/Do.lean
@@ -5,3 +5,8 @@ Authors: Sebastian Graf
 -/
 prelude
 import Lean.Elab.Tactic.Do.ProofMode
+import Lean.Elab.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.Attr
+import Lean.Elab.Tactic.Do.LetElim
+import Lean.Elab.Tactic.Do.Spec
+import Lean.Elab.Tactic.Do.VCGen
diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean
new file mode 100644
index 0000000000..5bcd1c22b7
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Do/Attr.lean
@@ -0,0 +1,235 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Lean.Meta
+import Std.Do.Triple.Basic
+import Std.Tactic.Do.Syntax
+
+namespace Lean.Elab.Tactic.Do.SpecAttr
+
+open Lean Meta Std.Do
+
+builtin_initialize registerTraceClass `Elab.Tactic.Do.specAttr
+
+/--
+  This attribute should not be used directly.
+  It is an implementation detail of the `mvcgen` tactic.
+-/
+builtin_initialize mvcgenSimpExt : Meta.SimpExtension ←
+  Meta.registerSimpAttr `mvcgen_simp "simp theorems internally used by `mvcgen`"
+
+/--
+  The simp set accumulated by the `@[spec]` attribute.
+  (This does not include Hoare triple specs.)
+  It is an implementation detail of the `mvcgen` tactic.
+-/
+def getSpecSimpTheorems : CoreM SimpTheorems :=
+  mvcgenSimpExt.getTheorems
+
+inductive SpecProof where
+  | global (declName : Name)
+  | local (fvarId : FVarId)
+  | stx (id : Name) (ref : Syntax) (proof : Expr)
+  deriving Inhabited, BEq
+
+/-- A unique identifier corresponding to the origin. -/
+def SpecProof.key : SpecProof → Name
+  | .global declName => declName
+  | .local fvarId => fvarId.name
+  | .stx id _ _ => id
+
+instance : Hashable SpecProof where
+  hash sp := hash sp.key
+
+def SpecProof.instantiate (proof : SpecProof) : MetaM (Array Expr × Array BinderInfo × Expr × Expr) := do
+  let prf ← match proof with
+    | .global declName => mkConstWithFreshMVarLevels declName
+    | .local fvarId => pure <| mkFVar fvarId
+    | .stx _ _ proof => pure proof -- TODO: Think about simp-like generalization
+  -- We instantiate here deeply specifically for local hypotheses, the type of which
+  -- may contain MVars at multiple levels.
+  -- An example is `ih` in `serialize_bytesize` from the serialization schema test
+  let type ← instantiateMVars (← inferType prf)
+  let (xs, bs, type) ← forallMetaTelescope type
+  return (xs, bs, prf.beta xs, type)
+
+instance : ToMessageData SpecProof where
+  toMessageData := fun
+    | .global declName => m!"SpecProof.global {declName}"
+    | .local fvarId => m!"SpecProof.local {mkFVar fvarId}"
+    | .stx _ ref proof => m!"SpecProof.stx _ {ref} {proof}"
+
+structure SpecTheorem where
+  keys : Array DiscrTree.Key
+  /--
+  Expr key tested for matching, in ∀-quantified form.
+  `keys = (← mkPath (← forallMetaTelescope prog).2.2)`.
+  -/
+  prog : Expr
+  /-- The proof for the theorem. -/
+  proof : SpecProof
+  /--
+  If `etaPotential` is non-zero, then the precondition contains meta variables that can be
+  instantiated after applying `mintro ∀s` `etaPotential` many times.
+  -/
+  etaPotential : Nat := 0
+  priority : Nat  := eval_prio default
+  deriving Inhabited, BEq
+
+abbrev SpecEntry := SpecTheorem
+
+structure SpecTheorems where
+  specs : DiscrTree SpecTheorem := DiscrTree.empty
+  erased : PHashSet SpecProof := {}
+  deriving Inhabited
+
+def SpecTheorems.isErased (d : SpecTheorems) (thmId : SpecProof) : Bool :=
+  d.erased.contains thmId
+
+def SpecTheorems.eraseCore (d : SpecTheorems) (thmId : SpecProof) : SpecTheorems :=
+  { d with erased := d.erased.insert thmId }
+
+abbrev SpecExtension := SimpleScopedEnvExtension SpecEntry SpecTheorems
+
+private partial def countBVarDependentMVars (xs : Array Expr) (e : Expr) : MetaM Nat :=
+  go e
+  where
+    go (e : Expr) : MetaM Nat := do
+      if !e.hasExprMVar then return 0
+      match e with
+      | .app f a =>
+        if let some (_, lhs, rhs) := e.eq? then
+          let l := lhs.getAppFn'
+          let r := rhs.getAppFn'
+          if l.isMVar && rhs.hasLooseBVars && xs.contains l then return 1
+          if r.isMVar && lhs.hasLooseBVars && xs.contains r then return 1
+          return ← (· + ·) <$> go lhs <*> go rhs
+        return ← (· + ·) <$> go f <*> go a
+      | .mdata _ e => go e
+      | .lam _ ty b _ => (· + ·) <$> go ty <*> go b
+      | .letE _ ty v b _ => (· + · + ·) <$> go ty <*> go v <*> go b
+      | .forallE _ ty b _ => (· + ·) <$> go ty <*> go b
+      | .proj _ _ e => go e
+      | .mvar .. => return 0
+      | .lit .. | .fvar .. | .bvar .. | .sort .. | .const .. => return 0
+
+def simpSPredConfig : ConfigWithKey :=
+  { simpGlobalConfig.config with
+    iota := true,
+    beta := true,
+    zeta := true,
+    zetaDelta := true,
+    proj := .yesWithDelta }.toConfigWithKey
+
+/-- If `σs : List Type`, then `e : SPred σs`.
+Return the number of times `e` needs to be applied
+in order to assign closed solutions to meta variables. -/
+partial def computeMVarBetaPotentialForSPred (xs : Array Expr) (σs : Expr) (e : Expr) : MetaM Nat :=
+  withNewMCtxDepth do
+  withConfigWithKey simpSPredConfig do
+  if xs.isEmpty then return 0
+  let ctx ← Simp.Context.mkDefault
+  let mut σs ← whnfR σs
+  let mut e := e
+  let mut n : Nat := 0
+  let mut lastSuccess := 0
+  let mut boundAssignments ← countBVarDependentMVars xs e
+  while σs.isAppOfArity ``List.cons 3 do
+    n := n+1
+    let σ := σs.getArg! 1
+    let s ← mkFreshExprMVar σ
+    e := e.beta #[s]
+    let (r, _) ← simp e ctx
+      -- In practice we only need to reduce `fun s => ...`, `SVal.curry` and functions that operate
+      -- on the state tuple bound by `SVal.curry`.
+      -- We could write a custom function should `simp` become a bottleneck.
+    e := r.expr
+    let count ← countBVarDependentMVars xs e
+    if count < boundAssignments || e.getAppFn'.isMVar then
+      lastSuccess := n
+      boundAssignments := count
+    σs ← whnfR (σs.getArg! 2)
+  return lastSuccess
+
+private def mkSpecTheorem (type : Expr) (proof : SpecProof) (prio : Nat) : MetaM SpecTheorem := do
+  -- cf. mkSimpTheoremCore
+  let type ← instantiateMVars type
+  unless (← isProp type) do
+    throwError "invalid 'spec', proposition expected{indentExpr type}"
+  withNewMCtxDepth do
+  let (xs, _, type) ← withSimpGlobalConfig (forallMetaTelescopeReducing type)
+  let type ← whnfR type
+  let_expr Triple _m ps _inst _α prog P _Q := type
+    | throwError "unexpected kind of spec theorem; not a triple{indentExpr type}"
+  let keys ← DiscrTree.mkPath prog (noIndexAtArgs := false)
+  -- beta potential of `P` describes how many times we want to `mintro ∀s`, that is,
+  -- *eta*-expand the goal.
+  let σs := mkApp (mkConst ``PostShape.args) ps
+  let etaPotential ← computeMVarBetaPotentialForSPred xs σs P
+  -- logInfo m!"Beta potential {etaPotential} for {P}"
+  -- logInfo m!"mkSpecTheorem: {keys}, proof: {proof}"
+  return { keys, prog := (← mkForallFVars xs prog), proof, etaPotential, priority := prio }
+
+def mkSpecTheoremFromConst (declName : Name) (prio : Nat := eval_prio default) : MetaM SpecTheorem := do
+  -- cf. mkSimpTheoremsFromConst
+  let cinfo ← getConstInfo declName
+  let us := cinfo.levelParams.map mkLevelParam
+  let val := mkConst declName us
+--  withSimpGlobalConfig do -- This sets iota := false, which we do not want (for computeMVarBetaPotentialForSPred)
+  let type ← inferType val
+  mkSpecTheorem type (.global declName) prio
+
+def mkSpecTheoremFromLocal (fvar : FVarId) (prio : Nat := eval_prio default) : MetaM SpecTheorem := do
+  let some decl ← fvar.findDecl? | throwError "invalid 'spec', local constant not found"
+  mkSpecTheorem decl.type (.local fvar) prio
+
+def mkSpecTheoremFromStx (ref : Syntax) (proof : Expr) (prio : Nat := eval_prio default) : MetaM SpecTheorem := do
+  let type ← inferType proof
+  mkSpecTheorem type (.stx (← mkFreshId) ref proof) prio
+
+def addSpecTheoremEntry (d : SpecTheorems) (e : SpecTheorem) : SpecTheorems :=
+  { d with specs := d.specs.insertCore e.keys e }
+
+def addSpecTheorem (ext : SpecExtension) (declName : Name) (prio : Nat) (attrKind : AttributeKind) : MetaM Unit := do
+  let thm ← mkSpecTheoremFromConst declName prio
+  ext.add thm attrKind
+
+def mkSpecExt : SimpleScopedEnvExtension.Descr SpecEntry SpecTheorems where
+  name     := `specMap
+  initial  := {}
+  addEntry := fun d e => addSpecTheoremEntry d e
+
+builtin_initialize specAttr : SpecExtension ← registerSimpleScopedEnvExtension mkSpecExt
+
+def mkSpecAttr (ext : SpecExtension) : AttributeImpl where
+  name  := `spec
+  descr := "Marks Hoare triple specifications and simp theorems to use with the `mspec` and `mvcgen` tactics"
+  -- .afterCompilation seems unnecessarily conservative, but the simp attribute impl needs it.
+  -- The reason is that we cannot annotate definitions with `@[spec]` otherwise; the error is
+  -- > trying to realize id.eq_1 but `enableRealizationsForConst` must be called for 'id' first
+  applicationTime := AttributeApplicationTime.afterCompilation
+  add   := fun declName stx attrKind => do
+    let go : MetaM Unit := do
+      let info ← getConstInfo declName
+      let prio ← Attribute.Builtin.getPrio stx
+      try
+        addSpecTheorem ext declName prio attrKind
+      catch _ =>
+      let impl ← getBuiltinAttributeImpl `mvcgen_simp
+      try
+        impl.add declName stx attrKind
+      catch e =>
+      trace[Elab.Tactic.Do.specAttr] "Reason for failure to apply spec attribute: {e.toMessageData}"
+      throwError "Invalid 'spec': target was neither a Hoare triple specification nor a 'simp' lemma"
+    discard <| go.run {} {}
+
+builtin_initialize registerBuiltinAttribute (mkSpecAttr specAttr)
+
+def SpecExtension.getTheorems (ext : SpecExtension) : CoreM SpecTheorems :=
+  return ext.getState (← getEnv)
+
+def getSpecTheorems : CoreM SpecTheorems :=
+  specAttr.getTheorems
diff --git a/src/Lean/Elab/Tactic/Do/LetElim.lean b/src/Lean/Elab/Tactic/Do/LetElim.lean
new file mode 100644
index 0000000000..5774cc289e
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Do/LetElim.lean
@@ -0,0 +1,177 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Lean.Meta
+
+namespace Lean.Elab.Tactic.Do
+
+open Lean Meta Tactic
+
+inductive Uses where
+  | zero
+  | one
+  | many
+deriving BEq, Ord, Inhabited
+
+def Uses.add : Uses → Uses → Uses
+  | .zero, b => b
+  | a, .zero => a
+  | _, _ => .many
+
+def Uses.toNat : Uses → Nat
+  | .zero => 0
+  | .one => 1
+  | .many => 2
+
+def Uses.fromNat : Nat → Uses
+  | 0 => .zero
+  | 1 => .one
+  | _ => .many
+
+instance : Add Uses where
+  add := Uses.add
+
+abbrev FVarUses := Std.HashMap FVarId Uses
+
+def FVarUses.add (a b : FVarUses) : FVarUses :=
+  a.fold (init := b) fun acc k v => acc.alter k fun
+    | none => some v
+    | some v' => some (v + v')
+
+instance : Add FVarUses where
+  add := FVarUses.add
+
+inductive BVarUses (n : Nat) where
+  | none
+  | some (uses : Vector Uses n) -- indexed by BVars in reverse order
+
+def BVarUses.single {numBVars : Nat} (n : Nat) (_ : n < numBVars := by get_elem_tactic) : BVarUses numBVars :=
+  -- NB: BVarUses is indexed by BVars in reverse order
+  .some <| .ofFn fun (i : Fin numBVars) => if i.val = numBVars - 1 - n then .one else .zero
+
+def BVarUses.pop {numBVars : Nat} : BVarUses (numBVars + 1) → (Uses × BVarUses numBVars)
+  | .none => (.zero, .none)
+  | .some uses => (uses.back, .some uses.pop)
+
+def BVarUses.add {numBVars : Nat} (a b : BVarUses numBVars) : BVarUses numBVars := match a, b with
+  | .none, b => b
+  | a, .none => a
+  | .some a, .some b => .some (a.zipWith (fun a b => a + b) b)
+
+instance : Add (BVarUses numBVars) where
+  add := BVarUses.add
+
+def over1Of2 (f : α₁ → α₂) (x : α₁ × β) : α₂ × β := (f x.1, x.2)
+
+def addMData (d : MData) (e : Expr) : Expr := match e with
+  | .mdata d' e => .mdata (d.mergeBy (fun _ new _ => new) d') e
+  | _ => .mdata d e
+
+private def okToDup (e : Expr) : Bool := match e with
+  | .bvar .. => true
+  | .fvar .. => false -- viable, but would invalidate use information (which we could work around)
+  | .lit .. | .const .. | .sort .. | .mvar .. => true
+  | .mdata _ e => okToDup e
+  | .proj _ _ e => okToDup e -- Not sure about this one. Do we want to duplicate projs?
+  | .app .. => Simp.isOfNatNatLit e || Simp.isOfScientificLit e || Simp.isCharLit e
+  | .lam .. | .forallE .. | .letE .. => false
+
+mutual
+partial def countUsesDecl (fvarId : FVarId) (ty : Expr) (val? : Option Expr) (bodyUses : FVarUses) (subst : Array FVarId := #[]) : MetaM (Expr × Option Expr × FVarUses) := do
+  let (ty, tyUses) ← countUses ty subst
+  let (val?, valUses) ← match val? with
+    | none => pure (none, {})
+    | some val => over1Of2 some <$> countUses val subst
+  let uses := bodyUses.getD fvarId .zero
+  let fvs := if uses == .zero then bodyUses else bodyUses + tyUses + valUses
+  let fvs := fvs.erase fvarId
+  let ty := addMData (MData.empty.setNat `uses uses.toNat) ty
+  return (ty, val?, fvs)
+
+partial def countUses (e : Expr) (subst : Array FVarId := #[]) : MetaM (Expr × FVarUses) := match e with
+  | .bvar n =>
+    if _ : n < subst.size then
+      return (e, {(subst[n], .one)})
+    else
+      throwError "BVar index out of bounds: {n} >= {subst.size}"
+  | .fvar fvarId => return (e, {(fvarId, .one)})
+  | .letE x ty val body b => do
+    let fv ← mkFreshFVarId
+    let (body, fvs) ← countUses body (subst.push fv)
+    let (ty, .some val, fvs) ← countUsesDecl fv ty (some val) fvs subst | failure
+    return (.letE x ty val body b, fvs)
+  | .lam x ty body bi => do
+    let fv ← mkFreshFVarId
+    let (ty, fvs₁) ← countUses ty subst
+    let (body, fvs₂) ← countUses body (subst.push fv)
+    let fvs := (fvs₁ + fvs₂).erase fv
+    return (.lam x ty body bi, fvs) -- NB: We do not track uses of lam-bound x
+  | .forallE x ty body bi => do -- (almost) identical to lam
+    let fv ← mkFreshFVarId
+    let (ty, fvs₁) ← countUses ty subst
+    let (body, fvs₂) ← countUses body (subst.push fv)
+    let fvs := (fvs₁ + fvs₂).erase fv
+    return (.forallE x ty body bi, fvs) -- NB: We do not track uses of forall-bound x
+  | .proj s i e => over1Of2 (Expr.proj s i) <$> countUses e subst
+  | .mdata d e => over1Of2 (Expr.mdata d) <$> countUses e subst
+  | .app f a => do
+    let (f, fvarUses₁) ← countUses f subst
+    let (a, fvarUses₂) ← countUses a subst
+    return (.app f a, fvarUses₁ + fvarUses₂)
+  | .lit .. | .const .. | .sort .. | .mvar .. => return (e, {})
+end
+
+def countUsesLCtx (ctx : LocalContext) (targetUses : FVarUses) : MetaM LocalContext := do
+  let decls : Array LocalDecl := Array.mkEmpty ctx.decls.size
+  let decls ← Prod.fst <$> ctx.foldrM (init := (decls, targetUses)) fun decl (decls, targetUses) => do
+    let (ty, val?, fvs) ← countUsesDecl decl.fvarId decl.type decl.value? targetUses
+    let decl := match val? with
+      | none => decl.setType ty
+      | some val => decl.setType ty |>.setValue val
+    return (decls.push decl, fvs)
+  -- NB: decls are in reverse order; root comes first
+  let decls ← StateRefT'.run' (ω:=IO.RealWorld) (s := decls) <| ctx.decls.mapM fun decl => do
+    if decl.isNone then return decl
+    modifyGet fun (decls : Array LocalDecl) => (some decls.back!, decls.pop)
+  return { ctx with decls }
+
+def doNotDup (u : Uses) (rhs : Expr) (elimTrivial : Bool) : Bool :=
+  u == .many && not (elimTrivial && okToDup rhs)
+
+def elimLetsCore (e : Expr) (elimTrivial := true) : MetaM Expr := StateRefT'.run' (s := Std.HashSet.emptyWithCapacity 10) do
+  -- Figure out if we can make this work with Core.transform.
+  -- I think that would entail keeping track of BVar shifts in `pre` and `post`.
+  let pre (e : Expr) : StateRefT (Std.HashSet FVarId) MetaM TransformStep := do
+    match e with
+    | .letE _ ty val body _ => do
+      let .mdata d _ := ty | return .continue
+      let uses := Uses.fromNat (d.getNat `uses 2) -- 2 goes to .many
+      if doNotDup uses val elimTrivial then return .continue
+      return .visit (body.instantiate1 val) -- urgh O(n^2). See comment above
+    | _ => return .continue
+  Meta.transform e (pre := pre)
+
+def elimLets (mvar : MVarId) (elimTrivial := true): MetaM MVarId := mvar.withContext do
+  let ctx ← getLCtx
+  let (ty, fvarUses) ← countUses (← mvar.getType)
+  let ctx ← countUsesLCtx ctx fvarUses
+  let mut fvs := #[]
+  let mut vals := #[]
+  for decl in ctx do
+    let .some val := decl.value? | continue
+    let .mdata d _ := decl.type | continue
+    let uses := Uses.fromNat (d.getNat `uses 2) -- 2 goes to .many
+    if doNotDup uses val elimTrivial then continue
+    fvs := fvs.push (mkFVar decl.fvarId)
+    vals := vals.push val
+  let ty := ty.replaceFVars fvs vals
+  let ty ← elimLetsCore ty elimTrivial
+  let newMVar ← mkFreshExprSyntheticOpaqueMVar ty (← mvar.getTag)
+  mvar.assign newMVar
+  let mut mvar := newMVar.mvarId!
+  for fvarId in fvs do
+    mvar ← mvar.tryClear fvarId.fvarId!
+  return mvar
diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean
new file mode 100644
index 0000000000..cf3f975792
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Do/Spec.lean
@@ -0,0 +1,246 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+import Lean.Elab.Tactic.Do.ProofMode.Intro
+import Lean.Elab.Tactic.Do.ProofMode.Pure
+import Lean.Elab.Tactic.Do.ProofMode.Frame
+import Lean.Elab.Tactic.Do.ProofMode.Assumption
+import Lean.Elab.Tactic.Do.Attr
+import Std.Do.Triple
+
+namespace Lean.Elab.Tactic.Do
+open Lean Elab Tactic Meta
+open Std.Do Do.SpecAttr Do.ProofMode
+
+builtin_initialize registerTraceClass `Elab.Tactic.Do.spec
+
+def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem := do
+  let_expr WP.wp _m _ps _instWP _α prog := wp | throwError "target not a wp application {wp}"
+  let prog ← instantiateMVarsIfMVarApp prog
+  let prog := prog.headBeta
+  let candidates ← database.specs.getMatch prog
+  let candidates := candidates.filter fun spec => !database.erased.contains spec.proof
+  let candidates := candidates.insertionSort fun s₁ s₂ => s₁.priority < s₂.priority
+  trace[Elab.Tactic.Do.spec] "Candidates for {prog}: {candidates.map (·.proof)}"
+  let specs ← candidates.filterM fun spec => do
+    let (_, _, _, type) ← spec.proof.instantiate
+    trace[Elab.Tactic.Do.spec] "{spec.proof} instantiates to {type}"
+    let_expr Triple m ps instWP α specProg _P _Q := type | throwError "Not a triple: {type}"
+    isDefEq wp (mkApp5 (← mkConstWithFreshMVarLevels ``WP.wp) m ps instWP α specProg)
+  trace[Elab.Tactic.Do.spec] "Specs for {prog}: {specs.map (·.proof)}"
+  if specs.isEmpty then throwError m!"No specs found for {indentExpr prog}\nCandidates: {candidates.map (·.proof)}"
+  return specs[0]!
+
+def elabTermIntoSpecTheorem (stx : TSyntax `term) (expectedTy : Expr) : TacticM (SpecTheorem × List MVarId) := do
+  if stx.raw.isIdent then
+    match ← Term.resolveId? stx.raw (withInfo := true) with
+    | some (.const declName _) => return (← mkSpecTheoremFromConst declName, [])
+    | some (.fvar fvarId) => return (← mkSpecTheoremFromLocal fvarId, [])
+    | _      => pure ()
+  try
+    let (prf, mvars) ← --Term.withSynthesize <|
+      elabTermWithHoles stx expectedTy `mspec (allowNaturalHoles := true)
+    let specThm ← mkSpecTheoremFromStx stx.raw prf
+    return (specThm, mvars)
+  catch e : Exception =>
+    trace[Elab.Tactic.Do.spec] "Internal error. This happens for example when the head symbol of the spec is wrong. Message:\n  {e.toMessageData}"
+    throw e
+
+def elabSpec (stx? : Option (TSyntax `term)) (wp : Expr) : TacticM (SpecTheorem × List MVarId) := do
+  let_expr f@WP.wp m ps instWP α prog := wp | throwError "target not a wp application {wp}"
+  let P ← mkFreshExprMVar (mkApp (mkConst ``Assertion) ps) (userName := `P)
+  let Q ← mkFreshExprMVar (mkApp2 (mkConst ``PostCond) α ps) (userName := `Q)
+  let expectedTy := mkApp7 (mkConst ``Triple f.constLevels!) m ps instWP α prog P Q
+  trace[Elab.Tactic.Do.spec] "spec syntax: {stx?}"
+  trace[Elab.Tactic.Do.spec] "expected type: {← instantiateMVars expectedTy}"
+  match stx? with
+  | none => pure (← findSpec (← getSpecTheorems) wp, [])
+  | some stx => elabTermIntoSpecTheorem stx expectedTy
+
+variable {n} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n]
+
+private def mkProj' (n : Name) (i : Nat) (Q : Expr) : MetaM Expr := do
+  return (← projectCore? Q i).getD (mkProj n i Q)
+
+mutual
+partial def dischargePostEntails (α : Expr) (ps : Expr) (Q : Expr) (Q' : Expr) (goalTag : Name) (discharge : Expr → Name → n Expr) : n Expr := do
+  -- Often, Q' is fully instantiated while Q contains metavariables. Try refl
+  if (← isDefEq Q Q') then
+    return mkApp3 (mkConst ``PostCond.entails.refl) α ps Q'
+  let Q ← whnfR Q
+  let Q' ← whnfR Q'
+  -- If Q (postcond of the spec) is just an fvar, we do not decompose further
+  if let some _fvarId := Q.fvarId? then
+    return ← discharge (mkApp4 (mkConst ``PostCond.entails) α ps Q Q') (goalTag ++ `post)
+  -- Otherwise decompose the conjunction
+  let prf₁ ← withLocalDeclD Name.anonymous α fun a => do
+    let Q1a := (← mkProj' ``Prod 0 Q).betaRev #[a]
+    let Q'1a := (← mkProj' ``Prod 0 Q').betaRev #[a]
+    let σs := mkApp (mkConst ``PostShape.args) ps
+    let uniq ← liftMetaM mkFreshId
+    let goal := MGoal.mk σs (Hyp.mk `h uniq Q1a).toExpr Q'1a
+    mkLambdaFVars #[a] (← discharge goal.toExpr (goalTag ++ `success))
+  let prf₂ ← dischargeFailEntails ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except) discharge
+  mkAppM ``And.intro #[prf₁, prf₂] -- This is just a bit too painful to construct by hand
+
+partial def dischargeFailEntails (ps : Expr) (Q : Expr) (Q' : Expr) (goalTag : Name) (discharge : Expr → Name → n Expr) : n Expr := do
+  if ps.isAppOf ``PostShape.pure then
+    return mkConst ``True.intro
+  if ← isDefEq Q Q' then
+    return mkApp2 (mkConst ``FailConds.entails.refl) ps Q
+  if ← isDefEq Q (mkApp (mkConst ``FailConds.false) ps) then
+    return mkApp2 (mkConst ``FailConds.entails_false) ps Q'
+  if ← isDefEq Q' (mkApp (mkConst ``FailConds.true) ps) then
+    return mkApp2 (mkConst ``FailConds.entails_true) ps Q
+  -- the remaining cases are recursive.
+  if let some (_σ, ps) := ps.app2? ``PostShape.arg then
+    return ← dischargeFailEntails ps Q Q' goalTag discharge
+  if let some (ε, ps) := ps.app2? ``PostShape.except then
+    let Q ← whnfR Q
+    let Q' ← whnfR Q'
+    let prf₁ ← withLocalDeclD Name.anonymous ε fun e => do
+      let Q1e := (← mkProj' ``Prod 0 Q).betaRev #[e]
+      let Q'1e := (← mkProj' ``Prod 0 Q').betaRev #[e]
+      let σs := mkApp (mkConst ``PostShape.args) ps
+      let uniq ← liftMetaM mkFreshId
+      let goal := MGoal.mk σs (Hyp.mk `h uniq Q1e).toExpr Q'1e
+      mkLambdaFVars #[e] (← discharge goal.toExpr (goalTag ++ `handle))
+    let prf₂ ← dischargeFailEntails ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except) discharge
+    return ← mkAppM ``And.intro #[prf₁, prf₂] -- This is just a bit too painful to construct by hand
+  -- This case happens when decomposing with unknown `ps : PostShape`
+  discharge (mkApp3 (mkConst ``FailConds.entails) ps Q Q') goalTag
+end
+
+def dischargeMGoal (goal : MGoal) (goalTag : Name) (discharge : Expr → Name → n Expr) : n Expr := do
+  -- controlAt MetaM (fun map => do trace[Elab.Tactic.Do.spec] "dischargeMGoal: {(← reduceProj? goal.target).getD goal.target}"; map (pure ()))
+  -- simply try one of the assumptions for now. Later on we might want to decompose conjunctions etc; full xsimpl
+  let some prf ← liftMetaM goal.assumption | discharge goal.toExpr goalTag
+  return prf
+
+def mkPreTag (goalTag : Name) : Name := Id.run do
+  let dflt := goalTag ++ `pre1
+  let .str p s := goalTag | return dflt
+  unless "pre".isPrefixOf s do return dflt
+  let some n := (s.toSubstring.drop 3).toString.toNat? | return dflt
+  return .str p ("pre" ++ toString (n + 1))
+
+/--
+  Returns the proof and the list of new unassigned MVars.
+-/
+def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n (SpecTheorem × List MVarId)) (discharge : Expr → Name → n Expr) (goalTag : Name) (mkPreTag := mkPreTag) : n (Expr × List MVarId) := do
+  -- First instantiate `fun s => ...` in the target via repeated `mintro ∀s`.
+  let (holes, prf) ← mIntroForallN goal goal.target.consumeMData.getNumHeadLambdas fun goal => do
+    -- Elaborate the spec for the wp⟦e⟧ app in the target
+    let T := goal.target.consumeMData
+    unless T.getAppFn.constName! == ``PredTrans.apply do
+      liftMetaM (throwError "target not a PredTrans.apply application {indentExpr T}")
+    let wp := T.getArg! 2
+    liftMetaM <| do trace[Elab.Tactic.Do.spec] "before elabSpecAtWP {wp}"
+    let (specThm, elabMVars) ← elabSpecAtWP wp
+    liftMetaM <| do trace[Elab.Tactic.Do.spec] "after elabSpecAtWP {specThm.proof} {wp}"
+
+    -- The precondition of `specThm` might look like `⌜?n = ‹Nat›ₛ ∧ ?m = ‹Bool›ₛ⌝`, which expands to
+    -- `SVal.curry (fun tuple => ?n = SVal.uncurry (getThe Nat tuple) ∧ ?m = SVal.uncurry (getThe Bool tuple))`.
+    -- Note that the assignments for `?n` and `?m` depend on the bound variable `tuple`.
+    -- Here, we further eta expand and simplify according to `etaPotential` so that the solutions for
+    -- `?n` and `?m` do not depend on `tuple`.
+    let residualEta := specThm.etaPotential - (T.getAppNumArgs - 4) -- 4 arguments expected for PredTrans.apply
+    mIntroForallN goal residualEta fun goal => do
+
+    -- Compute a frame of `P` that we duplicate into the pure context using `Spec.frame`
+    -- For now, frame = `P` or nothing at all
+    mTryFrame goal fun goal => do
+
+    -- Fully instantiate the specThm without instantiating its MVars to `wp` yet
+    let (schematicMVars, _, spec, specTy) ← specThm.proof.instantiate
+
+    -- Apply the spec to the excess arguments of the `wp⟦e⟧ Q` application
+    let T := goal.target.consumeMData
+    let args := T.getAppArgs
+    let Q' := args[3]!
+    let excessArgs := (args.extract 4 args.size).reverse
+
+    liftMetaM <| do trace[Elab.Tactic.Do.spec] "before WTF {wp} {spec} {specTy}"
+    -- Actually instantiate the specThm using the expected type computed from `wp`.
+    let_expr f@Triple m ps instWP α prog P Q := specTy | do liftMetaM (throwError "target not a Triple application {specTy}")
+    let wp' := mkApp5 (mkConst ``WP.wp f.constLevels!) m ps instWP α prog
+    unless (← withAssignableSyntheticOpaque <| isDefEq wp wp') do
+      Term.throwTypeMismatchError none wp wp' spec
+    liftMetaM <| do trace[Elab.Tactic.Do.spec] "WTF {wp} {wp'} {spec} {specTy}"
+
+    let P := P.betaRev excessArgs
+    let spec := spec.betaRev excessArgs
+
+    -- often P or Q are schematic (i.e. an MVar app). Try to solve by rfl.
+    let P ← instantiateMVarsIfMVarApp P
+    let Q ← instantiateMVarsIfMVarApp Q
+    let HPRfl ← withDefault <| withAssignableSyntheticOpaque <| isDefEqGuarded P goal.hyps
+    let QQ'Rfl ← withDefault <| withAssignableSyntheticOpaque <| isDefEqGuarded Q Q'
+
+    -- Discharge the validity proof for the spec if not rfl
+    let mut prePrf : Expr → Expr := id
+    if !HPRfl then
+      -- let P := (← reduceProjBeta? P).getD P
+      -- Try to avoid creating a longer name if the postcondition does not need to create a goal
+      let tag := if !QQ'Rfl then mkPreTag goalTag else goalTag
+      let HPPrf ← dischargeMGoal { goal with target := P } tag discharge
+      prePrf := mkApp6 (mkConst ``SPred.entails.trans) goal.σs goal.hyps P goal.target HPPrf
+
+    -- Discharge the entailment on postconditions if not rfl
+    let mut postPrf : Expr → Expr := id
+    if !QQ'Rfl then
+      -- Try to avoid creating a longer name if the precondition does not need to create a goal
+      let tag := if !HPRfl then goalTag ++ `post else goalTag
+      let wpApplyQ  := mkApp4 (mkConst ``PredTrans.apply) ps α wp Q  -- wp⟦x⟧.apply Q; that is, T without excess args
+      let wpApplyQ' := mkApp4 (mkConst ``PredTrans.apply) ps α wp Q' -- wp⟦x⟧.apply Q'
+      let QQ' ← dischargePostEntails α ps Q Q' tag discharge
+      let QQ'mono := mkApp6 (mkConst ``PredTrans.mono) ps α wp Q Q' QQ'
+      postPrf := fun h =>
+        mkApp6 (mkConst ``SPred.entails.trans) goal.σs P (wpApplyQ.betaRev excessArgs) (wpApplyQ'.betaRev excessArgs)
+          h (QQ'mono.betaRev excessArgs)
+
+    -- finally build the proof; HPPrf.trans (spec.trans QQ'mono)
+    let prf := prePrf (postPrf spec)
+    let holes := elabMVars ++ schematicMVars.toList.map (·.mvarId!)
+    let holes ← liftMetaM <| holes.filterM fun mv => not <$> mv.isAssignedOrDelayedAssigned
+    return (holes, prf)
+
+  -- (This is after closing the `mForallIntro` and `mTryFrame` blocks.)
+  -- Functions like `mkForallFVars` etc. might have instantiated some of the MVar holes and in
+  -- doing so have introduced new MVars in turn.
+  -- Thus we try and instantiate all MVars and collect the MVars of the instantiated expressions.
+  let holes ← liftMetaM <| holes.flatMapM fun mv => do
+    let e ← instantiateMVars (mkMVar mv)
+    let mvs ← getMVars e
+    let mvs ← mvs.filterM fun mv => not <$> mv.isAssignedOrDelayedAssigned
+    return mvs.toList
+  return (prf, holes)
+
+private def addMVar (mvars : IO.Ref (List MVarId)) (goal : Expr) (name : Name) : MetaM Expr := do
+  let m ← mkFreshExprSyntheticOpaqueMVar goal (tag := name)
+  mvars.modify (m.mvarId! :: ·)
+  return m
+
+@[builtin_tactic Lean.Parser.Tactic.mspecNoBind]
+def evalMSpecNoBind : Tactic
+  | `(tactic| mspec_no_bind $[$spec]?) => do
+    let (mvar, goal) ← mStartMVar (← getMainGoal)
+    mvar.withContext do
+    let goals ← IO.mkRef []
+    let (prf, specHoles) ← mSpec goal (elabSpec spec) (fun goal name => liftMetaM (addMVar goals goal name)) (← getMainTag)
+    mvar.assign prf
+    let goals ← goals.get
+    if let [mvar'] := goals then mvar'.setTag (← mvar.getTag)
+    replaceMainGoal (goals ++ specHoles)
+  | _ => throwUnsupportedSyntax
+
+-- TODO: Define the simp set as a list here and build `simpArgs` syntax from it
+macro_rules
+  | `(tactic| mspec_no_simp $[$spec]?) =>
+    `(tactic| ((try with_reducible mspec_no_bind $(mkIdent ``Std.Do.Spec.bind)); mspec_no_bind $[$spec]?))
+  | `(tactic| mspec $[$spec]?)         =>
+    `(tactic| mspec_no_simp $[$spec]?; open Std.Do in all_goals ((try simp only [SPred.true_intro_simp, SPred.true_intro_simp_nil, SVal.curry_cons, SVal.uncurry_cons, SVal.getThe_here, SVal.getThe_there]); (try mpure_intro; trivial)))
diff --git a/src/Lean/Elab/Tactic/Do/Syntax.lean b/src/Lean/Elab/Tactic/Do/Syntax.lean
new file mode 100644
index 0000000000..2be2cef884
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Do/Syntax.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Init.NotationExtra
+import Lean.Elab.BuiltinNotation
+import Std.Do.PostCond
+import Std.Do.Triple.Basic
+
+namespace Std.Do
+
+open Lean Parser Meta Elab Term
+
+def post_syntax := leading_parser
+  "post⟨" >> withoutPosition (withoutForbidden (sepBy termParser ", " (allowTrailingSep := true))) >> "⟩"
+scoped syntax:max "post⟨" term,+ "⟩" : term
+macro_rules | `(post⟨$handlers,*⟩) => `(by exact ⟨$handlers,*, ()⟩)
+  -- NB: Postponement through by exact is the entire point of this macro
+  -- until https://github.com/leanprover/lean4/pull/8074 lands
+example : PostCond Nat .pure := post⟨fun s => True⟩
+example : PostCond (Nat × Nat) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
+  post⟨fun (r, xs) s => r ≤ 4 ∧ s = 4 ∧ r + xs > 4, fun e s => e = 42 ∧ s = 4⟩
+
+open Lean Parser Term in
+def funArrow : Parser := unicodeSymbol " ↦ " " => "
+@[inherit_doc PostCond.total]
+scoped macro "⇓" xs:Lean.Parser.Term.funBinder+ funArrow e:term : term =>
+  `(PostCond.total (by exact (fun $xs* => spred($e)))) -- NB: Postponement through by exact
+
+@[app_unexpander PostCond.total]
+private def unexpandPostCondTotal : PrettyPrinter.Unexpander
+  | `($_ fun $xs* => $e) => do `(⇓ $xs* => $(← SPred.Notation.unpack e))
+  | _ => throw ()
+
+elab_rules : term
+  | `(⦃$P⦄ $x ⦃$Q⦄) => do
+    -- In a simple world, this would just be a macro expanding to
+    -- `Triple $x spred($P) spred($Q)`.
+    -- However, currently we need to help type inference for P and Q.
+    -- Specifically, if `x : StateT σ m α`, `[wp : WP m ps]` and `P : σ → Assertion ps`,
+    -- then `Triple x P _` will not elaborate because `σ → Assertion ps =?= Assertion ?ps` fails.
+    -- We must first instantiate `?ps` to `.arg σ ps` through the `outParam` of `WP`, hence this elaborator.
+    -- This is tracked in #8766, and #8074 might be a fix.
+    let x ← elabTerm x none
+    let ty ← inferType x
+    tryPostponeIfMVar ty
+    let ty ← instantiateMVars ty
+    let .app m α := ty.consumeMData | throwError "Not a type application {ty}"
+    let some u ← Level.dec <$> getLevel ty | throwError "Wrong level 0 {ty}"
+    let ps ← mkFreshExprMVar (mkConst ``PostShape)
+    let inst ← synthInstance (mkApp2 (mkConst ``WP [u]) m ps)
+    let P ← elabTerm (← `(spred($P))) (mkApp (mkConst ``Assertion) ps)
+    let Q ← elabTerm (← `(spred($Q))) (mkApp2 (mkConst ``PostCond) α ps)
+    return mkApp7 (mkConst ``Triple [u]) m ps inst α x P Q
+
+@[app_unexpander Triple]
+private def unexpandTriple : PrettyPrinter.Unexpander
+  | `($_ $x $P $Q) => do
+    `(⦃$(← SPred.Notation.unpack P)⦄ $x ⦃$Q⦄)
+  | _ => throw ()
diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean
new file mode 100644
index 0000000000..fa7f84f5f5
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -0,0 +1,392 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.WP
+import Std.Do.Triple
+import Lean.Elab.Tactic.Simp
+import Lean.Elab.Tactic.Meta
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+import Lean.Elab.Tactic.Do.ProofMode.Intro
+import Lean.Elab.Tactic.Do.ProofMode.Cases
+import Lean.Elab.Tactic.Do.ProofMode.Specialize
+import Lean.Elab.Tactic.Do.LetElim
+import Lean.Elab.Tactic.Do.Spec
+import Lean.Elab.Tactic.Do.Attr
+import Lean.Elab.Tactic.Do.Syntax
+
+namespace Lean.Elab.Tactic.Do
+
+open Lean Parser Elab Tactic Meta Do ProofMode SpecAttr
+open Std.Do
+
+builtin_initialize registerTraceClass `Elab.Tactic.Do.vcgen
+
+register_builtin_option mvcgen.warning : Bool := {
+  defValue := true
+  group    := "debug"
+  descr    := "disable `mvcgen` usage warning"
+}
+
+inductive Fuel where
+| limited (n : Nat)
+| unlimited
+deriving DecidableEq
+
+structure Config where
+  /--
+  If true, do not substitute away let-declarations that are used at most once before starting
+  VC generation.
+  -/
+  noLetElim : Bool := false
+
+declare_config_elab elabConfig Config
+
+structure Context where
+  config : Config
+  specThms : SpecTheorems
+  simpCtx : Simp.Context
+  simprocs : Simp.SimprocsArray
+
+structure State where
+  fuel : Fuel := .unlimited
+  simpState : Simp.State := {}
+  /--
+  The verification conditions that have been generated so far.
+  Includes `Type`-valued goals arising from instantiation of specifications.
+  -/
+  vcs : Array MVarId := #[]
+
+abbrev VCGenM := ReaderT Context (StateRefT State MetaM)
+
+def burnOne : VCGenM PUnit := do
+  let s ← get
+  match s.fuel with
+  | Fuel.limited 0 => return ()
+  | Fuel.limited (n + 1) => set { s with fuel := .limited n }
+  | Fuel.unlimited => return ()
+
+def ifOutOfFuel (x : VCGenM α) (k : VCGenM α) : VCGenM α := do
+  let s ← get
+  match s.fuel with
+  | Fuel.limited 0 => x
+  | _ => k
+
+def emitVC (subGoal : Expr) (name : Name) : VCGenM Expr := do
+  let m ← liftM <| mkFreshExprSyntheticOpaqueMVar subGoal (tag := name)
+  modify fun s => { s with vcs := s.vcs.push m.mvarId! }
+  return m
+
+def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
+  modify fun s => { s with vcs := s.vcs.push goal }
+
+def liftSimpM (x : SimpM α) : VCGenM α := do
+  let ctx ← read
+  let s ← get
+  let mref := (Simp.mkDefaultMethodsCore ctx.simprocs).toMethodsRef
+  let (a, simpState) ← x mref ctx.simpCtx |>.run s.simpState
+  set { s with simpState }
+  return a
+
+instance : MonadLift SimpM VCGenM where
+  monadLift x := liftSimpM x
+
+syntax (name := mvcgen_step) "mvcgen_step" optConfig
+ (num)? (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
+
+syntax (name := mvcgen_no_trivial) "mvcgen_no_trivial" optConfig
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
+
+syntax (name := mvcgen) "mvcgen" optConfig
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
+
+private def mkSpecContext (optConfig : Syntax) (lemmas : Syntax) (ignoreStarArg := false) : TacticM Context := do
+  let config ← elabConfig optConfig
+  let mut specThms ← getSpecTheorems
+  let mut simpStuff := #[]
+  let mut starArg := false
+  for arg in lemmas[1].getSepArgs do
+    if arg.getKind == ``simpErase then
+      try
+        -- Try and build SpecTheorems for the lemma to erase to see if it's
+        -- meant to be interpreted by SpecTheorems. Otherwise fall back to SimpTheorems.
+        let specThm ←
+          if let some fvar ← Term.isLocalIdent? arg[1] then
+            mkSpecTheoremFromLocal fvar.fvarId!
+          else
+            let id := arg[1]
+            if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
+              mkSpecTheoremFromConst declName
+            else
+              withRef id <| throwUnknownConstant id.getId.eraseMacroScopes
+        specThms := specThms.eraseCore specThm.proof
+      catch _ =>
+        simpStuff := simpStuff.push ⟨arg⟩ -- simp tracks its own erase stuff
+    else if arg.getKind == ``simpLemma then
+      unless arg[0].isNone && arg[1].isNone do
+        -- When there is ←, →, ↑ or ↓ then this is for simp
+        simpStuff := simpStuff.push ⟨arg⟩
+        continue
+      let term := arg[2]
+      match ← Term.resolveId? term (withInfo := true) <|> Term.elabCDotFunctionAlias? ⟨term⟩ with
+      | some (.const declName _) =>
+        let info ← getConstInfo declName
+        try
+          let thm ← mkSpecTheoremFromConst declName
+          specThms := addSpecTheoremEntry specThms thm
+        catch _ =>
+          simpStuff := simpStuff.push ⟨arg⟩
+      | some (.fvar fvar) =>
+        let decl ← getFVarLocalDecl (.fvar fvar)
+        try
+          let thm ← mkSpecTheoremFromLocal fvar
+          specThms := addSpecTheoremEntry specThms thm
+        catch _ =>
+          simpStuff := simpStuff.push ⟨arg⟩
+      | _ => withRef term <| throwError "Could not resolve {repr term}"
+    else if arg.getKind == ``simpStar then
+      starArg := true
+      simpStuff := simpStuff.push ⟨arg⟩
+    else
+      throwUnsupportedSyntax
+  -- Build a mock simp call to build a simp context that corresponds to `simp [simpStuff]`
+  let stx ← `(tactic| simp +unfoldPartialApp [$(Syntax.TSepArray.ofElems simpStuff),*])
+  -- logInfo s!"{stx}"
+  let res ← mkSimpContext stx.raw
+    (eraseLocal := false)
+    (simpTheorems := getSpecSimpTheorems)
+    (ignoreStarArg := ignoreStarArg)
+  -- logInfo m!"{res.ctx.simpTheorems.map (·.toUnfold.toList)}"
+  if starArg && !ignoreStarArg then
+    let fvars ← getPropHyps
+    for fvar in fvars do
+      unless specThms.isErased (.local fvar) do
+        try
+          let thm ← mkSpecTheoremFromLocal fvar
+          specThms := addSpecTheoremEntry specThms thm
+        catch _ => continue
+  return { config, specThms, simpCtx := res.ctx, simprocs := res.simprocs }
+
+def isDuplicable (e : Expr) : Bool := match e with
+  | .bvar .. => true
+  | .mvar .. => true
+  | .fvar .. => true
+  | .const .. => true
+  | .lit .. => true
+  | .sort .. => true
+  | .mdata _ e => isDuplicable e
+  | .proj _ _ e => isDuplicable e
+  | .lam .. => false
+  | .forallE .. => false
+  | .letE .. => false
+  | .app .. => e.isAppOf ``OfNat.ofNat
+
+def withSharing (name : Name) (type : Expr) (val : Expr) (k : Expr → (Expr → VCGenM Expr) → VCGenM α) (kind : LocalDeclKind := .default) : VCGenM α :=
+  if isDuplicable val then
+    k val pure
+  else
+    withLetDecl name type val (kind := kind) fun fv => do
+      k fv (liftM <| mkForallFVars #[fv] ·)
+
+/-- Reduces (1) Prod projection functions and (2) Projs in application heads,
+and (3) beta reduces. -/
+private partial def reduceProjBeta? (e : Expr) : MetaM (Option Expr) :=
+  go none e.getAppFn e.getAppRevArgs
+  where
+    go lastReduction f rargs := do
+      match f with
+      | .mdata _ f => go lastReduction f rargs
+      | .app f a => go lastReduction f (rargs.push a)
+      | .lam .. =>
+        if rargs.size = 0 then return lastReduction
+        let e' := f.betaRev rargs
+        go (some e') e'.getAppFn e'.getAppRevArgs
+      | .const name .. =>
+        let env ← getEnv
+        match env.getProjectionStructureName? name with
+        | some ``Prod => -- only reduce fst and snd for now
+          match ← Meta.unfoldDefinition? (mkAppRev f rargs) with
+          | some e' => go lastReduction e'.getAppFn e'.getAppRevArgs
+          | none => pure lastReduction
+        | _ => pure lastReduction
+      | .proj .. => match ← reduceProj? f with
+        | some f' =>
+          let e' := mkAppRev f' rargs
+          go (some e') e'.getAppFn e'.getAppRevArgs
+        | none    => pure lastReduction
+      | _ => pure lastReduction
+
+partial def step (ctx : Context) (fuel : Fuel) (goal : MGoal) (name : Name) : MetaM (Expr × Array MVarId) := do
+  withReducible do
+  let (res, state) ← StateRefT'.run (ReaderT.run (onGoal goal name) ctx) { fuel }
+  return (res, state.vcs)
+where
+  onFail (goal : MGoal) (name : Name) : VCGenM Expr := do
+    -- logInfo m!"fail {goal.toExpr}"
+    emitVC goal.toExpr name
+
+  tryGoal (goal : Expr) (name : Name) : VCGenM Expr := do
+    forallTelescope goal fun xs body => do
+      let res ← try mStart body catch _ =>
+        return ← mkLambdaFVars xs (← emitVC goal name)
+      let mut prf ← onGoal res.goal name
+      -- logInfo m!"tryGoal: {res.goal.toExpr}"
+      -- res.goal.checkProof prf
+      if let some proof := res.proof? then
+        prf := mkApp proof prf
+      mkLambdaFVars xs prf
+
+  assignMVars (mvars : List MVarId) : VCGenM PUnit := do
+    for mvar in mvars do
+      -- trace[Elab.Tactics.Do.vcgen] "assignMVars {← mvar.getTag}, assigned: {← mvar.isAssigned}"
+      if ← mvar.isAssigned then continue
+      -- I used to filter for `isProp` here and add any non-Props directly as subgoals,
+      -- but then we would get spurious instantiations of non-synthetic goals such as loop
+      -- invariants.
+      mvar.assign (← mvar.withContext <| tryGoal (← mvar.getType) (← mvar.getTag))
+
+  onGoal goal name : VCGenM Expr := do
+    let T := goal.target
+    let T := (← reduceProjBeta? T).getD T -- very slight simplification
+    -- logInfo m!"target: {T}"
+    let goal := { goal with target := T }
+
+    let f := T.getAppFn
+    if f.isLambda then
+      return ← onLambda goal name
+    if f.isConstOf ``SPred.imp then
+      return ← onImp goal name
+    else if f.isConstOf ``PredTrans.apply then
+      return ← onWPApp goal name
+    onFail { goal with target := T } name
+
+  onImp goal name : VCGenM Expr := ifOutOfFuel (onFail goal name) do
+    burnOne
+    (·.2) <$> mIntro goal (← `(binderIdent| _)) (fun g =>
+        do return ((), ← onGoal g name))
+
+  onLambda goal name : VCGenM Expr := ifOutOfFuel (onFail goal name) do
+    burnOne
+    (·.2) <$> mIntroForall goal (← `(binderIdent| _)) (fun g =>
+        do return ((), ← onGoal g name))
+
+  onWPApp goal name : VCGenM Expr := ifOutOfFuel (onFail goal name) do
+    let args := goal.target.getAppArgs
+    let trans := args[2]!
+    -- logInfo m!"trans: {trans}"
+    let Q := args[3]!
+    let wp ← instantiateMVarsIfMVarApp trans
+    match_expr wp with
+    | c@WP.wp m ps instWP α e =>
+      let e ← instantiateMVarsIfMVarApp e
+      let e := e.headBeta
+      trace[Elab.Tactics.Do.vcgen] "Target: {e}"
+      let goalWithNewProg e' :=
+        let wp' := mkApp5 c m ps instWP α e'
+        let args' := args.set! 2 wp'
+        { goal with target := mkAppN (mkConst ``PredTrans.apply) args' }
+
+      -- lambda-expressions
+      if e.getAppFn'.isLambda && false then
+        -- We are likely in the implementation of a StateT function; do `mintro ∀s`
+        return ← onLambda goal name
+      -- let-expressions
+      if let .letE x ty val body _nonDep := e.getAppFn' then
+        burnOne
+        return ← withSharing x ty val fun fv leave => do
+        let e' := ((body.instantiate1 fv).betaRev e.getAppRevArgs)
+        leave (← onWPApp (goalWithNewProg e') name)
+      -- match-expressions
+      if let .some info := isMatcherAppCore? (← getEnv) e then
+        -- Bring into simp NF
+        let res? ← Simp.simpMatchDiscrs? info e
+        let e ← -- returns/continues only if old e is defeq to new e
+          if let .some res := res? then
+            burnOne
+            if let .some heq := res.proof? then
+              let prf ← onWPApp (goalWithNewProg res.expr) name
+              let prf := mkApp10 (mkConst ``Triple.rewrite_program c.constLevels!) m ps α goal.hyps Q instWP e res.expr heq prf
+              return prf
+            else
+              pure res.expr
+          else
+            pure e
+        -- Try reduce the matcher
+        let e ← match (← reduceMatcher? e) with
+          | .reduced e' =>
+          burnOne
+          return ← onWPApp (goalWithNewProg e') name
+          | .stuck _ => pure e
+          | _ => pure e
+        -- Last resort: Split match
+        -- logInfo m!"split match {e}"
+        burnOne
+        let mvar ← mkFreshExprSyntheticOpaqueMVar goal.toExpr (tag := name)
+        let mvars ← Split.splitMatch mvar.mvarId! e
+        assignMVars mvars
+        return mvar
+      -- Unfold local bindings (TODO don't do this unconditionally)
+      let f := e.getAppFn'
+      if let some (some val) ← f.fvarId?.mapM (·.getValue?) then
+        burnOne
+        let e' := val.betaRev e.getAppRevArgs
+        -- logInfo m!"unfold local var {f}, new WP: {wpe}"
+        return ← onWPApp (goalWithNewProg e') name
+      -- Unfold definitions according to reducibility and spec attributes,
+      -- apply specifications
+      if f.isConst then
+        burnOne
+        try
+          let specThm ← findSpec ctx.specThms wp
+          trace[Elab.Tactics.Do.vcgen] "Candidate spec for {f.constName!}: {specThm.proof}"
+          let (prf, specHoles) ← mSpec goal (fun _wp  => return (specThm, [])) tryGoal name
+          assignMVars specHoles
+          return prf
+        catch ex =>
+          trace[Elab.Tactics.Do.vcgen] "Failed to find spec. Trying simp. Reason: {ex.toMessageData}"
+        let res ← Simp.simp e
+        unless res.expr != e do return ← onFail goal name
+        burnOne
+        if let .some heq := res.proof? then
+          trace[Elab.Tactics.Do.vcgen] "Simplified"
+          let prf ← onWPApp (goalWithNewProg res.expr) name
+          let prf := mkApp10 (mkConst ``Triple.rewrite_program c.constLevels!) m ps α goal.hyps Q instWP e res.expr heq prf
+          return prf
+        else
+          return ← onWPApp (goalWithNewProg res.expr) name
+      return ← onFail goal name
+    | _ => return ← onFail goal name
+
+def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : TacticM (Array MVarId) := do
+  let goal ← if ctx.config.noLetElim then pure goal else elimLets goal
+  let (mvar, goal) ← mStartMVar goal
+  mvar.withContext do
+  let (prf, vcs) ← step ctx (fuel := fuel) goal (← mvar.getTag)
+  mvar.assign prf
+  replaceMainGoal vcs.toList
+  return vcs
+
+@[builtin_tactic Lean.Parser.Tactic.mvcgenStep]
+def evalMVCGenStep : Tactic := fun stx => withMainContext do
+  let ctx ← mkSpecContext stx[1] stx[3]
+  let n := if stx[2].isNone then 1 else stx[2][0].toNat
+  discard <| genVCs (← getMainGoal) ctx (fuel := .limited n)
+
+@[builtin_tactic Lean.Parser.Tactic.mvcgenNoTrivial]
+def evalMVCGenNoTrivial : Tactic := fun stx => withMainContext do
+  let ctx ← mkSpecContext stx[0] stx[1]
+  discard <| genVCs (← getMainGoal) ctx (fuel := .unlimited)
+
+@[builtin_tactic Lean.Parser.Tactic.mvcgen]
+def evalMVCGen : Tactic := fun stx => withMainContext do
+  if mvcgen.warning.get (← getOptions) then
+    logWarningAt stx "The `mvcgen` tactic is experimental and still under development. Avoid using it in production projects."
+  -- I would like to define this simply as a macro
+  -- `(tactic| mvcgen_no_trivial $c $lemmas <;> try (guard_target =~ (⌜True⌝ ⊢ₛ _); mpure_intro; trivial))
+  -- but optConfig is not a leading_parser, and neither is the syntax for `lemmas`
+  let ctx ← mkSpecContext stx[1] stx[2]
+  let vcs ← genVCs (← getMainGoal) ctx (fuel := .unlimited)
+  let tac ← `(tactic| try (mpure_intro; trivial))
+  for vc in vcs do discard <| runTactic vc tac
diff --git a/src/Std/Do.lean b/src/Std/Do.lean
index 3bd6f8ceb5..d39b9786c7 100644
--- a/src/Std/Do.lean
+++ b/src/Std/Do.lean
@@ -5,3 +5,7 @@ Authors: Sebastian Graf
 -/
 prelude
 import Std.Do.SPred
+import Std.Do.WP
+import Std.Do.Triple
+import Std.Do.PredTrans
+import Std.Do.PostCond
diff --git a/src/Std/Do/PostCond.lean b/src/Std/Do/PostCond.lean
new file mode 100644
index 0000000000..ce59cfc57f
--- /dev/null
+++ b/src/Std/Do/PostCond.lean
@@ -0,0 +1,226 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.SPred
+
+/-!
+# Pre and postconditions
+
+This module defines `Assertion` and `PostCond`, the types which constitute
+the pre and postconditions of a Hoare triple in the program logic.
+
+## Predicate shapes
+
+Since `WP` supports arbitrary monads, `PostCond` must be general enough to
+cope with state and exceptions.
+For this reason, `PostCond` is indexed by a `PostShape` which is an abstraction
+of the stack of effects supported by the monad, corresponding directly to
+`StateT` and `ExceptT` layers in a transformer stack.
+For every `StateT σ` effect, we get one `PostShape.arg σ` layer, whereas for every
+`ExceptT ε` effect, we get one `PostShape.except ε` layer.
+Currently, the only supported base layer is `PostShape.pure`.
+
+## Pre and postconditions
+
+The type of preconditions `Assertion ps` is distinct from the type of postconditions `PostCond α ps`.
+
+This is because postconditions not only specify what happens upon successful termination of the
+program, but also need to specify a property that holds upon failure.
+We get one "barrel" for the success case, plus one barrel per `PostShape.except` layer.
+
+It does not make much sense to talk about failure barrels in the context of preconditions.
+Hence, `Assertion ps` is defined such that all `PostShape.except` layers are discarded from `ps`,
+via `PostShape.args`.
+-/
+
+namespace Std.Do
+
+inductive PostShape : Type 1 where
+  | pure : PostShape
+  | arg : (σ : Type) → PostShape → PostShape
+  | except : (ε : Type) → PostShape → PostShape
+
+abbrev PostShape.args : PostShape → List Type
+  | .pure => []
+  | .arg σ s => σ :: PostShape.args s
+  | .except _ s => PostShape.args s
+
+/--
+  An assertion on the `.arg`s in the given predicate shape.
+  ```
+  example : Assertion (.arg ρ .pure) = (ρ → Prop) := rfl
+  example : Assertion (.except ε .pure) = Prop := rfl
+  example : Assertion (.arg σ (.except ε .pure)) = (σ → Prop) := rfl
+  example : Assertion (.except ε (.arg σ .pure)) = (σ → Prop) := rfl
+  ```
+  This is an abbreviation for `SPred` under the hood, so all theorems about `SPred` apply.
+-/
+abbrev Assertion (ps : PostShape) : Type :=
+  SPred (PostShape.args ps)
+
+/--
+  Encodes one continuation barrel for each `PostShape.except` in the given predicate shape.
+  ```
+  example : FailConds (.pure) = Unit := rfl
+  example : FailConds (.except ε .pure) = ((ε → Prop) × Unit) := rfl
+  example : FailConds (.arg σ (.except ε .pure)) = ((ε → Prop) × Unit) := rfl
+  example : FailConds (.except ε (.arg σ .pure)) = ((ε → σ → Prop) × Unit) := rfl
+  ```
+-/
+def FailConds : PostShape → Type
+  | .pure => Unit
+  | .arg _ ps => FailConds ps
+  | .except ε ps => (ε → Assertion ps) × FailConds ps
+
+@[simp]
+def FailConds.const {ps : PostShape} (p : Prop) : FailConds ps := match ps with
+  | .pure => ()
+  | .arg _ ps => @FailConds.const ps p
+  | .except _ ps => (fun _ε => spred(⌜p⌝), @FailConds.const ps p)
+
+@[simp]
+def FailConds.true : FailConds ps := FailConds.const True
+
+@[simp]
+def FailConds.false : FailConds ps := FailConds.const False
+
+instance : Inhabited (FailConds ps) where
+  default := FailConds.true
+
+def FailConds.entails {ps : PostShape} (x y : FailConds ps) : Prop :=
+  match ps with
+  | .pure => True
+  | .arg _ ps => @entails ps x y
+  | .except _ ps => (∀ e, x.1 e ⊢ₛ y.1 e) ∧ @entails ps x.2 y.2
+
+infixr:25 " ⊢ₑ " => FailConds.entails
+
+@[simp, refl]
+theorem FailConds.entails.refl {ps : PostShape} (x : FailConds ps) : x ⊢ₑ x := by
+  induction ps <;> simp [entails, *]
+
+theorem FailConds.entails.rfl {ps : PostShape} {x : FailConds ps} : x ⊢ₑ x := refl x
+
+theorem FailConds.entails.trans {ps : PostShape} {x y z : FailConds ps} : (x ⊢ₑ y) → (y ⊢ₑ z) → x ⊢ₑ z := by
+  induction ps
+  case pure => intro _ _; trivial
+  case arg σ s ih => exact ih
+  case except ε s ih => intro h₁ h₂; exact ⟨fun e => (h₁.1 e).trans (h₂.1 e), ih h₁.2 h₂.2⟩
+
+@[simp]
+theorem FailConds.entails_false {x : FailConds ps} : FailConds.false ⊢ₑ x := by
+  induction ps <;> simp_all [false, const, entails, SPred.false_elim]
+
+@[simp]
+theorem FailConds.entails_true {x : FailConds ps} : x ⊢ₑ FailConds.true := by
+  induction ps <;> simp_all [true, const, entails]
+
+@[simp]
+def FailConds.and {ps : PostShape} (x : FailConds ps) (y : FailConds ps) : FailConds ps :=
+  match ps with
+  | .pure => ()
+  | .arg _ ps => @FailConds.and ps x y
+  | .except _ _ => (fun e => SPred.and (x.1 e) (y.1 e), FailConds.and x.2 y.2)
+
+infixr:35 " ∧ₑ " => FailConds.and
+
+theorem FailConds.and_true {x : FailConds ps} : x ∧ₑ FailConds.true ⊢ₑ x := by
+  induction ps
+  case pure => trivial
+  case arg ih => exact ih
+  case except ε ps ih =>
+    simp_all only [true, and, const]
+    constructor <;> simp only [SPred.and_true.mp, implies_true, ih]
+
+theorem FailConds.true_and {x : FailConds ps} : FailConds.true ∧ₑ x ⊢ₑ x := by
+  induction ps
+  case pure => trivial
+  case arg ih => exact ih
+  case except ε ps ih =>
+    simp_all only [true, and, const]
+    constructor <;> simp only [SPred.true_and.mp, implies_true, ih]
+
+theorem FailConds.and_false {x : FailConds ps} : x ∧ₑ FailConds.false ⊢ₑ FailConds.false := by
+  induction ps
+  case pure => trivial
+  case arg ih => exact ih
+  case except ε ps ih =>
+    simp_all only [false, and, const]
+    constructor <;> simp only [SPred.and_false.mp, implies_true, ih]
+
+theorem FailConds.false_and {x : FailConds ps} : FailConds.false ∧ₑ x ⊢ₑ FailConds.false := by
+  induction ps
+  case pure => trivial
+  case arg ih => exact ih
+  case except ε ps ih =>
+    simp_all only [and, false, const]
+    constructor <;> simp only [SPred.false_and.mp, implies_true, ih]
+
+theorem FailConds.and_eq_left {ps : PostShape} {p q : FailConds ps} (h : p ⊢ₑ q) :
+    p = (p ∧ₑ q) := by
+  induction ps
+  case pure => trivial
+  case arg ih => exact ih h
+  case except ε ps ih =>
+    simp_all only [and]
+    apply Prod.ext
+    · ext a; exact (SPred.and_eq_left.mp (h.1 a)).to_eq
+    · exact ih h.2
+
+/--
+  A multi-barreled postcondition for the given predicate shape.
+  ```
+  example : PostCond α (.arg ρ .pure) = ((α → ρ → Prop) × Unit) := rfl
+  example : PostCond α (.except ε .pure) = ((α → Prop) × (ε → Prop) × Unit) := rfl
+  example : PostCond α (.arg σ (.except ε .pure)) = ((α → σ → Prop) × (ε → Prop) × Unit) := rfl
+  example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → Prop) × (ε → σ → Prop) × Unit) := rfl
+  ```
+-/
+abbrev PostCond (α : Type) (s : PostShape) : Type :=
+  (α → Assertion s) × FailConds s
+
+/-- A postcondition expressing total correctness. -/
+abbrev PostCond.total (p : α → Assertion ps) : PostCond α ps :=
+  (p, FailConds.false)
+
+/-- A postcondition expressing partial correctness. -/
+abbrev PostCond.partial (p : α → Assertion ps) : PostCond α ps :=
+  (p, FailConds.true)
+
+instance : Inhabited (PostCond α ps) where
+  default := PostCond.total fun _ => default
+
+@[simp]
+def PostCond.entails (p q : PostCond α ps) : Prop :=
+  (∀ a, SPred.entails (p.1 a) (q.1 a)) ∧ FailConds.entails p.2 q.2
+
+infixr:25 " ⊢ₚ " => PostCond.entails
+
+@[refl,simp]
+theorem PostCond.entails.refl (Q : PostCond α ps) : Q ⊢ₚ Q := ⟨fun a => SPred.entails.refl (Q.1 a), FailConds.entails.refl Q.2⟩
+theorem PostCond.entails.rfl {Q : PostCond α ps} : Q ⊢ₚ Q := refl Q
+
+theorem PostCond.entails.trans {P Q R : PostCond α ps} (h₁ : P ⊢ₚ Q) (h₂ : Q ⊢ₚ R) : P ⊢ₚ R :=
+  ⟨fun a => (h₁.1 a).trans (h₂.1 a), h₁.2.trans h₂.2⟩
+
+@[simp]
+theorem PostCond.entails_total (p : α → Assertion ps) (q : PostCond α ps) : PostCond.total p ⊢ₚ q ↔ ∀ a, p a ⊢ₛ q.1 a := by
+  simp only [entails, FailConds.entails_false, and_true]
+
+@[simp]
+theorem PostCond.entails_partial (p : PostCond α ps) (q : α → Assertion ps) : p ⊢ₚ PostCond.partial q ↔ ∀ a, p.1 a ⊢ₛ q a := by
+  simp only [entails, FailConds.entails_true, and_true]
+
+abbrev PostCond.and (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
+  (fun a => SPred.and (p.1 a) (q.1 a), FailConds.and p.2 q.2)
+
+infixr:35 " ∧ₚ " => PostCond.and
+
+theorem PostCond.and_eq_left {p q : PostCond α ps} (h : p ⊢ₚ q) :
+    p = (p ∧ₚ q) := by
+  ext
+  · exact (SPred.and_eq_left.mp (h.1 _)).to_eq
+  · exact FailConds.and_eq_left h.2
diff --git a/src/Std/Do/PredTrans.lean b/src/Std/Do/PredTrans.lean
new file mode 100644
index 0000000000..7858e3315d
--- /dev/null
+++ b/src/Std/Do/PredTrans.lean
@@ -0,0 +1,239 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Init.Control.Lawful
+import Std.Do.PostCond
+
+/-!
+# Predicate transformers for arbitrary postcondition shapes
+
+This module defines the type `PredTrans ps` of *predicate transformers* for a given `ps :
+PostShape`.
+`PredTrans` forms the semantic domain of the weakest precondition interpretation
+`WP` in which we interpret monadic programs.
+
+A predicate transformer `x : PredTrans ps α` is a function that takes a postcondition
+`Q : PostCond α ps` and returns a precondition `x.apply Q : Assertion ps`, with the additional
+monotonicity property that the precondition is stronger the stronger the postcondition is:
+`Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂`.
+
+Since `PredTrans` itself forms a monad, we can interpret monadic programs by writing
+a monad morphism into `PredTrans`; this is exactly what `WP` encodes.
+This module defines interpretations of common monadic operations, such as `get`, `throw`,
+`liftM`, etc.
+-/
+
+namespace Std.Do
+
+/-- The stronger the postcondition, the stronger the transformed precondition. -/
+def PredTrans.Monotonic {ps : PostShape} {α : Type} (t : PostCond α ps → Assertion ps) : Prop :=
+  ∀ Q₁ Q₂, (Q₁ ⊢ₚ Q₂) → (t Q₁) ⊢ₛ (t Q₂)
+
+/-- Transforming a conjunction of postconditions is the same as the conjunction of transformed
+postconditions. -/
+def PredTrans.Conjunctive {ps : PostShape} {α : Type} (t : PostCond α ps → Assertion ps) : Prop :=
+  ∀ Q₁ Q₂, t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂
+
+/-- Any predicate transformer that is conjunctive is also monotonic. -/
+def PredTrans.Conjunctive.mono {ps : PostShape} {α : Type}
+    (t : PostCond α ps → Assertion ps) (h : PredTrans.Conjunctive t) : PredTrans.Monotonic t := by
+  intro Q₁ Q₂ hq
+  replace hq : Q₁ = (Q₁ ∧ₚ Q₂) := PostCond.and_eq_left hq
+  rw [hq, (h Q₁ Q₂).to_eq]
+  exact SPred.and_elim_r
+
+/--
+  The type of predicate transformers for a given `ps : PostShape` and return type `α : Type`.
+  A predicate transformer `x : PredTrans ps α` is a function that takes a postcondition
+  `Q : PostCond α ps` and returns a precondition `x.apply Q : Assertion ps`, with the additional
+  monotonicity property that the precondition is stronger the stronger the postcondition is:
+  `Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂`.
+ -/
+@[ext]
+structure PredTrans (ps : PostShape) (α : Type) : Type where
+  apply : PostCond α ps → Assertion ps
+  conjunctive : PredTrans.Conjunctive apply
+
+namespace PredTrans
+
+theorem mono {ps : PostShape} {α : Type} (t : PredTrans ps α) : Monotonic t.apply :=
+  Conjunctive.mono t.apply t.conjunctive
+
+/--
+  Given a fixed postcondition, the *stronger* predicate transformer will yield a
+  *weaker* precondition.
+-/
+def le {ps : PostShape} {α : Type} (x y : PredTrans ps α) : Prop :=
+  ∀ Q, y.apply Q ⊢ₛ x.apply Q -- the weaker the precondition, the smaller the PredTrans
+instance : LE (PredTrans ps α) := ⟨le⟩
+
+def pure {ps : PostShape} {α : Type} (a : α) : PredTrans ps α :=
+  { apply := fun Q => Q.1 a, conjunctive := by intro _ _; simp }
+
+def bind {ps : PostShape} {α β : Type} (x : PredTrans ps α) (f : α → PredTrans ps β) : PredTrans ps β :=
+  { apply := fun Q => x.apply (fun a => (f a).apply Q, Q.2),
+    conjunctive := by
+      intro Q₁ Q₂
+      apply SPred.bientails.of_eq
+      dsimp
+      conv => rhs; rw [← (x.conjunctive _ _).to_eq]
+      conv in (f _).apply _ => rw [((f _).conjunctive _ _).to_eq]
+  }
+
+def const {ps : PostShape} {α : Type} (p : Assertion ps) : PredTrans ps α :=
+  { apply := fun Q => p, conjunctive := by intro _ _; simp [SPred.and_self.to_eq] }
+
+instance : Monad (PredTrans ps) where
+  pure := pure
+  bind := bind
+
+@[simp]
+theorem pure_apply {ps : PostShape} {α : Type} (a : α) (Q : PostCond α ps) :
+  (PredTrans.pure a : PredTrans ps α).apply Q = Q.1 a := by rfl
+
+@[simp]
+theorem Pure_pure_apply {ps : PostShape} {α : Type} (a : α) (Q : PostCond α ps) :
+  (Pure.pure a : PredTrans ps α).apply Q = Q.1 a := by rfl
+
+@[simp]
+theorem map_apply {ps : PostShape} {α β : Type} (f : α → β) (x : PredTrans ps α) (Q : PostCond β ps) :
+  (f <$> x).apply Q = x.apply (fun a => Q.1 (f a), Q.2) := by rfl
+
+@[simp]
+theorem bind_apply {ps : PostShape} {α β : Type} (x : PredTrans ps α) (f : α → PredTrans ps β) (Q : PostCond β ps) :
+  (x >>= f).apply Q = x.apply (fun a => (f a).apply Q, Q.2) := by rfl
+
+@[simp]
+theorem seq_apply {ps : PostShape} {α β : Type} (f : PredTrans ps (α → β)) (x : PredTrans ps α) (Q : PostCond β ps) :
+  (f <*> x).apply Q = f.apply (fun g => x.apply (fun a => Q.1 (g a), Q.2), Q.2) := by rfl
+
+theorem bind_mono {ps : PostShape} {α β : Type} {x y : PredTrans ps α} {f : α → PredTrans ps β}
+  (h : x ≤ y) : x >>= f ≤ y >>= f := by intro Q; exact (h (_, Q.2))
+
+instance instLawfulMonad : LawfulMonad (PredTrans ps) :=
+  LawfulMonad.mk' (PredTrans ps)
+    (id_map := by simp +unfoldPartialApp [Functor.map, bind, pure])
+    (pure_bind := by simp +unfoldPartialApp [Bind.bind, bind, Pure.pure, pure])
+    (bind_assoc := by simp +unfoldPartialApp [Bind.bind, bind])
+
+-- The interpretation of `StateT σ (PredTrans ps) α` into `PredTrans (.arg σ ps) α`.
+-- Think: modifyGetM
+def pushArg {ps : PostShape} {σ : Type} {α : Type} (x : StateT σ (PredTrans ps) α) : PredTrans (.arg σ ps) α :=
+  { apply := fun Q s => (x s).apply (fun (a, s) => Q.1 a s, Q.2),
+    conjunctive := by
+      intro Q₁ Q₂
+      apply SPred.bientails.of_eq
+      ext s
+      dsimp
+      rw [← ((x s).conjunctive _ _).to_eq]
+  }
+
+def popArg {ps : PostShape} {α} (x : PredTrans (.arg σ ps) α) : StateT σ (PredTrans ps) α := fun s =>
+  { apply Q := x.apply (fun r s' => Q.1 (r, s'), Q.2) s,
+    conjunctive := by
+      intro Q₁ Q₂
+      apply SPred.bientails.of_eq
+      dsimp
+      have {Q₁ Q₂}: spred(x.apply Q₁ ∧ x.apply Q₂) s = spred(x.apply (Q₁ ∧ₚ Q₂) s) := by
+        rw[congrFun (x.conjunctive _ _).to_eq _]
+      simp only [SPred.and] at this
+      simp only [this]
+      rfl
+  }
+
+-- The interpretation of `ExceptT ε (PredTrans ps) α` into `PredTrans (.except ε ps) α`
+def pushExcept {ps : PostShape} {α ε} (x : ExceptT ε (PredTrans ps) α) : PredTrans (.except ε ps) α :=
+  { apply Q := x.apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2),
+    conjunctive := by
+      intro Q₁ Q₂
+      apply SPred.bientails.of_eq
+      dsimp
+      rw[← (x.conjunctive _ _).to_eq]
+      congr
+      ext x
+      cases x <;> simp
+  }
+
+def popExcept {ps : PostShape} {α} (x : PredTrans (.except ε ps) α) : ExceptT ε (PredTrans ps) α :=
+  { apply Q := x.apply (fun a => Q.1 (.ok a), fun e => Q.1 (.error e), Q.2),
+    conjunctive := by
+      intro Q₁ Q₂
+      apply SPred.bientails.of_eq
+      dsimp
+      rw[← (x.conjunctive _ _).to_eq]
+      rfl
+  }
+
+instance instMonadLiftArg : MonadLift (PredTrans m) (PredTrans (.arg σ m)) where
+  monadLift x := pushArg (StateT.lift x)
+
+instance instMonadLiftExcept : MonadLift (PredTrans m) (PredTrans (.except ε m)) where
+  monadLift x := pushExcept (ExceptT.lift x)
+
+instance instMonadFunctorArg : MonadFunctor (PredTrans m) (PredTrans (.arg σ m)) where
+  monadMap f x := pushArg (fun s => f (popArg x s))
+
+instance instMonadFunctorExcept : MonadFunctor (PredTrans m) (PredTrans (.except ε m)) where
+  monadMap f x := pushExcept (f x.popExcept)
+
+@[simp]
+def pushArg_apply {ps} {α : Type} {σ : Type} {Q : PostCond α (.arg σ ps)} (f : σ → PredTrans ps (α × σ)) :
+  (pushArg f).apply Q = fun s => (f s).apply (fun ⟨a, s⟩ => Q.1 a s, Q.2) := rfl
+
+@[simp]
+def pushExcept_apply {ps} {α ε} {Q : PostCond α (.except ε ps)} (x : PredTrans ps (Except ε α)) :
+  (pushExcept x).apply Q = x.apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := rfl
+
+def dite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : c → PredTrans ps α) (e : ¬ c → PredTrans ps α) :
+  (if h : c then t h else e h).apply Q = if h : c then (t h).apply Q else (e h).apply Q := by split <;> rfl
+
+def ite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : PredTrans ps α) (e : PredTrans ps α) :
+  (if c then t else e).apply Q = if c then t.apply Q else e.apply Q := by split <;> rfl
+
+@[simp]
+def monadLiftArg_apply {ps} {Q : PostCond α (.arg σ ps)} (t : PredTrans ps α) :
+  (MonadLift.monadLift t : PredTrans (.arg σ ps) α).apply Q = fun s => t.apply (fun a => Q.1 a s, Q.2) := rfl
+
+@[simp]
+def monadLiftExcept_apply {ps} {Q : PostCond α (.except ε ps)} (t : PredTrans ps α) :
+  (MonadLift.monadLift t : PredTrans (.except ε ps) α).apply Q = t.apply (fun a => Q.1 a, Q.2.2) := rfl
+
+@[simp]
+def monadMapArg_apply {ps} {Q : PostCond α (.arg σ ps)} (f : ∀{β}, PredTrans ps β → PredTrans ps β) (t : PredTrans (.arg σ ps) α) :
+  (MonadFunctor.monadMap (m:=PredTrans ps) f t).apply Q = fun s => (f (t.popArg s)).apply (fun (a, s) => Q.1 a s, Q.2) := rfl
+
+@[simp]
+def monadMapExcept_apply {ps} {Q : PostCond α (.except ε ps)} (f : ∀{β}, PredTrans ps β → PredTrans ps β) (t : PredTrans (.except ε ps) α) :
+  (MonadFunctor.monadMap (m:=PredTrans ps) f t).apply Q = (f t.popExcept).apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := rfl
+
+@[simp]
+def popArg_apply {ps} {Q : PostCond (α × σ) ps} (t : PredTrans (.arg σ ps) α) :
+  (t.popArg s).apply Q = t.apply (fun a s => Q.1 (a, s), Q.2) s := rfl
+
+@[simp]
+def popExcept_apply {ps} {Q : PostCond (Except ε α) ps} (t : PredTrans (.except ε ps) α) :
+  (t.popExcept).apply Q = t.apply (fun a => Q.1 (.ok a), fun e => Q.1 (.error e), Q.2) := rfl
+
+@[simp]
+theorem pushArg_popArg : pushArg (popArg x) = x := rfl
+
+@[simp]
+theorem popArg_pushArg : popArg (pushArg f) = f := rfl
+
+-- Just a reminder for me that the following would not hold for a suitable defn of pushReader and popReader:
+--theorem pushReader_popReader : pushReader (popReader x) = x := sorry
+--  goal: x.apply (fun a x => Q.1 a x✝, Q.2) x✝ = x.apply Q x✝
+
+@[simp]
+theorem pushExcept_popExcept : pushExcept (popExcept x) = x := rfl
+
+@[simp]
+theorem popExcept_pushExcept : popExcept (pushExcept x) = x := by
+  ext Q
+  simp only [ExceptT.run, popExcept, pushExcept]
+  congr
+  ext x
+  cases x <;> simp
diff --git a/src/Std/Do/Triple.lean b/src/Std/Do/Triple.lean
new file mode 100644
index 0000000000..272c365335
--- /dev/null
+++ b/src/Std/Do/Triple.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.Triple.Basic
+import Std.Do.Triple.SpecLemmas
diff --git a/src/Std/Do/Triple/Basic.lean b/src/Std/Do/Triple/Basic.lean
new file mode 100644
index 0000000000..83757221fc
--- /dev/null
+++ b/src/Std/Do/Triple/Basic.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.WP
+import Std.Do.SPred
+
+/-!
+# Hoare triples
+
+Hoare triples form the basis for compositional functional correctness proofs about monadic programs.
+
+As usual, `Triple x P Q` holds iff the precondition `P` entails the weakest precondition
+`wp⟦x⟧.apply Q` of `x : m α` for the postcondition `Q`.
+It is thus defined in terms of an instance `WP m ps`.
+-/
+
+namespace Std.Do
+
+universe u
+variable {m : Type → Type u} {ps : PostShape}
+
+/--
+  A Hoare triple for reasoning about monadic programs.
+  A proof for `Triple x P Q` is a *specification* for `x`:
+  If assertion `P` holds before `x`, then postcondition `Q` holds after running `x`.
+
+  `⦃P⦄ x ⦃Q⦄` is convenient syntax for `Triple x P Q`.
+-/
+def Triple [WP m ps] {α} (x : m α) (P : Assertion ps) (Q : PostCond α ps) : Prop :=
+  P ⊢ₛ wp⟦x⟧ Q
+
+@[inherit_doc Std.Do.Triple]
+scoped syntax:lead (name := triple) "⦃" term "⦄ " term:lead " ⦃" term "⦄" : term
+
+namespace Triple
+
+instance [WP m ps] (x : m α) : SPred.Tactic.PropAsSPredTautology (Triple x P Q) spred(P → wp⟦x⟧ Q) where
+  iff := (SPred.entails_true_intro P (wp⟦x⟧ Q)).symm
+
+theorem pure [Monad m] [WPMonad m ps] {α} {Q : PostCond α ps} (a : α) (himp : P ⊢ₛ Q.1 a) :
+  Triple (pure (f:=m) a) P Q := himp.trans (by simp)
+
+theorem bind [Monad m] [WPMonad m ps] {α β} {P : Assertion ps} {Q : α → Assertion ps} {R : PostCond β ps} (x : m α) (f : α → m β)
+    (hx : Triple x P (Q, R.2))
+    (hf : ∀ b, Triple (f b) (Q b) R) :
+    Triple (x >>= f) P R := by
+  apply SPred.entails.trans hx
+  simp only [WP.bind]
+  apply (wp x).mono _ _
+  simp only [PostCond.entails, Assertion, FailConds.entails.refl, and_true]
+  exact hf
+
+theorem and [WP m ps] (x : m α) (h₁ : Triple x P₁ Q₁) (h₂ : Triple x P₂ Q₂) : Triple x spred(P₁ ∧ P₂) (Q₁ ∧ₚ Q₂) :=
+  (SPred.and_mono h₁ h₂).trans ((wp x).conjunctive Q₁ Q₂).mpr
+
+theorem rewrite_program [WP m ps] {prog₁ prog₂ : m α}
+  (heq : prog₁ = prog₂) (hprf : Triple prog₂ P Q) :
+  Triple prog₁ P Q := heq ▸ hprf
+
+end Triple
diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean
new file mode 100644
index 0000000000..8f5b592fa5
--- /dev/null
+++ b/src/Std/Do/Triple/SpecLemmas.lean
@@ -0,0 +1,481 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.Triple.Basic
+import Std.Tactic.Do.Syntax
+import Std.Do.WP
+
+/-!
+# Hoare triple specifications for select functions
+
+This module contains Hoare triple specifications for some functions in Core.
+-/
+
+namespace Std.Range
+
+abbrev toList (r : Std.Range) : List Nat :=
+  List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step
+
+theorem toList_range' (r : Std.Range) (h : r.step = 1) :
+    toList r = List.range' r.start (r.stop - r.start) := by
+  simp [toList, h]
+
+end Std.Range
+
+namespace Std.List
+
+@[ext]
+structure Zipper {α : Type u} (l : List α) : Type u where
+  rpref : List α
+  suff : List α
+  property : rpref.reverse ++ suff = l
+
+abbrev Zipper.pref {α} {l : List α} (s : List.Zipper l) : List α := s.rpref.reverse
+
+abbrev Zipper.begin (l : List α) : Zipper l := ⟨[],l,rfl⟩
+abbrev Zipper.end (l : List α) : Zipper l := ⟨l.reverse,[],by simp⟩
+abbrev Zipper.tail (s : Zipper l) (h : s.suff = hd::tl) : Zipper l :=
+  { rpref := hd::s.rpref, suff := tl, property := by simp [s.property, ←h] }
+
+end Std.List
+
+namespace Std.Do
+
+-- We override the `Triple` notation in `Std.Do.Triple.Basic` just in this module.
+-- The reason is that the actual `Triple` notation is implemented as an elaborator in
+-- `Lean.Elab.Tactic.Do.Syntax` for reasons such as #8766. Perhaps #8074 will help.
+@[inherit_doc Std.Do.triple]
+local notation:lead "⦃" P "⦄ " x:lead " ⦃" Q "⦄" => Triple x (spred(P)) spred(Q)
+
+/-! # If/Then/Else -/
+
+-- @[spec]
+theorem Spec.ite {α m ps} {P : Assertion ps} {Q : PostCond α ps} (c : Prop) [Decidable c] [WP m ps] (t : m α) (e : m α)
+    (ifTrue : c → ⦃P⦄ t ⦃Q⦄) (ifFalse : ¬c → ⦃P⦄ e ⦃Q⦄) :
+    ⦃P⦄ if c then t else e ⦃Q⦄ := by
+  split <;> apply_rules
+
+-- @[spec]
+theorem Spec.dite {α m ps} {P : Assertion ps} {Q : PostCond α ps} (c : Prop) [Decidable c] [WP m ps] (t : c → m α) (e : ¬ c → m α)
+    (ifTrue : (h : c) → ⦃P⦄ t h ⦃Q⦄) (ifFalse : (h : ¬ c) → ⦃P⦄ e h ⦃Q⦄) :
+    ⦃P⦄ if h : c then t h else e h ⦃Q⦄ := by
+  split <;> apply_rules
+
+/-! # `Monad` -/
+
+universe u
+variable {m : Type → Type u} {ps : PostShape}
+
+theorem Spec.pure' [Monad m] [WPMonad m ps] {P : Assertion ps} {Q : PostCond α ps}
+    (h : P ⊢ₛ Q.1 a) :
+    ⦃P⦄ Pure.pure (f:=m) a ⦃Q⦄ := Triple.pure a h
+
+-- @[spec]
+theorem Spec.pure {m : Type → Type u} {ps : PostShape} [Monad m] [WPMonad m ps] {α} {a : α} {Q : PostCond α ps} :
+  ⦃Q.1 a⦄ Pure.pure (f:=m) a ⦃Q⦄ := Spec.pure' .rfl
+
+theorem Spec.bind' [Monad m] [WPMonad m ps] {x : m α} {f : α → m β} {P : Assertion ps} {Q : PostCond β ps}
+    (h : ⦃P⦄ x ⦃(fun a => wp⟦f a⟧ Q, Q.2)⦄) :
+    ⦃P⦄ (x >>= f) ⦃Q⦄ := Triple.bind x f h (fun _ => .rfl)
+
+-- @[spec]
+theorem Spec.bind {m : Type → Type u} {ps : PostShape} [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → m β} {Q : PostCond β ps} :
+  ⦃wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2)⦄ (x >>= f) ⦃Q⦄ := Spec.bind' .rfl
+
+-- @[spec]
+theorem Spec.map {m : Type → Type u} {ps : PostShape} [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → β} {Q : PostCond β ps} :
+  ⦃wp⟦x⟧ (fun a => Q.1 (f a), Q.2)⦄ (f <$> x) ⦃Q⦄ := by simp [Triple, SPred.entails.refl]
+
+-- @[spec]
+theorem Spec.seq {m : Type → Type u} {ps : PostShape} [Monad m] [WPMonad m ps] {α β} {x : m (α → β)} {y : m α} {Q : PostCond β ps} :
+  ⦃wp⟦x⟧ (fun f => wp⟦y⟧ (fun a => Q.1 (f a), Q.2), Q.2)⦄ (x <*> y) ⦃Q⦄ := by simp [Triple, SPred.entails.refl]
+
+/-! # `MonadLift` -/
+
+-- @[spec]
+theorem Spec.monadLift_StateT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.arg σ ps)) :
+  ⦃fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2)⦄ (MonadLift.monadLift x : StateT σ m α) ⦃Q⦄ := by simp [Triple, SPred.entails.refl]
+
+-- @[spec]
+theorem Spec.monadLift_ReaderT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.arg ρ ps)) :
+  ⦃fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2)⦄ (MonadLift.monadLift x : ReaderT ρ m α) ⦃Q⦄ := by simp [Triple, SPred.entails.refl]
+
+-- @[spec]
+theorem Spec.monadLift_ExceptT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.except ε ps)) :
+  Triple (ps:=.except ε ps)
+    (MonadLift.monadLift x : ExceptT ε m α)
+    (wp⟦x⟧ (fun a => Q.1 a, Q.2.2))
+    Q := by simp [Triple, SPred.entails.refl]
+
+/-! # `MonadLiftT` -/
+
+-- attribute [spec] liftM instMonadLiftTOfMonadLift instMonadLiftT
+
+/-! # `MonadFunctor` -/
+
+-- @[spec]
+theorem Spec.monadMap_StateT [Monad m] [WP m ps]
+    (f : ∀{β}, m β → m β) {α} (x : StateT σ m α) (Q : PostCond α (.arg σ ps)) :
+    ⦃fun s => wp⟦f (x.run s)⟧ (fun (a, s) => Q.1 a s, Q.2)⦄ (MonadFunctor.monadMap (m:=m) f x) ⦃Q⦄ := .rfl
+
+-- @[spec]
+theorem Spec.monadMap_ReaderT [Monad m] [WP m ps]
+    (f : ∀{β}, m β → m β) {α} (x : ReaderT ρ m α) (Q : PostCond α (.arg ρ ps)) :
+    ⦃fun s => wp⟦f (x.run s)⟧ (fun a => Q.1 a s, Q.2)⦄ (MonadFunctor.monadMap (m:=m) f x) ⦃Q⦄ := .rfl
+
+-- @[spec]
+theorem Spec.monadMap_ExceptT [Monad m] [WP m ps]
+    (f : ∀{β}, m β → m β) {α} (x : ExceptT ε m α) (Q : PostCond α (.except ε ps)) :
+  Triple (ps:=.except ε ps)
+    (MonadFunctor.monadMap (m:=m) f x)
+    (wp⟦f x.run⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2))
+    Q := by simp only [Triple, WP.monadMap_ExceptT]; rfl
+
+/-! # `MonadFunctorT` -/
+
+-- @[spec]
+theorem Spec.monadMap_trans [WP o ps] [MonadFunctor n o] [MonadFunctorT m n] :
+  Triple (ps:=ps)
+    (MonadFunctorT.monadMap f x : o α)
+    (wp⟦MonadFunctor.monadMap (m:=n) (MonadFunctorT.monadMap (m:=m) f) x : o α⟧ Q)
+    Q := by simp [Triple]
+
+-- @[spec]
+theorem Spec.monadMap_refl [WP m ps] :
+  ⦃wp⟦f x : m α⟧ Q⦄
+  (MonadFunctorT.monadMap f x : m α)
+  ⦃Q⦄ := by simp [Triple]
+
+/-! # `ReaderT` -/
+
+-- attribute [spec] ReaderT.run
+
+-- @[spec]
+theorem Spec.read_ReaderT [Monad m] [WPMonad m psm] :
+  ⦃fun r => Q.1 r r⦄ (MonadReaderOf.read : ReaderT ρ m ρ) ⦃Q⦄ := by simp [Triple]
+
+-- @[spec]
+theorem Spec.withReader_ReaderT [Monad m] [WPMonad m psm] :
+  ⦃fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r)⦄ (MonadWithReaderOf.withReader f x : ReaderT ρ m α) ⦃Q⦄ := by simp [Triple]
+
+/-! # `StateT` -/
+
+-- attribute [spec] StateT.run
+
+-- @[spec]
+theorem Spec.get_StateT [Monad m] [WPMonad m psm] :
+  ⦃fun s => Q.1 s s⦄ (MonadStateOf.get : StateT σ m σ) ⦃Q⦄ := by simp [Triple]
+
+-- @[spec]
+theorem Spec.set_StateT [Monad m] [WPMonad m psm] :
+  ⦃fun _ => Q.1 () s⦄ (MonadStateOf.set s : StateT σ m PUnit) ⦃Q⦄ := by simp [Triple]
+
+-- @[spec]
+theorem Spec.modifyGet_StateT [Monad m] [WPMonad m ps] :
+  ⦃fun s => Q.1 (f s).1 (f s).2⦄ (MonadStateOf.modifyGet f : StateT σ m α) ⦃Q⦄ := by
+    simp [Triple]
+
+/-! # `ExceptT` -/
+
+-- @[spec]
+theorem Spec.run_ExceptT [WP m ps] (x : ExceptT ε m α) :
+  Triple (ps:=ps)
+    (x.run : m (Except ε α))
+    (wp⟦x⟧ (fun a => Q.1 (.ok a), fun e => Q.1 (.error e), Q.2))
+    Q := by simp [Triple]
+
+-- @[spec]
+theorem Spec.throw_ExceptT [Monad m] [WPMonad m ps] :
+    ⦃Q.2.1 e⦄ (MonadExceptOf.throw e : ExceptT ε m α) ⦃Q⦄ := by
+  simp [Triple]
+
+-- @[spec]
+theorem Spec.tryCatch_ExceptT [Monad m] [WPMonad m ps] (Q : PostCond α (.except ε ps)) :
+    ⦃wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2)⦄ (MonadExceptOf.tryCatch x h : ExceptT ε m α) ⦃Q⦄ := by
+  simp [Triple]
+
+/-! # `Except` -/
+
+-- @[spec]
+theorem Spec.throw_Except [Monad m] [WPMonad m ps] :
+    ⦃Q.2.1 e⦄ (MonadExceptOf.throw e : Except ε α) ⦃Q⦄ := SPred.entails.rfl
+
+-- @[spec]
+theorem Spec.tryCatch_Except (Q : PostCond α (.except ε .pure)) :
+    ⦃wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2)⦄ (MonadExceptOf.tryCatch x h : Except ε α) ⦃Q⦄ := by
+  simp [Triple]
+
+/-! # `EStateM` -/
+
+-- @[spec]
+theorem Spec.get_EStateM :
+  ⦃fun s => Q.1 s s⦄ (MonadStateOf.get : EStateM ε σ σ) ⦃Q⦄ := SPred.entails.rfl
+
+-- @[spec]
+theorem Spec.set_EStateM :
+  ⦃fun _ => Q.1 () s⦄ (MonadStateOf.set s : EStateM ε σ PUnit) ⦃Q⦄ := SPred.entails.rfl
+
+-- @[spec]
+theorem Spec.modifyGet_EStateM :
+    ⦃fun s => Q.1 (f s).1 (f s).2⦄ (MonadStateOf.modifyGet f : EStateM ε σ α) ⦃Q⦄ := SPred.entails.rfl
+
+-- @[spec]
+theorem Spec.throw_EStateM :
+    ⦃Q.2.1 e⦄ (MonadExceptOf.throw e : EStateM ε σ α) ⦃Q⦄ := SPred.entails.rfl
+
+open EStateM.Backtrackable in
+-- @[spec]
+theorem Spec.tryCatch_EStateM (Q : PostCond α (.except ε (.arg σ .pure))) :
+    ⦃fun s => wp⟦x⟧ (Q.1, fun e s' => wp⟦h e⟧ Q (restore s' (save s)), Q.2.2) s⦄ (MonadExceptOf.tryCatch x h : EStateM ε σ α) ⦃Q⦄ := by
+  simp [Triple]
+
+/-! # Lifting `MonadStateOf` -/
+
+-- attribute [spec] modify modifyThe getThe
+--   instMonadStateOfMonadStateOf instMonadStateOfOfMonadLift
+
+/-! # Lifting `MonadReaderOf` -/
+
+-- attribute [spec] readThe withTheReader
+--   instMonadReaderOfMonadReaderOf instMonadReaderOfOfMonadLift
+--   instMonadWithReaderOfMonadWithReaderOf instMonadWithReaderOfOfMonadFunctor
+
+/-! # Lifting `MonadExceptOf` -/
+
+-- attribute [spec] throwThe tryCatchThe
+
+-- @[spec]
+theorem Spec.throw_MonadExcept [MonadExceptOf ε m] [WP m _]:
+    ⦃wp⟦MonadExceptOf.throw e : m α⟧ Q⦄ (throw e : m α) ⦃Q⦄ := SPred.entails.rfl
+
+-- @[spec]
+theorem Spec.tryCatch_MonadExcept [MonadExceptOf ε m] [WP m ps] (Q : PostCond α ps) :
+    ⦃wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q⦄ (tryCatch x h : m α) ⦃Q⦄ := SPred.entails.rfl
+
+-- @[spec]
+theorem Spec.throw_ReaderT  [WP m sh] [Monad m] [MonadExceptOf ε m] :
+    ⦃wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : ReaderT ρ m α⟧ Q⦄ (MonadExceptOf.throw e : ReaderT ρ m α) ⦃Q⦄ := SPred.entails.rfl
+
+-- @[spec]
+theorem Spec.throw_StateT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.arg σ ps)) :
+    ⦃wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : StateT σ m α⟧ Q⦄ (MonadExceptOf.throw e : StateT σ m α) ⦃Q⦄ := SPred.entails.rfl
+
+-- @[spec]
+theorem Spec.throw_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) :
+  Triple (ps:=.except ε' ps)
+    (MonadExceptOf.throw e : ExceptT ε' m α)
+    (wp⟦MonadExceptOf.throw (ε:=ε) e : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2))
+    Q := by
+  simp [Triple]
+  apply (wp _).mono
+  simp
+  intro x
+  split <;> rfl
+
+-- @[spec]
+theorem Spec.tryCatch_ReaderT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.arg ρ ps)) :
+    ⦃fun r => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run r) (fun e => (h e).run r) : m α⟧ (fun a => Q.1 a r, Q.2)⦄
+    (MonadExceptOf.tryCatch x h : ReaderT ρ m α)
+    ⦃Q⦄ := SPred.entails.rfl
+
+-- @[spec]
+theorem Spec.tryCatch_StateT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.arg σ ps)) :
+    ⦃fun s => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run s) (fun e => (h e).run s) : m (α × σ)⟧ (fun xs => Q.1 xs.1 xs.2, Q.2)⦄
+    (MonadExceptOf.tryCatch x h : StateT σ m α)
+    ⦃Q⦄ := SPred.entails.rfl
+
+-- @[spec]
+theorem Spec.tryCatch_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) :
+    Triple
+      (ps:=.except ε' ps)
+      (MonadExceptOf.tryCatch x h : ExceptT ε' m α)
+      (wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2))
+      Q := by
+  simp only [Triple, WP.tryCatch_lift_ExceptT]
+  apply (wp _).mono
+  simp
+  intro x
+  split <;> rfl
+
+/-! # `ForIn` -/
+
+-- @[spec]
+theorem Spec.forIn'_list {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
+    (inv : PostCond (β × List.Zipper xs) ps)
+    (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs = rpref.reverse ++ x :: suff),
+        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄
+        f x hx b
+        ⦃(fun r => match r with
+                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
+                   | .done b' => inv.1 (b', ⟨xs.reverse, [], by simp⟩), inv.2)⦄) :
+    ⦃inv.1 (init, ⟨[], xs, by simp⟩)⦄ forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)⦄ := by
+  suffices h : ∀ rpref suff (h : xs = rpref.reverse ++ suff),
+      ⦃inv.1 (init, ⟨rpref, suff, by simp [h]⟩)⦄
+      forIn' (m:=m) suff init (fun a ha => f a (by simp[h,ha]))
+      ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp [h]⟩), inv.2)⦄
+    from h [] xs rfl
+  intro rpref suff h
+  induction suff generalizing rpref init
+  case nil => apply Triple.pure; simp [h]
+  case cons x suff ih =>
+    simp only [List.forIn'_cons]
+    apply Triple.bind
+    case hx => exact step init rpref x (by simp[h]) suff h
+    case hf =>
+      intro r
+      split
+      next => apply Triple.pure; simp [h]
+      next b =>
+        simp
+        have := @ih b (x::rpref) (by simp [h])
+        simp at this
+        exact this
+
+-- using the postcondition as a constant invariant:
+theorem Spec.forIn'_list_const_inv {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
+    {inv : PostCond β ps}
+    (step : ∀ x (hx : x ∈ xs) b,
+        ⦃inv.1 b⦄
+        f x hx b
+        ⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)⦄) :
+    ⦃inv.1 init⦄ forIn' xs init f ⦃inv⦄ :=
+  Spec.forIn'_list (fun p => inv.1 p.1, inv.2) (fun b _ x hx _ _ => step x hx b)
+
+-- @[spec]
+theorem Spec.forIn_list {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : List α} {init : β} {f : α → β → m (ForInStep β)}
+    (inv : PostCond (β × List.Zipper xs) ps)
+    (step : ∀ b rpref x suff (h : xs = rpref.reverse ++ x :: suff),
+        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄
+        f x b
+        ⦃(fun r => match r with
+                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
+                   | .done b' => inv.1 (b', ⟨xs.reverse, [], by simp⟩), inv.2)⦄) :
+    ⦃inv.1 (init, ⟨[], xs, by simp⟩)⦄ forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)⦄ := by
+  simp only [← forIn'_eq_forIn]
+  exact Spec.forIn'_list inv (fun b rpref x _ suff h => step b rpref x suff h)
+
+-- using the postcondition as a constant invariant:
+theorem Spec.forIn_list_const_inv {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : List α} {init : β} {f : α → β → m (ForInStep β)}
+    {inv : PostCond β ps}
+    (step : ∀ hd b,
+        ⦃inv.1 b⦄
+        f hd b
+        ⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)⦄) :
+    ⦃inv.1 init⦄ forIn xs init f ⦃inv⦄ :=
+  Spec.forIn_list (fun p => inv.1 p.1, inv.2) (fun b _ hd _ _ => step hd b)
+
+-- @[spec]
+theorem Spec.foldlM_list {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : List α} {init : β} {f : β → α → m β}
+    (inv : PostCond (β × List.Zipper xs) ps)
+    (step : ∀ b rpref x suff (h : xs = rpref.reverse ++ x :: suff),
+        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄
+        f b x
+        ⦃(fun b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩), inv.2)⦄) :
+    ⦃inv.1 (init, ⟨[], xs, by simp⟩)⦄ List.foldlM f init xs ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)⦄ := by
+  have : xs.foldlM f init = forIn xs init (fun a b => .yield <$> f b a) := by
+    simp only [List.forIn_yield_eq_foldlM, id_map']
+  rw[this]
+  apply Spec.forIn_list inv
+  simp only [Triple, WPMonad.wp_map, PredTrans.map_apply]
+  exact step
+
+-- using the postcondition as a constant invariant:
+theorem Spec.foldlM_list_const_inv {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : List α} {init : β} {f : β → α → m β}
+    {inv : PostCond β ps}
+    (step : ∀ hd b,
+        ⦃inv.1 b⦄
+        f b hd
+        ⦃(fun b' => inv.1 b', inv.2)⦄) :
+  ⦃inv.1 init⦄ List.foldlM f init xs ⦃inv⦄ :=
+    Spec.foldlM_list (fun p => inv.1 p.1, inv.2) (fun b _ hd _ _ => step hd b)
+
+-- @[spec]
+theorem Spec.forIn'_range {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : Std.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
+    (inv : PostCond (β × List.Zipper xs.toList) ps)
+    (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff),
+        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄
+        f x hx b
+        ⦃(fun r => match r with
+                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
+                   | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄) :
+    ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)⦄ forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄ := by
+  simp only [Std.Range.forIn'_eq_forIn'_range', Std.Range.size, Std.Range.size.eq_1]
+  apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (Std.Range.mem_of_mem_range' hx) suff h)
+
+-- @[spec]
+theorem Spec.forIn_range {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : Std.Range} {init : β} {f : Nat → β → m (ForInStep β)}
+    (inv : PostCond (β × List.Zipper xs.toList) ps)
+    (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
+        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄
+        f x b
+        ⦃(fun r => match r with
+                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
+                   | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄) :
+    ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)⦄ forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄ := by
+  simp only [Std.Range.forIn_eq_forIn_range', Std.Range.size]
+  apply Spec.forIn_list inv step
+
+-- @[spec]
+theorem Spec.forIn'_array {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : Array α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
+    (inv : PostCond (β × List.Zipper xs.toList) ps)
+    (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff),
+        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄
+        f x hx b
+        ⦃(fun r => match r with
+                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
+                   | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄) :
+    ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)⦄ forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄ := by
+  cases xs
+  simp
+  apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (by simp[hx]) suff h)
+
+-- @[spec]
+theorem Spec.forIn_array {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : Array α} {init : β} {f : α → β → m (ForInStep β)}
+    (inv : PostCond (β × List.Zipper xs.toList) ps)
+    (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
+        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄
+        f x b
+        ⦃(fun r => match r with
+                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
+                   | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄) :
+    ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)⦄ forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄ := by
+  cases xs
+  simp
+  apply Spec.forIn_list inv step
+
+-- @[spec]
+theorem Spec.foldlM_array {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
+    [Monad m] [WPMonad m ps]
+    {xs : Array α} {init : β} {f : β → α → m β}
+    (inv : PostCond (β × List.Zipper xs.toList) ps)
+    (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
+        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄
+        f b x
+        ⦃(fun b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩), inv.2)⦄) :
+    ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)⦄ Array.foldlM f init xs ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄ := by
+  cases xs
+  simp
+  apply Spec.foldlM_list inv step
diff --git a/src/Std/Do/WP.lean b/src/Std/Do/WP.lean
new file mode 100644
index 0000000000..a889972579
--- /dev/null
+++ b/src/Std/Do/WP.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.WP.Basic
+import Std.Do.WP.Monad
+import Std.Do.WP.IO
+import Std.Do.WP.SimpLemmas
diff --git a/src/Std/Do/WP/Basic.lean b/src/Std/Do/WP/Basic.lean
new file mode 100644
index 0000000000..4e6142390b
--- /dev/null
+++ b/src/Std/Do/WP/Basic.lean
@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.PredTrans
+
+/-!
+# Weakest precondition interpretation
+
+This module defines the weakest precondition interpretation `WP` of monadic programs
+in terms of predicate transformers `PredTrans`.
+
+This interpretation forms the basis of our notion of Hoare triples.
+It is the main mechanism of this library for reasoning about monadic programs.
+
+An instance `WP m ps` determines an interpretation `wp⟦x⟧` of a program `x : m α` in terms of a
+predicate transformer `PredTrans ps α`; The monad `m` determines `ps : PostShape` and hence
+the particular shape of the predicate transformer.
+
+This library comes with pre-defined instances for common monads and transformers such as
+
+* `WP Id .pure`, interpreting pure computations `x : Id α` in terms of a function (isomorphic to)
+  `(α → Prop) → Prop`.
+* `WP (StateT σ m) (.arg σ ps)` given an instance `WP m ps`, interpreting `StateM σ α` in terms of
+  a function `(α → σ → Prop) → σ → Prop`.
+* `WP (ExceptT ε m) (.except ε ps)` given an instance `WP m ps`, interpreting `Except ε α` in terms
+  of `(α → Prop) → (ε → Prop) → Prop`.
+* `WP (EStateM ε σ) (.except ε (.arg σ .pure))` interprets `EStateM ε σ α` in terms of
+  a function `(α → σ → Prop) → (ε → σ → Prop) → σ → Prop`.
+
+These instances are all monad morphisms, a fact which is properly encoded and exploited
+by the subclass `WPMonad`.
+-/
+
+namespace Std.Do
+
+universe u
+variable {m : Type → Type u}
+
+/--
+  A weakest precondition interpretation of a monadic program `x : m α` in terms of a
+  predicate transformer `PredTrans ps α`.
+  The monad `m` determines `ps : PostShape`. See the module comment for more details.
+-/
+class WP (m : Type → Type u) (ps : outParam PostShape) where
+  wp {α} (x : m α) : PredTrans ps α
+
+export WP (wp)
+
+scoped syntax:max "wp⟦" term:min (":" term)? "⟧" : term
+macro_rules
+  | `(wp⟦$x:term⟧) => `((WP.wp $x).apply)
+  | `(wp⟦$x:term : $ty⟧) => `((WP.wp ($x : $ty)).apply)
+
+@[app_unexpander PredTrans.apply]
+protected def unexpandWP : Lean.PrettyPrinter.Unexpander
+  | `($_ $e) => match e with
+    | `(wp ($x : $ty)) => `(wp⟦$x : $ty⟧)
+    | `(wp $e) => `(wp⟦$e⟧)
+    | _ => throw ()
+  | _ => throw ()
+instance Id.instWP : WP Id .pure where
+  wp x := PredTrans.pure x.run
+
+instance StateT.instWP [WP m ps] : WP (StateT σ m) (.arg σ ps) where
+  wp x := PredTrans.pushArg (fun s => wp (x s))
+
+instance ReaderT.instWP [WP m ps] : WP (ReaderT ρ m) (.arg ρ ps) where
+  wp x := PredTrans.pushArg (fun s => (·, s) <$> wp (x s))
+
+instance ExceptT.instWP [WP m ps] : WP (ExceptT ε m) (.except ε ps) where
+  wp x := PredTrans.pushExcept (wp x)
+
+instance EStateM.instWP : WP (EStateM ε σ) (.except ε (.arg σ .pure)) where
+  wp x := -- Could define as PredTrans.mkExcept (PredTrans.modifyGetM (fun s => pure (EStateM.Result.toExceptState (x s))))
+    { apply := fun Q s => match x s with
+        | .ok a s' => Q.1 a s'
+        | .error e s' => Q.2.1 e s'
+      conjunctive := by
+        intro _ _
+        apply SPred.bientails.of_eq
+        ext s
+        dsimp
+        cases (x s) <;> simp
+    }
+
+instance State.instWP : WP (StateM σ) (.arg σ .pure) :=
+  inferInstanceAs (WP (StateT σ Id) (.arg σ .pure))
+instance Reader.instWP : WP (ReaderM ρ) (.arg ρ .pure) :=
+  inferInstanceAs (WP (ReaderT ρ Id) (.arg ρ .pure))
+instance Except.instWP : WP (Except ε) (.except ε .pure) :=
+  inferInstanceAs (WP (ExceptT ε Id) (.except ε .pure))
+
+theorem Id.by_wp {α} {x : α} {prog : Id α} (h : Id.run prog = x) (P : α → Prop) :
+  wp⟦prog⟧ (PostCond.total P) → P x := h ▸ id
+
+theorem StateM.by_wp {α} {x : α × σ} {prog : StateM σ α} (h : StateT.run prog s = x) (P : α × σ → Prop) :
+  wp⟦prog⟧ (PostCond.total (fun a s' => P (a, s'))) s → P x := by
+    intro hspec
+    simp only [wp, PredTrans.pure, PredTrans.pushArg_apply] at hspec
+    exact h ▸ hspec
+
+theorem EStateM.by_wp {α} {x : EStateM.Result ε σ α} {prog : EStateM ε σ α} (h : EStateM.run prog s = x) (P : EStateM.Result ε σ α → Prop) :
+  wp⟦prog⟧ (PostCond.total (fun a s' => P (EStateM.Result.ok a s'))) s → P x := by
+    intro hspec
+    simp only [wp, FailConds.false, FailConds.const, SVal.curry_cons, SVal.curry_nil] at hspec
+    split at hspec
+    case h_1 a s' heq => rw[← heq] at hspec; exact h ▸ hspec
+    case h_2 => contradiction
diff --git a/src/Std/Do/WP/IO.lean b/src/Std/Do/WP/IO.lean
new file mode 100644
index 0000000000..9507b70703
--- /dev/null
+++ b/src/Std/Do/WP/IO.lean
@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Init.System.IO
+import Std.Do.WP.Monad
+
+/-!
+# Barebones `WP` instance for `IO`
+
+This module defines a `WP` instance for `IO` without any synthetic model of the `IO.RealWorld` whatsoever.
+This is useful for reasoning about `IO` programs when the precise result of a side-effect is irrelevant;
+for example it can be used to reason about random number generation.
+It is however inadequate for reasoning about, e.g., `IO.Ref`s.
+-/
+
+namespace Std.Do.IO.Bare
+
+open Std.Do
+
+/--
+This is pretty much the instance for `EStateM` specialized to `σ = IO.RealWorld`.
+However, `IO.RealWorld` is ommitted in the `PredShape`.
+-/
+scoped instance instWP : WP (EIO ε) (.except ε .pure) where
+  wp x := -- Could define as PredTrans.mkExcept (PredTrans.modifyGetM (fun s => pure (EStateM.Result.toExceptState (x s))))
+    { apply := fun Q => match x () with
+        | .ok a _rw => Q.1 a
+        | .error e _rw => Q.2.1 e
+      conjunctive := by
+        intro _ _
+        apply SPred.bientails.of_eq
+        dsimp
+        cases (x ()) <;> rfl
+    }
+
+instance instLawfulMonad : LawfulMonad (EIO ε) := inferInstanceAs (LawfulMonad (EStateM ε IO.RealWorld))
+
+scoped instance instWPMonad : WPMonad (EIO ε) (.except ε .pure) where
+  wp_pure a := by simp only [wp, pure, EStateM.pure, PredTrans.pure]
+  wp_bind x f := by
+    ext Q : 2
+    simp only [wp, bind, EStateM.bind, PredTrans.bind]
+    cases (x ()) <;> rfl
diff --git a/src/Std/Do/WP/Monad.lean b/src/Std/Do/WP/Monad.lean
new file mode 100644
index 0000000000..e74670a6ed
--- /dev/null
+++ b/src/Std/Do/WP/Monad.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.WP.Basic
+
+/-!
+# Monad morphisms and weakest precondition interpretations
+
+A `WP m ps` is a `WPMonad m ps` if the interpretation `WP.wp` is also a monad morphism, that is,
+it preserves `pure` and `bind`.
+-/
+
+namespace Std.Do
+
+universe u
+variable {m : Type → Type u} {ps : PostShape}
+
+/--
+  A `WP` that is also a monad morphism, preserving `pure` and `bind`. (They all are.)
+-/
+class WPMonad (m : Type → Type u) (ps : outParam PostShape) [Monad m]
+  extends LawfulMonad m, WP m ps where
+  wp_pure : ∀ {α} (a : α), wp (pure a) = pure a
+  wp_bind : ∀ {α β} (x : m α) (f : α → m β), wp (do let a ← x; f a) = do let a ← wp x; wp (f a)
+
+theorem WPMonad.wp_map [Monad m] [WPMonad m ps] (f : α → β) (x : m α) :
+  wp (f <$> x) = f <$> wp x := by simp [← bind_pure_comp, wp_pure, wp_bind]
+
+theorem WPMonad.wp_seq [Monad m] [WPMonad m ps] (f : m (α → β)) (x : m α) :
+  wp (f <*> x) = wp f <*> wp x := by simp [← bind_map, wp_map, wp_bind]
+
+open WPMonad
+
+instance Id.instWPMonad : WPMonad Id .pure where
+  wp_pure a := by simp only [wp, PredTrans.pure, Pure.pure, Id.run]
+  wp_bind x f := by simp only [wp, PredTrans.pure, Bind.bind, Id.run, PredTrans.bind]
+
+instance StateT.instWPMonad [Monad m] [WPMonad m ps] : WPMonad (StateT σ m) (.arg σ ps) where
+  wp_pure a := by ext; simp only [wp, pure, StateT.pure, WPMonad.wp_pure, PredTrans.pure,
+    PredTrans.pushArg_apply]
+  wp_bind x f := by ext; simp only [wp, bind, StateT.bind, WPMonad.wp_bind, PredTrans.bind,
+    PredTrans.pushArg_apply]
+
+instance ReaderT.instWPMonad [Monad m] [WPMonad m ps] : WPMonad (ReaderT ρ m) (.arg ρ ps) where
+  wp_pure a := by ext; simp only [wp, pure, ReaderT.pure, WPMonad.wp_pure, PredTrans.pure,
+    PredTrans.pushArg_apply, PredTrans.map_apply]
+  wp_bind x f := by ext; simp only [wp, bind, ReaderT.bind, WPMonad.wp_bind, PredTrans.bind,
+    PredTrans.pushArg_apply, PredTrans.map_apply]
+
+instance ExceptT.instWPMonad [Monad m] [WPMonad m ps] : WPMonad (ExceptT ε m) (.except ε ps) where
+  wp_pure a := by ext; simp only [wp, pure, ExceptT.pure, ExceptT.mk, WPMonad.wp_pure,
+    PredTrans.pure, PredTrans.pushExcept_apply]
+  wp_bind x f := by
+    ext Q
+    simp only [wp, bind, ExceptT.bind, ExceptT.mk, WPMonad.wp_bind, PredTrans.bind,
+      ExceptT.bindCont, PredTrans.pushExcept_apply]
+    congr
+    ext b
+    cases b
+    case error a => simp [wp_pure]
+    case ok a => rfl
+
+instance EStateM.instWPMonad : WPMonad (EStateM ε σ) (.except ε (.arg σ .pure)) where
+  wp_pure a := by simp only [wp, pure, EStateM.pure, PredTrans.pure]
+  wp_bind x f := by
+    ext Q : 2
+    simp only [wp, bind, EStateM.bind, PredTrans.bind]
+    ext s : 1
+    cases (x s) <;> rfl
+
+instance Except.instWPMonad : WPMonad (Except ε) (.except ε .pure) where
+  wp_pure a := rfl
+  wp_bind x f := by cases x <;> rfl
+
+instance State.instWPMonad : WPMonad (StateM σ) (.arg σ .pure) :=
+  inferInstanceAs (WPMonad (StateT σ Id) (.arg σ .pure))
+instance Reader.instWPMonad : WPMonad (ReaderM ρ) (.arg ρ .pure) :=
+  inferInstanceAs (WPMonad (ReaderT ρ Id) (.arg ρ .pure))
diff --git a/src/Std/Do/WP/SimpLemmas.lean b/src/Std/Do/WP/SimpLemmas.lean
new file mode 100644
index 0000000000..346e31fb98
--- /dev/null
+++ b/src/Std/Do/WP/SimpLemmas.lean
@@ -0,0 +1,374 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.WP.Basic
+import Std.Do.WP.Monad
+
+/-!
+# Simp lemmas for working with weakest preconditions
+
+Many weakest preconditions are so simple that we can compute them directly or
+express them in terms of "simpler" weakest preconditions.
+This module provides simp lemmas targeting expressions of the form `wp⟦x⟧ Q`
+and rewrites them to expressions of simpler weakest preconditions.
+-/
+
+namespace Std.Do.WP
+
+open WPMonad
+
+universe u
+variable {m : Type → Type u} {ps : PostShape}
+
+/-! ## `WP` -/
+
+@[simp]
+theorem ReaderT_run [WP m ps] (x : ReaderT ρ m α) :
+  wp⟦x.run r⟧ Q = wp⟦x⟧ (fun a _ => Q.1 a, Q.2) r := rfl
+
+@[simp]
+theorem StateT_run [WP m ps] (x : StateT σ m α) :
+  wp⟦x.run s⟧ Q = wp⟦x⟧ (fun a s => Q.1 (a, s), Q.2) s := rfl
+
+@[simp]
+theorem ExceptT_run [WP m ps] (x : ExceptT ε m α) :
+    wp⟦x.run⟧ Q = wp⟦x⟧ (fun a => Q.1 (.ok a), fun e => Q.1 (.error e), Q.2) := by
+  simp [wp, ExceptT.run]
+  congr
+  (ext x; cases x) <;> rfl
+
+/-! ## `WPMonad` -/
+
+@[simp]
+theorem pure [Monad m] [WPMonad m ps] (a : α) (Q : PostCond α ps) :
+  wp⟦pure (f:=m) a⟧ Q = Q.1 a := by simp [WPMonad.wp_pure]
+
+@[simp]
+theorem bind [Monad m] [WPMonad m ps] (x : m α) (f : α → m β) (Q : PostCond β ps) :
+  wp⟦x >>= f⟧ Q = wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2) := by simp [WPMonad.wp_bind]
+
+@[simp]
+theorem map [Monad m] [WPMonad m ps] (f : α → β) (x : m α) (Q : PostCond β ps) :
+  wp⟦f <$> x⟧ Q = wp⟦x⟧ (fun a => Q.1 (f a), Q.2) := by simp [WPMonad.wp_map]
+
+@[simp]
+theorem seq [Monad m] [WPMonad m ps] (f : m (α → β)) (x : m α) (Q : PostCond β ps) :
+  wp⟦f <*> x⟧ Q = wp⟦f⟧ (fun f => wp⟦x⟧ (fun a => Q.1 (f a), Q.2), Q.2) := by simp [WPMonad.wp_seq]
+
+/-! ## `MonadLift`
+
+The definitions that follow interpret `liftM` and thus instances of, e.g., `MonadStateOf`.
+
+-/
+
+section MonadLift
+
+@[simp]
+theorem monadLift_StateT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.arg σ ps)) :
+  wp⟦MonadLift.monadLift x : StateT σ m α⟧ Q = fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2) := by simp [wp, MonadLift.monadLift, StateT.lift]
+
+@[simp]
+theorem monadLift_ReaderT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.arg ρ ps)) :
+  wp⟦MonadLift.monadLift x : ReaderT ρ m α⟧ Q = fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2) := rfl
+
+@[simp]
+theorem monadLift_ExceptT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.except ε ps)) :
+  wp⟦MonadLift.monadLift x : ExceptT ε m α⟧ Q = wp⟦x⟧ (fun a => Q.1 a, Q.2.2) := by
+    simp [wp, MonadLift.monadLift, ExceptT.lift, ExceptT.mk]
+
+@[simp]
+theorem monadLift_trans [WP o ps] [MonadLift n o] [MonadLiftT m n] :
+  wp⟦MonadLiftT.monadLift x : o α⟧ Q = wp⟦MonadLift.monadLift (m:=n) (MonadLiftT.monadLift (m:=m) x) : o α⟧ Q := rfl
+
+@[simp]
+theorem monadLift_refl [WP m ps] :
+  wp⟦MonadLiftT.monadLift x : m α⟧ Q = wp⟦x : m α⟧ Q := rfl
+
+-- instances
+
+@[simp]
+theorem lift_StateT [WP m ps] [Monad m] (x : m α) :
+  wp⟦StateT.lift x : StateT σ m α⟧ Q = wp⟦MonadLift.monadLift x : StateT σ m α⟧ Q := rfl
+
+@[simp]
+theorem lift_ExceptT [WP m ps] [Monad m] (x : m α) :
+  wp⟦ExceptT.lift x : ExceptT ε m α⟧ Q = wp⟦MonadLift.monadLift x : ExceptT ε m α⟧ Q := rfl
+
+
+-- MonadReader
+
+@[simp]
+theorem read_MonadReaderOf [MonadReaderOf ρ m] [MonadLift m n] [WP n _] :
+  wp⟦MonadReaderOf.read : n ρ⟧ Q = wp⟦MonadLift.monadLift (MonadReader.read : m ρ) : n ρ⟧ Q := rfl
+
+@[simp]
+theorem readThe [MonadReaderOf ρ m] [WP m ps] :
+  wp⟦readThe ρ : m ρ⟧ Q = wp⟦MonadReaderOf.read : m ρ⟧ Q := rfl
+
+@[simp]
+theorem read_MonadReader [MonadReaderOf ρ m] [WP m ps] :
+  wp⟦MonadReader.read : m ρ⟧ Q = wp⟦MonadReaderOf.read : m ρ⟧ Q := rfl
+
+-- MonadState
+
+@[simp]
+theorem get_MonadStateOf [MonadStateOf σ m] [MonadLift m n] [WP n _] :
+  wp⟦MonadStateOf.get : n σ⟧ Q = wp⟦MonadLift.monadLift (MonadStateOf.get : m σ) : n σ⟧ Q := rfl
+
+@[simp]
+theorem get_MonadState [WP m ps] [MonadStateOf σ m] :
+  wp⟦MonadState.get : m σ⟧ Q = wp⟦MonadStateOf.get : m σ⟧ Q := rfl
+
+@[simp]
+theorem getThe_MonadStateOf [WP m ps] [MonadStateOf σ m] :
+  wp⟦getThe σ : m σ⟧ Q = wp⟦MonadStateOf.get : m σ⟧ Q := rfl
+
+@[simp]
+theorem set_MonadStateOf [MonadStateOf σ m] [MonadLift m n] [WP n _] :
+  wp⟦MonadStateOf.set x : n PUnit⟧ Q = wp⟦MonadLift.monadLift (MonadStateOf.set (σ:=σ) x : m PUnit) : n PUnit⟧ Q := rfl
+
+@[simp]
+theorem set_MonadState [WP m ps] [MonadStateOf σ m] :
+  wp⟦MonadState.set x : m PUnit⟧ Q = wp⟦MonadStateOf.set x : m PUnit⟧ Q := rfl
+
+@[simp]
+theorem modifyGet_MonadStateOf [MonadStateOf σ m] [MonadLift m n] [WP n _]
+  (f : σ → α × σ) :
+  wp⟦MonadStateOf.modifyGet f : n α⟧ Q = wp⟦MonadLift.monadLift (MonadState.modifyGet f : m α) : n α⟧ Q := rfl
+
+@[simp]
+theorem modifyGet_MonadState [WP m ps] [MonadStateOf σ m] (f : σ → α × σ) :
+  wp⟦MonadState.modifyGet f : m α⟧ Q = wp⟦MonadStateOf.modifyGet f : m α⟧ Q := rfl
+
+@[simp]
+theorem modifyGetThe_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → α × σ) :
+  wp⟦modifyGetThe σ f : m α⟧ Q = wp⟦MonadStateOf.modifyGet f : m α⟧ Q := rfl
+
+@[simp]
+theorem modify_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → σ) :
+  wp⟦modify f : m PUnit⟧ Q = wp⟦MonadStateOf.modifyGet fun s => ((), f s) : m PUnit⟧ Q := rfl
+
+@[simp]
+theorem modifyThe_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → σ) :
+  wp⟦modifyThe σ f : m PUnit⟧ Q = wp⟦MonadStateOf.modifyGet fun s => ((), f s) : m PUnit⟧ Q := rfl
+
+-- instances
+
+@[simp]
+theorem read_ReaderT [Monad m] [WPMonad m ps] :
+    wp⟦MonadReaderOf.read : ReaderT ρ m ρ⟧ Q = fun r => Q.1 r r := by
+  simp [wp, MonadReaderOf.read, ReaderT.read]
+
+@[simp]
+theorem get_StateT [Monad m] [WPMonad m ps] :
+    wp⟦MonadStateOf.get : StateT σ m σ⟧ Q = fun s => Q.1 s s := by
+  simp [wp, MonadStateOf.get, StateT.get]
+
+@[simp]
+theorem set_StateT [Monad m] [WPMonad m ps] (x : σ) :
+    wp⟦MonadStateOf.set x : StateT σ m PUnit⟧ Q = fun _ => Q.1 ⟨⟩ x := by
+  simp [wp, set, StateT.set]
+
+@[simp]
+theorem modifyGet_StateT [Monad m] [WPMonad m ps] (f : σ → α × σ) :
+    wp⟦MonadStateOf.modifyGet f : StateT σ m α⟧ Q = fun s => Q.1 (f s).1 (f s).2 := by
+  simp [wp, MonadStateOf.modifyGet, StateT.modifyGet]
+
+@[simp]
+theorem get_EStateM :
+    wp⟦MonadStateOf.get : EStateM ε σ σ⟧ Q = fun s => Q.1 s s := by
+  simp [wp, MonadStateOf.get, EStateM.get]
+
+@[simp]
+theorem set_EStateM (x : σ) :
+    wp⟦MonadStateOf.set x : EStateM ε σ PUnit⟧ Q = fun _ => Q.1 ⟨⟩ x := by
+  simp [wp, set, EStateM.set]
+
+@[simp]
+theorem modifyGet_EStateM (f : σ → α × σ) :
+    wp⟦MonadStateOf.modifyGet f : EStateM ε σ α⟧ Q = fun s => Q.1 (f s).1 (f s).2 := by
+  simp [wp, MonadStateOf.modifyGet, EStateM.modifyGet]
+
+end MonadLift
+
+/-! ## `MonadFunctor`
+
+The definitions that follow interpret `monadMap` and thus instances of, e.g., `MonadReaderWithOf`.
+
+-/
+
+section MonadFunctor
+
+open MonadFunctor renaming monadMap → mmap
+
+-- The following 3 theorems are analogous to *.monadLift_apply.
+-- In the past, we experimented with a more tricky definition by rewriting to special monadMap defns on PredTrans, involving
+--   wp1 : (∀ {α}, m α → m α) → PredTrans ps α → PredTrans ps α
+-- that enjoys quite a tricky definition.
+-- However, we found that relying on specialised lemmas is both much simpler and more reliable.
+@[simp]
+theorem monadMap_StateT (m : Type → Type u) [Monad m] [WP m ps]
+  (f : ∀{β}, m β → m β) {α} (x : StateT σ m α) (Q : PostCond α (.arg σ ps)) :
+    wp⟦mmap (m:=m) f x⟧ Q = fun s => wp⟦f (x.run s)⟧ (fun (a, s) => Q.1 a s, Q.2) := by
+  simp [wp, MonadFunctor.monadMap, StateT.run]
+
+@[simp]
+theorem monadMap_ReaderT (m : Type → Type u) [Monad m] [WP m ps]
+  (f : ∀{β}, m β → m β) {α} (x : ReaderT ρ m α) (Q : PostCond α (.arg ρ ps)) :
+    wp⟦mmap (m:=m) f x⟧ Q = fun s => wp⟦f (x.run s)⟧ (fun a => Q.1 a s, Q.2) := by
+  simp [wp, MonadFunctor.monadMap, ReaderT.run]
+
+@[simp]
+theorem monadMap_ExceptT (m : Type → Type u) [Monad m] [WP m ps]
+  (f : ∀{β}, m β → m β) {α} (x : ExceptT ε m α) (Q : PostCond α (.except ε ps)) :
+    wp⟦mmap (m:=m) f x⟧ Q = wp⟦f x.run⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by
+  simp [wp, MonadFunctor.monadMap, ExceptT.run]
+  congr; ext; split <;> rfl
+
+@[simp]
+theorem monadMap_trans [WP o ps] [MonadFunctor n o] [MonadFunctorT m n] :
+  wp⟦MonadFunctorT.monadMap f x : o α⟧ Q = wp⟦MonadFunctor.monadMap (m:=n) (MonadFunctorT.monadMap (m:=m) f) x : o α⟧ Q := rfl
+
+@[simp]
+theorem monadMap_refl [WP m ps] :
+  wp⟦MonadFunctorT.monadMap f x : m α⟧ Q = wp⟦f x : m α⟧ Q := rfl
+
+@[simp]
+theorem withReader_ReaderT [WP m ps] :
+  wp⟦MonadWithReaderOf.withReader f x : ReaderT ρ m α⟧ Q = fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r) := rfl
+
+@[simp]
+theorem withReader_MonadWithReaderOf [MonadWithReaderOf ρ m] [WP n nsh] [MonadFunctor m n] (f : ρ → ρ) (x : n α) :
+  wp⟦MonadWithReaderOf.withReader f x⟧ Q = wp⟦mmap (m:=m) (MonadWithReaderOf.withReader f) x⟧ Q := rfl
+
+@[simp]
+theorem withReader_MonadWithReader [MonadWithReaderOf ρ m] [WP m ps] (f : ρ → ρ) (x : m α) :
+  wp⟦MonadWithReader.withReader f x⟧ Q = wp⟦MonadWithReaderOf.withReader f x⟧ Q := rfl
+
+@[simp]
+theorem withTheReader [MonadWithReaderOf ρ m] [WP m ps] (f : ρ → ρ) (x : m α) :
+  wp⟦withTheReader ρ f x⟧ Q = wp⟦MonadWithReaderOf.withReader f x⟧ Q := rfl
+
+end MonadFunctor
+
+/-! ## `MonadExceptOf`
+
+The definitions that follow interpret `throw`, `throwThe`, `tryCatch`, etc.
+
+Since `MonadExceptOf` cannot be lifted through `MonadLift` or `MonadFunctor`, there is one lemma per
+`MonadExceptOf` operation and instance to lift through; the classic m*n instances problem.
+
+-/
+
+section MonadExceptOf
+
+@[simp]
+theorem throw_MonadExcept [MonadExceptOf ε m] [WP m ps] :
+  wp⟦throw e : m α⟧ Q = wp⟦MonadExceptOf.throw e : m α⟧ Q := rfl
+
+@[simp]
+theorem throwThe [MonadExceptOf ε m] [WP m ps] :
+  wp⟦throwThe ε e : m α⟧ Q = wp⟦MonadExceptOf.throw e : m α⟧ Q := rfl
+
+@[simp]
+theorem throw_Except :
+    wp⟦MonadExceptOf.throw e : Except ε α⟧ Q = Q.2.1 e := by
+  simp [wp, MonadExceptOf.throw, Id.run]
+
+@[simp]
+theorem throw_ExceptT [Monad m] [WPMonad m ps] :
+    wp⟦MonadExceptOf.throw e : ExceptT ε m α⟧ Q = Q.2.1 e := by
+  simp [wp, MonadExceptOf.throw, ExceptT.mk]
+
+@[simp]
+theorem throw_EStateM :
+    wp⟦MonadExceptOf.throw e : EStateM ε σ α⟧ Q = Q.2.1 e := by
+  simp [wp, MonadExceptOf.throw, EStateM.throw]
+
+@[simp]
+theorem throw_ReaderT [WP m sh] [Monad m] [MonadExceptOf ε m] :
+  wp⟦MonadExceptOf.throw (ε:=ε) e : ReaderT ρ m α⟧ Q = wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : ReaderT ρ m α⟧ Q := rfl
+
+@[simp]
+theorem throw_StateT [WP m sh] [Monad m] [MonadExceptOf ε m] :
+  wp⟦MonadExceptOf.throw (ε:=ε) e : StateT ρ m α⟧ Q = wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : StateT ρ m α⟧ Q := rfl
+
+-- The following lemma is structurally different to StateT and others because of weird definitions
+-- for lifting throw
+@[simp]
+theorem throw_lift_ExceptT [WP m sh] [Monad m] [MonadExceptOf ε m] :
+    wp⟦MonadExceptOf.throw (ε:=ε) e : ExceptT ε' m α⟧ Q = wp⟦MonadExceptOf.throw (ε:=ε) e : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by
+  simp only [wp, MonadExceptOf.throw, PredTrans.pushExcept_apply]
+  congr
+  ext x
+  split <;> rfl
+
+@[simp]
+theorem tryCatch_MonadExcept [MonadExceptOf ε m] [WP m ps] :
+  wp⟦tryCatch x h : m α⟧ Q = wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q := rfl
+
+@[simp]
+theorem tryCatchThe [MonadExceptOf ε m] [WP m ps] :
+  wp⟦tryCatchThe ε x h : m α⟧ Q = wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q := rfl
+
+@[simp]
+theorem tryCatch_Except :
+    wp⟦MonadExceptOf.tryCatch x h : Except ε α⟧ Q = wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2) := by
+  simp only [wp, PredTrans.pure, Id.run, MonadExceptOf.tryCatch, Except.tryCatch,
+    PredTrans.pushExcept_apply]
+  cases x <;> simp
+
+@[simp]
+theorem tryCatch_ExceptT [Monad m] [WPMonad m ps] :
+    wp⟦MonadExceptOf.tryCatch x h : ExceptT ε m α⟧ Q = wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2) := by
+  simp only [wp, MonadExceptOf.tryCatch, ExceptT.tryCatch, ExceptT.mk, bind, PredTrans.pushExcept_apply]
+  congr
+  ext x
+  split <;> simp
+
+open EStateM.Backtrackable in
+@[simp]
+theorem tryCatch_EStateM {ε σ δ α x h Q} [EStateM.Backtrackable δ σ]:
+    wp⟦MonadExceptOf.tryCatch x h : EStateM ε σ α⟧ Q = fun s => wp⟦x⟧ (Q.1, fun e s' => wp⟦h e⟧ Q (restore s' (save s)), Q.2.2) s := by
+  ext s
+  simp only [wp, MonadExceptOf.tryCatch, EStateM.tryCatch]
+  cases x s <;> simp
+
+@[simp]
+theorem tryCatch_ReaderT [WP m sh] [Monad m] [MonadExceptOf ε m] :
+    wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : ReaderT ρ m α⟧ Q = fun r => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run r) (fun e => (h e).run r) : m α⟧ (fun a => Q.1 a r, Q.2) := by
+  simp [wp, MonadExceptOf.tryCatch, tryCatchThe, ReaderT.run]
+
+@[simp]
+theorem tryCatch_StateT [WP m sh] [Monad m] [MonadExceptOf ε m] :
+    wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : StateT σ m α⟧ Q = fun s => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run s) (fun e => (h e).run s) : m (α × σ)⟧ (fun xs => Q.1 xs.1 xs.2, Q.2) := by
+  simp [wp, MonadExceptOf.tryCatch, tryCatchThe, StateT.run]
+
+@[simp]
+theorem tryCatch_lift_ExceptT [WP m sh] [Monad m] [MonadExceptOf ε m] :
+    wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : ExceptT ε' m α⟧ Q = wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by
+  simp only [wp, MonadExceptOf.tryCatch, tryCatchThe, PredTrans.pushExcept_apply, ExceptT.mk]
+  congr
+  ext x
+  split <;> rfl
+
+/-
+example :
+  wp (m:= ReaderT Char (StateT Bool (ExceptT Nat Id))) (do set true; throw 42; set false; get) =
+  wp (m:= ReaderT Char (StateT Bool (ExceptT Nat Id))) (do set true; throw 42; get) := by
+    ext Q : 4
+    simp
+
+example :
+  wp (m:= ReaderT Char (StateT Bool (ExceptT Nat Id))) (do try { set true; throw 42 } catch _ => set false; get) =
+  wp (m:= ReaderT Char (StateT Bool (ExceptT Nat Id))) (do set false; get) := by
+    ext Q : 4
+    simp
+    -- This gets stuck because ExceptT.instMonad is not defeq to Except.instMonad and thus the `bind` rewrite does not apply.
+    admit
+-/
+
+end MonadExceptOf
diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean
index 500176a88b..0b6a8ab929 100644
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@@ -6,7 +6,25 @@ Authors: Sebastian Graf
 prelude
 import Init.NotationExtra
 
-namespace Lean.Parser.Tactic
+
+namespace Lean.Parser
+
+namespace Attr
+
+/--
+Theorems tagged with the `spec` attribute are used by the `mspec` and `mvcgen` tactics.
+
+* When used on a theorem `foo_spec : Triple (foo a b c) P Q`, then `mspec` and `mvcgen` will use
+  `foo_spec` as a specification for calls to `foo`.
+* Otherwise, when used on a definition that `@[simp]` would work on, it is added to the internal
+  simp set of `mvcgen` that is used within `wp⟦·⟧` contexts to simplify match discriminants and
+  applications of constants.
+-/
+syntax (name := specAttr) "spec" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+
+end Attr
+
+namespace Tactic
 
 @[inherit_doc Lean.Parser.Tactic.massumptionMacro]
 syntax (name := massumption) "massumption" : tactic
@@ -152,3 +170,46 @@ syntax "∀" binderIdent : mintroPat
 
 @[inherit_doc Lean.Parser.Tactic.mintroMacro]
 syntax (name := mintro) "mintro" (ppSpace colGt mintroPat)+ : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mspecMacro]
+syntax (name := mspec) "mspec" (ppSpace colGt term)? : tactic
+
+/--
+Like `mspec`, but does not attempt slight simplification and closing of trivial sub-goals.
+`mspec $spec` is roughly (the set of simp lemmas below might not be up to date)
+```
+mspec_no_simp $spec
+all_goals
+  ((try simp only [SPred.true_intro_simp, SPred.true_intro_simp_nil, SVal.curry_cons,
+                   SVal.uncurry_cons, SVal.getThe_here, SVal.getThe_there]);
+   (try mpure_intro; trivial))
+```
+-/
+syntax (name := mspecNoSimp) "mspec_no_simp" (ppSpace colGt term)? : tactic
+
+/--
+`mspec_no_simp $spec` first tries to decompose `Bind.bind`s before applying `$spec`.
+This variant of `mspec_no_simp` does not; `mspec_no_bind $spec` is defined as
+```
+try with_reducible mspec_no_bind Std.Do.Spec.bind
+mspec_no_bind $spec
+```
+-/
+syntax (name := mspecNoBind) "mspec_no_bind" (ppSpace colGt term)? : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mvcgenMacro]
+syntax (name := mvcgen) "mvcgen" optConfig
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
+
+/--
+Like `mvcgen`, but does not attempt to prove trivial VCs via `mpure_intro; trivial`.
+-/
+syntax (name := mvcgenNoTrivial) "mvcgen_no_trivial" optConfig
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
+
+/--
+Like `mvcgen_no_trivial`, but `mvcgen_step 42` will only do 42 steps of the VC generation procedure.
+This is helpful for bisecting bugs in `mvcgen` and tracing its execution.
+-/
+syntax (name := mvcgenStep) "mvcgen_step" optConfig
+ (num)? (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic