diff --git a/backends/lean/Aeneas/Data/Array.lean b/backends/lean/Aeneas/Data/Array.lean
index 0930b95b8..356c45bf1 100644
--- a/backends/lean/Aeneas/Data/Array.lean
+++ b/backends/lean/Aeneas/Data/Array.lean
@@ -108,13 +108,9 @@ theorem getElem_set! {α : Type u}
   simp only [set!_eq_setIfInBounds, ← getElem_toList, toList_setIfInBounds]
   simp_lists
 
-@[simp, simp_lists_safe]
-theorem getElem!_set!_ne {α : Type u}
-  [Inhabited α] {i j : ℕ} {x : α} {xs : Array α}
-  (h : i ≠ j) :
-  (xs.set! i x)[j]! = xs[j]! := by
-  simp only [set!_eq_setIfInBounds, ← getElem!_toList, toList_setIfInBounds]
-  simp_lists
+-- `Array.getElem!_set!_ne` is now provided by the core library; just register the
+-- Aeneas simp attributes on it.
+attribute [simp, simp_lists_safe] _root_.Array.getElem!_set!_ne
 
 @[simp, simp_lists_safe]
 theorem getElem_set!_ne {α : Type u}
diff --git a/backends/lean/Aeneas/Data/Vector.lean b/backends/lean/Aeneas/Data/Vector.lean
index 42118e3bb..b62c10e2d 100644
--- a/backends/lean/Aeneas/Data/Vector.lean
+++ b/backends/lean/Aeneas/Data/Vector.lean
@@ -108,16 +108,9 @@ theorem getElem!_set! {α : Type u}
     ← Array.getElem!_toList, Array.toList_setIfInBounds]
   simp_lists
 
-@[simp, simp_lists_safe]
-theorem getElem_set! {α : Type u}
-  [Inhabited α] {n i j : ℕ} {x : α} {xs : Vector α n}
-  (hi : i < n ∧ j = i) :
-  (xs.set! i x)[j] = x := by
-  have : i < xs.toArray.size := by scalar_tac
-  simp only [getElem_eq_toArray_getElem, toArray_set!, Array.set!_eq_setIfInBounds,
-    Array.size_setIfInBounds, size_toArray, Array.Inhabited_getElem_eq_getElem!,
-    ← Array.getElem!_toList, Array.toList_setIfInBounds, hi]
-  grind
+-- `Vector.getElem_set!_self` is now provided by the core library; register the
+-- Aeneas simp attribute on it.
+attribute [simp_lists_safe] getElem_set!_self
 
 @[simp, simp_lists_safe]
 theorem getElem!_set!_ne {α : Type u}
@@ -127,13 +120,9 @@ theorem getElem!_set!_ne {α : Type u}
   simp only [getElem!_eq_toArray_getElem!, toArray_set!]
   simp_lists
 
-@[simp, simp_lists_safe]
-theorem getElem_set!_ne {α : Type u}
-  [Inhabited α] {n i j : ℕ} {x : α} {xs : Vector α n}
-  (h : i ≠ j ∧ j < n) :
-  (xs.set! i x)[j] = xs[j] := by
-  simp only [getElem_eq_toArray_getElem, toArray_set!]
-  simp_lists
+-- `Vector.getElem_set!_ne` is now provided by the core library; register the
+-- Aeneas simp attribute on it.
+attribute [simp_lists_safe] getElem_set!_ne
 
 @[simp, simp_lists_safe]
 theorem getElem!_replicate {α : Type u} [Inhabited α] {i n : ℕ} {a : α} (h : i < n) :
diff --git a/backends/lean/Aeneas/Do/Tests.lean b/backends/lean/Aeneas/Do/Tests.lean
index f34c136e8..b8c56e16f 100644
--- a/backends/lean/Aeneas/Do/Tests.lean
+++ b/backends/lean/Aeneas/Do/Tests.lean
@@ -625,13 +625,15 @@ def do_match_cross_arm_used (t : Two) : Result Nat := do
 
 /-- warning: Variable name `n` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _n
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `n` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _n
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false` -/
 #guard_msgs in
@@ -647,7 +649,8 @@ def do_let_arrow_id_used : Result Nat := do
 
 /-- warning: Variable name `x` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _x
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false` -/
 #guard_msgs in
@@ -668,25 +671,29 @@ def do_let_arrow_pat_used : Result Nat := do
 /--
 warning: Variable name `a` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _a
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `b` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _b
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `c` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _c
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `d` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _d
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 -/
@@ -699,25 +706,29 @@ def do_let_arrow_pat_unused : Result Nat := do
 /--
 warning: Variable name `a` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _a
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `b` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _b
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `c` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _c
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `d` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _d
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 -/
diff --git a/backends/lean/Aeneas/Std/Array/Array.lean b/backends/lean/Aeneas/Std/Array/Array.lean
index 7571a44c5..8983fcac6 100644
--- a/backends/lean/Aeneas/Std/Array/Array.lean
+++ b/backends/lean/Aeneas/Std/Array/Array.lean
@@ -225,6 +225,7 @@ theorem Array.update_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (
   := by
   simp only [partialSpec, update, set]
   cases hopt : v[i]? <;> simp_all
+  rfl
 
 def Array.index_mut_usize {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
   Result (α × (α -> Array α n)) := do
@@ -244,8 +245,8 @@ theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i:
 @[simp]
 theorem Array.set_getElem!_eq {α} {n : Usize} [Inhabited α] (x : Array α n) (i : Usize) :
   x.set i (x.val[i.val]!) = x := by
-  have := @List.set_getElem_self _ x.val i.val
-  simp only [Array, Subtype.ext_iff, set_val_eq, List.set_getElem!]
+  apply Subtype.ext
+  simp only [set_val_eq, List.set_getElem!]
 
 @[simp]
 theorem Array.set_getElem_eq {α} {n : Usize} (x : Array α n) (i : Usize) (h : i.val < x.length) :
@@ -254,15 +255,14 @@ theorem Array.set_getElem_eq {α} {n : Usize} (x : Array α n) (i : Usize) (h :
     simpa using h
   have hself : x.val.set i.val x.val[i.val] = x.val :=
     List.set_getElem_self (as := x.val) (i := i.val) (h := h')
-  simp only [Array, Subtype.ext_iff, set_val_eq] at hself ⊢
+  apply Subtype.ext
+  simp only [set_val_eq]
   exact hself
 
 @[simp↓, simp_lists_safe↓]
 theorem Array.getElem_set_eq {α} {n : Usize} (v : Array α n) (i : Usize) (x : α) (h : i.val < (v.set i x).length) :
   (v.set i x)[i]'h = x := by
-  cases v
-  unfold set getElem instGetElemArrayUsizeLtNatValLengthValListEq
-  simp only [List.getElem_set_self]
+  simp only [Array.getElem_Usize_eq, Array.set_val_eq, List.getElem_set_self]
 
 @[simp↓, simp_lists_safe↓]
 theorem Array.getElem_set_eq' {α} {n : Usize} (v : Array α n) (i j : Usize) (x : α) (h : j.val < (v.set i x).length)
@@ -274,9 +274,8 @@ theorem Array.getElem_set_eq' {α} {n : Usize} (v : Array α n) (i j : Usize) (x
 theorem Array.getElem_set_neq {α} {n : Usize} (v : Array α n) (i j : Usize) (x : α)
   (h : j.val < (v.set i x).length) (h' : i ≠ j) :
   (v.set i x)[j]'h = v[j] := by
-  cases v
-  unfold set getElem instGetElemArrayUsizeLtNatValLengthValListEq
-  simp only [ne_eq, UScalar.neq_to_neq_val] at *
+  simp only [ne_eq, UScalar.neq_to_neq_val] at h'
+  simp only [Array.getElem_Usize_eq, Array.set_val_eq]
   simp_lists [List.getElem_set_ne]
 
 /-- Small helper (this function doesn't model a specific Rust function) -/
@@ -289,13 +288,19 @@ theorem Array.clone_length {α : Type u} {n : Usize} (clone : α → Result α)
   simp [Array.clone] at h
   simp [List.clone] at h
   split at h <;> simp_all
+  rename_i heq
+  have := List.mapM_Result_length heq
+  cases s'; simp_all
+  cases h; simp_all
 
 @[step]
 theorem Array.clone_spec {α : Type u} {n : Usize} {clone : α → Result α} {s : Array α n} (h : ∀ x ∈ s.val, clone x = ok x) :
   Array.clone clone s ⦃ s' => s' = s ⦄ := by
   simp only [Array.clone]
   have ⟨ l', h ⟩ := spec_imp_exists (List.clone_spec h)
-  simp [h]
+  simp only [h.1, bind_tc_ok]
+  apply (spec_ok _).mpr
+  exact Subtype.ext h.2.1
 
 @[rust_fun "core::array::{core::clone::Clone<[@T; @N]>}::clone"]
 def core.array.CloneArray.clone
@@ -307,8 +312,9 @@ theorem core.array.CloneArray.clone_spec {T : Type} {N : Usize} (cloneInst : cor
   (h : ∀ x ∈ a.val, cloneInst.clone x = ok x) :
   core.array.CloneArray.clone cloneInst a ⦃ a' => a = a' ⦄:= by
   unfold clone
-  have := spec_imp_exists (Array.clone_spec h)
-  grind
+  have ⟨a', h'⟩ := spec_imp_exists (Array.clone_spec h)
+  rw [h'.1]
+  exact (spec_ok _).mpr h'.2.symm
 
 @[rust_fun "core::array::{core::clone::Clone<[@T; @N]>}::clone_from"]
 def core.array.CloneArray.clone_from {T : Type} {N : Usize} (cloneInst : core.clone.Clone T)
@@ -320,8 +326,9 @@ theorem core.array.CloneArray.clone_from_spec {T : Type} {N : Usize} (cloneInst
   (self source : Array T N) (h : ∀ x ∈ source.val, cloneInst.clone x = ok x) :
   core.array.CloneArray.clone_from cloneInst self source ⦃ source' => source = source' ⦄ := by
   unfold clone_from
-  have := spec_imp_exists (Array.clone_spec h)
-  grind
+  have ⟨source', h'⟩ := spec_imp_exists (Array.clone_spec h)
+  rw [h'.1]
+  exact (spec_ok _).mpr h'.2.symm
 
 @[reducible, rust_trait_impl "core::clone::Clone<[@T; @N]>"]
 def core.clone.CloneArray {T : Type} (N : Usize)
@@ -337,7 +344,8 @@ def Array.setSlice! {α : Type u} {n} (s : Array α n) (i : ℕ) (s' : List α)
 theorem Array.setSlice!_getElem!_prefix {α} {n} [Inhabited α]
   (s : Array α n) (s' : List α) (i j : ℕ) (h : j < i) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Array.setSlice!, Array.getElem!_Nat_eq]
+  simp only [Array.getElem!_Nat_eq]
+  simp only [Array.setSlice!]
   simp_lists
 
 @[simp_lists_safe]
@@ -346,7 +354,8 @@ theorem Array.setSlice!_getElem_prefix {α} {n}
   (s.setSlice! i s')[j] = s[j] := by
   have hj' : j < (s.setSlice! i s').length := by scalar_tac
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Array.getElem?_Nat_eq, Array.setSlice!]
+    simp only [Array.getElem?_Nat_eq]
+    simp only [Array.setSlice!]
     simp_lists [List.setSlice!_getElem?_prefix]
   simp only [Array.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2,
     Option.some.injEq] at h1
@@ -356,7 +365,8 @@ theorem Array.setSlice!_getElem_prefix {α} {n}
 theorem Array.setSlice!_getElem!_middle {α} {n} [Inhabited α]
   (s : Array α n) (s' : List α) (i j : ℕ) (h : i ≤ j ∧ j - i < s'.length ∧ j < s.length) :
   (s.setSlice! i s')[j]! = s'[j - i]! := by
-  simp only [Array.setSlice!, Array.getElem!_Nat_eq]
+  simp only [Array.getElem!_Nat_eq]
+  simp only [Array.setSlice!]
   simp_lists
 
 @[simp_lists_safe]
@@ -367,7 +377,8 @@ theorem Array.setSlice!_getElem_middle {α} {n}
     scalar_tac
   have hji : j - i < s'.length := h.2.1
   have h1 : (s.setSlice! i s')[j]? = s'[j - i]? := by
-    simp only [Array.getElem?_Nat_eq, Array.setSlice!]
+    simp only [Array.getElem?_Nat_eq]
+    simp only [Array.setSlice!]
     simp_lists [List.setSlice!_getElem?_middle]
   simp only [Array.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem hji,
     Option.some.injEq] at h1
@@ -376,7 +387,8 @@ theorem Array.setSlice!_getElem_middle {α} {n}
 theorem Array.setSlice!_getElem!_suffix {α} {n} [Inhabited α]
   (s : Array α n) (s' : List α) (i j : ℕ) (h : i + s'.length ≤ j) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Array.setSlice!, Array.getElem!_Nat_eq]
+  simp only [Array.getElem!_Nat_eq]
+  simp only [Array.setSlice!]
   simp_lists
 
 theorem Array.setSlice!_getElem_suffix {α} {n}
@@ -384,7 +396,8 @@ theorem Array.setSlice!_getElem_suffix {α} {n}
   (s.setSlice! i s')[j] = s[j] := by
   have hj' : j < (s.setSlice! i s').length := by scalar_tac
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Array.getElem?_Nat_eq, Array.setSlice!]
+    simp only [Array.getElem?_Nat_eq]
+    simp only [Array.setSlice!]
     simp_lists [List.setSlice!_getElem?_suffix]
   simp only [Array.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2,
     Option.some.injEq] at h1
diff --git a/backends/lean/Aeneas/Std/Array/ArraySlice.lean b/backends/lean/Aeneas/Std/Array/ArraySlice.lean
index 3e190fdbb..d5d709259 100644
--- a/backends/lean/Aeneas/Std/Array/ArraySlice.lean
+++ b/backends/lean/Aeneas/Std/Array/ArraySlice.lean
@@ -41,7 +41,9 @@ theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (a : Array α n) :
   (lift (Array.to_slice_mut a))
   ⦃ (s : Slice α) (back : Slice α → Array α n) =>
     s.val = a.val ∧ back = Array.from_slice a ⦄ := by
-  simp [lift, to_slice_mut, to_slice, WP.spec_ok]
+  simp only [lift, to_slice_mut, to_slice]
+  apply (spec_ok _).mpr
+  simp [Std.WP.uncurry']
 
 def Array.subslice {α : Type u} {n : Usize} (a : Array α n) (r : Range Usize) : Result (Slice α) :=
   if r.start.val ≤ r.end.val ∧ r.end.val ≤ a.val.length then
@@ -92,9 +94,14 @@ theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a :
            | _ => False)
       False := by
   unfold update_subslice
-  split <;> rename_i h <;> simp [partialSpec]
-  · simp_lists
-  · scalar_tac
+  split
+  · rename_i h
+    simp only [partialSpec]
+    refine ⟨fun i hi => ?_, fun i hi hj => ?_, fun i hi hj => ?_⟩ <;>
+      (simp only [getElem!]; simp_lists)
+  · rename_i h
+    simp [partialSpec]
+    scalar_tac
 
 @[rust_fun "core::array::{core::ops::index::Index<[@T; @N], @I, @O>}::index"]
 def core.array.Array.index
@@ -135,7 +142,8 @@ theorem Array.val_to_slice {α} {n} (a : Array α n) : a.to_slice.val = a.val :=
 @[simp, simp_lists_safe, simp_scalar_safe, scalar_tac a.to_slice, grind =, agrind =]
 theorem Array.length_to_slice (a : Array α n) :
   a.to_slice.length = n := by
-  simp only [Slice.length, Array.to_slice, List.Vector.length_val]
+  simp only [Slice.length, Array.to_slice]
+  exact a.property
 
 @[rust_fun "core::array::equality::{core::cmp::PartialEq<[@T; @N], [@U; @N]>}::eq"]
 def core.array.equality.PartialEqArray.eq
@@ -313,7 +321,11 @@ theorem core.array.TryFromArrayCopySlice.try_from.step
         a.val = s.val ∧ a.length = N
       | .Err () => s.length ≠ N ⦄ := by
   simp only [core.array.TryFromArrayCopySlice.try_from]
-  grind only [usr Usize.cMax_bound, usr Usize.cMax_bound', = spec_ok]
+  split
+  · apply (spec_ok _).mpr
+    exact ⟨rfl, by scalar_tac⟩
+  · apply (spec_ok _).mpr
+    simpa using ‹¬ s.length = N›
 
 @[rust_fun "core::array::{core::convert::TryFrom<&'a [@T; @N], &'a [@T], core::array::TryFromSliceError>}::try_from"]
 def core.array.TryFromSharedArraySlice.try_from
@@ -381,7 +393,9 @@ theorem Array.Insts.CoreConvertAsRefSlice.as_ref.spec
     {T : Type} {N : Usize} (a : Array T N) :
     Array.Insts.CoreConvertAsRefSlice.as_ref a
     ⦃ (s : Slice T) => s.val = a.val ⦄ := by
-  simp [Array.Insts.CoreConvertAsRefSlice.as_ref, WP.spec_ok]
+  simp only [Array.Insts.CoreConvertAsRefSlice.as_ref]
+  apply (spec_ok _).mpr
+  rfl
 
 @[step]
 theorem Array.Insts.CoreConvertAsMutSlice.as_mut.spec
@@ -391,9 +405,13 @@ theorem Array.Insts.CoreConvertAsMutSlice.as_mut.spec
       s.val = a.val ∧
       s.length = N.val ∧
       ∀ s' : Slice T, s'.length = N.val → (back s').val = s'.val ⦄ := by
-  simp [Array.Insts.CoreConvertAsMutSlice.as_mut, WP.spec_ok, Slice.length]
-  intro s' hs'
-  simp [hs']
+  simp only [Array.Insts.CoreConvertAsMutSlice.as_mut]
+  apply (spec_ok _).mpr
+  simp only [Std.WP.uncurry', Slice.length]
+  refine ⟨?_, ?_, fun s' hs' => ?_⟩
+  · trivial
+  · scalar_tac
+  · simp [hs']
 
 @[simp, step_simps]
 theorem Array.index_SliceIndexRangeUsizeSlice {T : Type} {N : Usize}
@@ -414,7 +432,7 @@ theorem Array.index_SliceIndexRangeUsizeSlice.step {T : Type} {N : Usize} [Inhab
       (fun | .panic => ¬ (r.start ≤ r.end ∧ r.end ≤ N) | _ => False)
       False := by
   simp only [Array.index_SliceIndexRangeUsizeSlice]
-  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
+  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length, Array.length_eq]
   unfold core.slice.index.SliceIndexRangeUsizeSlice.index
   split <;> rename_i h <;> simp [partialSpec, Array.to_slice, Slice.length]
   · scalar_tac
@@ -434,10 +452,11 @@ theorem Array.index_mut_SliceIndexRangeUsizeSlice.step {T : Type} {N : Usize} [I
       False := by
   simp only [core.array.Array.index_mut, core.ops.index.IndexMutSlice,
     core.slice.index.Slice.index_mut]
-  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
+  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length, Array.length_eq]
   unfold core.slice.index.SliceIndexRangeUsizeSlice.index_mut
   split <;> rename_i h <;>
-    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length]
+    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length,
+      List.length_setSlice!, Array.length_eq]
   · simp_lists; scalar_tac
   · scalar_tac
 
@@ -464,10 +483,11 @@ theorem Array.index_mut_SliceIndexRangeToUsizeSlice {T : Type} {N : Usize}
       False := by
   simp only [core.array.Array.index_mut, core.ops.index.IndexMutSlice,
     core.slice.index.Slice.index_mut]
-  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
+  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length, Array.length_eq]
   unfold core.slice.index.SliceIndexRangeToUsizeSlice.index_mut
   split <;> rename_i h <;>
-    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length] <;>
+    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length,
+      List.length_setSlice!, Array.length_eq] <;>
     scalar_tac
 
 -- Array index/index_mut with RangeFrom
@@ -493,11 +513,12 @@ theorem Array.index_mut_SliceIndexRangeFromUsizeSlice {T : Type} {N : Usize}
       False := by
   simp only [core.array.Array.index_mut, core.ops.index.IndexMutSlice,
     core.slice.index.Slice.index_mut]
-  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
+  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length, Array.length_eq]
   unfold core.slice.index.SliceIndexRangeFromUsizeSlice.index_mut
   split <;> rename_i h <;>
     simp [partialSpec, Array.from_slice, Array.to_slice, uncurry',
-          Slice.length, Slice.drop, List.length_drop];
+          Slice.length, Slice.drop, List.length_drop,
+          List.length_setSlice!, Array.length_eq];
     scalar_tac
 
 @[reducible, rust_trait_impl "core::convert::AsRef<[@T; @N], [@T]>"]
diff --git a/backends/lean/Aeneas/Std/Core/Convert.lean b/backends/lean/Aeneas/Std/Core/Convert.lean
index bdcdca1ac..12b9126e4 100644
--- a/backends/lean/Aeneas/Std/Core/Convert.lean
+++ b/backends/lean/Aeneas/Std/Core/Convert.lean
@@ -129,8 +129,8 @@ theorem core.result.Result.is_ok.step_spec {T E : Type}
     core.result.Result.is_ok r
     ⦃ (b : Bool) => b = r.ok? ⦄ := by
   match r with
-  | .Ok v => grind [is_ok]
-  | .Err e => grind [is_ok]
+  | .Ok v => simp only [is_ok]; exact (WP.spec_ok _).mpr (by simp)
+  | .Err e => simp only [is_ok]; exact (WP.spec_ok _).mpr (by simp)
 
 /-- Step spec for `Result::branch` on an `Ok`: yields `Continue v`. -/
 theorem core.result.Result.Insts.CoreOpsTry.branch_Ok.spec
diff --git a/backends/lean/Aeneas/Std/Core/Core.lean b/backends/lean/Aeneas/Std/Core/Core.lean
index 8e17a5bd8..1ce724be8 100644
--- a/backends/lean/Aeneas/Std/Core/Core.lean
+++ b/backends/lean/Aeneas/Std/Core/Core.lean
@@ -97,7 +97,7 @@ def core.option.Option.unwrap {T : Type} (x : Option T) : Result T :=
 @[step]
 theorem core.option.Option.unwrap.spec {T : Type} (x : Option T) (h : x.isSome) :
   unwrap x ⦃ v => x = some v ⦄ := by
-  simp only [unwrap, ofOption]; grind
+  simp only [unwrap, ofOption]; cases x <;> simp_all
 
 @[step_pure_def, rust_fun "core::option::{core::option::Option<@T>}::unwrap_or" -canFail]
 def core.option.Option.unwrap_or (self : Option T) (default : T) : T :=
diff --git a/backends/lean/Aeneas/Std/Core/CoreOption.lean b/backends/lean/Aeneas/Std/Core/CoreOption.lean
index 5a22429d7..5ecbdb204 100644
--- a/backends/lean/Aeneas/Std/Core/CoreOption.lean
+++ b/backends/lean/Aeneas/Std/Core/CoreOption.lean
@@ -13,6 +13,6 @@ attribute [agrind =] Option.isSome_none Option.isSome_some
 
 theorem core.option.Option.expect.spec {T : Type} (x : Option T) (msg: Str) (h : x.isSome) :
   expect x msg ⦃ v => x = some v ⦄ := by
-  simp only [expect, Result.ofOption]; grind
+  simp only [expect, Result.ofOption]; cases x <;> simp_all
 
 end Aeneas.Std
diff --git a/backends/lean/Aeneas/Std/Primitives.lean b/backends/lean/Aeneas/Std/Primitives.lean
index b774f1c6a..d8499254e 100644
--- a/backends/lean/Aeneas/Std/Primitives.lean
+++ b/backends/lean/Aeneas/Std/Primitives.lean
@@ -1,5 +1,6 @@
 import Lean
 import Std.Do
+import Std.Internal.Do
 import Aeneas.Std.Global
 import Aeneas.Extract
 import AeneasMeta.BvEnumToBitVec
@@ -298,6 +299,71 @@ abbrev willDiverge {α : Type u} (Q : PostCond α Result.postShape) : Prop :=
 
 end
 
+/-!
+# Register `Result` for `vcgen`'s `WP` type class
+
+`vcgen` is the successor of `mvcgen`; it is built on a different Hoare-logic metatheory
+(`Std.Internal.Do` rather than `Std.Do`), so it needs its own weakest-precondition
+interpretation of `Result`. In that metatheory the assertion language is plain `Prop` (rather
+than `SPred`) and the exception postconditions form a heterogeneous list (`EPost`) rather than
+a `PostShape`-indexed tuple: we use one layer for failures (indexed by the `Error`) and one
+layer for divergence (which carries no data).
+-/
+
+section
+open Std.Internal.Do Lean.Order
+
+namespace VCGen
+
+/-- The exception postconditions of the `Result` monad, as used by `vcgen`: one layer for
+failures (indexed by the `Error` that was raised) and one for divergence. -/
+abbrev EPred : Type := EPost⟨Error → Prop, Prop⟩
+
+/-- The assertion that `epost` allows the program to fail with error `e`. -/
+abbrev willFail (e : Error) (epost : EPred) : Prop := epost.head e
+
+/-- The assertion that `epost` allows the program to diverge. -/
+abbrev willDiverge (epost : EPred) : Prop := epost.tail.head
+
+/-- Companion of `EPost.Cons.head_bot` for the tail. Propositional (not definitional) because `⊥`
+of a complete lattice is `csup ∅` rather than a constructor application. -/
+private theorem tail_bot {eh : Type u} {et : Type v} [CompleteLattice eh] [CompleteLattice et] :
+    EPost.Cons.tail (⊥ : EPost.Cons eh et) = (⊥ : et) := by
+  refine PartialOrder.rel_antisymm ?_ (bot_le _)
+  exact EPost.Cons.le_tail (bot_le (EPost.Cons.mk (⊥ : eh) (⊥ : et)))
+
+/-- The `⊥` exception postcondition — the one the `⦃ _ ⦄ _ ⦃ _ ⦄` notation defaults to, i.e.
+total correctness — forbids failure. -/
+@[simp, grind =]
+theorem willFail_bot (e : Error) : willFail e (⊥ : EPred) = False := by
+  simp [willFail, EPost.Cons.head_bot, Lean.Order.bot_apply]
+
+/-- The `⊥` exception postcondition forbids divergence. -/
+@[simp, grind =]
+theorem willDiverge_bot : willDiverge (⊥ : EPred) = False := by
+  simp [willDiverge, tail_bot, EPost.Cons.head_bot]
+
+end VCGen
+
+/-- WP interpretation of the `Result` monad in terms of `Std.Internal.Do`, used by `vcgen`.
+
+Following the standard library, this is a plain `def` rather than an `instance`: the `WP`
+instance is derived from `Result.instVCGenWPMonad` (see `Aeneas/Std/WP.lean`) through the
+generic `WPMonad → WP` instance, so that there is exactly one `WP` instance for `Result`. -/
+@[instance_reducible] def Result.vcgenWPInst {α : Type u} : WP (Result α) α Prop VCGen.EPred where
+  wpTrans x := ⟨fun post epost =>
+    match x with
+    | .ok a   => post a
+    | .fail e => VCGen.willFail e epost
+    | .div    => VCGen.willDiverge epost⟩
+  wp_trans_monotone x := fun _post _post' _epost _epost' hepost hpost => by
+    cases x with
+    | ok a   => exact hpost a
+    | fail e => exact EPost.Cons.le_head hepost e
+    | div    => exact EPost.Cons.le_head (EPost.Cons.le_tail hepost)
+
+end
+
 /-!
 # Loops
 -/
diff --git a/backends/lean/Aeneas/Std/Scalar/CoreConvertNum.lean b/backends/lean/Aeneas/Std/Scalar/CoreConvertNum.lean
index fac90e77e..5a829fd2a 100644
--- a/backends/lean/Aeneas/Std/Scalar/CoreConvertNum.lean
+++ b/backends/lean/Aeneas/Std/Scalar/CoreConvertNum.lean
@@ -594,19 +594,19 @@ iscalar_no_isize def core.num.«%S».to_be_bytes (x : «%S») : Array I8 (%Size)
 # From Little-Endian
 -/
 uscalar_no_usize def core.num.«%S».from_le_bytes (a : Array U8 (%Size)#usize) : «%S» :=
-  ⟨ (BitVec.fromLEBytes (List.map U8.bv a.val)).cast (by simp) ⟩
+  ⟨ (BitVec.fromLEBytes (List.map U8.bv a.val)).cast (by scalar_tac) ⟩
 
 iscalar_no_isize def core.num.«%S».from_le_bytes (a : Array I8 (%Size)#usize) : «%S» :=
-  ⟨ (BitVec.fromLEBytes (List.map I8.bv a.val)).cast (by simp) ⟩
+  ⟨ (BitVec.fromLEBytes (List.map I8.bv a.val)).cast (by scalar_tac) ⟩
 
 /-!
 # From Big-Endian
 -/
 uscalar_no_usize def core.num.«%S».from_be_bytes (a : Array U8 (%Size)#usize) : «%S» :=
-  ⟨ (BitVec.fromBEBytes (List.map U8.bv a.val)).cast (by simp) ⟩
+  ⟨ (BitVec.fromBEBytes (List.map U8.bv a.val)).cast (by scalar_tac) ⟩
 
 iscalar_no_isize def core.num.«%S».from_be_bytes (a : Array I8 (%Size)#usize) : «%S» :=
-  ⟨ (BitVec.fromBEBytes (List.map I8.bv a.val)).cast (by simp) ⟩
+  ⟨ (BitVec.fromBEBytes (List.map I8.bv a.val)).cast (by scalar_tac) ⟩
 
 /-!
 # Progress theorems: To Little-Endian
@@ -614,25 +614,29 @@ iscalar_no_isize def core.num.«%S».from_be_bytes (a : Array I8 (%Size)#usize)
 uscalar_no_usize @[step]
 theorem core.num.«%S».to_le_bytes.step_spec (x : «%S») :
   lift (core.num.«%S».to_le_bytes x) ⦃ y => y.val = x.bv.toLEBytes.map (@UScalar.mk UScalarTy.U8) ⦄ := by
-  simp only [spec_ok, lift, to_le_bytes, UScalarTy.U8_numBits_eq]
+  simp only [lift, to_le_bytes, UScalarTy.U8_numBits_eq]
+  exact (spec_ok _).mpr rfl
 
 iscalar_no_isize @[step]
 theorem core.num.«%S».to_le_bytes.step_spec (x : «%S») :
   lift (core.num.«%S».to_le_bytes x) ⦃ y => y.val = x.bv.toLEBytes.map (@IScalar.mk IScalarTy.I8) ⦄ := by
-  simp only [spec_ok, lift, to_le_bytes, IScalarTy.I8_numBits_eq]
+  simp only [lift, to_le_bytes, IScalarTy.I8_numBits_eq]
+  exact (spec_ok _).mpr rfl
 
 /-!
 # Progress theorems: From Little-Endian
 -/
 uscalar_no_usize @[step]
 theorem core.num.«%S».from_le_bytes.step_spec (x : Array U8 (%Size)#usize) :
-  lift (core.num.«%S».from_le_bytes x) ⦃ y => y.bv = (BitVec.fromLEBytes (x.val.map U8.bv)).cast (by simp) ⦄ := by
-  simp only [spec_ok, lift, from_le_bytes]
+  lift (core.num.«%S».from_le_bytes x) ⦃ y => y.bv = (BitVec.fromLEBytes (x.val.map U8.bv)).cast (by scalar_tac) ⦄ := by
+  simp only [lift, from_le_bytes]
+  exact (spec_ok _).mpr rfl
 
 iscalar_no_isize @[step]
 theorem core.num.«%S».from_le_bytes.step_spec (x : Array I8 (%Size)#usize) :
-  lift (core.num.«%S».from_le_bytes x) ⦃ y => y.bv = (BitVec.fromLEBytes (x.val.map I8.bv)).cast (by simp) ⦄  := by
-  simp only [spec_ok, lift, from_le_bytes]
+  lift (core.num.«%S».from_le_bytes x) ⦃ y => y.bv = (BitVec.fromLEBytes (x.val.map I8.bv)).cast (by scalar_tac) ⦄  := by
+  simp only [lift, from_le_bytes]
+  exact (spec_ok _).mpr rfl
 
 /-!
 # Progress theorems: To Big-Endian
@@ -640,25 +644,29 @@ theorem core.num.«%S».from_le_bytes.step_spec (x : Array I8 (%Size)#usize) :
 uscalar_no_usize @[step]
 theorem core.num.«%S».to_be_bytes.step_spec (x : «%S») :
   lift (core.num.«%S».to_be_bytes x) ⦃ y => y.val = x.bv.toBEBytes.map (@UScalar.mk UScalarTy.U8) ⦄ := by
-  simp only [spec_ok, lift, to_be_bytes, UScalarTy.U8_numBits_eq]
+  simp only [lift, to_be_bytes, UScalarTy.U8_numBits_eq]
+  exact (spec_ok _).mpr rfl
 
 iscalar_no_isize @[step]
 theorem core.num.«%S».to_be_bytes.step_spec (x : «%S») :
   lift (core.num.«%S».to_be_bytes x) ⦃ y => y.val = x.bv.toBEBytes.map (@IScalar.mk IScalarTy.I8) ⦄ := by
-  simp only [spec_ok, lift, to_be_bytes, IScalarTy.I8_numBits_eq]
+  simp only [lift, to_be_bytes, IScalarTy.I8_numBits_eq]
+  exact (spec_ok _).mpr rfl
 
 /-!
 # Progress theorems: From Big-Endian
 -/
 uscalar_no_usize @[step]
 theorem core.num.«%S».from_be_bytes.step_spec (x : Array U8 (%Size)#usize) :
-  lift (core.num.«%S».from_be_bytes x) ⦃ y => y.bv = (BitVec.fromBEBytes (x.val.map U8.bv)).cast (by simp) ⦄ := by
-  simp only [spec_ok, lift, from_be_bytes]
+  lift (core.num.«%S».from_be_bytes x) ⦃ y => y.bv = (BitVec.fromBEBytes (x.val.map U8.bv)).cast (by scalar_tac) ⦄ := by
+  simp only [lift, from_be_bytes]
+  exact (spec_ok _).mpr rfl
 
 iscalar_no_isize @[step]
 theorem core.num.«%S».from_be_bytes.step_spec (x : Array I8 (%Size)#usize) :
-  lift (core.num.«%S».from_be_bytes x) ⦃ y => y.bv = (BitVec.fromBEBytes (x.val.map I8.bv)).cast (by simp) ⦄  := by
-  simp only [spec_ok, lift, from_be_bytes]
+  lift (core.num.«%S».from_be_bytes x) ⦃ y => y.bv = (BitVec.fromBEBytes (x.val.map I8.bv)).cast (by scalar_tac) ⦄  := by
+  simp only [lift, from_be_bytes]
+  exact (spec_ok _).mpr rfl
 
 /-!
 # `cast_signed` / `cast_unsigned`
diff --git a/backends/lean/Aeneas/Std/Slice.lean b/backends/lean/Aeneas/Std/Slice.lean
index d8c770289..b1134d82f 100644
--- a/backends/lean/Aeneas/Std/Slice.lean
+++ b/backends/lean/Aeneas/Std/Slice.lean
@@ -118,7 +118,7 @@ def Slice.index_usize {α : Type u} (v: Slice α) (i: Usize) : Result α :=
   | some x => ok x
 
 theorem Slice.eq_iff {α} (s0 s1 : Slice α) : s0 = s1 ↔ s0.val = s1.val := by
-  simp only [Slice, Subtype.ext_iff]
+  exact Subtype.ext_iff
 
 @[rust_fun "core::slice::{[@T]}::is_empty", simp]
 def core.slice.Slice.is_empty {T : Type} (s : Slice T) : Result Bool := ok (s.length = 0)
@@ -133,7 +133,7 @@ theorem core.slice.Slice.is_empty_spec {T : Type} (s : Slice T) :
 theorem Slice.index_usize_spec {α : Type u} (v: Slice α) (i: Usize)
   (hbound : i.val < v.length) :
   v.index_usize i ⦃ x => x = v.val[i.val] ⦄ := by
-  grind [index_usize]
+  simp only [index_usize, Slice.getElem?_Usize_eq, List.getElem?_eq_getElem hbound, spec_ok]
 
 @[simp, scalar_tac_simps, simp_lists_hyps_simps, grind =]
 theorem Slice.set_val_eq {α : Type u} (v: Slice α) (i: Usize) (x: α) :
@@ -268,9 +268,9 @@ def Slice.update {α : Type u} (v: Slice α) (i: Usize) (x: α) : Result (Slice
 theorem Slice.update_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
   v.update i x ⦃ nv => nv = v.set i x ⦄ := by
-  simp only [update, set, setAtNat]
-  simp at *
-  simp [*]
+  simp only [update, List.getElem?_eq_getElem hbound]
+  apply (spec_ok _).mpr
+  rfl
 
 def Slice.index_mut_usize {α : Type u} (v: Slice α) (i: Usize) :
   Result (α × (α → Slice α)) := do
@@ -288,7 +288,8 @@ theorem Slice.index_mut_usize_spec {α : Type u} (v: Slice α) (i: Usize)
 @[simp, simp_lists_safe]
 theorem Slice.update_index_eq α [Inhabited α] (x : Slice α) (i : Usize) (h : i.val < x.val.length) :
   x.set i (x.val[i.val]'h) = x := by
-  simp only [Slice, Subtype.ext_iff, set_val_eq, List.set_getElem_self]
+  apply Subtype.ext
+  simp only [set_val_eq, List.set_getElem_self]
 
 def Slice.subslice {α : Type u} (s : Slice α) (r : Range Usize) : Result (Slice α) :=
   if r.start.val ≤ r.end.val ∧ r.end.val ≤ s.length then
@@ -305,7 +306,10 @@ theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Ran
   subslice s r ⦃ ns => ns.val = s.slice r.start.val r.end.val ∧
   (∀ i, i + r.start.val < r.end.val → ns[i]! = s[r.start.val + i]!) ⦄
   := by
-  simp_all only [subslice, length, and_self, ite_true, slice, spec_ok, true_and]
+  unfold subslice
+  rw [if_pos ⟨h0, h1⟩]
+  apply (spec_ok _).mpr
+  refine ⟨rfl, ?_⟩
   intro i _
   have := List.getElem!_slice r.start.val r.end.val i s.val (by scalar_tac)
   simp only [List.getElem!_eq_getElem?_getD, getElem!_Nat_eq] at *
@@ -324,9 +328,10 @@ theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (
     (∀ i, i < r.start.val → na[i]! = a[i]!) ∧
     (∀ i, r.start.val ≤ i → i < r.end.val → na[i]! = ss[i - r.start.val]!) ∧
     (∀ i, r.end.val ≤ i → i < a.length → na[i]! = a[i]!) ⦄ := by
-  simp only [update_subslice, length, and_self, ↓reduceDIte, getElem!_Nat_eq,
-    spec_ok, *]
-  simp_lists
+  simp only [update_subslice, length, and_self, ↓reduceDIte, *]
+  apply (spec_ok _).mpr
+  refine ⟨fun i hi => ?_, fun i hi hj => ?_, fun i hi hj => ?_⟩ <;>
+    (simp only [getElem!]; simp_lists)
 
 @[rust_fun "core::slice::{[@T]}::reverse" -canFail]
 def core.slice.Slice.reverse {T : Type} (s : Slice T) : Slice T :=
@@ -649,7 +654,9 @@ theorem _SliceIndexRangeFromUsizeSlice.index_mut.test {T} (s : Slice T) (r : cor
     back s1 = s
   | _ => False := by
   unfold core.slice.index.SliceIndexRangeFromUsizeSlice.index_mut
-  simp [h]
+  simp only [h, ↓reduceIte, Slice.drop]
+  apply Subtype.ext
+  simp
 
 @[reducible, rust_trait_impl "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeFrom<usize>>"]
 def core.slice.index.private_slice_index.SealedRangeFromUsize :
@@ -692,7 +699,9 @@ theorem Slice.clone_spec {T : Type} {clone : T → Result T} {s : Slice T} (h :
   Slice.clone clone s ⦃ s' => s = s' ⦄ := by
   simp only [Slice.clone]
   have ⟨ _, h ⟩ := spec_imp_exists (List.clone_spec h)
-  simp [h]
+  simp only [h.1, bind_tc_ok]
+  apply (spec_ok _).mpr
+  exact (Subtype.ext h.2.1).symm
 
 @[rust_fun "core::slice::{[@T]}::split_at"]
 def core.slice.Slice.split_at {T : Type} (s : Slice T) (n : Usize) :
@@ -732,7 +741,7 @@ theorem core.slice.Slice.split_at.spec {T : Type} (s : Slice T) (n : Usize)
         s0.length = n.val ∧ s1.length = s.length - n.val ∧
         s0.val = s.val.take n.val ∧ s1.val = s.val.drop n.val ⦄ := by
   unfold core.slice.Slice.split_at
-  simp only [h, ↓reduceDIte, WP.spec_ok, uncurry'_pair]
+  simp only [h, ↓reduceDIte, WP.spec_ok]
   refine ⟨?_, ?_, ?_, ?_⟩ <;>
   simp only [Slice.length, List.splitAt_eq, List.length_take, inf_eq_left, List.length_drop, *]
 
@@ -759,11 +768,13 @@ theorem core.slice.Slice.split_at_mut.spec {T : Type} (s : Slice T) (n : Usize)
   · simp [Slice.length, List.splitAt_eq]
   · simp [List.splitAt_eq]
   · simp [List.splitAt_eq]
-  · split_ifs with hcond
-    · exact ⟨rfl, by simp [Slice.length, List.length_append]; scalar_tac⟩
-    · exfalso; apply hcond
-      simp [Slice.length, List.splitAt_eq] at *
-      exact ⟨by scalar_tac, by scalar_tac⟩
+  · have hc : s0'.length = (s.val.splitAt n.val).1.length ∧ s1'.length = (s.val.splitAt n.val).2.length := by
+      simp only [List.splitAt_eq, List.length_take, List.length_drop, Slice.length]
+      constructor <;> scalar_tac
+    refine ⟨?_, ?_⟩
+    · simp only [hc.1, hc.2, and_self, ↓reduceDIte]
+    · simp only [hc.1, hc.2, and_self, ↓reduceDIte, Slice.length, List.length_append]
+      scalar_tac
 
 @[rust_fun "core::slice::{[@T]}::swap"]
 def core.slice.Slice.swap {T : Type} (s : Slice T) (a b : Usize) : Result (Slice T) := do
@@ -824,7 +835,8 @@ theorem Slice.setSlice!_length {α : Type u} (s : Slice α) (i : ℕ) (s' : List
 theorem Slice.setSlice!_getElem!_prefix {α} [Inhabited α]
   (s : Slice α) (s' : List α) (i j : ℕ) (h : j < i) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Slice.setSlice!, Slice.getElem!_Nat_eq]
+  simp only [Slice.getElem!_Nat_eq]
+  simp only [Slice.setSlice!]
   simp_lists
 
 @[simp_lists_safe]
@@ -834,7 +846,8 @@ theorem Slice.setSlice!_getElem_prefix {α}
   have hj' : j < (s.setSlice! i s').length := by
     simpa [Slice.setSlice!_length] using h.2
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Slice.getElem?_Nat_eq, Slice.setSlice!]
+    simp only [Slice.getElem?_Nat_eq]
+    simp only [Slice.setSlice!]
     simp_lists [List.setSlice!_getElem?_prefix]
   simp only [Slice.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2,
     Option.some.injEq] at h1
@@ -844,7 +857,8 @@ theorem Slice.setSlice!_getElem_prefix {α}
 theorem Slice.setSlice!_getElem!_middle {α} [Inhabited α]
   (s : Slice α) (s' : List α) (i j : ℕ) (h : i ≤ j ∧ j - i < s'.length ∧ j < s.length) :
   (s.setSlice! i s')[j]! = s'[j - i]! := by
-  simp only [Slice.setSlice!, Slice.getElem!_Nat_eq]
+  simp only [Slice.getElem!_Nat_eq]
+  simp only [Slice.setSlice!]
   simp_lists
 
 @[simp_lists_safe]
@@ -855,7 +869,8 @@ theorem Slice.setSlice!_getElem_middle {α}
     simpa [Slice.setSlice!_length] using h.2.2
   have hji : j - i < s'.length := h.2.1
   have h1 : (s.setSlice! i s')[j]? = s'[j - i]? := by
-    simp only [Slice.getElem?_Nat_eq, Slice.setSlice!]
+    simp only [Slice.getElem?_Nat_eq]
+    simp only [Slice.setSlice!]
     simp_lists [List.setSlice!_getElem?_middle]
   simp only [Slice.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem hji,
     Option.some.injEq] at h1
@@ -864,7 +879,8 @@ theorem Slice.setSlice!_getElem_middle {α}
 theorem Slice.setSlice!_getElem!_suffix {α} [Inhabited α]
   (s : Slice α) (s' : List α) (i j : ℕ) (h : i + s'.length ≤ j) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Slice.setSlice!, Slice.getElem!_Nat_eq]
+  simp only [Slice.getElem!_Nat_eq]
+  simp only [Slice.setSlice!]
   simp_lists
 
 theorem Slice.setSlice!_getElem_suffix {α}
@@ -873,7 +889,8 @@ theorem Slice.setSlice!_getElem_suffix {α}
   have hj' : j < (s.setSlice! i s').length := by
     simpa [Slice.setSlice!_length] using h.2
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Slice.getElem?_Nat_eq, Slice.setSlice!]
+    simp only [Slice.getElem?_Nat_eq]
+    simp only [Slice.setSlice!]
     simp_lists [List.setSlice!_getElem?_suffix]
   simp only [Slice.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2,
     Option.some.injEq] at h1
@@ -894,9 +911,9 @@ theorem core.slice.index.SliceIndexRangeUsizeSlice.index_mut.step_spec (r : core
   simp only [index_mut, UScalar.le_equiv, Slice.length]
   split
   . simp only [spec_ok, Std.WP.uncurry', true_and]
+    refine ⟨?_, fun s2 => rfl⟩
     simp_lists
     simp_scalar
-    simp_lists [Slice.eq_iff]
   . scalar_tac
 
 @[step]
@@ -907,9 +924,10 @@ theorem core.slice.index.SliceIndexRangeUsizeSlice.index.step_spec {α : Type}
       s1.length = r.end - r.start ⦄ := by
   simp only [core.slice.index.SliceIndexRangeUsizeSlice.index, UScalar.le_equiv, Slice.length]
   split
-  · simp only [spec_ok, true_and]
+  · apply (spec_ok _).mpr
+    refine ⟨rfl, ?_⟩
     simp_lists
-    omega
+    simp_scalar
   · simp only [spec_fail]
     scalar_tac
 
@@ -950,8 +968,11 @@ theorem core.slice.index.SliceIndexRangeToUsizeSlice.index.step_spec
       s1.length = r.end ⦄ := by
   simp only [index]
   split
-  · simp only [spec_ok, Slice.length, true_and]
-    simp; scalar_tac
+  · apply (spec_ok _).mpr
+    refine ⟨rfl, ?_⟩
+    simp only [Slice.length]
+    simp_lists
+    simp_scalar
   · scalar_tac
 
 -- RangeFrom step specs
@@ -991,8 +1012,11 @@ theorem core.slice.index.SliceIndexRangeFromUsizeSlice.index.step_spec
       s1.length = s.length - r.start.val ⦄ := by
   simp only [index]
   split
-  · simp only [spec_ok, Slice.drop, true_and]
-    simp [Slice.length, List.length_drop]
+  · apply (spec_ok _).mpr
+    refine ⟨rfl, ?_⟩
+    simp only [Slice.length]
+    simp_lists
+    simp_scalar
   · scalar_tac
 
 @[step]
@@ -1033,7 +1057,8 @@ theorem Slice.mapM_spec {α β} {f : α → Result β} {s : Slice α} {post : Na
   obtain ⟨l', hl'⟩ := hmapM_ok
   split
   case h_1 xs heq =>
-    simp only [UScalar.lt_equiv, Usize.ofNatCore_val_eq, spec_ok]
+    simp only [UScalar.lt_equiv, Usize.ofNatCore_val_eq]
+    apply (spec_ok _).mpr
     refine ⟨by grind [List.mapM_Result_length], fun i hi => ?_⟩
     have hlen : i < s.len := by have := List.mapM_Result_length heq; simp [Slice.len] at *; omega
     have hthis := List.mapM_Result_ok heq (↑i) (by scalar_tac)
@@ -1086,7 +1111,10 @@ theorem core.slice.Slice.fill.spec {T : Type} (cloneInst : core.clone.Clone T)
     | .div => exfalso; have := hclone; rw [hc] at this; simp at this
   have hmapM := List.mapM_const_ok s.val hcl
   split
-  · rename_i val heq; rw [hmapM] at heq; cases heq; simp [spec_ok, Slice.length, List.length_replicate]
+  · rename_i val heq; rw [hmapM] at heq; cases heq
+    apply (spec_ok _).mpr
+    refine ⟨?_, rfl⟩
+    simp [Slice.length, List.length_replicate]
   · exfalso; simp_all
   · exfalso; simp_all
 
diff --git a/backends/lean/Aeneas/Std/Spec.lean b/backends/lean/Aeneas/Std/Spec.lean
index 0204383a6..9231143b8 100644
--- a/backends/lean/Aeneas/Std/Spec.lean
+++ b/backends/lean/Aeneas/Std/Spec.lean
@@ -29,6 +29,9 @@ structure SpecInfo where
   qimp_elim_tactics : Array Lean.Name
 
   to_mvcgen: Option Name
+  /-- Conversion lemma turning a spec statement into a `vcgen` spec (an entailment
+  `pre ⊑ Std.Internal.Do.wp prog post epost`). See `Aeneas.Std.WP.spec_to_vcgen`. -/
+  to_vcgen: Option Name := none
 
   liftings : Array LiftingInfo
   deriving Inhabited
diff --git a/backends/lean/Aeneas/Std/Vec.lean b/backends/lean/Aeneas/Std/Vec.lean
index c58199c4b..c5a081239 100644
--- a/backends/lean/Aeneas/Std/Vec.lean
+++ b/backends/lean/Aeneas/Std/Vec.lean
@@ -130,7 +130,15 @@ def Vec.push {α : Type u} (v : Vec α) (x : α) : Result (Vec α)
 theorem Vec.push_spec {α : Type u} (v : Vec α) (x : α) (h : v.val.length < Usize.max) :
   v.push x ⦃ v1 =>
   v1.val = v.val ++ [x] ⦄ := by
-  unfold push; grind
+  unfold push
+  simp only []
+  split
+  · apply (spec_ok _).mpr
+    simp [List.concat_eq_append]
+  · exfalso
+    rename_i hc
+    simp only [Bool.or_eq_true, decide_eq_true_eq, not_or] at hc
+    scalar_tac
 
 @[rust_fun "alloc::vec::{alloc::vec::Vec<@T>}::insert" (keepParams := [true, false])]
 def Vec.insert {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
@@ -143,7 +151,9 @@ def Vec.insert {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
 theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
   (hbound : i.val < v.length) :
   v.insert i x ⦃ nv => nv.val = v.val.set i x ⦄ := by
-  simp [insert, *]
+  simp only [insert, hbound, ↓reduceIte]
+  apply (spec_ok _).mpr
+  rfl
 
 def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
   match v[i.val]? with
@@ -170,7 +180,9 @@ theorem Vec.update_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
   v.update i x ⦃ nv => nv = v.set i x ⦄ := by
   simp only [update, set]
   simp at *
-  split <;> simp_all
+  split
+  · simp_all
+  · apply (spec_ok _).mpr; rfl
 
 @[scalar_tac_simps, grind =, agrind =]
 theorem Vec.set_length {α : Type u} (v: Vec α) (i: Usize) (x: α) :
@@ -345,6 +357,8 @@ theorem alloc.vec.from_elem_spec {T : Type} (cloneInst : core.clone.Clone T)
   unfold from_elem
   have ⟨ l, h ⟩ := spec_imp_exists (@List.clone_spec _ cloneInst.clone (List.replicate n.val x) (by intros; simp_all))
   simp [h]
+  apply (spec_ok _).mpr
+  exact ⟨rfl, by simp⟩
 
 @[rust_fun "alloc::vec::{alloc::vec::Vec<@T>}::with_capacity" -canFail -lift]
 def alloc.vec.Vec.with_capacity (T : Type) (_ : Usize) : alloc.vec.Vec T := Vec.new T
@@ -400,24 +414,24 @@ theorem alloc.vec.Vec.resize_spec {T} (cloneInst : core.clone.Clone T)
     nv.val = v.val.resize new_len value ⦄ := by
   rw [resize]
   split
-  . simp
-  . simp [*]
+  · apply (spec_ok _).mpr; rfl
+  · simp only [hClone]
+    apply (spec_ok _).mpr; rfl
 
 @[simp↓, scalar_tac_simps↓, grind =, agrind =]
 theorem alloc.vec.Vec.set_getElem!_eq α [Inhabited α] (x : alloc.vec.Vec α) (i : Usize) :
   x.set i x[i]! = x := by
-  simp only [getElem!_Usize_eq]
-  simp only [Vec, set_val_eq, Subtype.ext_iff, List.set_getElem!]
+  apply Subtype.ext
+  simp only [getElem!_Usize_eq, set_val_eq, List.set_getElem!]
 
 @[simp↓, scalar_tac_simps, simp_lists_safe, grind =, agrind =]
 theorem alloc.vec.Vec.set_getElem_eq α (x : alloc.vec.Vec α) (i : Usize) (h : i.val < x.length) :
   x.set i x[i] = x := by
   have h' : i.val < x.val.length := by
     simpa using h
-  have hself : x.val.set i.val x.val[i.val] = x.val :=
-    List.set_getElem_self (as := x.val) (i := i.val) (h := h')
-  simp only [alloc.vec.Vec, Subtype.ext_iff, set_val_eq] at hself ⊢
-  exact hself
+  apply Subtype.ext
+  simp only [set_val_eq, getElem_Usize_eq]
+  exact List.set_getElem_self (as := x.val) (i := i.val) (h := h')
 
 @[simp_lists_safe↓]
 theorem alloc.vec.Vec.set_getElem_eq' α (x : alloc.vec.Vec α) (i j : Usize) (h : j.val < x.length) (hEq : i = j) :
@@ -462,7 +476,9 @@ def alloc.vec.FromBoxSliceVec.from {T : Type} (v : alloc.vec.Vec T) : Result (Sl
 @[step]
 theorem alloc.vec.FromBoxSliceVec.from_spec {T : Type} (v : alloc.vec.Vec T) :
   alloc.vec.FromBoxSliceVec.from v ⦃ s => s.length = v.length ∧ s.val = v.val⦄ := by
-  simp [alloc.vec.FromBoxSliceVec.from]
+  simp only [alloc.vec.FromBoxSliceVec.from]
+  apply (spec_ok _).mpr
+  exact ⟨rfl, rfl⟩
 
 @[reducible, rust_trait_impl "core::convert::From<Box<[@T]>, alloc::vec::Vec<@T>>" (keepParams := [true, false])]
 def core.convert.FromBoxSliceVec (T : Type) :
@@ -482,7 +498,8 @@ theorem alloc.vec.Vec.setSlice!_length {α : Type u} (s : alloc.vec.Vec α) (i :
 theorem alloc.vec.Vec.setSlice!_getElem!_prefix {α} [Inhabited α]
   (s : alloc.vec.Vec α) (s' : List α) (i j : ℕ) (h : j < i) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Vec.setSlice!, Vec.getElem!_Nat_eq]
+  rw [Vec.getElem!_Nat_eq]
+  simp only [Vec.setSlice!]
   simp_lists
 
 @[simp_lists_safe, grind =, agrind =]
@@ -492,7 +509,8 @@ theorem alloc.vec.Vec.setSlice!_getElem_prefix {α}
   have hj' : j < (s.setSlice! i s').length := by
     simpa [Vec.setSlice!_length] using h.2
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Vec.getElem?_Nat_eq, Vec.setSlice!]
+    rw [Vec.getElem?_Nat_eq]
+    simp only [Vec.setSlice!]
     simp_lists [List.setSlice!_getElem?_prefix]
   simpa [Vec.getElem?_Nat_eq, Vec.getElem_Nat_eq,
     List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2] using h1
@@ -501,7 +519,8 @@ theorem alloc.vec.Vec.setSlice!_getElem_prefix {α}
 theorem alloc.vec.Vec.setSlice!_getElem!_middle {α} [Inhabited α]
   (s : alloc.vec.Vec α) (s' : List α) (i j : ℕ) (h : i ≤ j ∧ j - i < s'.length ∧ j < s.length) :
   (s.setSlice! i s')[j]! = s'[j - i]! := by
-  simp only [Vec.setSlice!, Vec.getElem!_Nat_eq]
+  rw [Vec.getElem!_Nat_eq]
+  simp only [Vec.setSlice!]
   simp_lists
 
 @[simp_lists_safe, grind =, agrind =]
@@ -512,7 +531,8 @@ theorem alloc.vec.Vec.setSlice!_getElem_middle {α}
     simpa [Vec.setSlice!_length] using h.2.2
   have hji : j - i < s'.length := h.2.1
   have h1 : (s.setSlice! i s')[j]? = s'[j - i]? := by
-    simp only [Vec.getElem?_Nat_eq, Vec.setSlice!]
+    rw [Vec.getElem?_Nat_eq]
+    simp only [Vec.setSlice!]
     simp_lists [List.setSlice!_getElem?_middle]
   simpa [Vec.getElem?_Nat_eq, Vec.getElem_Nat_eq,
     List.getElem?_eq_getElem hj', List.getElem?_eq_getElem hji] using h1
@@ -520,7 +540,8 @@ theorem alloc.vec.Vec.setSlice!_getElem_middle {α}
 theorem alloc.vec.Vec.setSlice!_getElem!_suffix {α} [Inhabited α]
   (s : alloc.vec.Vec α) (s' : List α) (i j : ℕ) (h : i + s'.length ≤ j) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Vec.setSlice!, Vec.getElem!_Nat_eq]
+  rw [Vec.getElem!_Nat_eq]
+  simp only [Vec.setSlice!]
   simp_lists
 
 theorem alloc.vec.Vec.setSlice!_getElem_suffix {α}
@@ -529,7 +550,8 @@ theorem alloc.vec.Vec.setSlice!_getElem_suffix {α}
   have hj' : j < (s.setSlice! i s').length := by
     simpa [Vec.setSlice!_length] using h.2
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Vec.getElem?_Nat_eq, Vec.setSlice!]
+    rw [Vec.getElem?_Nat_eq]
+    simp only [Vec.setSlice!]
     simp_lists [List.setSlice!_getElem?_suffix]
   simpa [Vec.getElem?_Nat_eq, Vec.getElem_Nat_eq,
     List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2] using h1
diff --git a/backends/lean/Aeneas/Std/WP.lean b/backends/lean/Aeneas/Std/WP.lean
index 4acf11c26..dda38679c 100644
--- a/backends/lean/Aeneas/Std/WP.lean
+++ b/backends/lean/Aeneas/Std/WP.lean
@@ -8,8 +8,8 @@ namespace Aeneas.Std.WP
 
 open Std Result
 
-def Post α := (α -> Prop)
-def Pre := Prop
+@[reducible] def Post α := (α -> Prop)
+@[reducible] def Pre := Prop
 
 def Wp α := Post α → Pre
 
@@ -37,7 +37,7 @@ theorem spec_dspec (α) (x : Result α) (p: Post α) : spec x p → dspec x p :=
 theorem dspec_admissible {α} (p : Post α )
   : Lean.Order.admissible (fun x => dspec x p) := by
   apply Lean.Order.admissible_flatOrder
-  simp [dspec]
+  simp [dspec, Lean.Order.FlatOrder.mk]
 
 /-- Variant of `uncurry` used to decompose tuples in post-conditions.
 
@@ -764,7 +764,7 @@ example (x : Nat) :
 
 private theorem massert_spec' (b : Prop) [Decidable b] (h : b) :
   massert b ⦃ _ => True ⦄ := by
-  grind [massert]
+  simp only [massert, if_pos h, spec_ok]
 
 @[simp]
 theorem qimp_spec_unit {α} (P : Unit → Prop) (k : Unit → Result α) (Q : α → Prop) :
@@ -791,11 +791,9 @@ example :
   --
   apply spec_bind'
   · apply massert_spec'; omega
-  simp -failIfUnchanged only [qimp_spec_unit, forall_const]
-  --
-  apply spec_mono'
-  · apply massert_spec'; omega
-  simp -failIfUnchanged only [qimp_unit, forall_const]
+  -- eliminate the quantifier over the `()` output and the trivial precondition
+  intro _ _
+  apply massert_spec'; omega
 
 /- Example with a post-condition manipulating an ∃ -/
 example (zero : List Nat → Result (List Nat))
@@ -809,9 +807,9 @@ example (zero : List Nat → Result (List Nat))
   apply spec_bind'
   · apply zero_spec
   simp -failIfUnchanged only [qimp_spec_iff, imp_exists_iff]
-  rintro s' h0 h1
+  rintro s' h0
   --
-  simp only [pure, spec_ok]
+  simp only [pure, spec_ok, imp, implies_true]
 
 
 end Aeneas.Std.WP
@@ -915,6 +913,90 @@ theorem triple_in_hypothesis {f : Result α} {Q : α → Assertion _} (p : Prop)
 
 end Aeneas.Std.WP
 
+namespace Aeneas.Std.WP
+
+/-!
+# vcgen
+
+`vcgen` is the successor of `mvcgen`. It is built on a different Hoare-logic metatheory
+(`Std.Internal.Do` instead of `Std.Do`), so it needs its own `WPMonad` instance for `Result`
+(the `WP` interpretation itself is `Result.vcgenWPInst`, see `Aeneas/Std/Primitives.lean`) and
+its own bridges from the Aeneas spec predicates.
+
+Unlike the `mvcgen` bridges above we state the `vcgen` specs in the entailment form
+`pre ⊑ wp x post epost` rather than as `Std.Internal.Do.Triple`s. `vcgen` accepts both forms
+(see `Lean.Elab.Tactic.Do.Internal.SpecAttr.selectProg`), but `Triple` forces the assertion
+language and the result type to live in the *same* universe, which — the assertion language
+being `Prop` — would restrict the specs to `Type 0`. The `wp` entailment form has no such
+constraint, so the generated specs stay universe polymorphic like the theorems they come from.
+-/
+
+open Std Result
+open Std.Internal.Do Lean.Order
+
+instance Result.instVCGenWPMonad : WPMonad Result.{u} Prop VCGen.EPred where
+  toWP _ := Result.vcgenWPInst
+  pure_le_wp_pure _ _ _ := PartialOrder.rel_refl
+  bind_le_wp_bind x _ := fun _ _ => by cases x <;> exact id
+
+/-- Lift an Aeneas total-correctness step spec to a `vcgen`-compatible spec.
+
+A `spec` rules out failure and divergence, so the exception postcondition is arbitrary. -/
+theorem spec_to_vcgen {α : Type u} {x : Result α} {Q : α → Prop}
+    (h : spec x Q) (epost : VCGen.EPred) :
+    (True : Prop) ⊑ wp x Q epost := by
+  obtain ⟨v, hx, hQv⟩ := spec_imp_exists h
+  subst hx
+  exact fun _ => hQv
+
+/-- Lift an Aeneas partial-correctness (divergence-allowing) step spec to a `vcgen`-compatible
+spec. A `dspec` rules out failure but not divergence, hence the `x ≠ div` precondition. -/
+theorem dspec_to_vcgen {α : Type u} {x : Result α} {Q : α → Prop}
+    (h : dspec x Q) (epost : VCGen.EPred) :
+    (¬ x = .div) ⊑ wp x Q epost := by
+  cases x <;> simp_all [dspec, wp, Std.Internal.Do.WP.wpTrans]
+
+/-- Lift an Aeneas `partialSpec` to a `vcgen`-compatible spec. -/
+theorem partialSpec_to_vcgen {α : Type u} {x : Result α}
+    {p_ok : α → Prop} {p_fail : Error → Prop} {p_div : Prop}
+    (h : partialSpec x p_ok p_fail p_div)
+    {post : α → Prop} {epost : VCGen.EPred}
+    (h_ok   : ∀ r, p_ok r → post r)
+    (h_fail : ∀ e, p_fail e → VCGen.willFail e epost)
+    (h_div  : p_div → VCGen.willDiverge epost) :
+    (True : Prop) ⊑ wp x post epost := by
+  cases x <;> simp only [partialSpec] at h <;> intro _
+  · exact h_ok _ h
+  · exact h_fail _ h
+  · exact h_div h
+
+@[spec]
+theorem Result.ok_vcgen_spec {α : Type} (a : α) {post : α → Prop} {epost : VCGen.EPred} :
+    post a ⊑ wp (Result.ok a) post epost := PartialOrder.rel_refl
+
+@[spec]
+theorem Result.fail_vcgen_spec {α : Type} (e : Error) {post : α → Prop} {epost : VCGen.EPred} :
+    VCGen.willFail e epost ⊑ wp (Result.fail e : Result α) post epost := PartialOrder.rel_refl
+
+@[spec]
+theorem Result.div_vcgen_spec {α : Type} {post : α → Prop} {epost : VCGen.EPred} :
+    VCGen.willDiverge epost ⊑ wp (Result.div : Result α) post epost := PartialOrder.rel_refl
+
+/-- Let `vcgen` see through the `uncurry` that the `do` elaborator introduces for
+tuple-destructuring binds (`let (x, y) ← e`).
+
+We cannot simply register `uncurry`'s unfolding equation, because it is stated for a
+`Prod.mk` discriminant (`uncurry f (a, b) = f a b`) while the continuation of a bind is applied
+to an opaque variable. Phrasing the unfolding as a spec instead lets `vcgen` rewrite
+`uncurry f x` into `f x.1 x.2` and carry on with the continuation. -/
+@[spec]
+theorem uncurry_vcgen_spec {α : Type u} {β : Type v} {γ : Type w}
+    {f : α → β → Result γ} {x : α × β} {post : γ → Prop} {epost : VCGen.EPred} :
+    wp (f x.1 x.2) post epost ⊑ wp (Std.uncurry f x) post epost := by
+  cases x; exact PartialOrder.rel_refl
+
+end Aeneas.Std.WP
+
 namespace Aeneas.Std
 
 /-!
@@ -944,7 +1026,16 @@ theorem loop.spec {α : Type u} {β : Type v} {γ : Type w}
   apply @wf.wf.fix γ (fun x' =>
     ∀ x, measure x = x' →
     inv x → loop body x ⦃ post ⦄)
-  grind [loop]
+  intro x1 IH x2 hmeas hinv2
+  -- `body x2` succeeds and its result satisfies the loop invariant post-condition
+  obtain ⟨r, hbr, hr⟩ := WP.spec_imp_exists (hBody x2 hinv2)
+  rw [loop.eq_def, hbr]
+  cases r with
+  | done y => simpa using hr
+  | cont x' =>
+    obtain ⟨hinv', hrel⟩ := hr
+    -- the measure strictly decreases, so we can conclude by well-founded recursion
+    exact IH (measure x') (hmeas ▸ hrel) x' rfl hinv'
 
 theorem loop.spec_decr_nat {α : Type u} {β : Type v}
   (measure : α → Nat)
@@ -961,6 +1052,77 @@ theorem loop.spec_decr_nat {α : Type u} {β : Type v}
   have := loop.spec measure inv post body x hBody hInv
   apply this
 
+section
+open Std.Internal.Do Lean.Order
+
+/-- `vcgen` spec for the `loop` combinator.
+
+The `vcgen` counterpart of `loop_spec` (see `Aeneas/Std/Primitives.lean`): given a loop invariant
+`inv`, a well-founded relation `rel` and a termination measure, it discharges `loop body init`
+provided each iteration of `body` either finishes (`.done`) satisfying the postcondition or
+continues (`.cont`) preserving the invariant while decreasing the measure. -/
+@[spec]
+theorem loop_vcgen_spec
+  {α β γ : Type}
+  {post : β → Prop} {epost : VCGen.EPred}
+  {body : α → Result (ControlFlow α β)} {init : α}
+  (inv : α → Prop)
+  (rel : γ → γ → Prop)
+  (termination : α → γ)
+  (hwf : WellFounded rel)
+  (h_inv_init : inv init)
+  (h_body : ∀ x, inv x → (True : Prop) ⊑ wp (body x)
+    (fun cf => match cf with
+      | .cont r => inv r ∧ (rel (termination r) (termination x) ∨ VCGen.willDiverge epost)
+      | .done r => post r) epost) :
+  (True : Prop) ⊑ wp (loop body init) post epost := by
+  suffices h : ∀ x, inv x → wp (loop body x) post epost by
+    exact fun _ => h init h_inv_init
+  by_cases hdiv : VCGen.willDiverge epost
+  case pos => -- Divergence permitted: use partial-fixpoint induction.
+    intro x hinv
+    delta loop
+    refine Lean.Order.fix_induct (loop._proof_1 body)
+      (motive := fun g => ∀ x, inv x → wp (g x) post epost) ?_ ?_ x hinv
+    · apply Lean.Order.admissible_pi
+      intro y
+      apply Lean.Order.admissible_pi
+      intro _
+      apply Lean.Order.admissible_apply (β := fun _ => Result β)
+        (P := fun _ r => wp r post epost) y
+      exact Lean.Order.admissible_flatOrder _ hdiv
+    · intro g IH y hinvy
+      simp only []
+      have hb := h_body y hinvy trivial
+      cases hbe : body y with
+      | ok cf =>
+        rw [hbe] at hb
+        cases cf with
+        | cont r => exact IH r hb.1
+        | done r => exact hb
+      | fail e => rw [hbe] at hb; exact hb
+      | div => rw [hbe] at hb; exact hb
+  case neg => -- Divergence forbidden: termination via WF induction on `rel`.
+    intro x hinv
+    induction hg : termination x using hwf.induction generalizing x
+    rename_i g IH
+    have hb := h_body x hinv trivial
+    rw [loop.eq_1]
+    cases hbe : body x with
+    | ok cf =>
+      rw [hbe] at hb
+      cases cf with
+      | cont r =>
+        obtain ⟨hinvr, hrel | hd⟩ := hb
+        · subst hg
+          exact IH (termination r) hrel r hinvr rfl
+        · exact absurd hd hdiv
+      | done r => exact hb
+    | fail e => rw [hbe] at hb; exact hb
+    | div => rw [hbe] at hb; exact hb
+
+end
+
 end Aeneas.Std
 
 namespace Aeneas.Std.WP
@@ -991,6 +1153,7 @@ theorem forall_unit {p : Prop} : (Unit → p) ↔ p := by simp
       ``Std.WP.imp_exists_iff,
       ``forall_unit, ``true_imp_iff]
     to_mvcgen := .some ``Std.WP.spec_to_mvcgen
+    to_vcgen := .some ``Std.WP.spec_to_vcgen
     liftings := #[]
   }
 
@@ -1015,6 +1178,7 @@ theorem forall_unit {p : Prop} : (Unit → p) ↔ p := by simp
       ``Std.WP.imp_exists_iff,
       ``forall_unit, ``true_imp_iff]
     to_mvcgen := .some ``Std.WP.dspec_to_mvcgen
+    to_vcgen := .some ``Std.WP.dspec_to_vcgen
     liftings := #[
       { from_statement := ``Std.WP.spec
         conversion_thm := ``Std.WP.spec_dspec
diff --git a/backends/lean/Aeneas/Tactic/Simproc/ReduceZMod/ReduceZMod.lean b/backends/lean/Aeneas/Tactic/Simproc/ReduceZMod/ReduceZMod.lean
index 4e63f80b2..e19f8564c 100644
--- a/backends/lean/Aeneas/Tactic/Simproc/ReduceZMod/ReduceZMod.lean
+++ b/backends/lean/Aeneas/Tactic/Simproc/ReduceZMod/ReduceZMod.lean
@@ -80,10 +80,11 @@ simproc reduceZModInv (@Inv.inv _ (ZMod.instInv _) _) := fun e => do
 simproc reduceZModPow
   (@HPow.hPow _ Nat _
       (@instHPow _ Nat
-        (@Monoid.toPow _
-          (@MonoidWithZero.toMonoid _
-            (@Semiring.toMonoidWithZero _
-              (@CommSemiring.toSemiring _ (@CommRing.toCommSemiring _ (ZMod.commRing _)))))))
+        (@NPow.toPow _
+          (@Monoid.toNPow _
+            (@MonoidWithZero.toMonoid _
+              (@Semiring.toMonoidWithZero _
+                (@CommSemiring.toSemiring _ (@CommRing.toCommSemiring _ (ZMod.commRing _))))))))
       _ _) := fun e => do
   trace[ReduceZMod] "Visiting: {e}"
   match e.consumeMData.getAppFnArgs with
diff --git a/backends/lean/Aeneas/Tactic/Solver/BvTac/BvTac.lean b/backends/lean/Aeneas/Tactic/Solver/BvTac/BvTac.lean
index 65d1fca39..b9719b36c 100644
--- a/backends/lean/Aeneas/Tactic/Solver/BvTac/BvTac.lean
+++ b/backends/lean/Aeneas/Tactic/Solver/BvTac/BvTac.lean
@@ -7,7 +7,7 @@ namespace Aeneas.BvTac
 open Lean Lean.Meta Lean.Parser.Tactic Lean.Elab.Tactic
 open Bvify Utils
 
-structure Config extends Lean.Elab.Tactic.BVDecide.Frontend.BVDecideConfig, Bvify.Config where
+structure Config extends Lean.Elab.Tactic.BVDecide.BVDecideConfig, Bvify.Config where
 
 declare_config_elab elabConfig Config
 
@@ -79,7 +79,7 @@ partial def bvTacPreprocess (config : Config) (n : Option Expr): TacticM Unit :=
 elab "bv_tac_preprocess" config:Parser.Tactic.optConfig n:(colGt term)? : tactic => do
   bvTacPreprocess (← elabConfig config) (← optElabTerm n)
 
-open Lean.Elab.Tactic.BVDecide.Frontend Lean.Elab in
+open Lean.Meta.Tactic.BVDecide Lean.Elab in
 /-- `bv_tac n` solves goals about bit-vectors.
 
 **Usage**: `bv_tac n` where `n` is the bitwidth to use for the bit-vectors.
@@ -118,9 +118,9 @@ elab "bv_tac" config:Parser.Tactic.optConfig n:(colGt term)? : tactic =>
   -- Call bv_decide
   IO.FS.withTempFile fun _ lratFile => do
     let config := config.toBVDecideConfig
-    let cfg ← BVDecide.Frontend.TacticContext.new lratFile config
+    let cfg ← Lean.Meta.Tactic.BVDecide.TacticContext.new lratFile config
     liftMetaFinishingTactic fun g => do
-      discard <| bvDecide g cfg
+      discard <| Lean.Meta.Tactic.BVDecide.bvDecide g cfg
 
 /-!
 # Tests
diff --git a/backends/lean/Aeneas/Tactic/Step/DspecInduction.lean b/backends/lean/Aeneas/Tactic/Step/DspecInduction.lean
index 25ee63dd1..f91d2d1a3 100644
--- a/backends/lean/Aeneas/Tactic/Step/DspecInduction.lean
+++ b/backends/lean/Aeneas/Tactic/Step/DspecInduction.lean
@@ -94,7 +94,7 @@ theorem WP_func_admissible (α β : Type) (arg) (post)
   : Order.admissible fun (f : α → Result β) => WP.dspec (f arg) post := by
   apply Lean.Order.admissible_apply (fun _ fx => WP.dspec fx _)
   apply Lean.Order.admissible_flatOrder
-  simp only [WP.dspec]
+  simp only [WP.dspec, Lean.Order.FlatOrder.mk]
 
 def getParamNames (ty : Expr) : MetaM (Array Name) := do
   forallTelescope ty fun xs _ => do
diff --git a/backends/lean/Aeneas/Tactic/Step/Init.lean b/backends/lean/Aeneas/Tactic/Step/Init.lean
index 5b0fd16fe..d227b6abf 100644
--- a/backends/lean/Aeneas/Tactic/Step/Init.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Init.lean
@@ -571,11 +571,112 @@ private def saveMvcgenPartialSpecFromThm (stx : Syntax) (attrKind : AttributeKin
     let thmTy ← inferType proofTerm
     saveMvcgenDecl attrKind stx thDecl thmTy proofTerm
 
+/-! ## Convert a spec theorem into a spec theorem for `vcgen`
+
+`vcgen` is the successor of `mvcgen`; it is built on the `Std.Internal.Do` metatheory rather than
+on `Std.Do`, so it needs its own spec theorems. They are shaped as entailments
+`pre ⊑ Std.Internal.Do.wp prog post epost`, which `vcgen` accepts alongside
+`Std.Internal.Do.Triple`s and which — unlike `Triple` — do not force the result type into the
+same universe as the assertion language (see the comment in `Aeneas/Std/WP.lean`).
+
+The processing mirrors the `mvcgen` case above: `spec`/`dspec` theorems go through the
+`to_vcgen` conversion lemma registered with `#register_spec_info`, and `partialSpec` theorems go
+through `partialSpec_to_vcgen` plus a simplification pass on the generated side conditions.
+-/
+
+private def saveVcgenDecl (attrKind : AttributeKind) (stx : Syntax)
+    (originalThDecl : AsyncConstantInfo) (thmTy proofTerm : Expr) : MetaM Unit := do
+  let vcgenSpecName := Name.str originalThDecl.name "vcgen_spec"
+  let auxDecl : TheoremVal := {
+    name        := vcgenSpecName
+    levelParams := originalThDecl.sig.get.levelParams
+    type        := thmTy
+    value       := proofTerm
+  }
+  addDecl (.thmDecl auxDecl)
+  addDeclarationRangesFromSyntax vcgenSpecName stx
+  -- Register with @[spec] so vcgen can find it. The `spec` attribute dispatches on the shape of
+  -- the statement, so it lands in the `Std.Internal.Do` spec database used by `vcgen`.
+  Lean.Attribute.add vcgenSpecName `spec .missing attrKind
+  trace[Step] "Registered {vcgenSpecName} as `@[spec]`."
+
+/-- Register a theorem using `spec` (or `dspec`) with `vcgen`. -/
+private def saveVcgenSpecFromThm (stx : Syntax) (attrKind : AttributeKind)
+    (thDecl : AsyncConstantInfo) (ty : Expr) : MetaM Unit := do
+  trace[Step] "saveVcgenSpecFromThm: {thDecl.name}"
+  let (_, info) ← getStepSpecFunArgsExpr ty
+  let some to_vcgen := info.to_vcgen
+    | trace[Step] "No `to_vcgen` conversion function found: {thDecl.name}"
+      return
+  let sig := thDecl.sig.get
+  let thName := thDecl.name
+  forallTelescope sig.type fun fvars _ => do
+    let thConst := Lean.mkConst thName (sig.levelParams.map .param)
+    let thApp := mkAppN thConst fvars
+    /- Wrap with the conversion lemma to produce a `⊑ wp` statement. The lemma's trailing
+       exception-postcondition parameter is left unapplied, so it becomes a leading `∀` of the
+       generated statement and `vcgen` treats it as schematic (no exception VC). -/
+    let proof ← mkAppM to_vcgen #[thApp]
+    let innerTy ← inferType proof
+    let proofTerm ← mkLambdaFVars fvars proof
+    let thmTy ← mkForallFVars fvars innerTy
+    saveVcgenDecl attrKind stx thDecl thmTy proofTerm
+
+section
+open Aeneas.Std WP Result
+
+private theorem vcgen_fail_failEq_iff {epost : VCGen.EPred} {c : Error} {P : Prop} :
+    (∀ e, (e = c ∧ P) → VCGen.willFail e epost) ↔ (P → VCGen.willFail c epost) :=
+  ⟨fun h hP => h c ⟨rfl, hP⟩, fun h _ ⟨he, hP⟩ => he ▸ h hP⟩
+
+private theorem vcgen_fail_False_iff {epost : VCGen.EPred} :
+    (∀ e, False → VCGen.willFail e epost) ↔ True :=
+  ⟨fun _ => trivial, fun _ _ h => h.elim⟩
+
+end
+
+/-- Try to simplify the arguments produced by `partialSpec_to_vcgen`. -/
+private def simplifyVcgenHypotheses (mvarOk mvarFail mvarDiv : Expr) : MetaM Unit := do
+  let simpCtx ← mkSimpOnlyContext (#[
+      ``vcgen_fail_failEq_iff, ``vcgen_fail_False_iff,
+      ``mvcgen_uncurry', ``false_imp_iff, ``and_imp, ``forall_eq] ++ commonSimpLemmas)
+  let simplify (mv : Expr) (name : String) : MetaM Unit := do
+    trace[Step] "simplifyVcgenHypotheses: {name} type: {← inferType mv}"
+    try
+      let (mvarId?, _) ← simpTarget mv.mvarId! simpCtx (simprocs := {})
+      if let some mvarId := mvarId? then
+        discard <| splitAndGoals mvarId
+    catch e => trace[Step] "simplifyVcgenHypotheses: simp on {name} failed: {e.toMessageData}"
+  simplify mvarOk "hOk"
+  simplify mvarFail "hFail"
+  simplify mvarDiv "hDiv"
+
+/-- Register a theorem using `partialSpec` with `vcgen`. -/
+private def saveVcgenPartialSpecFromThm (stx : Syntax) (attrKind : AttributeKind)
+    (thDecl : AsyncConstantInfo) : MetaM Unit := do
+  trace[Step] "saveVcgenPartialSpecFromThm: {thDecl.name}"
+  let sig := thDecl.sig.get
+  let thName := thDecl.name
+  forallTelescope sig.type fun fvars _ => do
+    let thConst := Lean.mkConst thName (sig.levelParams.map .param)
+    let thApp ← canonicalizeFailPostcond (mkAppN thConst fvars)
+    let bridge ← mkAppOptM ``Aeneas.Std.WP.partialSpec_to_vcgen
+      #[none, none, none, none, none, some thApp]
+    let (extraMVars, _, _) ← forallMetaTelescope (← inferType bridge)
+    unless extraMVars.size = 5 do
+      throwError "partialSpec_to_vcgen: expected 5 extra arguments, got {extraMVars.size}"
+    simplifyVcgenHypotheses extraMVars[2]! extraMVars[3]! extraMVars[4]!
+    let proof := mkAppN bridge extraMVars
+    let { expr := proofAbstracted, .. } ← abstractMVars proof
+    let proofTerm ← mkLambdaFVars fvars proofAbstracted
+    let thmTy ← inferType proofTerm
+    saveVcgenDecl attrKind stx thDecl thmTy proofTerm
+
 /-! ## Applying the @[step] attribute
 
-When the `@[step]` attribute is attached to a lemma, we register this lemma both with the `step`
-tactic and with the `mvcgen` tactic. Depending whether the lemma uses the `partialSpec` predicate
-or one of the `step`-internal predicates `spec` and `dspec`, we need to apply different
+When the `@[step]` attribute is attached to a lemma, we register this lemma with the `step` tactic
+and with the `mvcgen` and `vcgen` tactics. Depending whether the lemma uses the `partialSpec`
+predicate or one of the `step`-internal predicates `spec` and `dspec`, we need to apply different
 preprocessing before registering the lemmas.
 -/
 
@@ -586,7 +687,7 @@ def isPartialSpec (ty : Expr) : MetaM Bool := do
   let (spec?, args) := ty₂.consumeMData.withApp (fun f args => (f, args))
   pure (spec?.isConstOf ``Std.WP.partialSpec ∧ args.size = 5)
 
-/-- Register a theorem (either `spec` or `partialSpec`) with `step` and `mvcgen`. -/
+/-- Register a theorem (either `spec` or `partialSpec`) with `step`, `mvcgen` and `vcgen`. -/
 private def applyStepAttr (ext : Extension) (attrKind : AttributeKind) (stx : Syntax)
     (thName : Name) : AttrM Unit := do
   -- Ignore some auxiliary definitions (see the comments for attrIgnoreMutRec)
@@ -605,11 +706,15 @@ private def applyStepAttr (ext : Extension) (attrKind : AttributeKind) (stx : Sy
         catch e => logWarning m!"Could not generate step spec for {thName}: {e.toMessageData}"
         try saveMvcgenPartialSpecFromThm stx attrKind thDecl
         catch e => logWarning m!"Could not generate mvcgen spec for {thName}: {e.toMessageData}"
+        try saveVcgenPartialSpecFromThm stx attrKind thDecl
+        catch e => logWarning m!"Could not generate vcgen spec for {thName}: {e.toMessageData}"
       else
         try saveStepSpecFromThm ext attrKind thName ty
         catch e => logWarning m!"Could not save step spec for {thName}: {e.toMessageData}"
         try saveMvcgenSpecFromThm stx attrKind thDecl ty
         catch e => logWarning m!"Could not generate mvcgen spec for {thName}: {e.toMessageData}"
+        try saveVcgenSpecFromThm stx attrKind thDecl ty
+        catch e => logWarning m!"Could not generate vcgen spec for {thName}: {e.toMessageData}"
 
 /-- Initialize the `step` attribute. -/
 initialize stepAttr : StepSpecAttr ← do
@@ -741,7 +846,8 @@ theorem intro_uncurry' (p : α × β → Prop) : p = uncurry' (fun x y => p (x,
   simp only
 
 theorem lift_to_spec x (p0 p1 : α → Prop) (h0 : p0 x) (h1 : p0 = p1) : spec (Std.lift x) p1 := by
-  grind [spec, Std.lift]
+  simp only [Std.lift, spec_ok, ← h1]
+  exact h0
 
 namespace Test
 
diff --git a/backends/lean/Aeneas/Tactic/Step/Step.lean b/backends/lean/Aeneas/Tactic/Step/Step.lean
index 3abf08fd6..48afa17b9 100644
--- a/backends/lean/Aeneas/Tactic/Step/Step.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Step.lean
@@ -1022,11 +1022,10 @@ def tryApply (info : SpecInfo) (lifting : Option LiftingInfo) (args : Args) (isL
     | some th => do
       trace[Step] "Lookuped up {kind}: {th}"
       -- Apply the theorem
-      let res ← do
-        try
-          let res ← stepWith info lifting args isLet fExpr th
-          pure (some res)
-        catch _ => pure none
+      try
+        let res ← stepWith info lifting args isLet fExpr th
+        pure (some res)
+      catch _ => pure none
   match res with
   | some res => pure (some res)
   | none => pure none
@@ -2069,7 +2068,7 @@ h1 : ∀ (i : ℕ) (x : i < s.length), s'[i] = 0#u32
 
   -- `Inhabited α` is not necessary: we add it for the purpose of testing
   theorem get_spec {α} [Inhabited α] (x : Option α) (h : x.isSome) : get x ⦃ _ => True ⦄ := by
-    cases x <;> grind [get]
+    cases x <;> simp_all [get]
 
   example {α} [Inhabited α] (x : Option α) (h : x.isSome) : get x ⦃ _ => True ⦄ := by
     step with get_spec
@@ -2173,7 +2172,7 @@ h1 : ∀ (i : ℕ) (x : i < s.length), s'[i] = 0#u32
         intros y
         apply Lean.Order.admissible_apply (fun _ fx => WP.dspec fx _)
         apply Lean.Order.admissible_flatOrder
-        simp only [WP.dspec]
+        simp only [WP.dspec, Lean.Order.FlatOrder.mk]
       · intros
         simp only
         split
diff --git a/backends/lean/Aeneas/Tactic/Step/StepArraySpec.lean b/backends/lean/Aeneas/Tactic/Step/StepArraySpec.lean
index 715196f73..e653d60e3 100644
--- a/backends/lean/Aeneas/Tactic/Step/StepArraySpec.lean
+++ b/backends/lean/Aeneas/Tactic/Step/StepArraySpec.lean
@@ -107,7 +107,7 @@ def parseStepArraySpec
   match stx with
   | `($[$vis]? step_array_spec (name := $thm_name:ident) $array:ident [ $i:ident ]! { $x:ident => $pred:term } by $tac:tacticSeq) => do
     -- Compute the visibility of the `step` theorem
-    let vis : TSyntax `declModifiers ← do
+    let vis : TSyntax `Lean.Parser.Command.declModifiers ← do
       match vis with
       | none => `(declModifiers|@[step])
       | some vis =>
diff --git a/backends/lean/Aeneas/Tactic/Step/StepStar.lean b/backends/lean/Aeneas/Tactic/Step/StepStar.lean
index bfbfd9312..c7eb4afd7 100644
--- a/backends/lean/Aeneas/Tactic/Step/StepStar.lean
+++ b/backends/lean/Aeneas/Tactic/Step/StepStar.lean
@@ -463,7 +463,7 @@ where
       {simpThms := #[← Step.stepSimpExt.getTheorems]}
       (.targets #[] true)
     /- We may have proven the goal already -/
-    let tac : Array Syntax.Tactic ← do
+    let tac : Array (TaskOrDone (Option Syntax.Tactic)) ← do
       let genSimp : Bool ← do
         if r.isNone then pure true
         else do
diff --git a/backends/lean/Aeneas/Tactic/Step/Tests.lean b/backends/lean/Aeneas/Tactic/Step/Tests.lean
index 3571ccb43..1494a3f7e 100644
--- a/backends/lean/Aeneas/Tactic/Step/Tests.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Tests.lean
@@ -5,5 +5,5 @@ import Aeneas.Tactic.Step.Tests.MvcgenSpec
 import Aeneas.Tactic.Step.Tests.SpecParameters
 import Aeneas.Tactic.Step.Tests.TupleDestruct
 import Aeneas.Tactic.Step.Tests.UncurryBind
-import Aeneas.Tactic.Step.Tests.MvcgenSpec
 import Aeneas.Tactic.Step.Tests.SpecPartial
+import Aeneas.Tactic.Step.Tests.VcgenSpec
diff --git a/backends/lean/Aeneas/Tactic/Step/Tests/SpecPartial.lean b/backends/lean/Aeneas/Tactic/Step/Tests/SpecPartial.lean
index 91abc0c64..7417bd9dd 100644
--- a/backends/lean/Aeneas/Tactic/Step/Tests/SpecPartial.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Tests/SpecPartial.lean
@@ -4,8 +4,8 @@ import Aeneas.Tactic.Step
 /-!
 # Tests: `@[step]` accepts `partialSpec` lemmas
 
-For a theorem using `partialSpec`, marking it with `@[step]` should register it for `step*` and
-for `mvcgen`.
+For a theorem using `partialSpec`, marking it with `@[step]` should register it for `step*`, for
+`mvcgen` and for `vcgen`.
 -/
 
 namespace Aeneas.Step.SpecPartialTests
@@ -134,4 +134,59 @@ info: Aeneas.Step.SpecPartialTests.infiniteLoop_partialSpec.mvcgen_spec (Q : Pos
 #guard_msgs in
 #check infiniteLoop_partialSpec.mvcgen_spec
 
+/-! ## `vcgen`
+
+The `vcgen` counterparts of the generated `mvcgen` specs above. `vcgen` specs are stated as
+entailments `pre ⊑ Std.Internal.Do.wp prog post epost` (see `Aeneas/Std/WP.lean`). -/
+
+section
+open Std.Internal.Do Lean.Order
+
+/-- vcgen: total correctness -/
+example (x y : U32) (h : y.val ≠ 0) :
+    Triple (myDiv x y) True (fun z => z.val = x.val / y.val) (⊥ : VCGen.EPred) := by
+  vcgen <;> simp_all
+
+/-- vcgen: partial correctness (failure is allowed by the exception postcondition) -/
+example (x y : U32) :
+    Triple (myDiv x y) True (fun z => z.val = x.val / y.val) epost⟨fun _ => True, True⟩ := by
+  vcgen <;> simp_all
+
+/--
+info: Aeneas.Step.SpecPartialTests.myDiv_partialSpec.vcgen_spec (x y : U32) (post : U32 → Prop) (epost : VCGen.EPred)
+  (h_ok : ∀ (r : U32), ↑r = ↑x / ↑y → post r) (h_fail : ∀ (e : Error), ↑y = 0 → VCGen.willFail e epost) :
+  True ⊑ Std.Internal.Do.wp (myDiv x y) post epost
+-/
+#guard_msgs in
+#check myDiv_partialSpec.vcgen_spec
+
+-- Pushing `¬` through `>` should produce `≤`, exactly as for the `mvcgen` spec.
+/--
+info: Aeneas.Step.SpecPartialTests.myAdd_partialSpec.vcgen_spec (x y : U32) (post : U32 → Prop) (epost : VCGen.EPred)
+  (h_ok : ∀ (r : U32), ↑r = ↑x + ↑y → post r)
+  (h_fail : U32.max < ↑x + ↑y → VCGen.willFail Error.integerOverflow epost) :
+  True ⊑ Std.Internal.Do.wp (myAdd x y) post epost
+-/
+#guard_msgs in
+#check myAdd_partialSpec.vcgen_spec
+
+/--
+info: Aeneas.Step.SpecPartialTests.myAddSigned_partialSpec.vcgen_spec (x y : I32) (post : I32 → Prop) (epost : VCGen.EPred)
+  (h_ok : ∀ (r : I32), ↑r = ↑x + ↑y → post r)
+  (h_fail_1 : I32.max < ↑x + ↑y → VCGen.willFail Error.integerOverflow epost)
+  (h_fail_2 : ↑x + ↑y < I32.min → VCGen.willFail Error.integerOverflow epost) :
+  True ⊑ Std.Internal.Do.wp (myAddSigned x y) post epost
+-/
+#guard_msgs in
+#check myAddSigned_partialSpec.vcgen_spec
+
+/--
+info: Aeneas.Step.SpecPartialTests.infiniteLoop_partialSpec.vcgen_spec (post : Unit → Prop) (epost : VCGen.EPred)
+  (h_div : VCGen.willDiverge epost) : True ⊑ Std.Internal.Do.wp infiniteLoop post epost
+-/
+#guard_msgs in
+#check infiniteLoop_partialSpec.vcgen_spec
+
+end
+
 end Aeneas.Step.SpecPartialTests
diff --git a/backends/lean/Aeneas/Tactic/Step/Tests/TupleDestruct.lean b/backends/lean/Aeneas/Tactic/Step/Tests/TupleDestruct.lean
index c2fe9364b..f483a0a20 100644
--- a/backends/lean/Aeneas/Tactic/Step/Tests/TupleDestruct.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Tests/TupleDestruct.lean
@@ -35,49 +35,57 @@ private theorem sixNats_spec : sixNats ⦃ ((a, b), c) ((d, e), f) => a = 3 ∧
 /--
 warning: Variable name `a` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _a
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `b` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _b
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `c` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _c
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `d` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _d
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `b` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _b
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `c` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _c
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `e` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _e
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `h` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _h
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 -/
diff --git a/backends/lean/Aeneas/Tactic/Step/Tests/VcgenSpec.lean b/backends/lean/Aeneas/Tactic/Step/Tests/VcgenSpec.lean
new file mode 100644
index 000000000..da534b442
--- /dev/null
+++ b/backends/lean/Aeneas/Tactic/Step/Tests/VcgenSpec.lean
@@ -0,0 +1,128 @@
+import Aeneas.Std.Scalar
+import Aeneas.Std.Array
+import Aeneas.Tactic.Step
+
+open Aeneas Aeneas.Std Result
+open Std.Internal.Do Lean.Order
+
+set_option mvcgen.warning false
+
+/-!
+# Tests: `vcgen` spec generation from `@[step]`
+
+For every `@[step]` theorem, the attribute handler also generates a `vcgen` spec (in addition to
+the `mvcgen` one, see `MvcgenSpec.lean`). The first three tests below are the `vcgen`
+counterparts of the `mvcgen` tests.
+
+Note that we spell the goals as `Std.Internal.Do.Triple` applications rather than with the
+`⦃ _ ⦄ _ ⦃ _ ⦄` notation: that notation clashes with Aeneas' own postfix `⦃ _ ⦄` notation for
+`spec`, which would swallow the postcondition.
+-/
+
+namespace Aeneas.Step.VcgenSpecTests
+
+example {x y : U8} (hmax : x.val + y.val ≤ U8.max) :
+    Triple (x + y) True (fun z => z.val = x.val + y.val) (⊥ : VCGen.EPred) := by
+  vcgen <;> scalar_tac
+
+example {x y : U8} :
+    Triple
+      ((do
+        if x < 10#u8
+        then x * 2#u8
+        else pure y : Result U8))
+      True (fun z => z.val ≠ y.val → z.val < 20) (⊥ : VCGen.EPred) := by
+  vcgen <;> scalar_tac
+
+example (arr : Array U8 25#usize) (i : Usize) (a : U8) (hi : i < arr.length) :
+    Triple (Array.update arr i a) True (fun r => r.get? i = some a) (⊥ : VCGen.EPred) := by
+  vcgen <;> grind
+
+/-! ## Tuple-destructuring binds
+
+`let (x, y) ← e` elaborates to a bind whose continuation is wrapped in `Std.uncurry`;
+`Std.WP.uncurry_vcgen_spec` lets `vcgen` see through it. -/
+
+example {α : Type} (v : Slice α) (i : Usize) (h : i.val < v.length) :
+    Triple
+      ((do
+        let (x, back) ← v.index_mut_usize i
+        pure (back x) : Result (Slice α)))
+      True (fun r => r = v.set i v.val[i.val]) (⊥ : VCGen.EPred) := by
+  vcgen <;> simp_all [WP.uncurry'_eq]
+
+/-! ## Generated specs
+
+`@[step]` generates a `vcgen` spec for `spec` and `dspec` theorems too (through the `to_vcgen`
+conversion lemma registered with `#register_spec_info`), not only for `partialSpec` ones (those
+are covered by `SpecPartial.lean`). A `dspec` does not rule out divergence, hence the
+`x ≠ div` precondition. -/
+
+opaque myId (x : U32) : Result U32
+
+@[step] axiom myId_spec (x : U32) : myId x ⦃ y => y = x ⦄
+
+/--
+info: Aeneas.Step.VcgenSpecTests.myId_spec.vcgen_spec (x : U32) (epost : VCGen.EPred) :
+  True ⊑ wp (myId x) (fun y => y = x) epost
+-/
+#guard_msgs in
+#check myId_spec.vcgen_spec
+
+example (x : U32) : Triple (myId x) True (fun y => y = x) (⊥ : VCGen.EPred) := by
+  vcgen
+
+opaque myMaybeLoop (x : U32) : Result U32
+
+@[step] axiom myMaybeLoop_dspec (x : U32) : WP.dspec (myMaybeLoop x) (fun y => y = x)
+
+/--
+info: Aeneas.Step.VcgenSpecTests.myMaybeLoop_dspec.vcgen_spec (x : U32) (epost : VCGen.EPred) :
+  (¬myMaybeLoop x = div) ⊑ wp (myMaybeLoop x) (fun y => y = x) epost
+-/
+#guard_msgs in
+#check myMaybeLoop_dspec.vcgen_spec
+
+example (x : U32) (h : myMaybeLoop x ≠ div) :
+    Triple (myMaybeLoop x) True (fun y => y = x) (⊥ : VCGen.EPred) := by
+  vcgen
+  simp_all
+
+/-! ## The `Result` constructors -/
+
+example {α : Type} (a : α) : Triple (Result.ok a) True (fun r => r = a) (⊥ : VCGen.EPred) := by
+  vcgen
+
+example {α : Type} (a : α) (epost : VCGen.EPred) (h : VCGen.willFail .panic epost) :
+    Triple (Result.fail .panic : Result α) True (fun r => r = a) epost := by
+  vcgen; assumption
+
+example {α : Type} (a : α) (epost : VCGen.EPred) (h : VCGen.willDiverge epost) :
+    Triple (Result.div : Result α) True (fun r => r = a) epost := by
+  vcgen; assumption
+
+/-! ## Loops
+
+`Std.loop_vcgen_spec` is the `vcgen` counterpart of `Std.loop_spec`. As for `mvcgen`, it is not
+picked up automatically (the invariant, the well-founded relation and the termination measure
+have to be supplied), so we apply it explicitly. -/
+
+/-- `count n` counts from `0` up to `n`. -/
+def count (n : Usize) : Result Usize :=
+  loop (β := Usize) (fun i =>
+    if i < n then do
+      let i' ← i + 1#usize
+      ok (ControlFlow.cont i')
+    else ok (ControlFlow.done i)) 0#usize
+
+example (n : Usize) : Triple (count n) True (fun r => r = n) (⊥ : VCGen.EPred) := by
+  unfold count
+  refine Triple.intro (Std.loop_vcgen_spec
+    (inv := fun i : Usize => i.val ≤ n.val)
+    (rel := fun (x y : Nat) => x < y)
+    (termination := fun i : Usize => n.val - i.val)
+    (hwf := Nat.lt_wfRel.wf) (h_inv_init := by scalar_tac) ?_)
+  intro i hi
+  vcgen <;> scalar_tac
+
+end Aeneas.Step.VcgenSpecTests
diff --git a/backends/lean/AeneasMeta/BvEnumToBitVec.lean b/backends/lean/AeneasMeta/BvEnumToBitVec.lean
index 2fadf4bc0..54f9d66ef 100644
--- a/backends/lean/AeneasMeta/BvEnumToBitVec.lean
+++ b/backends/lean/AeneasMeta/BvEnumToBitVec.lean
@@ -3,7 +3,7 @@ Copyright (c) 2025. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 import Lean
-import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Enums
+import Lean.Meta.Tactic.BVDecide.Normalize.Enums
 
 /-!
 # Eagerly realizing `bv_decide`'s enum conversion constants
@@ -44,7 +44,7 @@ module, turning the lazy per-use realisation into a single deterministic one.
 namespace Aeneas
 
 open Lean Meta Elab
-open Lean.Elab.Tactic.BVDecide.Frontend.Normalize
+open Lean.Meta.Tactic.BVDecide.Normalize
 
 /-- Marker class enabling `deriving BvEnumToBitVec` on an enum inductive.
 
@@ -69,11 +69,14 @@ def realizeBvEnumToBitVec (declName : Name) : CoreM Unit := do
       (parameter-free with only nullary constructors); \
       `bv_decide` only synthesises `enumToBitVec` for such types."
   enableRealizationsForConst declName
-  let act : MetaM Unit := do
-    discard <| getEnumToBitVecFor declName
-    discard <| getEnumToBitVecLeFor declName
-    discard <| getEqIffEnumToBitVecEqFor declName
-  discard <| act.run' {} {}
+  -- `bv_decide` registers these three constants as *reserved names* and realises
+  -- them lazily through a reserved-name action (see
+  -- `Lean.Meta.Tactic.BVDecide.Normalize`). The realiser functions themselves are
+  -- private to that module, so we trigger realisation by name instead. Only
+  -- `enumToBitVecSuffix` is exported; the other two suffixes are inlined here.
+  executeReservedNameAction (.str declName enumToBitVecSuffix)
+  executeReservedNameAction (.str declName "enumToBitVec_le")
+  executeReservedNameAction (.str declName "eq_iff_enumToBitVec_eq")
 
 /-- `#define_bv_decide_toBitVec T` eagerly realises `bv_decide`'s enum
 conversion constants for the enum inductive `T` in the current module.
diff --git a/backends/lean/AeneasMeta/Simp/Simp.lean b/backends/lean/AeneasMeta/Simp/Simp.lean
index 322ea73a5..455376f48 100644
--- a/backends/lean/AeneasMeta/Simp/Simp.lean
+++ b/backends/lean/AeneasMeta/Simp/Simp.lean
@@ -116,7 +116,7 @@ where
     let freshFVarIds ←
       match result? with
       | none => replaceMainGoal []; pure none
-      | some (fvars, mvarId) => replaceMainGoal [mvarId]; pure fvars
+      | some (fvars, mvarId) => replaceMainGoal [mvarId]; pure (some fvars)
     /- We need to filter the `fvarIdsToSimp` to remove those which have been replaced with fresh fvars -/
     let fvars ← do
       match freshFVarIds with
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index 276c521fe..033e1f3d4 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
+   "rev": "51e6992efd06126df61a496bebf8f49482a4e129",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.33.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "rev": "123d15766ba49356c02ebad2a4462dfe12d79899",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
+   "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
+   "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
+   "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
+   "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
+   "rev": "1319485273bf87833fa472afbcefdedecb16b45f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.33.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "aeneas",
diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean
index bc2d29015..d8b44fb33 100644
--- a/backends/lean/lakefile.lean
+++ b/backends/lean/lakefile.lean
@@ -3,11 +3,22 @@ open Lake DSL
 
 -- Important: mathlib imports std4 and quote4: we mustn't add a `require std4` line
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.31.0"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.33.0-rc2"
 
 package «aeneas» where
   preferReleaseBuild := true
   buildArchive := s!"lean-build-aeneas-{System.Platform.target}.tar.gz"
+  -- Lean v4.33 newly enables/strengthens these linters. They fire on generated
+  -- Rust-path declaration names (`dupNamespace`, e.g. `core.clone…​.clone`),
+  -- intentional `Prop`-valued definitions (`defProp`), and `open Std` now that
+  -- `Lean.Std` also exists (`ambiguousOpen`). None are cleanly fixable in the
+  -- generated / spec code, so we disable them to keep `lake build --iofail`
+  -- (used in CI) green after the toolchain bump.
+  leanOptions := #[
+    ⟨`weak.linter.dupNamespace, false⟩,
+    ⟨`weak.linter.defProp, false⟩,
+    ⟨`weak.linter.ambiguousOpen, false⟩
+  ]
 
 @[default_target] lean_lib «Aeneas» {}
 
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index 18640c8b0..c084c7fbe 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.33.0-rc2
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index c63c42845..31b9e8591 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -1000,7 +1000,7 @@ theorem get_mut_spec {α} (hm : HashMap α) (key : Usize) (hInv : hm.inv) :
     -- TODO: tactic to automate this
     have hSlotsEq :
       hm.slots.set hash_mod ((hm.slots.val)[(key.val % (hm.slots.val).length)]) = hm.slots := by
-      simp_all [alloc.vec.Vec.set]
+      apply Subtype.ext; simp_all [alloc.vec.Vec.set]
     simp_all
   · grind
 
diff --git a/tests/lean/Tutorial/Exercises.lean b/tests/lean/Tutorial/Exercises.lean
index 492a8dc47..42b1f3316 100644
--- a/tests/lean/Tutorial/Exercises.lean
+++ b/tests/lean/Tutorial/Exercises.lean
@@ -1,8 +1,12 @@
 import Aeneas
 open Aeneas Std Result
 
+-- Workaround for leanprover/lean4#14521: the default `get_elem_tactic` (`grind`)
+-- emits kernel-invalid proofs when an index bound depends on `_ ≠ 0#uN` (the
+-- BitVec width `numBits U32` is defeq but not syntactically `32`). `scalar_tac`
+-- discharges these bounds correctly; `grind` stays as a fallback.
 local macro_rules
-| `(tactic| get_elem_tactic) => `(tactic| grind)
+| `(tactic| get_elem_tactic) => `(tactic| first | scalar_tac | grind)
 
 set_option maxHeartbeats 1000000
 
diff --git a/tests/lean/Tutorial/Solutions.lean b/tests/lean/Tutorial/Solutions.lean
index 14571b756..dead789f7 100644
--- a/tests/lean/Tutorial/Solutions.lean
+++ b/tests/lean/Tutorial/Solutions.lean
@@ -2,8 +2,12 @@ import Aeneas
 import Tutorial.Tutorial
 open Aeneas Std Result
 
+-- Workaround for leanprover/lean4#14521: the default `get_elem_tactic` (`grind`)
+-- emits kernel-invalid proofs when an index bound depends on `_ ≠ 0#uN` (the
+-- BitVec width `numBits U32` is defeq but not syntactically `32`). `scalar_tac`
+-- discharges these bounds correctly; `grind` stays as a fallback.
 local macro_rules
-| `(tactic| get_elem_tactic) => `(tactic| grind)
+| `(tactic| get_elem_tactic) => `(tactic| first | scalar_tac | grind)
 
 set_option maxHeartbeats 1000000
 
@@ -135,10 +139,30 @@ theorem list_nth_mut1_spec'' {T: Type} [Inhabited T] (l : CList T) (i : U32)
   unfold list_nth_mut1 list_nth_mut1_loop
   /- `step*` repeatedly applies `step`, while doing a case disjunction whenever it
       encounters a branching. Note that one can automatically generate the corresponding
-      proof script by using `step*?`. -/
-  step*
-  simp
-  simp_lists [*]
+      proof script by using `step*?`.
+
+      Workaround for leanprover/lean4#14521: `step*` closes leaf goals with `agrind`,
+      which on the `i ≠ 0#u32` branch here emits a kernel-invalid proof (the BitVec
+      width `numBits U32` is defeq but not syntactically `32`). Until that upstream
+      `grind` bug is fixed, we spell out the case analysis explicitly (as `step*?`
+      would generate it), closing the branches with `scalar_tac`/`simp` instead. -/
+  split
+  · rename_i hd tl
+    split
+    · simp
+      split_conjs
+      · simp_all
+      · intro x
+        simp_all
+    · simp at *
+      step as ⟨ i1, _, hi ⟩
+      step as ⟨ tl1, back ⟩
+      simp
+      split_conjs
+      · simp_lists [*]
+      · intro x'
+        simp [*]
+  · simp at h
 
 /-- Theorem about `list_tail_loop`: verbose version -/
 @[step]
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
index 316a46c9a..4788db62e 100644
--- a/tests/lean/lake-manifest.json
+++ b/tests/lean/lake-manifest.json
@@ -12,17 +12,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
+   "rev": "51e6992efd06126df61a496bebf8f49482a4e129",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.33.0-rc2",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "rev": "123d15766ba49356c02ebad2a4462dfe12d79899",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -32,7 +32,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -42,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
+   "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -52,7 +52,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
+   "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -62,7 +62,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
+   "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -72,7 +72,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
+   "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -82,7 +82,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -92,10 +92,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
+   "rev": "1319485273bf87833fa472afbcefdedecb16b45f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.33.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "tests",
diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain
index 18640c8b0..c084c7fbe 100644
--- a/tests/lean/lean-toolchain
+++ b/tests/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.33.0-rc2