diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 777c7e000..91554d29e 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -40,36 +40,44 @@ jobs:
   build:
     name: Build (${{ matrix.artifact_name }})
     needs: prepare
-    runs-on: ${{ matrix.os }}
+    # The self-hosted runner only exists on aeneasverif/aeneas. On forks (and
+    # any other repo), fall back to the GitHub-hosted `matrix.os` runner.
+    runs-on: ${{ (matrix.self_hosted && github.repository == 'aeneasverif/aeneas') && fromJSON('["self-hosted","linux","nix"]') || matrix.os }}
     permissions:
       contents: write
       actions: write
+    env:
+      # True only when actually running on the self-hosted runner (which has
+      # nix pre-installed).
+      is_self_hosted: ${{ matrix.self_hosted && github.repository == 'aeneasverif/aeneas' }}
     strategy:
       fail-fast: false
       matrix:
         include:
-          - os: [self-hosted, linux, nix]
+          # On the main repo this runs on the self-hosted runner; on forks it
+          # falls back to `os` (see `runs-on` and `is_self_hosted` above).
+          - os: ubuntu-24.04
             artifact_name: aeneas-linux-x86_64
             nix_attr: aeneas-static-release
-            nix_machine: true
+            self_hosted: true
           - os: ubuntu-24.04-arm
             artifact_name: aeneas-linux-aarch64
             nix_attr: aeneas-static-release
-            nix_machine: false
+            self_hosted: false
           - os: macos-15-intel
             artifact_name: aeneas-macos-x86_64
             nix_attr: aeneas-release
-            nix_machine: false
+            self_hosted: false
           - os: macos-latest
             artifact_name: aeneas-macos-aarch64
             nix_attr: aeneas-release
-            nix_machine: false
+            self_hosted: false
 
     steps:
       - uses: actions/checkout@v4
 
       - name: Install nix
-        if: ${{ ! matrix.nix_machine }}
+        if: ${{ env.is_self_hosted != 'true' }}
         uses: nixbuild/nix-quick-install-action@v30
         with:
           nix_conf: |
@@ -79,7 +87,7 @@ jobs:
             extra-trusted-public-keys = hacl.cachix.org-1:FzsZ2xsByOwKwIWNPII7yMOelJNDZ12mDAj3d1eGX0c=
 
       - name: Restore Nix Cache
-        if: ${{ ! matrix.nix_machine }}
+        if: ${{ env.is_self_hosted != 'true' }}
         id: restore-nix-cache
         uses: nix-community/cache-nix-action/restore@v6
         with:
@@ -102,7 +110,7 @@ jobs:
           chmod -R +w dist_staging
 
       - name: Install elan (Lean toolchain manager)
-        if: ${{ ! matrix.nix_machine }}
+        if: ${{ env.is_self_hosted != 'true' }}
         run: |
           set -eo pipefail
 
@@ -123,7 +131,7 @@ jobs:
 
           script="$PWD/scripts/ci-precompile-lean.sh"
           cd dist_staging/backends/lean
-          if [[ "${{ matrix.nix_machine }}" == "true" ]]; then
+          if [[ "$is_self_hosted" == "true" ]]; then
             nix develop ../../.. --command "$script"
           else
             "$script"
@@ -171,7 +179,7 @@ jobs:
           files: ${{ matrix.artifact_name }}.tar.gz
 
       - name: Save Nix Cache
-        if: ${{ always() && ! matrix.nix_machine }}
+        if: ${{ always() && env.is_self_hosted != 'true' }}
         uses: nix-community/cache-nix-action/save@v6
         with:
           primary-key: ${{ steps.restore-nix-cache.outputs.primary-key }}
diff --git a/.github/workflows/select-runner.yml b/.github/workflows/select-runner.yml
index 54a4d721e..58a19ef3f 100644
--- a/.github/workflows/select-runner.yml
+++ b/.github/workflows/select-runner.yml
@@ -16,6 +16,8 @@ jobs:
       runs_on: ${{ steps.select.outputs.runs_on }}
     steps:
       - id: select
+        env:
+          current_repository: ${{ github.repository }}
         run: |
           set -euo pipefail
 
@@ -24,6 +26,14 @@ jobs:
           github_hosted='["ubuntu-latest"]'
           max_age_seconds=$((3 * 60 * 60))
 
+          # The self-hosted runner is only available on the main Aeneas repo.
+          # On forks (and any other repo), always fall back to GitHub-hosted.
+          if [ "$current_repository" != "aeneasverif/aeneas" ]; then
+            echo "::notice title=Not on aeneasverif/aeneas::Selecting GitHub-hosted runner; current repository is ${current_repository}."
+            echo "runs_on=$github_hosted" >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+
           query_error="$(mktemp)"
           if default_branch=$(curl -fsSL "https://api.github.com/repos/${heartbeat_repository}" 2>"$query_error" | jq -r .default_branch); then
             :
diff --git a/backends/lean/Aeneas/Std/Array/Array.lean b/backends/lean/Aeneas/Std/Array/Array.lean
index 32b402354..7571a44c5 100644
--- a/backends/lean/Aeneas/Std/Array/Array.lean
+++ b/backends/lean/Aeneas/Std/Array/Array.lean
@@ -116,9 +116,11 @@ theorem Array.repeat_val (n : Usize) (x : α) : (Array.repeat n x).val = List.re
   simp only [Array.repeat]
 
 @[step]
-theorem Array.index_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize)
-  (hbound : i.val < v.length) :
-  (v.index_usize i) ⦃ x => x = v.val[i.val] ⦄ := by
+theorem Array.index_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
+    partialSpec (v.index_usize i)
+      (fun x => ∃ _ : i.val < v.length, x = v.val[i.val])
+      (fun | .arrayOutOfBounds => i.val ≥ v.length | _ => False)
+      False := by
   grind [index_usize]
 
 def Array.set {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x: α) : Array α n :=
@@ -215,13 +217,14 @@ def Array.update {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x: α) :
     ok ⟨ v.val.set i.val x, by have := v.property; simp [*] ⟩
 
 @[step]
-theorem Array.update_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
-  (hbound : i.val < v.length) :
-  v.update i x ⦃ nv => nv = v.set i x ⦄
+theorem Array.update_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α) :
+    partialSpec (v.update i x)
+      (fun nv => nv = v.set i x)
+      (fun | .arrayOutOfBounds => i.val ≥ v.length | _ => False)
+      False
   := by
-  simp only [update, set]
-  simp at *
-  split <;> simp_all
+  simp only [partialSpec, update, set]
+  cases hopt : v[i]? <;> simp_all
 
 def Array.index_mut_usize {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
   Result (α × (α -> Array α n)) := do
@@ -229,12 +232,14 @@ def Array.index_mut_usize {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
   ok (x, set v i)
 
 @[step]
-theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize)
-  (hbound : i.val < v.length) :
-  v.index_mut_usize i ⦃ x back => x = v.val[i.val] ∧ back = set v i ⦄ := by
-  simp only [index_mut_usize, Bind.bind, bind]
-  have ⟨ x, h ⟩ := spec_imp_exists (index_usize_spec v i hbound)
-  simp [h]
+theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
+    partialSpec (v.index_mut_usize i)
+      (uncurry' fun x back => ∃ _ : i.val < v.length, x = v.val[i.val] ∧ back = set v i)
+      (fun | .arrayOutOfBounds => i.val ≥ v.length | _ => False)
+      False := by
+  have h := index_usize_spec v i
+  simp only [partialSpec, index_mut_usize, Bind.bind, bind, uncurry'] at h ⊢
+  cases hres : v.index_usize i <;> simp_all
 
 @[simp]
 theorem Array.set_getElem!_eq {α} {n : Usize} [Inhabited α] (x : Array α n) (i : Usize) :
diff --git a/backends/lean/Aeneas/Std/Array/ArraySlice.lean b/backends/lean/Aeneas/Std/Array/ArraySlice.lean
index 32b7f7417..5867bdcd1 100644
--- a/backends/lean/Aeneas/Std/Array/ArraySlice.lean
+++ b/backends/lean/Aeneas/Std/Array/ArraySlice.lean
@@ -54,16 +54,20 @@ def Array.subslice {α : Type u} {n : Usize} (a : Array α n) (r : Range Usize)
     fail panic
 
 @[step]
-theorem Array.subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
-  (h0 : r.start.val < r.end.val) (h1 : r.end.val ≤ a.val.length) :
-  subslice a r ⦃ s =>
-  s.val = a.val.slice r.start.val r.end.val ∧
-  (∀ i, i + r.start.val < r.end.val → s.val[i]! = a.val[r.start.val + i]!) ⦄
+theorem Array.subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) :
+    partialSpec (subslice a r)
+      (fun s =>
+        s.val = a.val.slice r.start.val r.end.val ∧
+        (∀ i, i + r.start.val < r.end.val → s.val[i]! = a.val[r.start.val + i]!))
+      (fun | .panic => ¬ (r.start.val < r.end.val ∧ r.end.val ≤ a.val.length) | _ => False)
+      False
   := by
-  simp only [subslice, true_and, h0, h1, ↓reduceIte, spec_ok, true_and]
-  intro i _
-  have := List.getElem!_slice r.start.val r.end.val i a.val (by scalar_tac)
-  simp only [this]
+  unfold subslice
+  split <;> rename_i h <;> simp [partialSpec]
+  · intro i _
+    have := List.getElem!_slice r.start.val r.end.val i a.val (by scalar_tac)
+    simp only [this]
+  · scalar_tac
 
 
 def Array.update_subslice {α : Type u} {n : Usize} (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) :=
@@ -79,17 +83,20 @@ def Array.update_subslice {α : Type u} {n : Usize} (a : Array α n) (r : Range
 -- We should introduce special symbols for the monadic arithmetic operations
 -- (the user will never write those symbols directly).
 @[step]
-theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
-  (_ : r.start.val < r.end.val) (_ : r.end.val ≤ a.length) (_ : s.length = r.end.val - r.start.val) :
-  update_subslice a r s ⦃ na =>
-  (∀ i, i < r.start.val → na[i]! = a[i]!) ∧
-  (∀ i, r.start.val ≤ i → i < r.end.val → na[i]! = s[i - r.start.val]!) ∧
-  (∀ i, r.end.val ≤ i → i < n.val → na[i]! = a[i]!) ⦄ := by
-  simp [update_subslice]
-  split
-  . simp [spec_ok]
-    simp_lists
-  . scalar_tac
+theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α) :
+    partialSpec (update_subslice a r s)
+      (fun na =>
+        (∀ i, i < r.start.val → na[i]! = a[i]!) ∧
+        (∀ i, r.start.val ≤ i → i < r.end.val → na[i]! = s[i - r.start.val]!) ∧
+        (∀ i, r.end.val ≤ i → i < n.val → na[i]! = a[i]!))
+      (fun | .panic =>
+              ¬ (r.start.val < r.end.val ∧ r.end.val ≤ a.length ∧ s.val.length = r.end.val - r.start.val)
+           | _ => False)
+      False := by
+  unfold update_subslice
+  split <;> rename_i h <;> simp [partialSpec]
+  · simp_lists
+  · scalar_tac
 
 @[rust_fun "core::array::{core::ops::index::Index<[@T; @N], @I, @O>}::index"]
 def core.array.Array.index
@@ -399,38 +406,41 @@ theorem Array.index_SliceIndexRangeUsizeSlice {T : Type} {N : Usize}
 
 @[step]
 theorem Array.index_SliceIndexRangeUsizeSlice.step {T : Type} {N : Usize} [Inhabited T]
-    (a : Array T N) (r : core.ops.range.Range Usize)
-    (h0 : r.start ≤ r.end) (h1 : r.end ≤ N) :
-    core.array.Array.index (core.ops.index.IndexSlice
-      (core.slice.index.SliceIndexRangeUsizeSlice T)) a r
-    ⦃ (s : Slice T) =>
-      s.val = a.val.slice r.start r.end ∧
-      s.length = r.end.val - r.start.val ⦄ := by
+    (a : Array T N) (r : core.ops.range.Range Usize) :
+    partialSpec
+      (core.array.Array.index (core.ops.index.IndexSlice
+        (core.slice.index.SliceIndexRangeUsizeSlice T)) a r)
+      (fun (s : Slice T) =>
+        s.val = a.val.slice r.start r.end ∧
+        s.length = r.end.val - r.start.val)
+      (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]
-  simp only [core.slice.index.SliceIndexRangeUsizeSlice.index, UScalar.le_equiv, Slice.length]
-  split
-  · simp [spec_ok, Array.to_slice]; scalar_tac
+  unfold core.slice.index.SliceIndexRangeUsizeSlice.index
+  split <;> rename_i h <;> simp [partialSpec, Array.to_slice, Slice.length]
+  · scalar_tac
   · scalar_tac
 
 @[step]
 theorem Array.index_mut_SliceIndexRangeUsizeSlice.step {T : Type} {N : Usize} [Inhabited T]
-    (a : Array T N) (r : core.ops.range.Range Usize)
-    (h0 : r.start ≤ r.end) (h1 : r.end ≤ N) :
-    core.array.Array.index_mut (core.ops.index.IndexMutSlice
-      (core.slice.index.SliceIndexRangeUsizeSlice T)) a r
-    ⦃ (s : Slice T) (back : Slice T → Array T N) =>
-      s.val = a.val.slice r.start r.end ∧
-      s.length = r.end.val - r.start.val ∧
-      ∀ s', (back s').val = a.val.setSlice! r.start.val s'.val ⦄ := by
+    (a : Array T N) (r : core.ops.range.Range Usize) :
+    partialSpec
+      (core.array.Array.index_mut (core.ops.index.IndexMutSlice
+        (core.slice.index.SliceIndexRangeUsizeSlice T)) a r)
+      (uncurry' fun (s : Slice T) (back : Slice T → Array T N) =>
+        s.val = a.val.slice r.start r.end ∧
+        s.length = r.end.val - r.start.val ∧
+        ∀ s', (back s').val = a.val.setSlice! r.start.val s'.val)
+      (fun | .panic => ¬ (r.start ≤ r.end ∧ r.end ≤ N) | _ => False)
+      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]
-  simp only [core.slice.index.SliceIndexRangeUsizeSlice.index_mut,
-    UScalar.le_equiv, Slice.length]
-  split
-  · simp [spec_ok, Array.from_slice, Array.to_slice]
-    simp_lists; scalar_tac
+  unfold core.slice.index.SliceIndexRangeUsizeSlice.index_mut
+  split <;> rename_i h <;>
+    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length]
+  · simp_lists; scalar_tac
   · scalar_tac
 
 -- Array index/index_mut with RangeTo
@@ -444,23 +454,23 @@ theorem Array.index_SliceIndexRangeToUsizeSlice {T : Type} {N : Usize}
 
 @[step]
 theorem Array.index_mut_SliceIndexRangeToUsizeSlice {T : Type} {N : Usize}
-    (a : Array T N) (r : core.ops.range.RangeTo Usize)
-    (h : r.end ≤ N) :
-    core.array.Array.index_mut (core.ops.index.IndexMutSlice
-      (core.slice.index.SliceIndexRangeToUsizeSlice T)) a r
-    ⦃ (s : Slice T) (back : Slice T → Array T N) =>
-      s.val = a.val.slice 0 r.end ∧
-      s.length = r.end.val ∧
-      ∀ s', (back s').val = a.val.setSlice! 0 s'.val ⦄ := by
+    (a : Array T N) (r : core.ops.range.RangeTo Usize) :
+    partialSpec
+      (core.array.Array.index_mut (core.ops.index.IndexMutSlice
+        (core.slice.index.SliceIndexRangeToUsizeSlice T)) a r)
+      (uncurry' fun (s : Slice T) (back : Slice T → Array T N) =>
+        s.val = a.val.slice 0 r.end ∧
+        s.length = r.end.val ∧
+        ∀ s', (back s').val = a.val.setSlice! 0 s'.val)
+      (fun | .panic => ¬ r.end ≤ N | _ => False)
+      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]
-  simp only [core.slice.index.SliceIndexRangeToUsizeSlice.index_mut,
-    show (r.end : Usize) ≤ a.to_slice.length from by scalar_tac]
-  refine ⟨?_, ?_, ?_⟩
-  · simp [Array.to_slice]
-  · simp [Slice.length]; scalar_tac
-  · intro s'; simp [Array.from_slice, Array.to_slice]
+  unfold core.slice.index.SliceIndexRangeToUsizeSlice.index_mut
+  split <;> rename_i h <;>
+    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length] <;>
+    scalar_tac
 
 -- Array index/index_mut with RangeFrom
 
@@ -473,24 +483,24 @@ theorem Array.index_SliceIndexRangeFromUsizeSlice {T : Type} {N : Usize}
 
 @[step]
 theorem Array.index_mut_SliceIndexRangeFromUsizeSlice {T : Type} {N : Usize}
-    (a : Array T N) (r : core.ops.range.RangeFrom Usize)
-    (h : r.start ≤ N) :
-    core.array.Array.index_mut (core.ops.index.IndexMutSlice
-      (core.slice.index.SliceIndexRangeFromUsizeSlice T)) a r
-    ⦃ (s : Slice T) (back : Slice T → Array T N) =>
-      s.val = a.val.drop r.start ∧
-      s.length = N.val - r.start.val ∧
-      ∀ s', (back s').val = a.val.setSlice! r.start.val s'.val ⦄ := by
+    (a : Array T N) (r : core.ops.range.RangeFrom Usize) :
+    partialSpec
+      (core.array.Array.index_mut (core.ops.index.IndexMutSlice
+        (core.slice.index.SliceIndexRangeFromUsizeSlice T)) a r)
+      (uncurry' fun (s : Slice T) (back : Slice T → Array T N) =>
+        s.val = a.val.drop r.start ∧
+        s.length = N.val - r.start.val ∧
+        ∀ s', (back s').val = a.val.setSlice! r.start.val s'.val)
+      (fun | .panic => ¬ r.start ≤ N | _ => False)
+      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]
-  simp only [core.slice.index.SliceIndexRangeFromUsizeSlice.index_mut,
-    Slice.drop,
-    show (r.start : Usize) ≤ a.to_slice.length from by scalar_tac]
-  refine ⟨?_, ?_, ?_⟩
-  · simp [Array.to_slice]
-  · simp [Slice.length, List.length_drop]
-  · intro s'; simp [Array.from_slice, Array.to_slice]
+  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];
+    scalar_tac
 
 @[reducible, rust_trait_impl "core::convert::AsRef<[@T; @N], [@T]>"]
 def Array.Insts.CoreConvertAsRefSlice (T : Type) (N : Std.Usize) :
diff --git a/backends/lean/Aeneas/Std/Scalar/Ops/Add.lean b/backends/lean/Aeneas/Std/Scalar/Ops/Add.lean
index a4e909a1c..fda4dc970 100644
--- a/backends/lean/Aeneas/Std/Scalar/Ops/Add.lean
+++ b/backends/lean/Aeneas/Std/Scalar/Ops/Add.lean
@@ -39,14 +39,14 @@ theorem UScalar.add_equiv {ty} (x y : UScalar ty) :
   | ok z => x.val + y.val < 2^ty.numBits ∧
     z.val = x.val + y.val ∧
     z.bv = x.bv + y.bv
-  | fail _ => ¬ (UScalar.inBounds ty (x.val + y.val))
+  | fail e => e = .integerOverflow ∧ ¬ (UScalar.inBounds ty (x.val + y.val))
   | _ => ⊥ := by
   have : x + y = add x y := by rfl
   rw [this]
-  simp [add]
-  have h := tryMk_eq ty (↑x + ↑y)
+  simp [add, tryMk, Result.ofOption]
+  have h := tryMkOpt_eq ty (↑x + ↑y)
   simp [inBounds] at h
-  split at h <;> simp_all
+  cases hopt : tryMkOpt ty (↑x + ↑y) <;> simp_all
   zify; simp
   zify at h
   have := @Int.emod_eq_of_lt (x.val + y.val) (2^ty.numBits) (by omega) (by omega)
@@ -58,14 +58,14 @@ theorem IScalar.add_equiv {ty} (x y : IScalar ty) :
     IScalar.inBounds ty (x.val + y.val) ∧
     z.val = x.val + y.val ∧
     z.bv = x.bv + y.bv
-  | fail _ => ¬ (IScalar.inBounds ty (x.val + y.val))
+  | fail e => e = .integerOverflow ∧ ¬ (IScalar.inBounds ty (x.val + y.val))
   | _ => ⊥ := by
   have : x + y = add x y := by rfl
   rw [this]
-  simp [add]
-  have h := tryMk_eq ty (↑x + ↑y)
+  simp [add, tryMk, Result.ofOption]
+  have h := tryMkOpt_eq ty (↑x + ↑y)
   simp [inBounds] at h
-  split at h <;> simp_all
+  cases hopt : tryMkOpt ty (↑x + ↑y) <;> simp_all
   apply BitVec.eq_of_toInt_eq
   simp
   have := bmod_pow_numBits_eq_of_lt ty (x.val + y.val) (by omega) (by omega)
@@ -111,31 +111,41 @@ only integers. Those are the most common to use, so we mark them with the
 
 /-- Generic theorem - shouldn't be used much -/
 @[step]
-theorem UScalar.add_spec {ty} {x y : UScalar ty}
-  (hmax : ↑x + ↑y ≤ UScalar.max ty) :
-  x + y ⦃ z => (↑z : Nat) = ↑x + ↑y ⦄ := by
+theorem UScalar.add_spec {ty} {x y : UScalar ty} :
+    partialSpec (x + y)
+      (fun z => (↑z : Nat) = ↑x + ↑y)
+      (fun | .integerOverflow => ↑x + ↑y > UScalar.max ty | _ => False)
+      False := by
   have h := @add_equiv ty x y
-  split at h <;> simp_all [max]
+  simp only [partialSpec]
+  split <;> simp_all [max]
   have : 0 < 2^ty.numBits := by simp
   omega
 
 /-- Generic theorem - shouldn't be used much -/
 @[step]
-theorem IScalar.add_spec {ty} {x y : IScalar ty}
-  (hmin : IScalar.min ty ≤ ↑x + ↑y)
-  (hmax : ↑x + ↑y ≤ IScalar.max ty) :
-  x + y ⦃ z => (↑z : Int) = ↑x + ↑y ⦄ := by
+theorem IScalar.add_spec {ty} {x y : IScalar ty} :
+    partialSpec (x + y)
+      (fun z => (↑z : Int) = ↑x + ↑y)
+      (fun | .integerOverflow => ↑x + ↑y < IScalar.min ty ∨ ↑x + ↑y > IScalar.max ty | _ => False)
+      False := by
   have h := @add_equiv ty x y
-  split at h <;> simp_all [min, max]
+  simp only [partialSpec]
+  split <;> simp_all [min, max, inBounds]
   omega
 
-uscalar @[step] theorem «%S».add_spec {x y : «%S»} (hmax : x.val + y.val ≤ «%S».max) :
-  x + y ⦃ z => (↑z : Nat) = ↑x + ↑y ⦄ :=
-  UScalar.add_spec (by scalar_tac)
-
-iscalar @[step] theorem «%S».add_spec {x y : «%S»}
-  (hmin : «%S».min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ «%S».max) :
-  x + y ⦃ z => (↑z : Int) = ↑x + ↑y ⦄ :=
-  IScalar.add_spec (by scalar_tac) (by scalar_tac)
+uscalar @[step] theorem «%S».add_spec {x y : «%S»} :
+    partialSpec (x + y)
+      (fun z => (↑z : Nat) = ↑x + ↑y)
+      (fun | .integerOverflow => ↑x + ↑y > «%S».max | _ => False)
+      False := by
+  convert @UScalar.add_spec _ x y; scalar_tac
+
+iscalar @[step] theorem «%S».add_spec {x y : «%S»} :
+    partialSpec (x + y)
+      (fun z => (↑z : Int) = ↑x + ↑y)
+      (fun | .integerOverflow => ↑x + ↑y < «%S».min ∨ ↑x + ↑y > «%S».max | _ => False)
+      False := by
+  convert @IScalar.add_spec _ x y <;> scalar_tac
 
 end Aeneas.Std
diff --git a/backends/lean/Aeneas/Std/Scalar/Ops/Div.lean b/backends/lean/Aeneas/Std/Scalar/Ops/Div.lean
index 682a0dddd..fc5d2c9f3 100644
--- a/backends/lean/Aeneas/Std/Scalar/Ops/Div.lean
+++ b/backends/lean/Aeneas/Std/Scalar/Ops/Div.lean
@@ -414,13 +414,36 @@ theorem IScalar.div_spec {ty} {x y : IScalar ty}
   have ⟨ z, hz ⟩ := IScalar.div_bv_spec hzero hNoOverflow
   simp [hz]
 
-uscalar @[step] theorem «%S».div_spec (x : «%S») {y : «%S»} (hnz : ↑y ≠ (0 : Nat)) :
-  (x / y) ⦃ z => (↑z : Nat) = ↑x / ↑y ⦄ :=
-  exists_imp_spec (UScalar.div_spec x hnz)
-
-iscalar @[step] theorem «%S».div_spec {x y : «%S»} (hnz : ↑y ≠ (0 : Int))
-  (hNoOverflow : ¬ (x.val = «%S».min ∧ y.val = -1)) :
-  (x / y) ⦃ z => (↑z : Int) = Int.tdiv ↑x ↑y ⦄ :=
-  exists_imp_spec (IScalar.div_spec hnz (by scalar_tac))
+uscalar @[step] theorem «%S».div_spec (x : «%S») {y : «%S»} :
+    partialSpec (x / y)
+      (fun z => (↑z : Nat) = ↑x / ↑y)
+      (fun | .divisionByZero => (↑y : Nat) = 0 | _ => False)
+      False := by
+  have hxy : (x / y : Result _) = UScalar.div x y := rfl
+  rw [hxy]
+  by_cases hy : y.val = 0
+  · have hbv : y.bv = 0#_ := by zify; simp_all
+    simp [partialSpec, UScalar.div, hbv]; exact hy
+  · have ⟨ z, hz, hzVal ⟩ := UScalar.div_spec x hy
+    rw [hxy] at hz
+    simp [partialSpec, hz, hzVal]
+
+iscalar @[step] theorem «%S».div_spec {x y : «%S»} :
+    partialSpec (x / y)
+      (fun z => (↑z : Int) = Int.tdiv ↑x ↑y)
+      (fun | .divisionByZero => (↑y : Int) = 0
+           | .integerOverflow => (↑x : Int) = «%S».min ∧ (↑y : Int) = -1
+           | _ => False)
+      False := by
+  have hxy : (x / y : Result _) = IScalar.div x y := rfl
+  rw [hxy]
+  by_cases hy : y.val = 0
+  · simp [partialSpec, IScalar.div, hy]
+  · by_cases ho : x.val = IScalar.min (IScalarTy.«%S») ∧ y.val = -1
+    · simp [partialSpec, IScalar.div, ho.1, ho.2]
+      try scalar_tac
+    · have ⟨ z, hz, hzVal ⟩ := IScalar.div_spec hy ho
+      rw [hxy] at hz
+      simp [partialSpec, hz, hzVal]
 
 end Aeneas.Std
diff --git a/backends/lean/Aeneas/Std/Scalar/Ops/Mul.lean b/backends/lean/Aeneas/Std/Scalar/Ops/Mul.lean
index fc1ab6f61..88aa471d2 100644
--- a/backends/lean/Aeneas/Std/Scalar/Ops/Mul.lean
+++ b/backends/lean/Aeneas/Std/Scalar/Ops/Mul.lean
@@ -42,23 +42,29 @@ Theorems with a specification which use integers and bit-vectors
 theorem UScalar.mul_equiv {ty} (x y : UScalar ty) :
   match mul x y with
   | ok z => x.val * y.val ≤ UScalar.max ty ∧ (↑z : Nat) = ↑x * ↑y ∧ z.bv = x.bv * y.bv
-  | fail _ => UScalar.max ty < x.val * y.val
+  | fail e => e = .integerOverflow ∧ UScalar.max ty < x.val * y.val
   | .div => False := by
   simp only [mul]
   have := tryMk_eq ty (x.val * y.val)
-  split <;> simp_all only [inBounds, true_and, not_lt, gt_iff_lt]
-  simp_all only [tryMk, ofOption, tryMkOpt, check_bounds, decide_true, dite_true, ok.injEq]
-  rename_i hEq; simp only [← hEq, ofNatCore, val]
-  split_conjs
-  . simp only [bv_toNat, max]; omega
-  . zify at this; zify; simp only [bv_toNat, BitVec.toNat_ofFin, Nat.cast_mul, BitVec.toNat_mul,
-    Int.natCast_emod, Nat.cast_pow, Nat.cast_ofNat] at *
-    rw [Int.emod_eq_of_lt]
-    . apply Int.pos_mul_pos_is_pos <;> simp
-    . simp only [this]
-  . have : 0 < 2^ty.numBits := by simp
-    simp only [max, gt_iff_lt]
-    omega
+  have hfail : ∀ e, mul x y = fail e → e = .integerOverflow := by
+    intro e he
+    simp only [mul, tryMk, Result.ofOption] at he
+    split at he <;> simp_all
+  split <;> simp_all only [inBounds, true_and, not_lt]
+  · simp_all only [tryMk, ofOption, tryMkOpt, check_bounds, decide_true, dite_true, ok.injEq]
+    rename_i hEq; simp only [← hEq, ofNatCore, val]
+    split_conjs
+    . simp only [bv_toNat, max]; omega
+    . zify at this; zify; simp only [bv_toNat, BitVec.toNat_ofFin, Nat.cast_mul, BitVec.toNat_mul,
+      Int.natCast_emod, Nat.cast_pow, Nat.cast_ofNat] at *
+      rw [Int.emod_eq_of_lt]
+      . apply Int.pos_mul_pos_is_pos <;> simp
+      . simp only [this]
+  · refine ⟨ hfail _ ?_, ?_ ⟩
+    · rw [mul]; assumption
+    · have : 0 < 2^ty.numBits := by simp
+      simp only [max, gt_iff_lt]
+      omega
 
 /-- Generic theorem - shouldn't be used much -/
 theorem UScalar.mul_bv_spec {ty} {x y : UScalar ty}
@@ -72,7 +78,7 @@ theorem UScalar.mul_bv_spec {ty} {x y : UScalar ty}
 theorem IScalar.mul_equiv {ty} (x y : IScalar ty) :
   match mul x y with
   | ok z => IScalar.min ty ≤ x.val * y.val ∧ x.val * y.val ≤ IScalar.max ty ∧ z.val = x.val * y.val ∧ z.bv = x.bv * y.bv
-  | fail _ => ¬(IScalar.min ty ≤ x.val * y.val ∧ x.val * y.val ≤ IScalar.max ty)
+  | fail e => e = .integerOverflow ∧ ¬(IScalar.min ty ≤ x.val * y.val ∧ x.val * y.val ≤ IScalar.max ty)
   | .div => False := by
   simp only [mul, not_and, not_le]
   have := tryMk_eq ty (x.val * y.val)
@@ -109,7 +115,7 @@ theorem IScalar.mul_equiv {ty} (x y : IScalar ty) :
       simp_all only [iff_true, sup_eq_left, ge_iff_le, iff_false,
         not_lt, sub_left_inj, sup_eq_left] <;>
       omega
-  . omega
+  . grind
 
 /-- Generic theorem - shouldn't be used much -/
 theorem IScalar.mul_bv_spec {ty} {x y : IScalar ty}
@@ -150,13 +156,24 @@ theorem IScalar.mul_spec {ty} {x y : IScalar ty}
   apply @mul_bv_spec ty x y (by scalar_tac) (by scalar_tac)
   grind
 
-uscalar @[step] theorem «%S».mul_spec {x y : «%S»} (hmax : x.val * y.val ≤ «%S».max) :
-  x * y ⦃ z => (↑z : Nat) = ↑x * ↑y ⦄ :=
-  UScalar.mul_spec (by scalar_tac)
-
-iscalar @[step] theorem «%S».mul_spec {x y : «%S»}
-  (hmin : «%S».min ≤ ↑x * ↑y) (hmax : ↑x * ↑y ≤ «%S».max) :
-  (x * y) ⦃ z => (↑z : Int) = ↑x * ↑y ⦄ :=
-  IScalar.mul_spec (by scalar_tac) (by scalar_tac)
+uscalar @[step] theorem «%S».mul_spec {x y : «%S»} :
+    partialSpec (x * y)
+      (fun z => (↑z : Nat) = ↑x * ↑y)
+      (fun | .integerOverflow => ↑x * ↑y > «%S».max | _ => False)
+      False := by
+  have h := UScalar.mul_equiv x y
+  show partialSpec (UScalar.mul x y) _ _ _
+  simp only [partialSpec]
+  split <;> simp_all <;> scalar_tac
+
+iscalar @[step] theorem «%S».mul_spec {x y : «%S»} :
+    partialSpec (x * y)
+      (fun z => (↑z : Int) = ↑x * ↑y)
+      (fun | .integerOverflow => ↑x * ↑y < «%S».min ∨ ↑x * ↑y > «%S».max | _ => False)
+      False := by
+  have h := IScalar.mul_equiv x y
+  show partialSpec (IScalar.mul x y) _ _ _
+  simp only [partialSpec]
+  split <;> simp_all; scalar_tac
 
 end Aeneas.Std
diff --git a/backends/lean/Aeneas/Std/Scalar/Ops/Neg.lean b/backends/lean/Aeneas/Std/Scalar/Ops/Neg.lean
index 6b72d5ada..9b67cee82 100644
--- a/backends/lean/Aeneas/Std/Scalar/Ops/Neg.lean
+++ b/backends/lean/Aeneas/Std/Scalar/Ops/Neg.lean
@@ -6,7 +6,7 @@ import Mathlib.Data.BitVec
 
 namespace Aeneas.Std
 
-open Result Error Arith
+open Result Error Arith WP
 
 /-!
 # Negation: Definitions
@@ -14,11 +14,15 @@ open Result Error Arith
 def IScalar.neg {ty : IScalarTy} (x : IScalar ty) : Result (IScalar ty) := IScalar.tryMk ty (- x.val)
 
 @[step]
-theorem IScalar.neg_step {ty} (x: IScalar ty) (h: x ≠ IScalar.min ty): IScalar.neg x ⦃ r => r = -x.val ⦄ := by
-  simp [neg]
-  have h := tryMk_eq ty (-x.val)
+theorem IScalar.neg_step {ty} (x: IScalar ty) :
+    partialSpec (IScalar.neg x)
+      (fun r => r = -x.val)
+      (fun | .integerOverflow => (x : Int) = IScalar.min ty | _ => False)
+      False := by
+  simp only [neg, tryMk, Result.ofOption]
+  have h := tryMkOpt_eq ty (-x.val)
   simp [inBounds] at h
-  split at h <;> simp_all
+  cases hopt : tryMkOpt ty (-x.val) <;> simp_all [partialSpec]
   have := IScalar.hBounds x
   simp [IScalar.min] at *
   grind
@@ -59,9 +63,12 @@ attribute [match_pattern] HNeg.hNeg
 instance {ty} : HNeg (IScalar ty) (Result (IScalar ty)) where hNeg x := IScalar.neg x
 
 @[step]
-theorem HNeg.hNeg.step {ty} (x: IScalar ty) (h: x ≠ IScalar.min ty): HNeg.hNeg x ⦃ r => r = -x.val ⦄ := by
-  simp [HNeg.hNeg]
-  apply IScalar.neg_step
-  grind
+theorem HNeg.hNeg.step {ty} (x: IScalar ty) :
+    partialSpec (HNeg.hNeg x : Result (IScalar ty))
+      (fun r => r = -x.val)
+      (fun | .integerOverflow => (x : Int) = IScalar.min ty | _ => False)
+      False := by
+  show partialSpec (IScalar.neg x) _ _ _
+  exact IScalar.neg_step x
 
 end Aeneas.Std
diff --git a/backends/lean/Aeneas/Std/Scalar/Ops/Rem.lean b/backends/lean/Aeneas/Std/Scalar/Ops/Rem.lean
index 460262a56..b1425e072 100644
--- a/backends/lean/Aeneas/Std/Scalar/Ops/Rem.lean
+++ b/backends/lean/Aeneas/Std/Scalar/Ops/Rem.lean
@@ -117,12 +117,32 @@ theorem IScalar.rem_spec {ty} (x : IScalar ty) {y : IScalar ty} (hzero : y.val 
   · intros x' h
     exact h.1
 
-uscalar @[step] theorem «%S».rem_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0) :
-  x % y ⦃ z => (↑z : Nat) = ↑x % ↑y ⦄ :=
-  UScalar.rem_spec x hnz
-
-iscalar @[step] theorem «%S».rem_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0) :
-  x % y ⦃ z => (↑z : Int) = Int.tmod ↑x ↑y ⦄ :=
-  IScalar.rem_spec x hnz
+uscalar @[step] theorem «%S».rem_spec (x : «%S») {y : «%S»} :
+    partialSpec (x % y)
+      (fun z => (↑z : Nat) = ↑x % ↑y)
+      (fun | .divisionByZero => (↑y : Nat) = 0 | _ => False)
+      False := by
+  have hxy : (x % y : Result _) = UScalar.rem x y := rfl
+  rw [hxy]
+  by_cases hy : y.val = 0
+  · simp [partialSpec, UScalar.rem, hy]
+  · have h := UScalar.rem_spec x hy
+    rw [hxy] at h
+    simp_all [partialSpec]
+    split <;> simp_all
+
+iscalar @[step] theorem «%S».rem_spec (x : «%S») {y : «%S»} :
+    partialSpec (x % y)
+      (fun z => (↑z : Int) = Int.tmod ↑x ↑y)
+      (fun | .divisionByZero => (↑y : Int) = 0 | _ => False)
+      False := by
+  have hxy : (x % y : Result _) = IScalar.rem x y := rfl
+  rw [hxy]
+  by_cases hy : y.val = 0
+  · simp [partialSpec, IScalar.rem, hy]
+  · have h := IScalar.rem_spec x hy
+    rw [hxy] at h
+    simp_all [partialSpec]
+    split <;> simp_all
 
 end Aeneas.Std
diff --git a/backends/lean/Aeneas/Std/Scalar/Ops/Sub.lean b/backends/lean/Aeneas/Std/Scalar/Ops/Sub.lean
index 060181a6c..c5dfb20ae 100644
--- a/backends/lean/Aeneas/Std/Scalar/Ops/Sub.lean
+++ b/backends/lean/Aeneas/Std/Scalar/Ops/Sub.lean
@@ -42,7 +42,7 @@ theorem UScalar.sub_equiv {ty} (x y : UScalar ty) :
     y.val ≤ x.val ∧
     x.val = z.val + y.val ∧
     z.bv = x.bv - y.bv
-  | fail _ => x.val < y.val
+  | fail e => e = .integerOverflow ∧ x.val < y.val
   | _ => ⊥ := by
   have : x - y = sub x y := by rfl
   simp [this, sub]
@@ -86,13 +86,13 @@ theorem IScalar.sub_equiv {ty} (x y : IScalar ty) :
     IScalar.inBounds ty (x.val - y.val) ∧
     z.val = x.val - y.val ∧
     z.bv = x.bv - y.bv
-  | fail _ => ¬ (IScalar.inBounds ty (x.val - y.val))
+  | fail e => e = .integerOverflow ∧ ¬ (IScalar.inBounds ty (x.val - y.val))
   | _ => ⊥ := by
   have : x - y = sub x y := by rfl
-  simp [this, sub]
-  have h := tryMk_eq ty (↑x - ↑y)
+  simp [this, sub, tryMk, Result.ofOption]
+  have h := tryMkOpt_eq ty (↑x - ↑y)
   simp [inBounds] at h
-  split at h <;> simp_all
+  cases hopt : tryMkOpt ty (↑x - ↑y) <;> simp_all
   apply BitVec.eq_of_toInt_eq
   simp
   have := bmod_pow_numBits_eq_of_lt ty (x.val - y.val) (by omega) (by omega)
@@ -134,30 +134,39 @@ Theorems with a specification which only uses integers
 
 /- Generic theorem - shouldn't be used much -/
 @[step]
-theorem UScalar.sub_spec {ty} {x y : UScalar ty}
-  (h : y.val ≤ x.val) :
-  x - y ⦃ z => z.val = x.val - y.val ∧ y.val ≤ x.val ⦄ := by
+theorem UScalar.sub_spec {ty} {x y : UScalar ty} :
+    partialSpec (x - y)
+      (fun z => z.val = x.val - y.val ∧ y.val ≤ x.val)
+      (fun | .integerOverflow => x.val < y.val | _ => False)
+      False := by
   have h := @sub_equiv ty x y
-  split at h <;> simp_all
-  omega
+  simp only [partialSpec]
+  split <;> simp_all
 
 /- Generic theorem - shouldn't be used much -/
 @[step]
-theorem IScalar.sub_spec {ty} {x y : IScalar ty}
-  (hmin : IScalar.min ty ≤ ↑x - ↑y)
-  (hmax : ↑x - ↑y ≤ IScalar.max ty) :
-  x - y ⦃ z => (↑z : Int) = ↑x - ↑y ⦄ := by
+theorem IScalar.sub_spec {ty} {x y : IScalar ty} :
+    partialSpec (x - y)
+      (fun z => (↑z : Int) = ↑x - ↑y)
+      (fun | .integerOverflow => ↑x - ↑y < IScalar.min ty ∨ ↑x - ↑y > IScalar.max ty | _ => False)
+      False := by
   have h := @sub_equiv ty x y
-  split at h <;> simp_all [min, max]
+  simp only [partialSpec]
+  split <;> simp_all [min, max, inBounds]
   omega
 
-uscalar @[step] theorem «%S».sub_spec {x y : «%S»} (h : y.val ≤ x.val) :
-  x - y ⦃ z => z.val = x.val - y.val ∧ y.val ≤ x.val ⦄ :=
-  UScalar.sub_spec h
-
-iscalar @[step] theorem «%S».sub_spec {x y : «%S»}
-  (hmin : «%S».min ≤ ↑x - ↑y) (hmax : ↑x - ↑y ≤ «%S».max) :
-  x - y ⦃ z => (↑z : Int) = ↑x - ↑y ⦄ :=
-  IScalar.sub_spec (by scalar_tac) (by scalar_tac)
+uscalar @[step] theorem «%S».sub_spec {x y : «%S»} :
+    partialSpec (x - y)
+      (fun z => z.val = x.val - y.val ∧ y.val ≤ x.val)
+      (fun | .integerOverflow => x.val < y.val | _ => False)
+      False :=
+  @UScalar.sub_spec _ x y
+
+iscalar @[step] theorem «%S».sub_spec {x y : «%S»} :
+    partialSpec (x - y)
+      (fun z => (↑z : Int) = ↑x - ↑y)
+      (fun | .integerOverflow => ↑x - ↑y < «%S».min ∨ ↑x - ↑y > «%S».max | _ => False)
+      False := by
+  convert @IScalar.sub_spec _ x y <;> scalar_tac
 
 end Aeneas.Std
diff --git a/backends/lean/Aeneas/Std/WP.lean b/backends/lean/Aeneas/Std/WP.lean
index 84b6a8404..0105e5d80 100644
--- a/backends/lean/Aeneas/Std/WP.lean
+++ b/backends/lean/Aeneas/Std/WP.lean
@@ -243,6 +243,42 @@ theorem dspec_imp_forall {m:Result α} {P:Post α} :
   dspec m P → (∀ y, m = ok y → P y) := by
   grind only [= dspec_ok]
 
+/-- Partial-correctness variant of `spec`.
+
+`partialSpec x p_ok p_fail p_div` reads as: "if `x` reduces to `ok a` then `p_ok a` holds; if it
+reduces to `fail e` then `p_fail e` holds; if it diverges then `p_div` holds". Unlike `spec`, it
+does not assume the program terminates without exception. -/
+def partialSpec {α} (x : Result α)
+    (p_ok : α → Prop) (p_fail : Error → Prop) (p_div : Prop) : Prop :=
+  match x with
+  | ok a   => p_ok a
+  | fail e => p_fail e
+  | div    => p_div
+
+@[simp, grind =, agrind =]
+theorem partialSpec_ok (a : α) (p_ok : α → Prop) p_fail p_div :
+    partialSpec (ok a) p_ok p_fail p_div ↔ p_ok a := by
+  simp [partialSpec]
+
+@[simp, grind =, agrind =]
+theorem partialSpec_fail (e : Error) p_ok p_fail p_div :
+    partialSpec (α := α) (fail e) p_ok p_fail p_div ↔ p_fail e := by
+  simp [partialSpec]
+
+@[simp, grind =, agrind =]
+theorem partialSpec_div (p_ok : α → Prop) p_fail p_div :
+    partialSpec div p_ok p_fail p_div ↔ p_div := by
+  simp [partialSpec]
+
+/-- Derive a total-correctness `spec` from `partialSpec` by ruling out the failure and divergence
+cases. Used by `@[step]` to generate a step-tactic lemma from a `partialSpec` theorem. -/
+theorem spec_of_partialSpec
+    {α} {x : Result α} {p_ok : α → Prop} {p_fail : Error → Prop} {p_div : Prop}
+    (h : partialSpec x p_ok p_fail p_div)
+    (h_fail : ∀ e, ¬ p_fail e) (h_div : ¬ p_div) :
+    spec x p_ok := by
+  cases x <;> simp_all [partialSpec, spec, theta, wp_return]
+
 end Aeneas.Std.WP
 
 /-
@@ -789,7 +825,9 @@ namespace Aeneas.Std.WP
 open Std Result
 open Std.Do
 
-instance Result.instWP : WP Result.{u} (.except (ULift Error) (.except PUnit .pure)) where
+abbrev Result.postShape : PostShape := (.except (ULift Error) (.except PUnit .pure))
+
+instance Result.instWP : WP Result.{u} postShape where
   wp x := {
     trans Q := match x with | .ok a => Q.1 a | .fail e => Q.2.1 (ULift.up e) | .div => Q.2.2.1 .unit
     conjunctiveRaw Q₁ Q₂ := by
@@ -797,6 +835,15 @@ instance Result.instWP : WP Result.{u} (.except (ULift Error) (.except PUnit .pu
       cases x <;> simp
   }
 
+abbrev willYield {α : Type u} (r : α) (Q : PostCond α Result.postShape) : Prop :=
+  (Q.1 r).down
+
+abbrev willFail {α : Type u} (e : Error) (Q : PostCond α Result.postShape) : Prop :=
+  (Q.2.1 (.up e)).down
+
+abbrev willDiverge {α : Type u} (Q : PostCond α Result.postShape) : Prop :=
+  (Q.2.2.1 .unit).down
+
 instance : LawfulMonad Result where
     map_const := by intros; rfl
     id_map := by intros _ x; cases x <;> rfl
@@ -834,6 +881,19 @@ theorem dspec_to_mvcgen {α : Type u} {x : Result α} {Q : α → Prop}
   simp [Triple, WP.wp, PredTrans.apply, SPred.pure]
   cases x <;> simp [*, dspec] at * <;> trivial
 
+/-- Lift an Aeneas partial-correctness spec to an mvcgen-compatible `Triple`. -/
+theorem partialSpec_to_mvcgen {α : Type u} {x : Result α}
+    {p_ok : α → Prop} {p_fail : Error → Prop} {p_div : Prop}
+    (h : partialSpec x p_ok p_fail p_div)
+    {Q : PostCond α Result.postShape}
+    (h_ok   : ∀ r, p_ok r → willYield r Q)
+    (h_fail : ∀ e, p_fail e → willFail e Q)
+    (h_div  : p_div → willDiverge Q) :
+    ⦃ ⌜ True ⌝ ⦄ x ⦃ Q ⦄ := by
+  cases x
+    <;> simp only [partialSpec] at h
+    <;> simp [Triple, WP.wp, PredTrans.apply, h_ok, h_fail, h_div, h]
+
 end Aeneas.Std.WP
 
 namespace Aeneas.Std
diff --git a/backends/lean/Aeneas/Tactic/Step/Init.lean b/backends/lean/Aeneas/Tactic/Step/Init.lean
index bd90cd489..85cad0510 100644
--- a/backends/lean/Aeneas/Tactic/Step/Init.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Init.lean
@@ -5,6 +5,7 @@ import AeneasMeta.Extensions
 import Aeneas.Tactic.Step.Trace
 import Aeneas.Std.WP
 import AeneasMeta.OptionConfig
+import Mathlib.Order.Defs.LinearOrder
 
 namespace Aeneas
 
@@ -212,13 +213,7 @@ section Methods
     withLocalDeclsD ⟨ tys ⟩ k
 end Methods
 
-/- Analyze a goal or a step theorem to decompose its arguments.
-
-  StepSpec theorems should be of the following shape:
-  ```
-  ∀ x1 ... xn, H1 → ... Hn → spec (f x1 ... xn) P
-  ```
--/
+/- Analyze a goal or a step theorem to decompose its arguments. -/
 def getStepSpecFunArgsExpr (ty : Expr) :
   MetaM (Expr × SpecInfo) := do
   let ty := ty.consumeMData
@@ -283,65 +278,348 @@ structure StepSpecAttr where
   ext  : Extension
   deriving Inhabited
 
-private def generateMvcgenSpec (toMvcgenThm : Name) (stx : Syntax) (attrKind : AttributeKind)
+/-! ## Register a spec for the `step` tactic -/
+
+/-- Register a theorem using `spec` with `step`. -/
+private def saveStepSpecFromThm (ext : Extension) (attrKind : AttributeKind)
+    (thName : Name) (ty : Expr) : MetaM Unit := do
+  let (fExpr, info) ← getStepSpecFunArgsExpr ty
+  trace[Step] "Registering spec theorem for expr: {fExpr}"
+  -- Convert the function expression to a discrimination tree key
+  let fKey ← DiscrTree.mkPath fExpr
+  -- TODO: use info.name to use a different discrimination tree here!
+  ScopedEnvExtension.add ext ((info.spec_name, fKey), thName) attrKind
+  trace[Step] "Saved the entry"
+
+section
+open Aeneas.Std
+
+/-! ## Convert a `partialSpec` theorem into a theorem for the `step` tactic
+
+The `step` tactic cannot directly handle spec lemmas that use the `partialSpec` predicate.
+So, when the `@[step]` attribute is applied to `partialSpec` theorems, we need to convert
+the statement about `partialSpec` into a statement about `spec`. We use the following mechanisms
+to do that:
+
+- A `partialSpec` theorem may use match-syntax of the form
+  `fun | .integerOverflow => ↑x + ↑y > UScalar.max ty | _ => False`
+  to distinguish various kinds of panics.
+  We canoncialize this syntax into an expression like
+  `fun e => e = integerOverflow ∧ ↑x + ↑y > UScalar.max ty`.
+
+- We apply the lemma `spec_of_partialSpec` to replace the `partialSpec` statement with an
+  corresponding statement using the `spec` predicate
+
+- We use the simplifier with a restricted simp set to make the preconditions of the `spec` theorem
+  look nicer. For instance, we rewrite `¬a ≤ b` into `b < a`.
+-/
+
+/-- For `simplifyStepHypotheses`: rewrites `∀ e, ¬ (e = c ∧ P)` to `¬ P`. -/
+private theorem step_fail_failEq_iff {c : Aeneas.Std.Error} {P : Prop} :
+    (∀ e, ¬ (e = c ∧ P)) ↔ ¬ P :=
+  ⟨fun h hP => h c ⟨rfl, hP⟩, fun h _ h' => h h'.2⟩
+
+/-- For `simplifyStepHypotheses`: rewrites `∀ _ : Error, P` to `P`. -/
+private theorem step_fail_remove_forall_iff {P : Prop} :
+    (∀ _ : Aeneas.Std.Error, P) ↔ P :=
+  ⟨fun h => h Error.panic, fun h _ => h⟩
+
+/-- For `simplifyStepHypotheses`: rewrites `∀ e, ¬ False` to `True`. -/
+private theorem step_fail_False_iff :
+    (∀ (_ : Aeneas.Std.Error), ¬ False) ↔ True :=
+  ⟨fun _ => trivial, fun _ _ h => h⟩
+
+/-- For `simplifyStepHypotheses`: rewrites `¬ False` to `True`. -/
+private theorem step_div_False_iff : (¬ False) ↔ True :=
+  ⟨fun _ => trivial, fun _ h => h⟩
+
+end
+
+/-- Build a `Simp.Context` containing exactly the given lemmas (no default simp set,
+    no simprocs). The resulting `simp` call is equivalent to `simp only [lemmas...]`. -/
+private def mkSimpOnlyContext (lemmas : Array Name) : MetaM Simp.Context := do
+  let mut simpThms : SimpTheorems := {}
+  for thmName in lemmas do
+    simpThms ← simpThms.addConst thmName (post := false) (inv := false)
+  Simp.mkContext
+    (config := { failIfUnchanged := false })
+    (simpTheorems := #[simpThms])
+    (congrTheorems := ← getSimpCongrTheorems)
+
+/-- Recursively split a metavariable whose target is `P ∧ Q` into separate goals
+    for each conjunct, by assigning it to `⟨?m₁, ?m₂⟩`. When at least one split
+    happens, leaf mvars get a fresh `userName` derived from the original mvar's
+    tag with an index suffix appended (e.g. `h_fail` becomes `h_fail_1`,
+    `h_fail_2`, …), so they remain distinct once abstracted. If the target is not
+    an `And`, the mvar is returned unchanged. Returns the list of leaf mvars. -/
+private partial def splitAndGoals (mvarId : MVarId) : MetaM (Array MVarId) := do
+  let target ← instantiateMVars (← mvarId.getType)
+  if target.app2? ``And |>.isNone then
+    return #[mvarId]
+  let baseTag ← mvarId.getTag
+  Prod.snd <$> go baseTag mvarId 0 #[]
+where
+  go (baseTag : Name) (mvarId : MVarId) (idx : Nat) (acc : Array MVarId) :
+      MetaM (Nat × Array MVarId) := do
+    let target ← instantiateMVars (← mvarId.getType)
+    match target.app2? ``And with
+    | some (p, q) =>
+      let m₁ ← mkFreshExprSyntheticOpaqueMVar p
+      let m₂ ← mkFreshExprSyntheticOpaqueMVar q
+      mvarId.assign (← mkAppM ``And.intro #[m₁, m₂])
+      let (idx, acc) ← go baseTag m₁.mvarId! idx acc
+      go baseTag m₂.mvarId! idx acc
+    | none =>
+      if !baseTag.isAnonymous then
+        mvarId.setTag (baseTag.appendIndexAfter (idx + 1))
+      return (idx + 1, acc.push mvarId)
+
+/-- Simp lemmas shared by `simplifyStepHypotheses` and `simplifyMvcgenHypotheses` -/
+private def commonPushNotLemmas : Array Name :=
+  #[``gt_iff_lt, ``ge_iff_le, ``not_or, ``not_lt, ``not_le, ``or_imp, ``imp_true_iff, ``not_true,
+    ``true_implies, ``forall_and, ``true_and, ``and_true]
+
+/-- To bring a match on `Error` into canonical form, the following lemma is helpful.
+It's used in `canonicalizeFailPostcond` below.  -/
+private theorem error_pred_eq_disj (p : Aeneas.Std.Error → Prop) :
+    p = fun e =>
+      (e = .assertionFailure    ∧ p .assertionFailure)    ∨
+      (e = .integerOverflow     ∧ p .integerOverflow)     ∨
+      (e = .divisionByZero      ∧ p .divisionByZero)      ∨
+      (e = .arrayOutOfBounds    ∧ p .arrayOutOfBounds)    ∨
+      (e = .maximumSizeExceeded ∧ p .maximumSizeExceeded) ∨
+      (e = .panic               ∧ p .panic)               ∨
+      (e = .undef               ∧ p .undef) := by
+  funext e; cases e <;> simp
+
+/-- If the failure postcondition `p_fail` of `partialSpec` is written as a `match`
+    of the shape `fun | Cᵢ => Pᵢ | … | _ => False`, return a proof of the
+    same `partialSpec` but with `p_fail` replaced by the equivalent disjunction
+    `fun e => (e = C₁ ∧ p_fail C₁) ∨ … ∨ (e = Cₖ ∧ p_fail Cₖ)`.
+
+    Returns `thApp` unchanged if `p_fail` is not such a `match`. -/
+private def canonicalizeFailPostcond (thApp : Expr) : MetaM Expr := do
+  try
+    let ty ← instantiateMVars (← inferType thApp)
+    let fn := ty.getAppFn
+    unless fn.isConstOf ``Aeneas.Std.WP.partialSpec do return thApp
+    let args := ty.getAppArgs
+    unless args.size == 5 do return thApp
+    let p_fail := args[3]!
+    -- Only rewrite when `p_fail` is a `match` on the error; leave the `e = c ∧ P` form, constants,
+    -- etc. untouched (rewriting them would only add work for the downstream simp set to undo).
+    let isMatch ← withLocalDeclD `e (.const ``Aeneas.Std.Error []) fun e =>
+      return (← matchMatcherApp? (p_fail.beta #[e]).headBeta).isSome
+    unless isMatch do return thApp
+    -- `heq : p_fail = fun e => ⋁ᵢ (e = Cᵢ ∧ p_fail Cᵢ)`; transport `thApp` across it along the
+    -- motive `fun pf => partialSpec x p_ok pf p_div`.
+    let heq ← mkAppM ``error_pred_eq_disj #[p_fail]
+    let motive ← withLocalDeclD `pf (← inferType p_fail) fun pf =>
+      mkLambdaFVars #[pf] (mkAppN fn (args.set! 3 pf))
+    mkEqMP (← mkCongrArg motive heq) thApp
+  catch _ => return thApp
+
+/-- Try to simplify the arguments produced by `spec_of_partialSpec` -/
+private def simplifyStepHypotheses (mvarFail mvarDiv : Expr) : MetaM Unit := do
+  let simpCtx ← mkSimpOnlyContext (#[
+      ``step_fail_failEq_iff, ``step_fail_remove_forall_iff,
+      ``step_fail_False_iff, ``step_div_False_iff] ++ commonPushNotLemmas)
+  let simplify (mv : Expr) (name : String) : MetaM Unit := do
+    trace[Step] "simplifyStepHypotheses: {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] "simplifyStepHypotheses: simp on {name} failed: {e.toMessageData}"
+  simplify mvarFail "hFail"
+  simplify mvarDiv "hDiv"
+
+/-- Register a theorem using `partialSpec` with `step`. This function generates a auxiliary lemma
+using `spec` instead of `partialSpec` and registers that one with `step`, so that the `step`
+tactic will only ever see `spec`. -/
+private def saveStepPartialSpecFromThm (ext : Extension) (attrKind : AttributeKind) (stx : Syntax)
+    (thDecl : AsyncConstantInfo) (ty : Expr) : MetaM Unit := do
+  trace[Step] "saveStepPartialSpecFromThm: {thDecl.name}"
+  let sig := thDecl.sig.get
+  let levelParams := sig.levelParams
+  let (newName, newTy) ← forallTelescope ty fun fvars _ => do
+    let thConst := Lean.mkConst thDecl.name (levelParams.map Level.param)
+    let thApp ← canonicalizeFailPostcond (mkAppN thConst fvars)
+    let bridge ← mkAppM ``Aeneas.Std.WP.spec_of_partialSpec #[thApp]
+    let (extraMVars, _, _) ← forallMetaTelescope (← inferType bridge)
+    unless extraMVars.size = 2 do
+      throwError "spec_of_partialSpec: expected 2 extra arguments, got {extraMVars.size}"
+    simplifyStepHypotheses extraMVars[0]! extraMVars[1]!
+    let proof := mkAppN bridge extraMVars
+    let { expr := proofAbstracted, .. } ← abstractMVars proof
+    let proofTerm ← mkLambdaFVars fvars proofAbstracted
+    let thmTy ← inferType proofTerm
+    let name := Name.str thDecl.name "step_spec"
+    let auxDecl : TheoremVal := {
+      name
+      levelParams
+      type  := thmTy
+      value := proofTerm
+    }
+    addDecl (.thmDecl auxDecl)
+    addDeclarationRangesFromSyntax name stx
+    pure (name, thmTy)
+  saveStepSpecFromThm ext attrKind newName newTy
+
+/-! ## Convert a `spec` theorem into a spec theorem for `mvcgen`
+
+The `mvcgen` tactic cannot process spec theorems that use the `spec` predicate. Instead, `mvcgen`
+expects the `Triple` predicate. We use the `spec_to_mvcgen` lemma to convert a statement about
+`spec` into a statement about `Triple`.
+-/
+
+private def saveMvcgenDecl (attrKind : AttributeKind) (stx : Syntax)
+    (originalThDecl : AsyncConstantInfo) (thmTy proofTerm : Expr) : MetaM Unit := do
+  let mvcgenSpecName := Name.str originalThDecl.name "mvcgen_spec"
+  let auxDecl : TheoremVal := {
+    name        := mvcgenSpecName
+    levelParams := originalThDecl.sig.get.levelParams
+    type        := thmTy
+    value       := proofTerm
+  }
+  addDecl (.thmDecl auxDecl)
+  addDeclarationRangesFromSyntax mvcgenSpecName stx
+  -- Register with @[spec] so mvcgen can find it
+  Lean.Attribute.add mvcgenSpecName `spec .missing attrKind
+  trace[Step] "Registered {mvcgenSpecName} as `@[spec]`."
+
+/-- Register a theorem using `spec` with `mvcgen`. -/
+private def saveMvcgenSpecFromThm (stx : Syntax) (attrKind : AttributeKind)
     (thDecl : AsyncConstantInfo) : MetaM Unit := do
+  trace[Step] "saveMvcgenSpecFromThm: {thDecl.name}"
   let sig := thDecl.sig.get
   let thName := thDecl.name
   forallTelescope sig.type fun fvars _ => do
-    -- Apply the original theorem to all fvars to get: spec (f args) Q
     let thConst := Lean.mkConst thName (sig.levelParams.map .param)
     let thApp := mkAppN thConst fvars
-    -- Wrap with spec_to_mvcgen to produce: Triple (f args) ⌜True⌝ post⟨...⟩
-    let proof ← mkAppM toMvcgenThm #[thApp]
+    -- Wrap with spec_to_mvcgen to produce a statement about `Triple`.
+    let proof ← mkAppM ``Aeneas.Std.WP.spec_to_mvcgen #[thApp]
     let innerTy ← inferType proof
-    -- Re-introduce all fvars as binders
     let proofTerm ← mkLambdaFVars fvars proof
     let thmTy ← mkForallFVars fvars innerTy
-    let mvcgenSpecName := Name.str thName "mvcgen_spec"
-    let auxDecl : TheoremVal := {
-      name        := mvcgenSpecName
-      levelParams := sig.levelParams
-      type        := thmTy
-      value       := proofTerm
-    }
-    addDecl (.thmDecl auxDecl)
-    addDeclarationRangesFromSyntax mvcgenSpecName stx
-    -- Register with @[spec] so mvcgen can find it
-    Lean.Attribute.add mvcgenSpecName `spec .missing attrKind
+    saveMvcgenDecl attrKind stx thDecl thmTy proofTerm
+
+/-! ## Convert a `partialSpec` theorem into a spec theorem for `mvcgen`
+
+The `mvcgen` tactic cannot process spec theorems that use the `partialSpec` predicate either.
+We convert a `partialSpec` theorem into a `Triple` theorem for `mvcgen` as follows:
+
+- A `partialSpec` theorem may use match-syntax of the form
+  `fun | .integerOverflow => ↑x + ↑y > UScalar.max ty | _ => False`
+  to distinguish various kinds of panics.
+  We canoncialize this syntax into an expression like
+  `fun e => e = integerOverflow ∧ ↑x + ↑y > UScalar.max ty`.
+
+- We apply the lemma `partialSpec_to_mvcgen` to replace the `partialSpec` statement with an
+  corresponding statement using the `Triple` predicate
 
-private def saveStepSpecFromThm (ext : Extension) (attrKind : AttributeKind) (stx : Syntax)
+- We use the simplifier with a restricted simp set to make the preconditions of the `spec` theorem
+  look nicer. For instance, we rewrite `¬a ≤ b` into `b < a`.
+-/
+section
+open Aeneas.Std WP Result
+
+private theorem mvcgen_fail_failEq_iff {α : Type u} {Q : Std.Do.PostCond α postShape}
+    {c : Error} {P : Prop} :
+    (∀ e, (e = c ∧ P) → willFail e Q) ↔ (P → willFail c Q) :=
+  ⟨fun h hP => h c ⟨rfl, hP⟩, fun h _ ⟨he, hP⟩ => he ▸ h hP⟩
+
+private theorem mvcgen_fail_False_iff {α : Type u} {Q : Std.Do.PostCond α postShape} :
+    (∀ e, False → willFail e Q) ↔ True :=
+  ⟨fun _ => trivial, fun _ _ h => h.elim⟩
+
+private theorem mvcgen_div_False_iff {P : Prop} :
+    (False → P) ↔ True :=
+  ⟨fun _ => trivial, fun _ h => h.elim⟩
+
+private theorem mvcgen_uncurry' {α β} {p : α → β → Prop} {q : α × β → Prop} :
+    (∀ (r : α × β), uncurry' p r → q r) ↔ (∀ (r₁ : α) (r₂ : β), p r₁ r₂ → q (r₁, r₂)) := by simp
+
+end
+
+/-- Try to simplify the arguments produced by `partialSpec_to_mvcgen`. -/
+private def simplifyMvcgenHypotheses (mvarOk mvarFail mvarDiv : Expr) : MetaM Unit := do
+  let simpCtx ← mkSimpOnlyContext (#[
+      ``mvcgen_fail_failEq_iff, ``mvcgen_fail_False_iff,
+      ``mvcgen_div_False_iff, ``mvcgen_uncurry', ``and_imp, ``forall_eq] ++ commonPushNotLemmas)
+  let simplify (mv : Expr) (name : String) : MetaM Unit := do
+    trace[Step] "simplifyMvcgenHypotheses: {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] "simplifyMvcgenHypotheses: simp on {name} failed: {e.toMessageData}"
+  simplify mvarOk "hOk"
+  simplify mvarFail "hFail"
+  simplify mvarDiv "hDiv"
+
+/-- Register a theorem using `partialSpec` with `mvcgen`. -/
+private def saveMvcgenPartialSpecFromThm (stx : Syntax) (attrKind : AttributeKind)
+    (thDecl : AsyncConstantInfo) : MetaM Unit := do
+  trace[Step] "saveMvcgenPartialSpecFromThm: {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_mvcgen
+      #[none, none, none, none, none, some thApp]
+    let (extraMVars, _, _) ← forallMetaTelescope (← inferType bridge)
+    unless extraMVars.size = 4 do
+      throwError "partialSpec_to_mvcgen: expected 4 extra arguments, got {extraMVars.size}"
+    simplifyMvcgenHypotheses extraMVars[1]! extraMVars[2]! extraMVars[3]!
+    let proof := mkAppN bridge extraMVars
+    let { expr := proofAbstracted, .. } ← abstractMVars proof
+    let proofTerm ← mkLambdaFVars fvars proofAbstracted
+    let thmTy ← inferType proofTerm
+    saveMvcgenDecl 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
+preprocessing before registering the lemmas.
+-/
+
+/-- Check whether a theorem is a `partialSpec` -/
+def isPartialSpec (ty : Expr) : MetaM Bool := do
+  let ty := ty.consumeMData
+  let (_, _, ty₂) ← forallMetaTelescope ty
+  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`. -/
+private def applyStepAttr (ext : Extension) (attrKind : AttributeKind) (stx : Syntax)
     (thName : Name) : AttrM Unit := do
-  -- Lookup the theorem
-  let env ← getEnv
   -- Ignore some auxiliary definitions (see the comments for attrIgnoreMutRec)
   attrIgnoreAuxDef thName (pure ()) do
     trace[Step] "Registering `step` theorem for {thName}"
-    let some thDecl := env.findAsync? thName
-      | throwError "Could not find theorem {thName}"
-    let type := thDecl.sig.get.type
-    let (fKey, info) ← MetaM.run' (do
+    MetaM.run' do
+      let env ← getEnv
+      let some thDecl := env.findAsync? thName
+        | throwError "Could not find theorem {thName}"
+      let type := thDecl.sig.get.type
       trace[Step] "Theorem: {type}"
-      -- Normalize to eliminate the let-bindings
       let ty ← normalizeLetBindings type
       trace[Step] "Theorem after normalization (to eliminate the let bindings): {ty}"
-      let (fExpr, info) ← getStepSpecFunArgsExpr ty
-      trace[Step] "Registering spec theorem for expr: {fExpr}"
-      -- Convert the function expression to a discrimination tree key
-      pure (← DiscrTree.mkPath fExpr, info))
-    -- Save the entry
-    -- TODO: use info.name to use a different discrimination tree here!
-    ScopedEnvExtension.add ext ((info.spec_name, fKey), thName) attrKind
-    trace[Step] "Saved the entry"
-    -- Also generate a corresponding mvcgen (@[spec]) lemma
-    try
-      trace[Step] "Registering with mvcgen"
-      if let .some thm := info.to_mvcgen then
-        MetaM.run' (generateMvcgenSpec thm stx attrKind thDecl)
-    catch e =>
-      logWarning m!"Could not generate mvcgen spec for {thName}: {e.toMessageData}"
-    pure ()
-
-/- Initiliaze the `step` attribute. -/
+      if ← isPartialSpec ty then
+        try saveStepPartialSpecFromThm ext attrKind stx thDecl ty
+        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}"
+      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
+        catch e => logWarning m!"Could not generate mvcgen spec for {thName}: {e.toMessageData}"
+
+/-- Initialize the `step` attribute. -/
 initialize stepAttr : StepSpecAttr ← do
   let ext ← mkExtension `stepMap
   let attrImpl : AttributeImpl := {
@@ -349,7 +627,7 @@ initialize stepAttr : StepSpecAttr ← do
     descr := "Adds theorems to the `step` database"
     add := fun thName stx attrKind => do
       Attribute.Builtin.ensureNoArgs stx
-      saveStepSpecFromThm ext attrKind stx thName
+      applyStepAttr ext attrKind stx thName
     erase := fun thName => do
       let s := ext.getState (← getEnv)
       let s := s.erase thName
@@ -880,7 +1158,7 @@ initialize stepPureAttribute : StepPureSpecAttr ← do
         -- Introduce the lifted theorem
         let liftedThmName ← MetaM.run' (liftThm stx thName pat)
         -- Save the lifted theorem to the `step` database
-        saveStepSpecFromThm stepAttr.ext attrKind stx liftedThmName
+        applyStepAttr stepAttr.ext attrKind stx liftedThmName
   }
   registerBuiltinAttribute attrImpl
   pure { attr := attrImpl }
@@ -1021,7 +1299,7 @@ initialize stepPureDefAttribute : StepPureDefSpecAttr ← do
         -- Introduce the lifted theorem
         let thmName ← MetaM.run' (mkStepPureDefThm stx pat declName)
         -- Save the lifted theorem to the `step` database
-        saveStepSpecFromThm stepAttr.ext attrKind stx thmName
+        applyStepAttr stepAttr.ext attrKind stx thmName
   }
   registerBuiltinAttribute attrImpl
   pure { attr := attrImpl }
diff --git a/backends/lean/Aeneas/Tactic/Step/Step.lean b/backends/lean/Aeneas/Tactic/Step/Step.lean
index 2c4312fb2..18f321e2f 100644
--- a/backends/lean/Aeneas/Tactic/Step/Step.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Step.lean
@@ -1579,7 +1579,7 @@ namespace Test
   -/
   /--
   error: unsolved goals
-case hmax
+case h_fail
 ty : UScalarTy
 x y : UScalar ty
 ⊢ ↑x + ↑y ≤ UScalar.max ty
@@ -1589,6 +1589,8 @@ x y : UScalar ty
     x + y ⦃ _ => True ⦄ := by
     step as ⟨ z, h1 ⟩
 
+  #check UScalar.add_spec.step_spec
+
   example {ty} {x y : UScalar ty} (h : x.val + y.val ≤ UScalar.max ty) :
     x + y ⦃ _ => True ⦄ := by
     step as ⟨ z, h1 ⟩
@@ -1623,7 +1625,7 @@ _✝ : z1 = y + 2
 
   /--
   info: Try this:
-  [apply] let* ⟨ z, h1 ⟩ ← UScalar.add_spec
+  [apply] let* ⟨ z, h1 ⟩ ← UScalar.add_spec.step_spec
   -/
   #guard_msgs in
   example {ty} {x y : UScalar ty} (h : x.val + y.val ≤ UScalar.max ty) :
@@ -1646,7 +1648,7 @@ info: example
   set_option linter.unusedTactic false in
   example {ty} {x y : UScalar ty} (h : x.val + y.val ≤ UScalar.max ty) :
     x + y ⦃ z => z.val = x.val + y.val ⦄ := by
-    let* ⟨ z, h1 ⟩ ← UScalar.add_spec
+    let* ⟨ z, h1 ⟩ ← UScalar.add_spec.step_spec
     extract_goal0
     scalar_tac
 
@@ -1671,8 +1673,8 @@ info: example
     (do
       let z1 ← x + y
       z1 + x) ⦃ z => z.val = 2 * x.val + y.val ⦄ := by
-    let* ⟨ z1, h1 ⟩ ← UScalar.add_spec
-    let* ⟨ z2, h2 ⟩ ← UScalar.add_spec
+    let* ⟨ z1, h1 ⟩ ← UScalar.add_spec.step_spec
+    let* ⟨ z2, h2 ⟩ ← UScalar.add_spec.step_spec
     extract_goal0
     scalar_tac
 
@@ -1680,8 +1682,8 @@ info: example
     (do
       let z1 ← x + y
       z1 + x) ⦃ z => z.val = 2 * x.val + y.val ⦄ := by
-    step with UScalar.add_spec as ⟨ z1, h1 ⟩
-    step with UScalar.add_spec as ⟨ z2, h2 ⟩
+    step with UScalar.add_spec.step_spec as ⟨ z1, h1 ⟩
+    step with UScalar.add_spec.step_spec as ⟨ z2, h2 ⟩
     scalar_tac
 
   example {ty} {x y : UScalar ty}
@@ -1700,40 +1702,40 @@ info: example
   example {ty} {x y : UScalar ty}
     (hmax : x.val + y.val ≤ UScalar.max ty) :
     x + y ⦃ z => z.val = x.val + y.val ⦄ := by
-    step? as ⟨ z, h1 ⟩ says step with UScalar.add_spec as ⟨ z, h1 ⟩
+    step? as ⟨ z, h1 ⟩ says step with UScalar.add_spec.step_spec as ⟨ z, h1 ⟩
     scalar_tac
 
   example {ty} {x y : IScalar ty}
     (hmin : IScalar.min ty ≤ x.val + y.val)
     (hmax : x.val + y.val ≤ IScalar.max ty) :
     x + y ⦃ z => z.val = x.val + y.val ⦄ := by
-    step? as ⟨ z, h1 ⟩ says step with IScalar.add_spec as ⟨ z, h1 ⟩
+    step? as ⟨ z, h1 ⟩ says step with IScalar.add_spec.step_spec as ⟨ z, h1 ⟩
     scalar_tac
 
   example {ty} {x y : UScalar ty}
     (hmax : x.val + y.val ≤ UScalar.max ty) :
     x + y ⦃ z => z.val = x.val + y.val ⦄ := by
-    step with UScalar.add_spec as ⟨ z ⟩
+    step with UScalar.add_spec.step_spec as ⟨ z ⟩
     scalar_tac
 
   example {ty} {x y : IScalar ty}
     (hmin : IScalar.min ty ≤ x.val + y.val)
     (hmax : x.val + y.val ≤ IScalar.max ty) :
     x + y ⦃ z => z.val = x.val + y.val ⦄ := by
-    step with IScalar.add_spec as ⟨ z ⟩
+    step with IScalar.add_spec.step_spec as ⟨ z ⟩
     scalar_tac
 
   example {x y : U32}
     (hmax : x.val + y.val ≤ U32.max) :
     x + y ⦃ z => z.val = x.val + y.val ⦄ := by
     -- This spec theorem is suboptimal (compared to `U32.add_spec`), but it is good to check that it works
-    step with UScalar.add_spec as ⟨ z, h1 ⟩
+    step with UScalar.add_spec.step_spec as ⟨ z, h1 ⟩
     scalar_tac
 
   example {x y : U32}
     (hmax : x.val + y.val ≤ U32.max) :
     x + y ⦃ z => z.val = x.val + y.val ⦄ := by
-    step with U32.add_spec as ⟨ z, h1 ⟩
+    step with U32.add_spec.step_spec as ⟨ z, h1 ⟩
     scalar_tac
 
   example {x y : U32}
@@ -1794,7 +1796,7 @@ info: example
     (hmax : x.val + y.val ≤ IScalar.max ty) :
     False ∨ x + y ⦃ z => z.val = x.val + y.val ⦄ := by
     right
-    step? as ⟨ z, h1 ⟩ says step with IScalar.add_spec as ⟨ z, h1 ⟩
+    step? as ⟨ z, h1 ⟩ says step with IScalar.add_spec.step_spec as ⟨ z, h1 ⟩
     scalar_tac
 
   /--
@@ -1870,7 +1872,7 @@ hf : ∀ (x y : U32), ↑x < 10 → ↑y < 10 → f x y ⦃ x✝ => True ⦄
       let tot := x.val + y.val
       x + y ⦃ z => z.val = tot ⦄ := by
       simp
-      step with U32.add_spec
+      step with U32.add_spec.step_spec
       scalar_tac
 
     def add1 (x y : U32) : Std.Result U32 := do
@@ -1906,8 +1908,8 @@ x y : U32
   example (x y : U32) (h : 2 * x.val + 2 * y.val ≤ U32.max) :
     add1 x y ⦃ _ => True ⦄ := by
     rw [add1]
-    step? as ⟨ z1, h ⟩ says step with U32.add_spec as ⟨ z1, h ⟩
-    step? as ⟨ z2, h ⟩ says step with U32.add_spec as ⟨ z2, h ⟩
+    step? as ⟨ z1, h ⟩ says step with U32.add_spec.step_spec as ⟨ z1, h ⟩
+    step? as ⟨ z2, h ⟩ says step with U32.add_spec.step_spec as ⟨ z2, h ⟩
 end Test
 
 namespace Test
@@ -2012,7 +2014,7 @@ _✝ : ↑z = ↑x + y
   -- Test that we properly extract the names from the post-conditions
   /--
   error: unsolved goals
-case hmax
+case h_fail
 x y : U32
 ⊢ ↑x + ↑y ≤ U32.max
 
@@ -2230,8 +2232,8 @@ h1 : ∀ (i : ℕ) (x : i < s.length), s'[i] = 0#u32
     (do let x ← 1#i32 + 2#i32
         let y ← x + x
         ok y) (fun z => z.val == 6) := by
-    step with I32.add_spec
-    step with I32.add_spec
+    step with I32.add_spec.step_spec
+    step with I32.add_spec.step_spec
     simp [*]
 
   -- test lifting an assumption
diff --git a/backends/lean/Aeneas/Tactic/Step/StepStar.lean b/backends/lean/Aeneas/Tactic/Step/StepStar.lean
index e1313f0be..bfbfd9312 100644
--- a/backends/lean/Aeneas/Tactic/Step/StepStar.lean
+++ b/backends/lean/Aeneas/Tactic/Step/StepStar.lean
@@ -928,9 +928,9 @@ def add1 (x0 x1 : U32) : Std.Result U32 := do
 /--
 info: Try this:
 
-  [apply]     let* ⟨ x2, x2_post ⟩ ← U32.add_spec
-    let* ⟨ x3, x3_post ⟩ ← U32.add_spec
-    let* ⟨ ⟩ ← U32.add_spec
+  [apply]     let* ⟨ x2, x2_post ⟩ ← U32.add_spec.step_spec
+    let* ⟨ x3, x3_post ⟩ ← U32.add_spec.step_spec
+    let* ⟨ ⟩ ← U32.add_spec.step_spec
 -/
 #guard_msgs in
 example (x y : U32) (h : 2 * x.val + 2 * y.val + 4 ≤ U32.max) :
@@ -941,9 +941,9 @@ example (x y : U32) (h : 2 * x.val + 2 * y.val + 4 ≤ U32.max) :
 /--
 info: Try this:
 
-  [apply]     let* ⟨ x2, x2_post ⟩ ← [ +scalarTac -grind ] U32.add_spec
-    let* ⟨ x3, x3_post ⟩ ← [ +scalarTac -grind ] U32.add_spec
-    let* ⟨ ⟩ ← [ +scalarTac -grind ] U32.add_spec
+  [apply]     let* ⟨ x2, x2_post ⟩ ← [ +scalarTac -grind ] U32.add_spec.step_spec
+    let* ⟨ x3, x3_post ⟩ ← [ +scalarTac -grind ] U32.add_spec.step_spec
+    let* ⟨ ⟩ ← [ +scalarTac -grind ] U32.add_spec.step_spec
 -/
 #guard_msgs in
 example (x y : U32) (h : 2 * x.val + 2 * y.val + 4 ≤ U32.max) :
@@ -972,8 +972,8 @@ example (x y : U32) (h : 2 * x.val + 2 * y.val + 4 ≤ U32.max) :
 /--
 info: Try this:
 
-  [apply]     let* ⟨ x2, x2_post ⟩ ← U32.add_spec
-    let* ⟨ x3, x3_post ⟩ ← U32.add_spec
+  [apply]     let* ⟨ x2, x2_post ⟩ ← U32.add_spec.step_spec
+    let* ⟨ x3, x3_post ⟩ ← U32.add_spec.step_spec
 ---
 error: unsolved goals
 x y : U32
@@ -996,9 +996,9 @@ example (x y : U32) (h : 2 * x.val + 2 * y.val + 4 ≤ U32.max) :
 info: Try this:
 
   [apply]     simp only [step_simps]
-    let* ⟨ x2, x2_post ⟩ ← U32.add_spec
-    let* ⟨ x3, x3_post ⟩ ← U32.add_spec
-    let* ⟨ z, z_post ⟩ ← U32.add_spec
+    let* ⟨ x2, x2_post ⟩ ← U32.add_spec.step_spec
+    let* ⟨ x3, x3_post ⟩ ← U32.add_spec.step_spec
+    let* ⟨ z, z_post ⟩ ← U32.add_spec.step_spec
     agrind
 -/
 #guard_msgs in
@@ -1021,11 +1021,11 @@ def add2 (b : Bool) (x0 x1 : U32) : Std.Result U32 := do
 info: Try this:
 
   [apply]     spec_split
-    · let* ⟨ x2, x2_post ⟩ ← U32.add_spec
-      let* ⟨ x3, x3_post ⟩ ← U32.add_spec
-      let* ⟨ ⟩ ← U32.add_spec
-    · let* ⟨ y, y_post ⟩ ← U32.add_spec
-      let* ⟨ ⟩ ← U32.add_spec
+    · let* ⟨ x2, x2_post ⟩ ← U32.add_spec.step_spec
+      let* ⟨ x3, x3_post ⟩ ← U32.add_spec.step_spec
+      let* ⟨ ⟩ ← U32.add_spec.step_spec
+    · let* ⟨ y, y_post ⟩ ← U32.add_spec.step_spec
+      let* ⟨ ⟩ ← U32.add_spec.step_spec
 -/
 #guard_msgs in
 example b (x y : U32) (h : 2 * x.val + 2 * y.val + 4 ≤ U32.max) :
@@ -1037,10 +1037,10 @@ example b (x y : U32) (h : 2 * x.val + 2 * y.val + 4 ≤ U32.max) :
 info: Try this:
 
   [apply]     spec_split
-    · let* ⟨ x2, x2_post ⟩ ← U32.add_spec
-      let* ⟨ x3, x3_post ⟩ ← U32.add_spec
-    · let* ⟨ y, y_post ⟩ ← U32.add_spec
-      let* ⟨ ⟩ ← U32.add_spec
+    · let* ⟨ x2, x2_post ⟩ ← U32.add_spec.step_spec
+      let* ⟨ x3, x3_post ⟩ ← U32.add_spec.step_spec
+    · let* ⟨ y, y_post ⟩ ← U32.add_spec.step_spec
+      let* ⟨ ⟩ ← U32.add_spec.step_spec
 ---
 error: unsolved goals
 b : Bool
@@ -1065,25 +1065,25 @@ example b (x y : U32) (h : 2 * x.val + 2 * y.val + 4 ≤ U32.max) :
 info: Try this:
 
   [apply]     spec_split
-    · let* ⟨ x2, x2_post ⟩ ← U32.add_spec
+    · let* ⟨ x2, x2_post ⟩ ← U32.add_spec.step_spec
       · sorry
-      let* ⟨ x3, x3_post ⟩ ← U32.add_spec
+      let* ⟨ x3, x3_post ⟩ ← U32.add_spec.step_spec
       · sorry
-      let* ⟨ ⟩ ← U32.add_spec
+      let* ⟨ ⟩ ← U32.add_spec.step_spec
       · sorry
-    · let* ⟨ y, y_post ⟩ ← U32.add_spec
+    · let* ⟨ y, y_post ⟩ ← U32.add_spec.step_spec
       · sorry
-      let* ⟨ ⟩ ← U32.add_spec
+      let* ⟨ ⟩ ← U32.add_spec.step_spec
       · sorry
 ---
 error: unsolved goals
-case hmax
+case h_fail
 b : Bool
 x y : U32
 h✝ : b = true
 ⊢ ↑x + ↑y ≤ U32.max
 
-case hmax
+case h_fail
 b : Bool
 x y : U32
 h✝ : b = true
@@ -1092,7 +1092,7 @@ _ : [> let x2 ← x + y <]
 x2_post : ↑x2 = ↑x + ↑y
 ⊢ ↑x2 + ↑x2 ≤ U32.max
 
-case hmax
+case h_fail
 b : Bool
 x y : U32
 h✝ : b = true
@@ -1104,13 +1104,13 @@ _ : [> let x3 ← x2 + x2 <]
 x3_post : ↑x3 = ↑x2 + ↑x2
 ⊢ ↑x3 + ↑4#u32 ≤ U32.max
 
-case hmax
+case h_fail
 b : Bool
 x y : U32
 h✝ : ¬b = true
 ⊢ ↑x + ↑y ≤ U32.max
 
-case hmax
+case h_fail
 b : Bool
 x y✝ : U32
 h✝ : ¬b = true
@@ -1130,9 +1130,9 @@ example b (x y : U32) :
 /--
 info: Try this:
 
-  [apply]     let* ⟨ x2, x2_post ⟩ ← U32.add_spec
-    let* ⟨ x3, x3_post ⟩ ← U32.add_spec
-    let* ⟨ _, _ ⟩ ← U32.add_spec
+  [apply]     let* ⟨ x2, x2_post ⟩ ← U32.add_spec.step_spec
+    let* ⟨ x3, x3_post ⟩ ← U32.add_spec.step_spec
+    let* ⟨ _, _ ⟩ ← U32.add_spec.step_spec
     sorry
 ---
 error: unsolved goals
@@ -1304,7 +1304,7 @@ example (a b : U32) (h : a = b) (hbnd : a.val + b.val ≤ U32.max) :
 info: Try this:
 
   [apply]     spec_split
-    · let* ⟨ c, c_post ⟩ ← U32.add_spec
+    · let* ⟨ c, c_post ⟩ ← U32.add_spec.step_spec
       agrind
     · agrind
 -/
@@ -1321,7 +1321,7 @@ example (a b : U32) (h : a = b) (hbnd : a.val + b.val ≤ U32.max) :
     grindContradictionFn a b ⦃ c => c.val = a.val + b.val ⦄ := by
   unfold grindContradictionFn
   spec_split
-  · let* ⟨ c, c_post ⟩ ← U32.add_spec
+  · let* ⟨ c, c_post ⟩ ← U32.add_spec.step_spec
     agrind
   · agrind
 
diff --git a/backends/lean/Aeneas/Tactic/Step/Tests.lean b/backends/lean/Aeneas/Tactic/Step/Tests.lean
index 017241bb2..049d95f9e 100644
--- a/backends/lean/Aeneas/Tactic/Step/Tests.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Tests.lean
@@ -4,3 +4,5 @@ import Aeneas.Tactic.Step.Tests.MaxRecDepthMetavar
 import Aeneas.Tactic.Step.Tests.MvcgenSpec
 import Aeneas.Tactic.Step.Tests.TupleDestruct
 import Aeneas.Tactic.Step.Tests.UncurryBind
+import Aeneas.Tactic.Step.Tests.MvcgenSpec
+import Aeneas.Tactic.Step.Tests.SpecPartial
diff --git a/backends/lean/Aeneas/Tactic/Step/Tests/HigherOrder.lean b/backends/lean/Aeneas/Tactic/Step/Tests/HigherOrder.lean
index 250a8e426..431b8b390 100644
--- a/backends/lean/Aeneas/Tactic/Step/Tests/HigherOrder.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Tests/HigherOrder.lean
@@ -19,7 +19,7 @@ info: Try this:
 
   [apply]     let* ⟨ y, y_post ⟩ ← [ +inferPost ] applyF_spec
     case hf =>
-      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec
+      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec.step_spec
       agrind
     agrind
 ---
@@ -51,10 +51,10 @@ info: Try this:
 
   [apply]     let* ⟨ ab, ab_post1, ab_post2 ⟩ ← [ +inferPost ] callPair_spec
     case hf =>
-      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec
+      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec.step_spec
       agrind
     case hg =>
-      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec
+      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec.step_spec
       agrind
     agrind
 ---
@@ -85,11 +85,11 @@ info: Try this:
 
   [apply]     let* ⟨ y, y_post ⟩ ← [ +inferPost ] callFThenG_spec
     case hf =>
-      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec
+      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec.step_spec
       agrind
     case hg =>
       intros y _
-      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec
+      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec.step_spec
       agrind
     agrind
 ---
@@ -111,7 +111,7 @@ info: Try this:
   [apply]     let* ⟨ y, y_post1, y_post2 ⟩ ← [ +inferPost ] Slice.mapM_spec
     case hf =>
       intros i hi
-      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec
+      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec.step_spec
       agrind
     agrind
 ---
@@ -136,7 +136,7 @@ example (s : Slice U32) (h : ∀ i (hi : i < s.len), s[i] < U32.max) :
   let* ⟨ y, y_post1, y_post2 ⟩ ← [ +inferPost ] Slice.mapM_spec
   case hf =>
     intros i hi
-    let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec
+    let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec.step_spec
     agrind (instances := 20) (ematch := 1)
   agrind (instances := 40) (ematch := 2)
 
@@ -151,12 +151,12 @@ info: Try this:
   [apply]     let* ⟨ y, y_post1, y_post2 ⟩ ← [ +inferPost ] Slice.mapM_spec
     case hf =>
       intros i hi
-      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec
+      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec.step_spec
       agrind
     let* ⟨ z, z_post1, z_post2 ⟩ ← [ +inferPost ] Slice.mapM_spec
     case hf =>
       intros i hi
-      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.mul_spec
+      let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.mul_spec.step_spec
       agrind
     agrind
 ---
@@ -182,12 +182,12 @@ example (s : Slice U32) (h : ∀ i (hi : i < s.len), (s[i] + 1) * (s[i] + 1) ≤
   let* ⟨ y, y_post1, y_post2 ⟩ ← [ +inferPost ] Slice.mapM_spec
   case hf =>
     intros i hi
-    let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec
+    let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.add_spec.step_spec
     agrind (instances := 20) (ematch := 1)
   let* ⟨ z, z_post1, z_post2 ⟩ ← [ +inferPost ] Slice.mapM_spec
   case hf =>
     intros i hi
-    let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.mul_spec
+    let* ⟨ _, _ ⟩ ← [ +inferPost ] U32.mul_spec.step_spec
     agrind (instances := 20) (ematch := 1)
   agrind (instances := 100) (ematch := 2)
 
diff --git a/backends/lean/Aeneas/Tactic/Step/Tests/MvcgenSpec.lean b/backends/lean/Aeneas/Tactic/Step/Tests/MvcgenSpec.lean
index ab18dc289..eaa2fe62e 100644
--- a/backends/lean/Aeneas/Tactic/Step/Tests/MvcgenSpec.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Tests/MvcgenSpec.lean
@@ -28,4 +28,4 @@ example (arr : Array U8 25#usize) (i : Usize) (a : U8) (hi : i < arr.length) :
     ⦃ ⌜ True ⌝ ⦄
       Array.update arr i a
     ⦃ ⇓ r => ⌜ r.get? i = some a ⌝ ⦄ := by
-  mvcgen; grind
+  mvcgen <;> grind
diff --git a/backends/lean/Aeneas/Tactic/Step/Tests/SpecPartial.lean b/backends/lean/Aeneas/Tactic/Step/Tests/SpecPartial.lean
new file mode 100644
index 000000000..82fefef3a
--- /dev/null
+++ b/backends/lean/Aeneas/Tactic/Step/Tests/SpecPartial.lean
@@ -0,0 +1,137 @@
+import Aeneas.Std.Scalar
+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`.
+-/
+
+namespace Aeneas.Step.SpecPartialTests
+
+open Aeneas Aeneas.Std Result Std.Do WP
+
+set_option mvcgen.warning false
+
+/- ## Mock division: panics when dividing by zero, but does not specify `Error`. -/
+
+opaque myDiv (x y : U32) : Result U32
+
+@[step]
+axiom myDiv_partialSpec (x y : U32) :
+  partialSpec (myDiv x y)
+    (fun z => z.val = x.val / y.val)
+    (fun _ => y.val = 0)
+    False
+
+/-- step* -/
+example (x y : U32) (h : y.val ≠ 0) :
+    spec (myDiv x y) (fun z => z.val = x.val / y.val) := by
+  step*
+
+/-- mvcgen: total correctness -/
+example (x y : U32) (h : y.val ≠ 0) :
+    ⦃ ⌜ True ⌝ ⦄ (myDiv x y) ⦃ ⇓ z => ⌜ z.val = x.val / y.val ⌝ ⦄ := by
+  mvcgen
+
+/-- mvcgen: partial correctness -/
+example (x y : U32) :
+    ⦃ ⌜ True ⌝ ⦄ (myDiv x y) ⦃ ⇓? z => ⌜ z.val = x.val / y.val ⌝ ⦄ := by
+  mvcgen
+
+/--
+info: Aeneas.Step.SpecPartialTests.myDiv_partialSpec.step_spec (x y : U32) (h_fail : ¬↑y = 0) :
+  myDiv x y ⦃ z => ↑z = ↑x / ↑y ⦄
+-/
+#guard_msgs in
+#check myDiv_partialSpec.step_spec
+
+/--
+info: Aeneas.Step.SpecPartialTests.myDiv_partialSpec.mvcgen_spec (x y : U32) (Q : PostCond U32 Result.postShape)
+  (h_ok : ∀ (r : U32), ↑r = ↑x / ↑y → willYield r Q) (h_fail : ∀ (e : Error), ↑y = 0 → willFail e Q) :
+  ⦃⌜True⌝⦄ myDiv x y ⦃Q⦄
+-/
+#guard_msgs in
+#check myDiv_partialSpec.mvcgen_spec
+
+/- ## Mock addition: panics on overflow, specifies `Error.integerOverflow` -/
+
+opaque myAdd (x y : U32) : Result U32
+
+@[step]
+axiom myAdd_partialSpec (x y : U32) :
+  partialSpec (myAdd x y)
+    (fun z => z.val = x.val + y.val)
+    (fun | .integerOverflow => x.val + y.val > U32.max | _ => False)
+    False
+
+-- Pushing `¬` through `>` should produce `≤`.
+/--
+info: Aeneas.Step.SpecPartialTests.myAdd_partialSpec.step_spec (x y : U32) (h_fail : ↑x + ↑y ≤ U32.max) :
+  myAdd x y ⦃ z => ↑z = ↑x + ↑y ⦄
+-/
+#guard_msgs in
+#check myAdd_partialSpec.step_spec
+
+/--
+info: Aeneas.Step.SpecPartialTests.myAdd_partialSpec.mvcgen_spec (x y : U32) (Q : PostCond U32 Result.postShape)
+  (h_ok : ∀ (r : U32), ↑r = ↑x + ↑y → willYield r Q) (h_fail : U32.max < ↑x + ↑y → willFail Error.integerOverflow Q) :
+  ⦃⌜True⌝⦄ myAdd x y ⦃Q⦄
+-/
+#guard_msgs in
+#check myAdd_partialSpec.mvcgen_spec
+
+
+/- ## Mock signed add: panics on over- and underflow -/
+
+opaque myAddSigned (x y : I32) : Result I32
+
+@[step]
+axiom myAddSigned_partialSpec (x y : I32) :
+  partialSpec (myAddSigned x y)
+    (fun z => z.val = x.val + y.val)
+    (fun | .integerOverflow => (x.val + y.val > I32.max ∨ x.val + y.val < I32.min) | _ => False)
+    False
+
+/--
+info: Aeneas.Step.SpecPartialTests.myAddSigned_partialSpec.step_spec (x y : I32) (h_fail_1 : ↑x + ↑y ≤ I32.max)
+  (h_fail_2 : I32.min ≤ ↑x + ↑y) : myAddSigned x y ⦃ z => ↑z = ↑x + ↑y ⦄
+-/
+#guard_msgs in
+#check myAddSigned_partialSpec.step_spec
+
+/--
+info: Aeneas.Step.SpecPartialTests.myAddSigned_partialSpec.mvcgen_spec (x y : I32) (Q : PostCond I32 Result.postShape)
+  (h_ok : ∀ (r : I32), ↑r = ↑x + ↑y → willYield r Q) (h_fail_1 : I32.max < ↑x + ↑y → willFail Error.integerOverflow Q)
+  (h_fail_2 : ↑x + ↑y < I32.min → willFail Error.integerOverflow Q) : ⦃⌜True⌝⦄ myAddSigned x y ⦃Q⦄
+-/
+#guard_msgs in
+#check myAddSigned_partialSpec.mvcgen_spec
+
+
+/- ## Mock infinte loop: always diverges -/
+
+opaque infiniteLoop : Result Unit
+
+@[step]
+axiom infiniteLoop_partialSpec :
+  partialSpec infiniteLoop
+    (fun _ => False)
+    (fun _ => False)
+    True
+
+/--
+info: Aeneas.Step.SpecPartialTests.infiniteLoop_partialSpec.step_spec (h_div : False) : infiniteLoop ⦃ x✝ => False ⦄
+-/
+#guard_msgs in
+#check infiniteLoop_partialSpec.step_spec
+
+/--
+info: Aeneas.Step.SpecPartialTests.infiniteLoop_partialSpec.mvcgen_spec (Q : PostCond Unit Result.postShape)
+  (h_div : willDiverge Q) : ⦃⌜True⌝⦄ infiniteLoop ⦃Q⦄
+-/
+#guard_msgs in
+#check infiniteLoop_partialSpec.mvcgen_spec
+
+end Aeneas.Step.SpecPartialTests
diff --git a/flake.nix b/flake.nix
index 9960ffb1a..87efb9eef 100644
--- a/flake.nix
+++ b/flake.nix
@@ -208,6 +208,11 @@
             ppx_deriving
           ]);
         };
+        
+        # Vendor all cargo dependencies for the hax_specs test crate
+        haxSpecsVendor = pkgs.rustPlatform.importCargoLock {
+          lockFile = ./tests/src/hax_specs/Cargo.lock;
+        };
 
         # Run the translation on various files.
         # Make sure we don't need to recompile the package whenever we make
@@ -234,6 +239,19 @@
             export RUSTC_CMD=rustc
             export CARGO_CMD=cargo
 
+            # Configure cargo to use pre-vendored dependencies
+            for dir in tests/src/hax_specs tests/src/hax_specs_step; do
+              mkdir -p "$dir/.cargo"
+              cat > "$dir/.cargo/config.toml" <<CARGOEOF
+            [net]
+            offline = true
+            [source.crates-io]
+            replace-with = "vendored-sources"
+            [source.vendored-sources]
+            directory = "${haxSpecsVendor}"
+            CARGOEOF
+            done
+
             # Copy the tests
             cp -r tests tests-copy
             make clean-generated-aeneas
diff --git a/src/Config.ml b/src/Config.ml
index cb919aeb1..e942f7cef 100644
--- a/src/Config.ml
+++ b/src/Config.ml
@@ -26,6 +26,45 @@ let set_backend (b : string) : unit =
          belonging to the proper set *)
       raise (Failure "Unexpected")
 
+(** {1 Specs config} *)
+
+type spec_source = Hax
+type spec_backend = Mvcgen | Step
+type spec_config = spec_source * spec_backend
+
+let spec_config_options = [ "hax"; "hax-step" ]
+
+(** Utility to compute a spec source from an input parameter *)
+let spec_config_of_string (s : string) : spec_config option =
+  match s with
+  | "hax" | "Hax" -> Some (Hax, Mvcgen)
+  | "hax-step" | "Hax-Step" -> Some (Hax, Step)
+  | _ -> None
+
+(** The spec source requested via [-specs] *)
+let opt_spec_config : spec_config option ref = ref None
+
+let set_spec_config (s : string) : unit =
+  match spec_config_of_string s with
+  | Some s -> opt_spec_config := Some s
+  | None ->
+      (* We shouldn't get there: the string should have been checked as
+         belonging to the proper set *)
+      raise (Failure "Unexpected")
+
+(** Returns [true] if the config for specs is enabled. *)
+let spec_config_enabled () = Option.is_some !opt_spec_config
+
+(** Returns [true] if the saved config for specs uses Hax annotations as a
+    source *)
+let spec_config_is_hax () =
+  match !opt_spec_config with
+  | Some (Hax, _) -> true
+  | _ -> false
+
+(** The spec backend selected via [-specs], if specs are enabled. *)
+let spec_backend () : spec_backend option = Option.map snd !opt_spec_config
+
 (** Specify the namespace of the extract code.
 
     For instance, if the crate name is [foo] the namespace used for the
@@ -598,3 +637,14 @@ let max_recdepth = ref 2048
 (** If [false], evaluate [drop(p)] as [p := bottom]. Otherwise, evaluate it as a
     no-op (which means that we do not borrow-check the drops). *)
 let drop_as_no_op = ref true
+
+(** For Lean only: disable the Rust core library overrides defined in
+    [ExtractBuiltinLean.ml].
+
+    With this flag, references to items such as [core::clone::Clone<[T; N]>] are
+    extracted using the standard name-mangling scheme rather than the hand-tuned
+    names like [core.array.CloneArray.clone], and the associated shape overrides
+    ([keep_params], [can_fail], etc.) are ignored. This is useful when
+    extracting against a separate Lean library that mirrors the Rust core API
+    under the standard names. *)
+let core_models_lib = ref false
diff --git a/src/Main.ml b/src/Main.ml
index 8073dba6b..dd7196968 100644
--- a/src/Main.ml
+++ b/src/Main.ml
@@ -136,6 +136,10 @@ let () =
       ( "-lean-default-lakefile",
         Arg.Clear lean_gen_lakefile,
         " Generate a default lakefile.lean (Lean only)" );
+      ( "-specs",
+        Arg.Symbol (spec_config_options, set_spec_config),
+        " Gather and emit specs from the given source. Available: "
+        ^ String.concat ", " spec_config_options );
       ( "-emit-json",
         Arg.Set emit_json,
         " Emit a translation.json file alongside the Lean files (Lean only)" );
@@ -211,6 +215,14 @@ let () =
          collisions with field projectors. Example: the `len` method in `impl \
          Struct { fn len(&self) -> usize { ... } }` would be named \
          `Struct.impl.len`." );
+      ( "-core-models-lib",
+        Arg.Set core_models_lib,
+        " For Lean: disable the Rust core library overrides from \
+         ExtractBuiltinLean.ml. Items like the `Clone` impl for arrays are \
+         extracted using the standard name-mangling scheme rather than \
+         hand-tuned names such as `core.array.CloneArray.clone`, and the \
+         associated shape overrides (keep_params, can_fail, etc.) are ignored."
+      );
       ( "-all-computable",
         Arg.Set all_computable,
         " For Lean: do not insert `noncomputable section` at the top of the \
@@ -457,6 +469,9 @@ let () =
   if !lean_gen_lakefile && not (backend () = Lean) then
     fail_with_error
       "The -lean-default-lakefile option is valid only for the Lean backend";
+  if !core_models_lib && not (backend () = Lean) then
+    fail_with_error
+      "The -core-models-lib option is valid only for the Lean backend";
   if !set_max_heartbeats && not (backend () = Lean) then
     fail_with_error
       "The -max-heartbeats option is valid only for the Lean backend";
@@ -465,6 +480,8 @@ let () =
       "The -max-recdepth option is valid only for the Lean backend";
   if !emit_json && not (backend () = Lean) then
     fail_with_error "The -emit-json option is valid only for the Lean backend";
+  if Option.is_some !opt_spec_config && not (backend () = Lean) then
+    fail_with_error "The -specs option is valid only for the Lean backend";
 
   check_arg_implies !diagnose_detailed "-diagnose-detailed"
     !diagnose_micro_passes "-diagnose-micro-passes";
@@ -597,8 +614,15 @@ let () =
       (* Print the external definitions which are not listed in the builtin functions *)
       if !print_unknown_externals then (
         let open TranslateCore in
-        let { type_decls; fun_decls; global_decls; trait_decls; trait_impls; _ }
-            =
+        let ({
+               type_decls;
+               fun_decls;
+               global_decls;
+               trait_decls;
+               trait_impls;
+               _;
+             }
+              : crate) =
           m
         in
         (* Filter the definitions *)
diff --git a/src/PrePasses.ml b/src/PrePasses.ml
index b613aba1b..ce7122cb0 100644
--- a/src/PrePasses.ml
+++ b/src/PrePasses.ml
@@ -1220,6 +1220,135 @@ let filter_marker_traits (crate : crate) : crate =
     in
     visitor#visit_crate () crate
 
+(** Under [-core-models-lib], remove the [Eq] marker method (named
+    [assert_fields_are_eq] in current rustc, formerly
+    [assert_receiver_is_total_eq]) from the [core::cmp::Eq] trait declaration,
+    from any impls of [Eq], and drop the corresponding function declarations.
+    This is a Rust-only, [#[doc(hidden)]] method with an empty default body that
+    Aeneas's own standard library handles via a hand-tuned override; an external
+    library like [core_models] doesn't model it, so emitting an impl field for
+    it would not typecheck against [core_models]'s [Eq] structure. *)
+let filter_eq_assert_fields_method (crate : crate) : crate =
+  if not !Config.core_models_lib then crate
+  else
+    let mctx = NameMatcher.ctx_from_crate crate in
+    let pat = NameMatcher.parse_pattern "core::cmp::Eq" in
+    let match_config =
+      {
+        NameMatcher.map_vars_to_vars = true;
+        match_with_trait_decl_refs = Config.match_patterns_with_trait_decl_refs;
+      }
+    in
+    let eq_id =
+      TraitDeclId.Map.fold
+        (fun id (decl : trait_decl) acc ->
+          if
+            acc = None
+            && NameMatcher.match_name mctx match_config pat decl.item_meta.name
+          then Some id
+          else acc)
+        crate.trait_decls None
+    in
+    match eq_id with
+    | None -> crate
+    | Some eq_id ->
+        (* The method is named [assert_fields_are_eq] in current rustc; older
+           versions called it [assert_receiver_is_total_eq]. Match either so the
+           pass is robust across charon updates. *)
+        let method_names =
+          [ "assert_fields_are_eq"; "assert_receiver_is_total_eq" ]
+        in
+        let eq_decl = TraitDeclId.Map.find eq_id crate.trait_decls in
+        let filtered_method_ids =
+          TraitMethodId.Map.fold
+            (fun mid (m : trait_method binder) acc ->
+              if List.mem m.binder_value.name method_names then
+                TraitMethodId.Set.add mid acc
+              else acc)
+            eq_decl.methods TraitMethodId.Set.empty
+        in
+        if TraitMethodId.Set.is_empty filtered_method_ids then crate
+        else
+          let trait_decls =
+            TraitDeclId.Map.update eq_id
+              (function
+                | None -> None
+                | Some (d : trait_decl) ->
+                    Some
+                      {
+                        d with
+                        methods =
+                          TraitMethodId.Map.filter
+                            (fun mid _ ->
+                              not
+                                (TraitMethodId.Set.mem mid filtered_method_ids))
+                            d.methods;
+                      })
+              crate.trait_decls
+          in
+          (* Collect fun_decl_ids backing the filtered methods of every [Eq]
+             trait impl, and strip those methods from the impl's method map. *)
+          let dropped_fun_decl_ids = ref FunDeclId.Set.empty in
+          let trait_impls =
+            TraitImplId.Map.map
+              (fun (impl : trait_impl) ->
+                if impl.impl_trait.id <> eq_id then impl
+                else
+                  let methods =
+                    TraitMethodId.Map.filter
+                      (fun mid (m : fun_decl_ref binder) ->
+                        if TraitMethodId.Set.mem mid filtered_method_ids then begin
+                          dropped_fun_decl_ids :=
+                            FunDeclId.Set.add m.binder_value.id
+                              !dropped_fun_decl_ids;
+                          false
+                        end
+                        else true)
+                      impl.methods
+                  in
+                  { impl with methods })
+              crate.trait_impls
+          in
+          let fun_decls =
+            FunDeclId.Map.filter
+              (fun id _ -> not (FunDeclId.Set.mem id !dropped_fun_decl_ids))
+              crate.fun_decls
+          in
+          let declarations =
+            List.filter_map
+              (fun (g : declaration_group) ->
+                match g with
+                | FunGroup (NonRecGroup id) ->
+                    if FunDeclId.Set.mem id !dropped_fun_decl_ids then None
+                    else Some g
+                | FunGroup (RecGroup ids) ->
+                    let ids =
+                      List.filter
+                        (fun id ->
+                          not (FunDeclId.Set.mem id !dropped_fun_decl_ids))
+                        ids
+                    in
+                    if ids = [] then None else Some (FunGroup (RecGroup ids))
+                | MixedGroup g -> (
+                    let is_dropped (id : item_id) =
+                      match id with
+                      | IdFun id -> FunDeclId.Set.mem id !dropped_fun_decl_ids
+                      | _ -> false
+                    in
+                    match g with
+                    | NonRecGroup id ->
+                        if is_dropped id then None else Some (MixedGroup g)
+                    | RecGroup ids ->
+                        let ids =
+                          List.filter (fun id -> not (is_dropped id)) ids
+                        in
+                        if ids = [] then None
+                        else Some (MixedGroup (RecGroup ids)))
+                | _ -> Some g)
+              crate.declarations
+          in
+          { crate with trait_decls; trait_impls; fun_decls; declarations }
+
 (* Remove the type aliases from the type declarations and declaration groups *)
 let filter_type_aliases (crate : crate) : crate =
   let type_decl_is_alias (ty : type_decl) =
@@ -2265,6 +2394,185 @@ let fix_closure_lifetimes (crate : crate) (f : fun_decl) : fun_decl =
           f
       | _, _ -> f)
 
+(** Drop items marked with hax's [late_skip] attribute.
+
+    Hax annotates several internal helpers — the [const _: () = { … }] wrappers
+    around its decoration functions, the [fn future] helper it inserts inside
+    every [ensures] block, … — with
+    [#[_hax::json("{\"ItemStatus\":{\"Included\":{\"late_skip\":true}}}")]]. The
+    marker tells consumers "this item is hax-internal, don't include it in the
+    extracted output". This pass acts on that marker by filtering every
+    top-level decl list of the {b LLBC} crate, before Pure translation runs —
+    that way translation, spec/proof-obligation production and extraction all
+    see a consistent crate with no late_skip items.
+
+    The [_hax::json] payload is parsed via {!HaxAttributes.parse_attr}; this
+    module just decides whether each item should be kept. *)
+module HaxLateSkipFilterPrePass = struct
+  module A = LlbcAst
+  module T = Types
+
+  (** [true] iff the item should be dropped: it carries [late_skip] and is NOT
+      also a decoration fn (i.e. doesn't carry a [Uid]). Decoration fns have
+      [late_skip + Uid] but are consumed by {!HaxProducer.produce} *)
+  let drop_item (attr_info : Charon.Meta.attr_info) : bool =
+    let payloads =
+      List.filter_map HaxAttributes.parse_attr attr_info.attributes
+    in
+    let has_late_skip = List.mem HaxAttributes.Late_skip payloads in
+    let has_uid =
+      List.exists
+        (function
+          | HaxAttributes.Uid _ -> true
+          | _ -> false)
+        payloads
+    in
+    has_late_skip && not has_uid
+
+  let is_late_skip_fun (decls : A.fun_decl A.FunDeclId.Map.t)
+      (id : A.FunDeclId.id) : bool =
+    match A.FunDeclId.Map.find_opt id decls with
+    | None -> false
+    | Some d -> drop_item d.item_meta.attr_info
+
+  let is_late_skip_global (decls : A.global_decl A.GlobalDeclId.Map.t)
+      (id : A.GlobalDeclId.id) : bool =
+    match A.GlobalDeclId.Map.find_opt id decls with
+    | None -> false
+    | Some d -> drop_item d.item_meta.attr_info
+
+  let is_late_skip_type (decls : T.type_decl T.TypeDeclId.Map.t)
+      (id : T.TypeDeclId.id) : bool =
+    match T.TypeDeclId.Map.find_opt id decls with
+    | None -> false
+    | Some d -> drop_item d.item_meta.attr_info
+
+  let is_late_skip_trait_decl (decls : A.trait_decl T.TraitDeclId.Map.t)
+      (id : T.TraitDeclId.id) : bool =
+    match T.TraitDeclId.Map.find_opt id decls with
+    | None -> false
+    | Some d -> drop_item d.item_meta.attr_info
+
+  let is_late_skip_trait_impl (decls : A.trait_impl T.TraitImplId.Map.t)
+      (id : T.TraitImplId.id) : bool =
+    match T.TraitImplId.Map.find_opt id decls with
+    | None -> false
+    | Some d -> drop_item d.item_meta.attr_info
+
+  (** Filter the ids inside one [g_declaration_group]. Returns [None] if the
+      group becomes empty. *)
+  let filter_group (is_dropped : 'id -> bool) (g : 'id A.g_declaration_group) :
+      'id A.g_declaration_group option =
+    match g with
+    | NonRecGroup id -> if is_dropped id then None else Some (NonRecGroup id)
+    | RecGroup ids -> (
+        match List.filter (fun id -> not (is_dropped id)) ids with
+        | [] -> None
+        | xs -> Some (RecGroup xs))
+
+  let filter_declaration (crate : A.crate) (d : A.declaration_group) :
+      A.declaration_group option =
+    let wrap ctor g = Option.map ctor g in
+    match d with
+    | FunGroup g ->
+        wrap
+          (fun g -> A.FunGroup g)
+          (filter_group (is_late_skip_fun crate.fun_decls) g)
+    | GlobalGroup g ->
+        wrap
+          (fun g -> A.GlobalGroup g)
+          (filter_group (is_late_skip_global crate.global_decls) g)
+    | TypeGroup g ->
+        wrap
+          (fun g -> A.TypeGroup g)
+          (filter_group (is_late_skip_type crate.type_decls) g)
+    | TraitDeclGroup g ->
+        wrap
+          (fun g -> A.TraitDeclGroup g)
+          (filter_group (is_late_skip_trait_decl crate.trait_decls) g)
+    | TraitImplGroup g ->
+        wrap
+          (fun g -> A.TraitImplGroup g)
+          (filter_group (is_late_skip_trait_impl crate.trait_impls) g)
+    | MixedGroup g ->
+        (* A mixed (mutually-recursive, cross-kind) group: dispatch each item to
+           the per-kind check, so a late_skip item buried in such a group is
+           dropped from the declaration list too (keeping it consistent with the
+           filtered [crate.*_decls] maps). *)
+        let is_late_skip_item (id : item_id) : bool =
+          match id with
+          | IdFun id -> is_late_skip_fun crate.fun_decls id
+          | IdGlobal id -> is_late_skip_global crate.global_decls id
+          | IdType id -> is_late_skip_type crate.type_decls id
+          | IdTraitDecl id -> is_late_skip_trait_decl crate.trait_decls id
+          | IdTraitImpl id -> is_late_skip_trait_impl crate.trait_impls id
+        in
+        wrap (fun g -> A.MixedGroup g) (filter_group is_late_skip_item g)
+
+  (** Run the pass on an LLBC crate. *)
+  let run (crate : A.crate) : A.crate =
+    if not (Config.spec_config_is_hax ()) then crate
+    else
+      let n_funs_before = A.FunDeclId.Map.cardinal crate.fun_decls in
+      let n_globals_before = A.GlobalDeclId.Map.cardinal crate.global_decls in
+      let n_types_before = T.TypeDeclId.Map.cardinal crate.type_decls in
+      let n_decls_before = List.length crate.declarations in
+      let fun_decls =
+        A.FunDeclId.Map.filter
+          (fun _ (d : A.fun_decl) -> not (drop_item d.item_meta.attr_info))
+          crate.fun_decls
+      in
+      let global_decls =
+        A.GlobalDeclId.Map.filter
+          (fun _ (d : A.global_decl) -> not (drop_item d.item_meta.attr_info))
+          crate.global_decls
+      in
+      let type_decls =
+        T.TypeDeclId.Map.filter
+          (fun _ (d : T.type_decl) -> not (drop_item d.item_meta.attr_info))
+          crate.type_decls
+      in
+      let trait_decls =
+        T.TraitDeclId.Map.filter
+          (fun _ (d : A.trait_decl) -> not (drop_item d.item_meta.attr_info))
+          crate.trait_decls
+      in
+      let trait_impls =
+        T.TraitImplId.Map.filter
+          (fun _ (d : A.trait_impl) -> not (drop_item d.item_meta.attr_info))
+          crate.trait_impls
+      in
+      let declarations =
+        List.filter_map (filter_declaration crate) crate.declarations
+      in
+      let n_dropped_funs = n_funs_before - A.FunDeclId.Map.cardinal fun_decls in
+      let n_dropped_globals =
+        n_globals_before - A.GlobalDeclId.Map.cardinal global_decls
+      in
+      let n_dropped_types =
+        n_types_before - T.TypeDeclId.Map.cardinal type_decls
+      in
+      let n_dropped_decls = n_decls_before - List.length declarations in
+      let total =
+        n_dropped_funs + n_dropped_globals + n_dropped_types + n_dropped_decls
+      in
+      if total > 0 then
+        [%ldebug
+          Printf.sprintf
+            "late-skip-pass: dropped %d fn(s), %d global(s), %d type(s), %d \
+             decl-group(s)"
+            n_dropped_funs n_dropped_globals n_dropped_types n_dropped_decls];
+      {
+        crate with
+        fun_decls;
+        global_decls;
+        type_decls;
+        trait_decls;
+        trait_impls;
+        declarations;
+      }
+end
+
 let apply_passes (crate : crate) : crate =
   (* Passes that apply to the whole crate *)
   let crate = update_array_default crate in
@@ -2327,8 +2635,10 @@ let apply_passes (crate : crate) : crate =
   in
   let crate = { crate with fun_decls } in
   let crate = strip_unnecessary_target_suffixes crate in
+  let crate = filter_eq_assert_fields_method crate in
   let crate = filter_marker_traits crate in
   let crate = filter_type_aliases crate in
+  let crate = HaxLateSkipFilterPrePass.run crate in
   let crate = replace_static crate in
   let crate = remove_vtables crate in
   let crate = rename_type_vars crate in
diff --git a/src/Translate.ml b/src/Translate.ml
index 8df1bc5fc..e0803e8a2 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -13,6 +13,12 @@ open Parallel
 (** The local logger *)
 let log = TranslateCore.log
 
+(** When [-core-models-lib] is on, non-local items are skipped from the main
+    extracted files (the user is expected to provide them via a separate Lean
+    library, e.g. [core_models] for [core::*] items). *)
+let skip_for_core_models_lib (is_local : bool) : bool =
+  !Config.core_models_lib && not is_local
+
 (** The result of running the symbolic interpreter on a function:
     - the list of symbolic values used for the input values
     - the generated symbolic AST *)
@@ -304,15 +310,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (marked_ids : marked_ids)
       ^ compute_local_uses_error_message trans_ctx (IdFun fdef.def_id));
     None
 
-type translated_crate = {
-  type_decls : Pure.type_decl list;
-  builtin_fun_sigs : Pure.fun_sig BuiltinFunIdMap.t;
-  fun_decls : pure_fun_translation list;
-  global_decls : Pure.global_decl list;
-  trait_decls : Pure.trait_decl list;
-  trait_impls : Pure.trait_impl list;
-}
-
 (* TODO: factor out the return type *)
 let translate_crate_to_pure (crate : crate) (marked_ids : marked_ids) :
     trans_ctx * translated_crate =
@@ -609,8 +606,8 @@ let translate_crate_to_pure (crate : crate) (marked_ids : marked_ids) :
       type_decls trait_impls pure_translations
   in
 
-  (* Return *)
-  ( trans_ctx,
+  (* Assemble the translated crate *)
+  let translated =
     {
       type_decls;
       builtin_fun_sigs;
@@ -618,7 +615,20 @@ let translate_crate_to_pure (crate : crate) (marked_ids : marked_ids) :
       global_decls;
       trait_decls;
       trait_impls;
-    } )
+      specs = [];
+      proof_obligations = [];
+    }
+  in
+
+  (* Gather specs/proofs obligations *)
+  let translated =
+    match !Config.opt_spec_config with
+    | Some (Hax, _) -> HaxProducer.produce trans_ctx translated
+    | None -> translated
+  in
+
+  (* Return *)
+  (trans_ctx, translated)
 
 type gen_ctx = ExtractBase.extraction_ctx
 
@@ -641,6 +651,12 @@ type gen_config = {
   extract_globals : bool;
       (** If [true], generate a definition/declaration for top-level (global)
           declarations *)
+  extract_specs : bool;
+      (** If [true], emit the produced {!Spec.spec} entries (Lean only). See
+          {!module:ExtractSpec}. *)
+  extract_proof_obligations : bool;
+      (** If [true], emit the produced {!Spec.proof_obligation} entries (Lean
+          only). See {!module:ExtractSpec}. *)
   interface : bool;
       (** [true] if we generate an interface file, [false] otherwise. For now,
           this only impacts whether we use [val] or [assume val] for the opaque
@@ -766,6 +782,12 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
   if List.exists (fun b -> b) builtin then
     (* Sanity check *)
     assert (List.for_all (fun b -> b) builtin)
+  else if
+    List.exists
+      (fun (d : Pure.type_decl) ->
+        skip_for_core_models_lib d.item_meta.is_local)
+      defs
+  then ()
   else if List.exists dont_extract defs then
     (* Check if we have to ignore declarations *)
     (* Sanity check *)
@@ -846,6 +868,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     && match_name_find_opt ctx.trans_ctx global.item_meta.name
          (builtin_globals_map ())
        = None
+    && not (skip_for_core_models_lib global.item_meta.is_local)
   in
   if extract then (
     (* We don't wrap global declaration groups between calls to functions
@@ -975,6 +998,12 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   if List.exists (fun b -> b) builtin then
     (* Sanity check *)
     assert (List.for_all (fun b -> b) builtin)
+  else if
+    List.exists
+      (fun (trans : pure_fun_translation) ->
+        skip_for_core_models_lib trans.f.item_meta.is_local)
+      pure_ls
+  then ()
   else
     (* Utility to check a function has a decrease clause *)
     let has_decreases_clause (def : Pure.fun_decl) : bool =
@@ -1078,7 +1107,10 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
       (TraitDeclId.Map.find_opt trait_decl_id ctx.trans_trait_decls)
   in
   (* Check if the trait declaration is builtin, in which case we ignore it *)
-  if not (trait_decl_is_builtin ctx trait_decl_id) then (
+  if
+    (not (trait_decl_is_builtin ctx trait_decl_id))
+    && not (skip_for_core_models_lib trait_decl.item_meta.is_local)
+  then (
     let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
     if extract_decl then (
       Extract.extract_trait_decl ctx fmt trait_decl;
@@ -1096,7 +1128,10 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
     [%silent_unwrap_opt_span] None
       (TraitImplId.Map.find_opt trait_impl_id ctx.trans_trait_impls)
   in
-  if not (trait_impl_is_builtin ctx trait_impl_id) then (
+  if
+    (not (trait_impl_is_builtin ctx trait_impl_id))
+    && not (skip_for_core_models_lib trait_impl.item_meta.is_local)
+  then (
     Extract.extract_trait_impl ctx fmt ~is_rec trait_impl;
     EmitJson.record_trait_impl_if_enabled ctx trait_impl)
 
@@ -1260,7 +1295,12 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
       with CFailure _ ->
         (* An exception was raised: ignore it *)
         ())
-    ctx.crate.declarations
+    ctx.crate.declarations;
+
+  (* Emit hax specs/proof obligations, if requested. *)
+  if config.extract_specs then ExtractSpec.extract_specs ctx fmt;
+  if config.extract_proof_obligations then
+    ExtractSpec.extract_proof_obligations ctx fmt
 
 type extract_file_info = {
   filename : string;
@@ -1351,12 +1391,23 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       Printf.fprintf out "Module %s.\n" fi.module_name
   | Lean ->
       Printf.fprintf out "import Aeneas\n";
+      if !Config.core_models_lib then Printf.fprintf out "import CoreModels\n";
       (* Add the custom imports *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_imports;
       (* Add the custom includes *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_includes;
       (* Always open the Primitives namespace *)
-      Printf.fprintf out "open Aeneas Aeneas.Std Result ControlFlow Error\n";
+      if !Config.core_models_lib then begin
+        Printf.fprintf out "open CoreModels Aeneas\n";
+        Printf.fprintf out "open Aeneas.Std hiding namespace core alloc\n";
+        Printf.fprintf out "open Result ControlFlow Error\n"
+      end
+      else
+        Printf.fprintf out "open Aeneas Aeneas.Std Result ControlFlow Error\n";
+      (* In Mvcgen mode, we need to open Std.Do *)
+      (match Config.spec_backend () with
+      | Some Config.Mvcgen -> Printf.fprintf out "open Std.Do\n"
+      | Some Config.Step | None -> ());
       (* It happens that we generate duplicated namespaces, like `betree.betree`.
          We deactivate the linter for this, because otherwise it leads to too much
          noise. *)
@@ -1446,6 +1497,8 @@ let extract_translated_crate (filename : string) (dest_dir : string)
     global_decls = trans_globals;
     trait_decls = trans_trait_decls;
     trait_impls = trans_trait_impls;
+    specs = trans_specs;
+    proof_obligations = trans_proof_obligations;
   } =
     trans_crate
   in
@@ -1519,6 +1572,8 @@ let extract_translated_crate (filename : string) (dest_dir : string)
       trans_trait_impls;
       trans_types;
       trans_funs;
+      specs = trans_specs;
+      proof_obligations = trans_proof_obligations;
       builtin_sigs;
       trans_globals;
       functions_with_decreases_clause = rec_functions;
@@ -1839,6 +1894,12 @@ let extract_translated_crate (filename : string) (dest_dir : string)
   in
   let has_opaque = has_opaque_types || has_opaque_funs in
 
+  (* Extra Lean imports the produced specs require (empty when there are none);
+     the source-specific logic lives in {!Spec.required_imports}. *)
+  let spec_imports =
+    if trans_specs = [] then [] else Spec.required_imports ()
+  in
+
   (* Extract one or several files, depending on the configuration *)
   (if !Config.split_files then (
      let base_gen_config =
@@ -1852,6 +1913,8 @@ let extract_translated_crate (filename : string) (dest_dir : string)
          extract_transparent = true;
          extract_opaque = false;
          extract_globals = false;
+         extract_specs = false;
+         extract_proof_obligations = false;
          interface = false;
        }
      in
@@ -2074,7 +2137,38 @@ let extract_translated_crate (filename : string) (dest_dir : string)
          noncomputable = has_opaque && not !Config.all_computable;
        }
      in
-     extract_file fun_config ctx file_info)
+     extract_file fun_config ctx file_info;
+
+     (* Dedicated Specs.lean (statements of correctness) and
+        ProofObligations.lean (the obligations), if any *)
+     let specs_module = import_prefix ^ "Specs" in
+     (if trans_specs <> [] then
+        let specs_config = { base_gen_config with extract_specs = true } in
+        let file_info =
+          {
+            file_info with
+            filename = extract_filebasename ^ "Specs" ^ ext;
+            module_name = specs_module;
+            custom_msg = ": specs (statements of correctness)";
+            custom_imports = spec_imports;
+            custom_includes = [ types_module; fun_module ];
+          }
+        in
+        extract_file specs_config ctx file_info);
+     if trans_proof_obligations <> [] then
+       let obligations_config =
+         { base_gen_config with extract_proof_obligations = true }
+       in
+       let file_info =
+         {
+           file_info with
+           filename = extract_filebasename ^ "ProofObligations" ^ ext;
+           module_name = import_prefix ^ "ProofObligations";
+           custom_msg = ": proof obligations";
+           custom_includes = [ types_module; fun_module; specs_module ];
+         }
+       in
+       extract_file obligations_config ctx file_info)
    else
      let gen_config =
        {
@@ -2088,6 +2182,8 @@ let extract_translated_crate (filename : string) (dest_dir : string)
          extract_transparent = true;
          extract_opaque = true;
          extract_globals = true;
+         extract_specs = Config.spec_config_enabled ();
+         extract_proof_obligations = Config.spec_config_enabled ();
          interface = false;
        }
      in
@@ -2101,7 +2197,7 @@ let extract_translated_crate (filename : string) (dest_dir : string)
          rust_module_name = crate.name;
          module_name = crate_name;
          custom_msg = "";
-         custom_imports = [];
+         custom_imports = spec_imports;
          custom_includes = [];
          noncomputable = has_opaque && not !Config.all_computable;
        }
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 55e2abe89..0548db894 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -17,6 +17,18 @@ type fun_and_loops = {
 type pure_fun_translation_no_loops = Pure.fun_decl
 type pure_fun_translation = fun_and_loops
 
+(** The whole crate, translated to pure. *)
+type translated_crate = {
+  type_decls : Pure.type_decl list;
+  builtin_fun_sigs : Pure.fun_sig Builtin.BuiltinFunIdMap.t;
+  fun_decls : pure_fun_translation list;
+  global_decls : Pure.global_decl list;
+  trait_decls : Pure.trait_decl list;
+  trait_impls : Pure.trait_impl list;
+  specs : Spec.spec list;
+  proof_obligations : Spec.proof_obligation list;
+}
+
 let trans_ctx_to_fmt_env (ctx : trans_ctx) : Print.fmt_env =
   Print.Contexts.decls_ctx_to_fmt_env ctx
 
diff --git a/src/dune b/src/dune
index 146485851..67d032b69 100644
--- a/src/dune
+++ b/src/dune
@@ -37,7 +37,8 @@
   str
   progress
   domainslib
-  ppx_deriving_yojson)
+  ppx_deriving_yojson
+  yojson)
  (modules
   BorrowCheck
   Builtin
@@ -57,10 +58,15 @@
   ExtractBuiltinCore
   ExtractBuiltinLean
   ExtractErrors
+  ExtractHaxSpecs
   ExtractName
+  ExtractSpec
   ExtractTypes
   FunsAnalysis
   GitVersion
+  HaxAttributes
+  HaxSpecs
+  HaxProducer
   Identifiers
   InterpAbs
   InterpBorrowsCore
@@ -107,6 +113,7 @@
   ReorderDecls
   SCC
   Scalars
+  Spec
   StringUtils
   Substitute
   SymbolicAst
diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml
index cfe078123..63aae1075 100644
--- a/src/extract/Extract.ml
+++ b/src/extract/Extract.ml
@@ -23,11 +23,188 @@ let generic_args_to_string (ctx : extraction_ctx) =
 let texpr_to_string (ctx : extraction_ctx) =
   PrintPure.texpr_to_string (extraction_ctx_to_fmt_env ctx) false "" "  "
 
+(** Under [-core-models-lib], detect type parameters and trait clauses left
+    dangling by Charon's [hide_allocator] pass (which strips the [A] parameter
+    from [Vec], [Box], etc. and removes the [core::alloc::Allocator] trait
+    declaration but leaves the function-level [A] and [A: Clone]-style clauses
+    in place).
+
+    A type parameter is dropped iff it is unused in the function's inputs,
+    output, and predicates. A trait clause is dropped iff every type variable it
+    references is itself being dropped (i.e., it is "orphan" — only constraining
+    dropped parameters). The "used" set is saturated through trait clauses so
+    that a parameter pulled in by a kept clause is itself kept.
+
+    [scan]: caller-supplied closure that gets invoked with a visitor and may
+    visit any extra structures (e.g. a trait_impl's [impl_trait] /
+    [parent_trait_refs]) so their type variables also count as used. Pass a
+    no-op closure when there is nothing extra to scan.
+
+    [extra_trait_decl_refs] / [extra_trait_refs]: caller-supplied additional
+    things to scan for used type variables. Trait impls in particular have no
+    function-style inputs; instead, the type variables they bind appear in
+    [impl_trait] and the parent trait refs, which the caller passes here.
+
+    Returns [None] if nothing needs filtering. *)
+let compute_allocator_filter
+    ?(extra_trait_decl_refs : Pure.trait_decl_ref list = [])
+    ?(extra_trait_refs : Pure.trait_ref list = [])
+    ?(type_args_filter : Pure.type_decl_id -> bool list option = fun _ -> None)
+    (generics : Pure.generic_params) (inputs : Pure.ty list)
+    (output : Pure.ty option) (preds : Pure.predicates) :
+    (bool list * bool list) option =
+  let type_params = generics.types in
+  let trait_clauses = generics.trait_clauses in
+  if type_params = [] then None
+  else
+    (* When visiting a type application of an ADT whose own allocator parameter
+       is being filtered (e.g. [IntoIter T A] -> [IntoIter T]), we must not count
+       the type variables that only appear in the dropped argument positions as
+       "used". Otherwise an allocator parameter that only shows up in, say, the
+       output type [IntoIter<T, A>] would be wrongly kept. *)
+    let visit_filtered_ty_args (self : _) (env : unit) (type_id : Pure.type_id)
+        (generics : Pure.generic_args) : bool =
+      match type_id with
+      | TAdtId id -> (
+          match type_args_filter id with
+          | Some keep when List.length keep = List.length generics.types ->
+              List.iter2
+                (fun b ty -> if b then self#visit_ty env ty)
+                keep generics.types;
+              List.iter (self#visit_const_generic env) generics.const_generics;
+              List.iter (self#visit_trait_ref env) generics.trait_refs;
+              true
+          | _ -> false)
+      | _ -> false
+    in
+    let used = ref Pure.TypeVarId.Set.empty in
+    let body_visitor =
+      object (self)
+        inherit [_] Pure.iter_type_decl as super
+
+        method! visit_ty env t =
+          match t with
+          | Pure.TAdt (type_id, generics)
+            when visit_filtered_ty_args self env type_id generics -> ()
+          | _ -> super#visit_ty env t
+
+        method! visit_type_var_id _ id = used := Pure.TypeVarId.Set.add id !used
+      end
+    in
+    List.iter (body_visitor#visit_ty ()) inputs;
+    (match output with
+    | Some o -> body_visitor#visit_ty () o
+    | None -> ());
+    body_visitor#visit_predicates () preds;
+    List.iter (body_visitor#visit_trait_decl_ref ()) extra_trait_decl_refs;
+    List.iter (body_visitor#visit_trait_ref ()) extra_trait_refs;
+    let clause_tvars (c : Pure.trait_param) : Pure.TypeVarId.Set.t =
+      let s = ref Pure.TypeVarId.Set.empty in
+      let v =
+        object (self)
+          inherit [_] Pure.iter_type_decl as super
+
+          method! visit_ty env t =
+            match t with
+            | Pure.TAdt (type_id, generics)
+              when visit_filtered_ty_args self env type_id generics -> ()
+            | _ -> super#visit_ty env t
+
+          method! visit_type_var_id _ id = s := Pure.TypeVarId.Set.add id !s
+        end
+      in
+      v#visit_trait_param () c;
+      !s
+    in
+    let rec saturate () =
+      let changed = ref false in
+      List.iter
+        (fun (c : Pure.trait_param) ->
+          let tvars = clause_tvars c in
+          if
+            Pure.TypeVarId.Set.exists
+              (fun id -> Pure.TypeVarId.Set.mem id !used)
+              tvars
+          then
+            Pure.TypeVarId.Set.iter
+              (fun id ->
+                if not (Pure.TypeVarId.Set.mem id !used) then begin
+                  used := Pure.TypeVarId.Set.add id !used;
+                  changed := true
+                end)
+              tvars)
+        trait_clauses;
+      if !changed then saturate ()
+    in
+    saturate ();
+    let unused_set =
+      List.fold_left
+        (fun acc (p : Pure.type_param) ->
+          if Pure.TypeVarId.Set.mem p.index !used then acc
+          else Pure.TypeVarId.Set.add p.index acc)
+        Pure.TypeVarId.Set.empty type_params
+    in
+    let is_orphan_clause (c : Pure.trait_param) : bool =
+      let tvars = clause_tvars c in
+      (not (Pure.TypeVarId.Set.is_empty tvars))
+      && Pure.TypeVarId.Set.for_all
+           (fun id -> Pure.TypeVarId.Set.mem id unused_set)
+           tvars
+    in
+    let any_orphan = List.exists is_orphan_clause trait_clauses in
+    let any_unused = not (Pure.TypeVarId.Set.is_empty unused_set) in
+    if (not any_orphan) && not any_unused then None
+    else
+      let keep_params =
+        List.map
+          (fun (p : Pure.type_param) ->
+            not (Pure.TypeVarId.Set.mem p.index unused_set))
+          type_params
+      in
+      let keep_trait_clauses =
+        List.map (fun c -> not (is_orphan_clause c)) trait_clauses
+      in
+      Some (keep_params, keep_trait_clauses)
+
 (** Compute the names for all the pure functions generated from a rust function.
 *)
 let extract_fun_decl_register_names (ctx : extraction_ctx)
     (has_decreases_clause : fun_decl -> bool) (def : pure_fun_translation) :
     extraction_ctx =
+  let maybe_register_allocator_filter (ctx : extraction_ctx) : extraction_ctx =
+    if not !Config.core_models_lib then ctx
+    else
+      let sg = def.f.signature in
+      let type_args_filter id =
+        TypeDeclId.Map.find_opt id ctx.types_filter_type_args_map
+      in
+      match
+        compute_allocator_filter ~type_args_filter sg.generics sg.inputs
+          (Some sg.output) sg.preds
+      with
+      | None -> ctx
+      | Some (keep_params, keep_trait_clauses) ->
+          let ctx =
+            if FunDeclId.Map.mem def.f.def_id ctx.funs_filter_type_args_map then
+              ctx
+            else
+              {
+                ctx with
+                funs_filter_type_args_map =
+                  FunDeclId.Map.add def.f.def_id keep_params
+                    ctx.funs_filter_type_args_map;
+              }
+          in
+          if FunDeclId.Map.mem def.f.def_id ctx.funs_filter_trait_clauses_map
+          then ctx
+          else
+            {
+              ctx with
+              funs_filter_trait_clauses_map =
+                FunDeclId.Map.add def.f.def_id keep_trait_clauses
+                  ctx.funs_filter_trait_clauses_map;
+            }
+  in
   (* Use the builtin names if necessary *)
   match def.f.builtin_info with
   | Some info ->
@@ -54,11 +231,13 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
             }
         | _ -> ctx
       in
+      let ctx = maybe_register_allocator_filter ctx in
       let f = def.f in
       let fun_id = (Pure.FunId (FRegular f.def_id), f.loop_id) in
       ctx_add f.item_meta.span (FunId (FromLlbc fun_id)) info.extract_name ctx
   | None ->
       (* Not builtin *)
+      let ctx = maybe_register_allocator_filter ctx in
       (* Register the decrease clauses, if necessary *)
       let register_decreases ctx def =
         if has_decreases_clause def then
@@ -278,7 +457,7 @@ let fun_builtin_filter_types_trait_clauses (ty_to_string : 'a -> string)
     match FunDeclId.Map.find_opt id ctx.funs_filter_trait_clauses_map with
     | None -> Result.Ok clauses
     | Some filter ->
-        if List.length filter <> List.length types then (
+        if List.length filter <> List.length clauses then (
           let decl =
             [%silent_unwrap_opt_span] None (ctx_lookup_fun_decl_info ctx id)
           in
@@ -333,6 +512,16 @@ let fun_builtin_filter_types_trait_clauses (ty_to_string : 'a -> string)
       Result.Ok (types, explicit, clauses)
   | Result.Error msg, _ | _, Result.Error msg -> Result.Error msg
 
+(** Emit a boxed delimiter: [<l> <inner> <r>] inside an [hovbox] *)
+let emit_delim ?(add_spaces = true) fmt l k r : unit =
+  F.pp_open_hovbox fmt 0;
+  F.pp_print_string fmt l;
+  if add_spaces then F.pp_print_space fmt ();
+  k ();
+  if add_spaces then F.pp_print_space fmt ();
+  F.pp_print_string fmt r;
+  F.pp_close_box fmt ()
+
 (** [inside]: see {!extract_ty}. [with_type]: do we also generate a type
     annotation? This is necessary for backends like Coq when we write lambdas
     (Coq is not powerful enough to infer the type).
@@ -2978,6 +3167,52 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
         in
         (ctx, Some builtin_info)
   in
+  (* Under [-core-models-lib], drop dangling allocator-shaped type params and
+     orphan trait clauses (same heuristic as for functions). Trait impls have
+     no "inputs"; the type variables they bind show up in [impl_trait], its
+     parent trait refs, the associated types it implements, and so on. We
+     pass all of those as extra scan context so they don't get wrongly
+     classified as unused. *)
+  let ctx =
+    if not !Config.core_models_lib then ctx
+    else
+      let assoc_tys = List.map (fun (_, _, ty) -> ty) trait_impl.types in
+      let type_args_filter id =
+        TypeDeclId.Map.find_opt id ctx.types_filter_type_args_map
+      in
+      match
+        compute_allocator_filter
+          ~extra_trait_decl_refs:[ trait_impl.impl_trait ]
+          ~extra_trait_refs:trait_impl.parent_trait_refs ~type_args_filter
+          trait_impl.generics assoc_tys None trait_impl.preds
+      with
+      | None -> ctx
+      | Some (keep_params, keep_trait_clauses) ->
+          let ctx =
+            if
+              TraitImplId.Map.mem trait_impl.def_id
+                ctx.trait_impls_filter_type_args_map
+            then ctx
+            else
+              {
+                ctx with
+                trait_impls_filter_type_args_map =
+                  TraitImplId.Map.add trait_impl.def_id keep_params
+                    ctx.trait_impls_filter_type_args_map;
+              }
+          in
+          if
+            TraitImplId.Map.mem trait_impl.def_id
+              ctx.trait_impls_filter_trait_clauses_map
+          then ctx
+          else
+            {
+              ctx with
+              trait_impls_filter_trait_clauses_map =
+                TraitImplId.Map.add trait_impl.def_id keep_trait_clauses
+                  ctx.trait_impls_filter_trait_clauses_map;
+            }
+  in
 
   (* Everything is taken care of by {!extract_trait_decl_register_names} *but*
      the name of the implementation itself *)
diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml
index 629543ede..44dd40c02 100644
--- a/src/extract/ExtractBase.ml
+++ b/src/extract/ExtractBase.ml
@@ -602,6 +602,11 @@ type extraction_ctx = {
   functions_with_decreases_clause : PureUtils.FunLoopIdSet.t;
   trans_trait_decls : Pure.trait_decl Pure.TraitDeclId.Map.t;
   trans_trait_impls : Pure.trait_impl Pure.TraitImplId.Map.t;
+  specs : Spec.spec list;
+      (** Gathered specs (statements of correctness) for this crate (see
+          {!module:Spec}). *)
+  proof_obligations : Spec.proof_obligation list;
+      (** Gathered proof obligations for this crate (see {!module:Spec}). *)
   types_filter_type_args_map : bool list TypeDeclId.Map.t;
       (** The map to filter the type arguments for the builtin type definitions.
 
@@ -1923,8 +1928,27 @@ let ctx_compute_trait_impl_name_raw (ctx : extraction_ctx)
             in
             [%ldebug "trait_name: " ^ trait_name];
 
-            (* Put together *)
-            let name = flatten_name [ self_name; "Insts"; trait_name ] in
+            (* Put together. Under [-core-models-lib], non-local trait impls
+               get prefixed with the Rust crate they originate from (matching
+               the convention used for non-impl items, where the crate is the
+               leading namespace component). For local impls, the local crate
+               is stripped, as elsewhere. We also skip the prefix if the self
+               type's name already starts with that crate (the ADT case),
+               which would otherwise yield a duplicated crate component. *)
+            let name_parts = [ self_name; "Insts"; trait_name ] in
+            let name_parts =
+              if !core_models_lib && not trait_impl.item_meta.is_local then
+                match trait_impl.item_meta.name with
+                | PeIdent (crate, _) :: _ ->
+                    let already_prefixed =
+                      self_name = crate
+                      || String.starts_with ~prefix:(crate ^ ".") self_name
+                    in
+                    if already_prefixed then name_parts else crate :: name_parts
+                | _ -> name_parts
+              else name_parts
+            in
+            let name = flatten_name name_parts in
             [%ldebug "Final name: " ^ name];
             name)
   | Some name -> name
diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml
index 6e28b984b..f76049e16 100644
--- a/src/extract/ExtractBuiltin.ml
+++ b/src/extract/ExtractBuiltin.ml
@@ -43,7 +43,7 @@ let builtin_globals () : Pure.builtin_global_info list =
          unit_metadata;
        ];
      ]
-    @ mk_lean_only lean_builtin_consts)
+    @ mk_lean_only_unless_core_models_lib lean_builtin_consts)
 
 let mk_builtin_globals_map () : Pure.builtin_global_info NameMatcherMap.t =
   NameMatcherMap.of_list
@@ -170,7 +170,7 @@ let builtin_types () : Pure.builtin_type_info list =
                   ]);
          };
        ])
-  @ mk_lean_only lean_builtin_types
+  @ mk_lean_only_unless_core_models_lib lean_builtin_types
 
 let mk_builtin_types_map () =
   NameMatcherMap.of_list
@@ -180,6 +180,27 @@ let mk_builtin_types_map () =
 
 let builtin_types_map = mk_memoized mk_builtin_types_map
 
+(** Map from rust type name to its builtin info, restricted to the types that
+    carry a [keep_params] filter (i.e. types from which Charon's
+    [hide_allocator] pass leaves a dangling allocator type parameter, such as
+    [alloc::vec::into_iter::IntoIter]).
+
+    Unlike {!builtin_types_map}, this map is *not* emptied under
+    [-core-models-lib]: even when the builtin type overrides are disabled, we
+    still need to drop the dangling allocator type parameter so that the
+    extracted types match the [core_models] library, which models them without
+    an allocator (e.g. [IntoIter T] rather than [IntoIter T Global]). *)
+let mk_builtin_types_keep_params_map () =
+  NameMatcherMap.of_list
+    (List.filter_map
+       (fun (info : Pure.builtin_type_info) ->
+         match info.keep_params with
+         | Some _ -> Some (info.rust_name, info)
+         | None -> None)
+       lean_builtin_types)
+
+let builtin_types_keep_params_map = mk_memoized mk_builtin_types_keep_params_map
+
 let int_and_smaller_list : (string * string) list =
   let uint_names = List.rev [ "u8"; "u16"; "u32"; "u64"; "u128" ] in
   let int_names = List.rev [ "i8"; "i16"; "i32"; "i64"; "i128" ] in
@@ -324,7 +345,7 @@ let builtin_trait_decls_info () =
       (* Copy *)
       mk_trait "core::marker::Copy" ~parent_clauses:[ "cloneInst" ] ();
     ]
-  @ mk_lean_only lean_builtin_trait_decls
+  @ mk_lean_only_unless_core_models_lib lean_builtin_trait_decls
 
 let mk_builtin_trait_decls_map () =
   NameMatcherMap.of_list
@@ -420,90 +441,96 @@ let builtin_trait_impls_info () : (pattern * Pure.builtin_trait_impl_info) list
       fmt "core::clone::Clone<bool>"
         ~extract_name:(Some "core::clone::CloneBool") ();
     ]
-  @ mk_lean_only lean_builtin_trait_impls
-  (* From<INT, bool> *)
-  @ List.map
-      (fun ty ->
-        fmt
-          ("core::convert::From<" ^ ty ^ ", bool>")
-          ~extract_name:
-            (Some
-               ("core.convert.From"
-               ^ StringUtils.capitalize_first_letter ty
-               ^ "Bool"))
-          ())
-      all_int_names
-  (* From<INT, INT> *)
-  @ List.map
-      (fun (big, small) ->
-        fmt
-          ("core::convert::From<" ^ big ^ ", " ^ small ^ ">")
-          ~extract_name:
-            (Some
-               ("core.convert.From"
-               ^ StringUtils.capitalize_first_letter big
-               ^ StringUtils.capitalize_first_letter small))
-          ())
-      int_and_smaller_list
-  (* Clone<INT> *)
-  @ List.map
-      (fun ty ->
-        fmt
-          ("core::clone::Clone<" ^ ty ^ ">")
-          ~extract_name:
-            (Some ("core.clone.Clone" ^ StringUtils.capitalize_first_letter ty))
-          ())
-      all_int_names
-  (* Copy<INT> *)
-  @ List.map
-      (fun ty ->
-        fmt
-          ("core::marker::Copy<" ^ ty ^ ">")
-          ~extract_name:
-            (Some ("core.marker.Copy" ^ StringUtils.capitalize_first_letter ty))
-          ())
-      all_int_names
-  (* PartialEq<INT, INT> *)
-  @ List.map
-      (fun ty ->
-        fmt
-          ("core::cmp::PartialEq<" ^ ty ^ "," ^ ty ^ ">")
-          ~extract_name:
-            (Some ("core.cmp.PartialEq" ^ StringUtils.capitalize_first_letter ty))
-          ())
-      all_int_names
-  (* Eq<INT> *)
-  @ List.map
-      (fun ty ->
-        fmt
-          ("core::cmp::Eq<" ^ ty ^ ">")
-          ~extract_name:
-            (Some ("core.cmp.Eq" ^ StringUtils.capitalize_first_letter ty))
-          ())
-      all_int_names
-  (* PartialOrd<INT, INT> *)
-  @ List.map
-      (fun ty ->
-        fmt
-          ("core::cmp::PartialOrd<" ^ ty ^ "," ^ ty ^ ">")
-          ~extract_name:
-            (Some
-               ("core.cmp.PartialOrd" ^ StringUtils.capitalize_first_letter ty))
-          ())
-      all_int_names
-  (* Ord<INT> *)
-  @ List.map
-      (fun ty ->
-        fmt
-          ("core::cmp::Ord<" ^ ty ^ ">")
-          ~extract_name:
-            (Some ("core.cmp.Ord" ^ StringUtils.capitalize_first_letter ty))
-          ())
-      all_int_names
-  (* Default<INT> *)
-  @ List.map
-      (fun ty -> fmt ("core::default::Default<" ^ ty ^ ">") ())
-      all_int_names
+  @ mk_lean_only_unless_core_models_lib lean_builtin_trait_impls
+  @ unless_core_models_lib
+      ((* From<INT, bool> *)
+       List.map
+         (fun ty ->
+           fmt
+             ("core::convert::From<" ^ ty ^ ", bool>")
+             ~extract_name:
+               (Some
+                  ("core.convert.From"
+                  ^ StringUtils.capitalize_first_letter ty
+                  ^ "Bool"))
+             ())
+         all_int_names
+      (* From<INT, INT> *)
+      @ List.map
+          (fun (big, small) ->
+            fmt
+              ("core::convert::From<" ^ big ^ ", " ^ small ^ ">")
+              ~extract_name:
+                (Some
+                   ("core.convert.From"
+                   ^ StringUtils.capitalize_first_letter big
+                   ^ StringUtils.capitalize_first_letter small))
+              ())
+          int_and_smaller_list
+      (* Clone<INT> *)
+      @ List.map
+          (fun ty ->
+            fmt
+              ("core::clone::Clone<" ^ ty ^ ">")
+              ~extract_name:
+                (Some
+                   ("core.clone.Clone" ^ StringUtils.capitalize_first_letter ty))
+              ())
+          all_int_names
+      (* Copy<INT> *)
+      @ List.map
+          (fun ty ->
+            fmt
+              ("core::marker::Copy<" ^ ty ^ ">")
+              ~extract_name:
+                (Some
+                   ("core.marker.Copy" ^ StringUtils.capitalize_first_letter ty))
+              ())
+          all_int_names
+      (* PartialEq<INT, INT> *)
+      @ List.map
+          (fun ty ->
+            fmt
+              ("core::cmp::PartialEq<" ^ ty ^ "," ^ ty ^ ">")
+              ~extract_name:
+                (Some
+                   ("core.cmp.PartialEq"
+                   ^ StringUtils.capitalize_first_letter ty))
+              ())
+          all_int_names
+      (* Eq<INT> *)
+      @ List.map
+          (fun ty ->
+            fmt
+              ("core::cmp::Eq<" ^ ty ^ ">")
+              ~extract_name:
+                (Some ("core.cmp.Eq" ^ StringUtils.capitalize_first_letter ty))
+              ())
+          all_int_names
+      (* PartialOrd<INT, INT> *)
+      @ List.map
+          (fun ty ->
+            fmt
+              ("core::cmp::PartialOrd<" ^ ty ^ "," ^ ty ^ ">")
+              ~extract_name:
+                (Some
+                   ("core.cmp.PartialOrd"
+                   ^ StringUtils.capitalize_first_letter ty))
+              ())
+          all_int_names
+      (* Ord<INT> *)
+      @ List.map
+          (fun ty ->
+            fmt
+              ("core::cmp::Ord<" ^ ty ^ ">")
+              ~extract_name:
+                (Some ("core.cmp.Ord" ^ StringUtils.capitalize_first_letter ty))
+              ())
+          all_int_names
+      (* Default<INT> *)
+      @ List.map
+          (fun ty -> fmt ("core::default::Default<" ^ ty ^ ">") ())
+          all_int_names)
 
 let mk_builtin_trait_impls_map () =
   let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in
@@ -583,81 +610,89 @@ let mk_builtin_funs () : (pattern * Pure.builtin_fun_info) list =
              funs)
          all_int_names)
   in
-  List.flatten
-    (List.map
-       (fun op ->
-         mk_scalar_fun
-           (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op)
-           (fun ty -> StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op)
-           ~can_fail:false ())
-       [ "add"; "sub"; "mul"; "div"; "rem" ])
-  (* From<INT, bool> *)
-  @ mk_scalar_fun
-      (fun ty ->
-        "core::convert::num::{core::convert::From<" ^ ty ^ ", bool>}::from")
-      (fun ty ->
-        "core.convert.num.From"
-        ^ StringUtils.capitalize_first_letter ty
-        ^ "Bool.from")
-      ~can_fail:false ()
-  (* From<INT, INT> *)
-  @ List.map
-      (fun (big, small) ->
-        mk_fun
-          ("core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small
-         ^ ">}::from")
-          ~extract_name:
-            (Some
-               ("core.convert.num.From"
-               ^ StringUtils.capitalize_first_letter big
-               ^ StringUtils.capitalize_first_letter small
-               ^ ".from"))
-          ~can_fail:false ())
-      int_and_smaller_list
-  (* Leading zeros *)
-  @ mk_scalar_fun
-      (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros")
-      (fun ty ->
-        "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".leading_zeros")
-      ~can_fail:false ()
-  (* to_le_bytes *)
-  @ mk_scalar_fun
-      (fun ty -> "core::num::{" ^ ty ^ "}::to_le_bytes")
-      (fun ty ->
-        "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_le_bytes")
-      ~can_fail:false ()
-  (* to_be_bytes *)
-  @ mk_scalar_fun
-      (fun ty -> "core::num::{" ^ ty ^ "}::to_be_bytes")
-      (fun ty ->
-        "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_be_bytes")
-      ~can_fail:false ()
-  (* from_le_bytes *)
-  @ mk_scalar_fun
-      (fun ty -> "core::num::{" ^ ty ^ "}::from_le_bytes")
-      (fun ty ->
-        "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".from_le_bytes")
-      ~can_fail:false ()
-  (* from_be_bytes *)
-  @ mk_scalar_fun
-      (fun ty -> "core::num::{" ^ ty ^ "}::from_be_bytes")
-      (fun ty ->
-        "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".from_be_bytes")
-      ~can_fail:false ()
-  (* Clone<bool> *)
-  @ mk_funs
-      (fun fn -> "core::clone::impls::{core::clone::Clone<bool>}::" ^ fn)
-      (fun fn -> "core.clone.impls.CloneBool." ^ fn)
-      [ (false, "clone"); (false, "clone_from") ]
-  (* Clone<INT> *)
-  @ mk_scalar_funs
-      (fun ty fn ->
-        "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::" ^ fn)
-      (fun ty fn ->
-        "core.clone.impls.Clone"
-        ^ StringUtils.capitalize_first_letter ty
-        ^ "." ^ fn)
-      [ (false, "clone"); (false, "clone_from") ]
+  unless_core_models_lib
+    (List.flatten
+       (List.map
+          (fun op ->
+            mk_scalar_fun
+              (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op)
+              (fun ty ->
+                StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op)
+              ~can_fail:false ())
+          [ "add"; "sub"; "mul"; "div"; "rem" ])
+    (* From<INT, bool> *)
+    @ mk_scalar_fun
+        (fun ty ->
+          "core::convert::num::{core::convert::From<" ^ ty ^ ", bool>}::from")
+        (fun ty ->
+          "core.convert.num.From"
+          ^ StringUtils.capitalize_first_letter ty
+          ^ "Bool.from")
+        ~can_fail:false ()
+    (* From<INT, INT> *)
+    @ List.map
+        (fun (big, small) ->
+          mk_fun
+            ("core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small
+           ^ ">}::from")
+            ~extract_name:
+              (Some
+                 ("core.convert.num.From"
+                 ^ StringUtils.capitalize_first_letter big
+                 ^ StringUtils.capitalize_first_letter small
+                 ^ ".from"))
+            ~can_fail:false ())
+        int_and_smaller_list
+    (* Leading zeros *)
+    @ mk_scalar_fun
+        (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros")
+        (fun ty ->
+          "core.num."
+          ^ StringUtils.capitalize_first_letter ty
+          ^ ".leading_zeros")
+        ~can_fail:false ()
+    (* to_le_bytes *)
+    @ mk_scalar_fun
+        (fun ty -> "core::num::{" ^ ty ^ "}::to_le_bytes")
+        (fun ty ->
+          "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_le_bytes")
+        ~can_fail:false ()
+    (* to_be_bytes *)
+    @ mk_scalar_fun
+        (fun ty -> "core::num::{" ^ ty ^ "}::to_be_bytes")
+        (fun ty ->
+          "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_be_bytes")
+        ~can_fail:false ()
+    (* from_le_bytes *)
+    @ mk_scalar_fun
+        (fun ty -> "core::num::{" ^ ty ^ "}::from_le_bytes")
+        (fun ty ->
+          "core.num."
+          ^ StringUtils.capitalize_first_letter ty
+          ^ ".from_le_bytes")
+        ~can_fail:false ()
+    (* from_be_bytes *)
+    @ mk_scalar_fun
+        (fun ty -> "core::num::{" ^ ty ^ "}::from_be_bytes")
+        (fun ty ->
+          "core.num."
+          ^ StringUtils.capitalize_first_letter ty
+          ^ ".from_be_bytes")
+        ~can_fail:false ()
+    (* Clone<bool> *)
+    @ mk_funs
+        (fun fn -> "core::clone::impls::{core::clone::Clone<bool>}::" ^ fn)
+        (fun fn -> "core.clone.impls.CloneBool." ^ fn)
+        [ (false, "clone"); (false, "clone_from") ]
+    (* Clone<INT> *)
+    @ mk_scalar_funs
+        (fun ty fn ->
+          "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::" ^ fn)
+        (fun ty fn ->
+          "core.clone.impls.Clone"
+          ^ StringUtils.capitalize_first_letter ty
+          ^ "." ^ fn)
+        [ (false, "clone"); (false, "clone_from") ])
   (* Definitions not for Lean *)
   @ mk_not_lean
       [
@@ -795,7 +830,7 @@ let mk_builtin_funs () : (pattern * Pure.builtin_fun_info) list =
           ();
       ]
   (* Lean-only definitions *)
-  @ mk_lean_only
+  @ mk_lean_only_unless_core_models_lib
       ((* PartialEq, Eq, PartialOrd, Ord *)
        mk_scalar_funs
          (fun ty fun_name ->
diff --git a/src/extract/ExtractBuiltinCore.ml b/src/extract/ExtractBuiltinCore.ml
index 60961bddc..ecc9b92d9 100644
--- a/src/extract/ExtractBuiltinCore.ml
+++ b/src/extract/ExtractBuiltinCore.ml
@@ -39,6 +39,26 @@ let mk_lean_only (funs : 'a list) : 'a list =
   | Lean -> funs
   | _ -> []
 
+(** Like [mk_lean_only], but additionally returns [[]] when the
+    [-core-models-lib] CLI option is on. Used to disable the Rust core library
+    overrides defined in [ExtractBuiltinLean.ml] (both the hand-tuned extract
+    names and the associated shape overrides such as [keep_params] and
+    [can_fail]). *)
+let mk_lean_only_unless_core_models_lib (funs : 'a list) : 'a list =
+  match backend () with
+  | Lean -> if !core_models_lib then [] else funs
+  | _ -> []
+
+(** Returns [[]] when the [-core-models-lib] CLI option is on, otherwise returns
+    the input list unchanged. Used to disable Rust core library overrides that
+    produce hand-tuned, Lean-style flat names (e.g.
+    [core.convert.num.FromU16U8.from]) and the associated shape overrides (e.g.
+    [~can_fail:false]) for sections that are otherwise applied to all backends.
+    The flag is rejected on non-Lean backends, so this only ever affects Lean.
+*)
+let unless_core_models_lib (funs : 'a list) : 'a list =
+  if !core_models_lib then [] else funs
+
 let mk_not_lean (funs : 'a list) : 'a list =
   match backend () with
   | Lean -> []
diff --git a/src/extract/ExtractHaxSpecs.ml b/src/extract/ExtractHaxSpecs.ml
new file mode 100644
index 000000000..d65a38f0e
--- /dev/null
+++ b/src/extract/ExtractHaxSpecs.ml
@@ -0,0 +1,357 @@
+module F = Format
+
+module Helpers = struct
+  (** Emit [words] separated by breakable spaces *)
+  let emit_words (fmt : F.formatter) (words : string list) : unit =
+    List.iteri
+      (fun i w ->
+        if i > 0 then F.pp_print_space fmt ();
+        F.pp_print_string fmt w)
+      words
+
+  (** Emit a pre/post condition function declaration. [extract_fun_decl] emits
+      its own leading break, so we add no trailing separator here. *)
+  let emit_cond (ctx : ExtractBase.extraction_ctx) (fmt : F.formatter)
+      (f : Pure.fun_decl) : unit =
+    Extract.extract_fun_decl ctx fmt ExtractBase.SingleNonRec false f
+
+  (** Run [k] on its own line inside an [hovbox] *)
+  let line (fmt : F.formatter) (k : unit -> unit) : unit =
+    F.pp_print_cut fmt ();
+    F.pp_open_hovbox fmt 0;
+    k ();
+    F.pp_close_box fmt ()
+
+  (** Wrap [k] in a Hoare-triple postcondition delimiter [⦃ … ⦄]. *)
+  let emit_wp (fmt : F.formatter) (k : unit -> unit) : unit =
+    Extract.emit_delim fmt "⦃" k "⦄"
+
+  (** Emit [<name> <generics> <args>] — an application head applied to its
+      generic and value arguments (caller controls the surrounding box). *)
+  let emit_app span ctx fmt explicit generics args (name : string) =
+    F.pp_print_string fmt name;
+    (* Generic args, matching the head's generic binders. *)
+    ExtractTypes.extract_generic_args span ctx fmt Pure.TypeDeclId.Set.empty
+      ~explicit:(Some explicit) generics;
+    List.iter
+      (fun te ->
+        F.pp_print_space fmt ();
+        Extract.extract_texpr span ctx fmt ~inside:true ~inside_do:false te)
+      args
+
+  (** Emit [(<cond> <generics> <args>).holds] for a fn [f] *)
+  let emit_holds span ctx fmt explicit generics args (f : Pure.fun_decl) =
+    let name = ExtractBase.ctx_get_local_function span f.def_id None ctx in
+    F.pp_open_hovbox fmt 0;
+    F.pp_print_string fmt "(";
+    emit_app span ctx fmt explicit generics args name;
+    F.pp_print_string fmt ").holds";
+    F.pp_close_box fmt ()
+end
+
+open Helpers
+
+(** Emit the proof of a spec/theorem as [:= by <tactic>]. *)
+let emit_proof fmt (p : HaxSpecs.proof) =
+  let tactic =
+    match p with
+    | Admitted -> "sorry"
+  in
+  F.pp_print_string fmt (":= by " ^ tactic)
+
+(** Emit the pre/post condition function declarations, if present. *)
+let emit_conditions ctx fmt ~pre ~post =
+  Option.iter (emit_cond ctx fmt) pre;
+  Option.iter (emit_cond ctx fmt) post
+
+(** Compute the [<fn>.spec] definition name for a hax-annotated function: the
+    formatted function name followed by the [.spec] suffix. The single source of
+    truth for the spec name — used by both the spec declaration ({!emit_spec})
+    and the proof obligation that references it ({!emit_obligation}). *)
+let compute_spec_name (def : Pure.fun_decl) (ctx : ExtractBase.extraction_ctx) :
+    string =
+  let fname =
+    ExtractBase.ctx_compute_fun_global_name_no_suffix def.item_meta def.src
+      ~is_trait_decl_field:false ctx
+  in
+  let lp_suffix =
+    ExtractBase.default_fun_suffix def.num_loops def.loop_id def.loop_pos
+  in
+  fname ^ lp_suffix ^ ".spec"
+
+(** Prelude shared by both statement styles: register the result variable (a
+    collision-safe fvar), build the [.holds] / application printers, emit the
+    (shared) optional precondition hypothesis [(<fn>.pre <args>).holds →] *)
+let emit_statement_prelude ctx fmt span (fn : Pure.FunDeclId.id) explicit
+    generics output_ty arg_texprs res_id ~(pre : Pure.fun_decl option)
+    ~(post : Pure.fun_decl option) =
+  let open ExtractBase in
+  (* Register the postcondition's result variable *)
+  let ctx, res_name = ctx_add_var span "res" res_id ctx in
+  let res_texpr : Pure.texpr = { e = FVar res_id; ty = output_ty } in
+
+  let emit_holds = emit_holds span ctx fmt explicit generics in
+
+  (* The real function application [<fn> <args>], via the standard printer. *)
+  let emit_fn_call () : unit =
+    let head : Pure.texpr =
+      {
+        e =
+          Qualif
+            {
+              id = FunOrOp (Fun (FromLlbc (FunId (FRegular fn), None)));
+              generics;
+            };
+        ty = output_ty;
+      }
+    in
+    Extract.extract_App span ctx fmt ~inside:false ~inside_do:false head
+      arg_texprs output_ty
+  in
+
+  (* Optional pre-hypothesis: [(<fn>.pre <args>).holds →]. *)
+  (match pre with
+  | None -> ()
+  | Some pre_fn ->
+      line fmt (fun () ->
+          emit_holds arg_texprs pre_fn;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "→"));
+
+  (* The postcondition body: [(<fn>.post <args> res).holds] or [True] *)
+  let emit_post_content () =
+    match post with
+    | None -> F.pp_print_string fmt "True"
+    | Some post_fn -> emit_holds (arg_texprs @ [ res_texpr ]) post_fn
+  in
+  (emit_fn_call, res_name, emit_post_content)
+
+(** Emits the [Step]-style spec statement — the body of
+    [def foo.spec … : Prop :=] (the
+    [@[step] theorem foo.spec.proof … := by sorry] wrapper is the obligation,
+    emitted separately):
+    {[
+      (foo.pre args).holds →
+      foo args
+      ⦃ res => (foo.post args res).holds ⦄
+    ]} *)
+let emit_statement_step ctx fmt span fn explicit generics output_ty arg_texprs
+    res_id pre post =
+  let emit_fn_call, res_name, emit_post_content =
+    emit_statement_prelude ctx fmt span fn explicit generics output_ty
+      arg_texprs res_id ~pre ~post
+  in
+  line fmt emit_fn_call;
+  line fmt (fun () ->
+      emit_wp fmt (fun () ->
+          emit_words fmt [ res_name; "=>" ];
+          F.pp_print_space fmt ();
+          emit_post_content ()))
+
+(** Emits the [Mvcgen]-style spec statement — the body of
+    [def foo.spec … : Prop :=] (the
+    [@[spec] theorem foo.spec.proof … := by sorry] wrapper is the obligation,
+    emitted separately):
+    {[
+      (foo.pre args).holds →
+      ⦃ ⌜ True ⌝ ⦄
+      foo args
+      ⦃ ⇓ res => ⌜ (foo.post args res).holds ⌝ ⦄
+    ]} *)
+let emit_statement_mvcgen ctx fmt span fn explicit generics output_ty arg_texprs
+    res_id pre post =
+  let emit_fn_call, res_name, emit_post_content =
+    emit_statement_prelude ctx fmt span fn explicit generics output_ty
+      arg_texprs res_id ~pre ~post
+  in
+  let emit_pure k = Extract.emit_delim fmt "⌜" k "⌝" in
+  line fmt (fun () ->
+      emit_wp fmt (fun () -> emit_pure (fun () -> F.pp_print_string fmt "True")));
+  line fmt emit_fn_call;
+  line fmt (fun () ->
+      emit_wp fmt (fun () ->
+          emit_words fmt [ "⇓"; res_name; "=>" ];
+          F.pp_print_space fmt ();
+          emit_pure emit_post_content))
+
+(** The spec backend selected via [-specs] (defaults to [Step]). *)
+let current_spec_backend () : Config.spec_backend =
+  Option.value (Config.spec_backend ()) ~default:Config.Step
+
+(** Emit the spec statement shape, dispatching on the spec backend configured
+    via [-specs]. *)
+let emit_statement ctx fmt span fn explicit generics output_ty arg_texprs res_id
+    pre post =
+  let emit =
+    match current_spec_backend () with
+    | Config.Mvcgen -> emit_statement_mvcgen
+    | Config.Step -> emit_statement_step
+  in
+  emit ctx fmt span fn explicit generics output_ty arg_texprs res_id pre post
+
+(** Emit one [Spec.spec] entry *)
+let emit_spec ctx fmt (s : HaxSpecs.spec) opt_span =
+  let open ExtractBase in
+  match s with
+  | FunctionSpec { fn; pre; post } -> (
+      match Pure.FunDeclId.Map.find_opt fn ctx.trans_funs with
+      | None ->
+          [%warn_opt_span] opt_span
+            ("Trying to print a spec for an unknown function '"
+            ^ Pure.FunDeclId.to_string fn
+            ^ "'")
+      | Some ft ->
+          (* Register the pre/post condition fns' names in the (local) context *)
+          let reg f_opt ctx =
+            Option.fold ~some:(fun f -> ctx_add_fun_decl f ctx) ~none:ctx f_opt
+          in
+          let ctx = ctx |> reg pre |> reg post in
+          let parent = ft.f in
+          let span = parent.item_meta.span in
+          let sg = parent.signature in
+          let explicit = sg.explicit_info in
+          let generics = PureUtils.generic_args_of_params sg.generics in
+
+          (* Open the parent's body binders *)
+          let _, fresh_fvar_id = Pure.FVarId.fresh_stateful_generator () in
+          let parent =
+            {
+              parent with
+              body =
+                Option.map
+                  (fun b ->
+                    snd (PureUtils.open_all_fun_body fresh_fvar_id span b))
+                  parent.body;
+            }
+          in
+          let arg_texprs =
+            match parent.body with
+            | None -> []
+            | Some { inputs; _ } ->
+                List.filter_map (PureUtils.tpat_to_texpr span) inputs
+          in
+          (* Fresh result-var id, from the body generator so it can't clash. *)
+          let res_id = fresh_fvar_id () in
+
+          (* Blank line before the entry. *)
+          F.pp_print_break fmt 0 0;
+
+          emit_conditions ctx fmt ~pre ~post;
+
+          (* Spec definition header: [def <fn>.spec <binders> : Prop :=] *)
+          F.pp_print_break fmt 0 0;
+          F.pp_open_vbox fmt 0;
+          F.pp_open_vbox fmt ctx.indent_incr;
+          F.pp_open_hovbox fmt ctx.indent_incr;
+          (match fun_decl_kind_to_qualif SingleNonRec with
+          | Some qualif ->
+              F.pp_print_string fmt qualif;
+              F.pp_print_space fmt ()
+          | None -> ());
+          F.pp_print_string fmt (compute_spec_name parent ctx);
+          (* Generic + value binders via the standard param extractor. *)
+          let space = ref false in
+          let _, ctx, _ = Extract.extract_fun_parameters space ctx fmt parent in
+          ExtractTypes.insert_req_space fmt space;
+          F.pp_print_string fmt ": Prop :=";
+          F.pp_close_box fmt ();
+
+          (* Statement shape (the def body). *)
+          emit_statement ctx fmt span fn explicit generics sg.output arg_texprs
+            res_id pre post;
+          F.pp_close_box fmt ();
+          (* inner vbox *)
+          F.pp_close_box fmt ();
+          (* outer vbox *)
+          F.pp_print_cut fmt ())
+
+(** Emit one [HaxSpecs.obligation] entry as the proof obligation that discharges
+    a spec's statement of correctness:
+    {[
+      @[spec]/@[step]
+      theorem foo.spec.proof args : foo.spec args := by sorry
+    ]}
+    The attribute ([step] / [spec]) follows the configured spec backend. *)
+let emit_obligation ctx fmt (o : HaxSpecs.obligation) opt_span =
+  let open ExtractBase in
+  match o with
+  | FunctionContract { spec = { fn; _ }; proof } -> (
+      match Pure.FunDeclId.Map.find_opt fn ctx.trans_funs with
+      | None ->
+          [%warn_opt_span] opt_span
+            ("Trying to print a proof obligation for an unknown function '"
+            ^ Pure.FunDeclId.to_string fn
+            ^ "'")
+      | Some ft ->
+          let parent = ft.f in
+          let span = parent.item_meta.span in
+          let sg = parent.signature in
+          let explicit = sg.explicit_info in
+          let generics = PureUtils.generic_args_of_params sg.generics in
+          (* The canonical [<fn>.spec] name, from the shared {!compute_spec_name}
+           (same as the spec declaration). *)
+          let spec_name = compute_spec_name parent ctx in
+
+          (* Open the parent's body binders *)
+          let _, fresh_fvar_id = Pure.FVarId.fresh_stateful_generator () in
+          let parent =
+            {
+              parent with
+              body =
+                Option.map
+                  (fun b ->
+                    snd (PureUtils.open_all_fun_body fresh_fvar_id span b))
+                  parent.body;
+            }
+          in
+          let arg_texprs =
+            match parent.body with
+            | None -> []
+            | Some { inputs; _ } ->
+                List.filter_map (PureUtils.tpat_to_texpr span) inputs
+          in
+
+          (* Blank line before the entry. *)
+          F.pp_print_break fmt 0 0;
+
+          (* Box layout (brackets = boxes):
+             [ [theorem name] binders : [statement] ]  [:= by sorry]
+             The outer [hvbox] keeps the whole theorem on one line if it fits;
+             otherwise [:= by sorry] breaks onto its own line first, and only if
+             the statement box itself still overflows do the binders/type wrap.
+             [extract_attributes]'s trailing break becomes a newline in the vbox. *)
+          let attr =
+            match current_spec_backend () with
+            | Config.Mvcgen -> "spec"
+            | Config.Step -> "step"
+          in
+          F.pp_open_vbox fmt 0;
+          ExtractTypes.extract_attributes span ctx fmt parent.item_meta.name
+            None [ attr ] "" [] ~is_external:false;
+          (* Outer box: [<statement> := by sorry] — break before the proof first. *)
+          F.pp_open_hvbox fmt ctx.indent_incr;
+          (* The theorem statement: [theorem name binders : <type>]. *)
+          F.pp_open_hovbox fmt ctx.indent_incr;
+          F.pp_print_string fmt "theorem";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt (spec_name ^ ".proof");
+          (* Generic + value binders via the standard param extractor. *)
+          let space = ref false in
+          let _, ctx, _ = Extract.extract_fun_parameters space ctx fmt parent in
+          ExtractTypes.insert_req_space fmt space;
+          F.pp_print_string fmt ":";
+          F.pp_print_space fmt ();
+          (* The statement of correctness, in its own box:
+             [<fn>.spec <generics> <args>]. *)
+          F.pp_open_hovbox fmt 0;
+          emit_app span ctx fmt explicit generics arg_texprs spec_name;
+          F.pp_close_box fmt ();
+          F.pp_close_box fmt ();
+          (* statement hovbox *)
+          F.pp_print_space fmt ();
+          emit_proof fmt proof;
+          F.pp_close_box fmt ();
+          (* outer hvbox *)
+          F.pp_close_box fmt ();
+          (* attribute vbox *)
+          F.pp_print_cut fmt ())
diff --git a/src/extract/ExtractHaxSpecs.mli b/src/extract/ExtractHaxSpecs.mli
new file mode 100644
index 000000000..7089c4b34
--- /dev/null
+++ b/src/extract/ExtractHaxSpecs.mli
@@ -0,0 +1,20 @@
+(** Lean printer for {!HaxSpecs.spec} and {!HaxSpecs.obligation} entries. *)
+
+module F = Format
+
+(** Emits one [HaxSpecs.spec] entry. The [span option] is used for errors *)
+val emit_spec :
+  ExtractBase.extraction_ctx ->
+  F.formatter ->
+  HaxSpecs.spec ->
+  Meta.span option ->
+  unit
+
+(** Emits one [HaxSpecs.obligation] entry. The [span option] is used for errors
+*)
+val emit_obligation :
+  ExtractBase.extraction_ctx ->
+  F.formatter ->
+  HaxSpecs.obligation ->
+  Meta.span option ->
+  unit
diff --git a/src/extract/ExtractSpec.ml b/src/extract/ExtractSpec.ml
new file mode 100644
index 000000000..d26462ffb
--- /dev/null
+++ b/src/extract/ExtractSpec.ml
@@ -0,0 +1,20 @@
+(** Dispatcher from the generic {!Spec} IR to the concrete spec printer.
+
+    Currently, guarded by a config flag to be only for the Lean backend. *)
+
+module F = Format
+
+(** Emit one [Spec.spec] entry. *)
+let emit_spec ctx fmt (s : Spec.spec) =
+  match s.kind with
+  | HaxSpec hs -> ExtractHaxSpecs.emit_spec ctx fmt hs s.span
+
+(** Emit one [Spec.proof_obligation] entry. *)
+let emit_proof_obligation ctx fmt (o : Spec.proof_obligation) =
+  match o.kind with
+  | HaxProof ho -> ExtractHaxSpecs.emit_obligation ctx fmt ho o.span
+
+let extract_specs ctx fmt = List.iter (emit_spec ctx fmt) ctx.specs
+
+let extract_proof_obligations ctx fmt =
+  List.iter (emit_proof_obligation ctx fmt) ctx.proof_obligations
diff --git a/src/pure/PureMicroPassesLoops.ml b/src/pure/PureMicroPassesLoops.ml
index b3f8e9182..311af2a50 100644
--- a/src/pure/PureMicroPassesLoops.ml
+++ b/src/pure/PureMicroPassesLoops.ml
@@ -2132,7 +2132,19 @@ let reorder_loop_outputs (ctx : ctx) (def : fun_decl) =
           if not (List.for_all Option.is_some arg_to_index) then None
           else
             let arg_to_index = List.map Option.get arg_to_index in
-            if List.for_all (fun (i, i') -> i = i') arg_to_index then
+            (* Check that the arguments are a true permutation of the pattern
+               variables: the lengths must be equal and the indices must be
+               duplicate-free. Note that the ok-tuple may repeat an fvar when
+               the forward result coincides with a given-back value (e.g.,
+               [return *x] inside a loop over [x : &mut u32] leads to
+               [ok (v, v)]): in this case we simply skip the reordering. *)
+            if
+              List.length args <> List.length patl_fvars
+              || Collections.IntSet.cardinal
+                   (Collections.IntSet.of_list (List.map snd arg_to_index))
+                 <> List.length arg_to_index
+            then None
+            else if List.for_all (fun (i, i') -> i = i') arg_to_index then
               (* Order is the same: no need to reorder *)
               None
             else
diff --git a/src/specs/HaxProducer.ml b/src/specs/HaxProducer.ml
new file mode 100644
index 000000000..e32734bf8
--- /dev/null
+++ b/src/specs/HaxProducer.ml
@@ -0,0 +1,191 @@
+(** The hax specs producer.
+
+    Hax encodes [#[hax_lib::requires(...)]] / [#[hax_lib::ensures(|r| ...)]]
+    annotations as separate "decoration" functions plus [_hax::json] attributes
+    that link a real function to its pre/post decorations by UUID. This module
+    parses those attributes, and the [produce] producer folds them into
+    {!Spec.spec} / {!Spec.proof_obligation} entries (consuming the decoration
+    functions). The [_hax::json] attribute payloads are parsed by
+    {!HaxAttributes}. *)
+
+open HaxAttributes
+
+let log = Logging.translate_log
+
+(** Per-parent accumulator while scanning attributes. *)
+type assoc = {
+  parent : Pure.fun_decl;
+  requires_uid : string option;
+  ensures_uid : string option;
+}
+
+let empty_assoc parent = { parent; requires_uid = None; ensures_uid = None }
+
+(** Update an accumulator with one [AssociatedItem]. Per design we accept at
+    most one of each role per fn: extras are logged and ignored. *)
+let update_assoc (role : hax_role) (uid : string) (a : assoc) : assoc =
+  let warn_extra side =
+    [%lwarning
+      Printf.sprintf "hax-specs: multiple #[%s] on fn `%s`; ignoring extras"
+        side a.parent.name]
+  in
+  match role with
+  | Requires -> (
+      match a.requires_uid with
+      | None -> { a with requires_uid = Some uid }
+      | Some _ ->
+          warn_extra "requires";
+          a)
+  | Ensures -> (
+      match a.ensures_uid with
+      | None -> { a with ensures_uid = Some uid }
+      | Some _ ->
+          warn_extra "ensures";
+          a)
+  | Other_role -> a
+
+(** Read a hax-annotated crate: emit one [FunctionSpec] per real fn that carries
+    [AssociatedItem] attribute(s), and strip the decoration fns whose bodies
+    have been folded into those specs. *)
+let produce (_ctx : TranslateCore.trans_ctx)
+    (crate : TranslateCore.translated_crate) : TranslateCore.translated_crate =
+  let _, fresh_spec_id = Spec.SpecId.fresh_stateful_generator () in
+  let _, fresh_proof_id = Spec.ProofId.fresh_stateful_generator () in
+  let uid_map : Pure.fun_decl Collections.StringMap.t ref =
+    ref Collections.StringMap.empty
+  in
+  let dec_set : Pure.FunDeclId.Set.t ref = ref Pure.FunDeclId.Set.empty in
+  let assoc_map : assoc Pure.FunDeclId.Map.t ref =
+    ref Pure.FunDeclId.Map.empty
+  in
+  (* Pass 1: classify each fun_decl by its [_hax::json] payloads. *)
+  List.iter
+    (fun (ft : TranslateCore.pure_fun_translation) ->
+      let f = ft.f in
+      List.iter
+        (fun a ->
+          match parse_attr a with
+          | None | Some Other_payload | Some Late_skip -> ()
+          | Some (Uid uid) ->
+              uid_map := Collections.StringMap.add uid f !uid_map;
+              dec_set := Pure.FunDeclId.Set.add f.def_id !dec_set
+          | Some (Associated_item { role; uid }) ->
+              let cur =
+                match Pure.FunDeclId.Map.find_opt f.def_id !assoc_map with
+                | Some a -> a
+                | None -> empty_assoc f
+              in
+              assoc_map :=
+                Pure.FunDeclId.Map.add f.def_id
+                  (update_assoc role uid cur)
+                  !assoc_map)
+        f.item_meta.attr_info.attributes)
+    crate.fun_decls;
+
+  (* Pass 2: resolve uids to decoration fns and build [Spec.spec] /
+     [Spec.proof_obligation] entries.
+
+     A decoration fn is reused as a proper function: we rename it to
+     [<parent>::<suffix>] and mark it [reducible], so the standard function
+     extractor prints it as [@[reducible] def <fn>.pre …] / [… .post …]. The
+     whole [Pure.fun_decl] is stashed in the spec (it is stripped from
+     [crate.fun_decls] in pass 3, so it isn't also printed among the regular
+     functions). *)
+  let rename_decoration (parent : Pure.fun_decl) (suffix : string)
+      (dec : Pure.fun_decl) : Pure.fun_decl =
+    let name =
+      parent.item_meta.name
+      @ [ Types.PeIdent (suffix, Pure.Disambiguator.zero) ]
+    in
+    let item_meta = { dec.item_meta with name } in
+    {
+      dec with
+      item_meta;
+      name = parent.name ^ "." ^ suffix;
+      backend_attributes = { reducible = true };
+    }
+  in
+  (* Resolve a decoration uid. Checks the arity. *)
+  let lookup_dec (parent : Pure.fun_decl) ~(suffix : string) ?(is_post = false)
+      (uid : string) : Pure.fun_decl option =
+    match Collections.StringMap.find_opt uid !uid_map with
+    | None ->
+        [%lwarning
+          Printf.sprintf
+            "hax-specs: fn `%s` references unknown decoration uid %s; skipping \
+             that side"
+            parent.name uid];
+        None
+    | Some dec ->
+        let decl = rename_decoration parent suffix dec in
+        let expected_arity =
+          List.length parent.signature.inputs + if is_post then 1 else 0
+        in
+        let actual_arity = List.length decl.signature.inputs in
+        if expected_arity = actual_arity then Some decl
+        else begin
+          [%lwarning
+            Printf.sprintf
+              "hax-specs: argument count mismatch for `%s.%s` (takes %d, \
+               expected %d); dropping this condition"
+              parent.name suffix actual_arity expected_arity];
+          None
+        end
+  in
+  let shape = function
+    | None -> "absent"
+    | Some _ -> "present"
+  in
+  (* Build the spec (statement of correctness) and the proof obligation that
+     discharges it, for one parent fn's accumulated [AssociatedItem]s. *)
+  let build_entry (parent_id, a) : (Spec.spec * Spec.proof_obligation) option =
+    let pre = Option.bind a.requires_uid (lookup_dec a.parent ~suffix:"pre") in
+    let post =
+      Option.bind a.ensures_uid
+        (lookup_dec a.parent ~suffix:"post" ~is_post:true)
+    in
+    if Option.is_none pre && Option.is_none post then None
+    else (
+      [%ltrace
+        Printf.sprintf "hax-specs:   fn=%s pre=%s post=%s" a.parent.name
+          (shape pre) (shape post)];
+      let span = Some a.parent.item_meta.span in
+      (* One [function_spec] payload, shared between the spec and the proof
+         obligation that discharges it. *)
+      let fspec : HaxSpecs.function_spec = { fn = parent_id; pre; post } in
+      let spec : Spec.spec =
+        { id = fresh_spec_id (); span; kind = HaxSpec (FunctionSpec fspec) }
+      in
+      let obligation : Spec.proof_obligation =
+        {
+          id = fresh_proof_id ();
+          span;
+          kind = HaxProof (FunctionContract { spec = fspec; proof = Admitted });
+        }
+      in
+      Some (spec, obligation))
+  in
+  let new_specs, new_obligations =
+    Pure.FunDeclId.Map.bindings !assoc_map
+    |> List.filter_map build_entry
+    |> List.split
+  in
+
+  (* Pass 3: strip consumed decoration fns from [crate.fun_decls]. *)
+  let new_fun_decls =
+    List.filter
+      (fun (ft : TranslateCore.pure_fun_translation) ->
+        not (Pure.FunDeclId.Set.mem ft.f.def_id !dec_set))
+      crate.fun_decls
+  in
+
+  [%linfo
+    Printf.sprintf "hax-specs: produced %d FunctionSpec entries"
+      (List.length new_specs)];
+
+  {
+    crate with
+    fun_decls = new_fun_decls;
+    specs = crate.specs @ new_specs;
+    proof_obligations = crate.proof_obligations @ new_obligations;
+  }
diff --git a/src/specs/HaxSpecs.ml b/src/specs/HaxSpecs.ml
new file mode 100644
index 000000000..81c4841d9
--- /dev/null
+++ b/src/specs/HaxSpecs.ml
@@ -0,0 +1,28 @@
+(** The Hax spec-objects
+
+    Hax_lib macros allow for specs written directly in rust. This module
+    provides type definitions to represent such specs. Currently, it supports
+    only pre/post on standalone functions. *)
+
+(** Type for spec objects *)
+type spec = FunctionSpec of function_spec [@@deriving show]
+
+and function_spec = {
+  fn : Pure.FunDeclId.id;
+  pre : Pure.fun_decl option;  (** Precondition *)
+  post : Pure.fun_decl option;  (** Postcondition *)
+}
+[@@deriving show]
+
+(** Type for proof-obligation objects. *)
+and obligation = FunctionContract of { spec : function_spec; proof : proof }
+[@@deriving show]
+
+(** Type for proof objects *)
+and proof = Admitted [@@deriving show]
+
+(** The extra Lean modules hax specs need to elaborate *)
+let required_imports () : string list =
+  match Config.spec_backend () with
+  | Some Config.Mvcgen -> [ "Hax" ]
+  | Some Config.Step | None -> []
diff --git a/src/specs/Spec.ml b/src/specs/Spec.ml
new file mode 100644
index 000000000..f70547d2b
--- /dev/null
+++ b/src/specs/Spec.ml
@@ -0,0 +1,28 @@
+open Identifiers
+open Meta
+module SpecId = IdGen ()
+module ProofId = IdGen ()
+
+(** The shape of a spec entry *)
+type spec_kind = HaxSpec of HaxSpecs.spec [@@deriving show]
+
+(** A spec entry: a statement of correctness *)
+type spec = { id : SpecId.id; kind : spec_kind; span : span option }
+[@@deriving show]
+
+(** The shape of a proof-obligation entry *)
+type proof_kind = HaxProof of HaxSpecs.obligation [@@deriving show]
+
+(** A proof obligation: a theorem to discharge *)
+type proof_obligation = {
+  id : ProofId.id;
+  kind : proof_kind;
+  span : span option;
+}
+[@@deriving show]
+
+(** The extra Lean modules the configured spec source needs to elaborate *)
+let required_imports () : string list =
+  match !Config.opt_spec_config with
+  | Some (Config.Hax, _) -> HaxSpecs.required_imports ()
+  | None -> []
diff --git a/src/symbolic/SymbolicToPureTypes.ml b/src/symbolic/SymbolicToPureTypes.ml
index 5ea3e9be6..71629fad8 100644
--- a/src/symbolic/SymbolicToPureTypes.ml
+++ b/src/symbolic/SymbolicToPureTypes.ml
@@ -311,6 +311,21 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
     match_name_find_opt ctx def.item_meta.name
       (ExtractBuiltin.builtin_types_map ())
   in
+  (* Under [-core-models-lib] the builtin type overrides are disabled, so the
+     lookup above returns [None]. We still need the allocator [keep_params] of
+     types like [IntoIter] so that the dangling allocator type parameter (left
+     by Charon's [hide_allocator] pass) is filtered out, matching the
+     [core_models] library. Recover it from the dedicated, non-disabled map.
+     This only carries [keep_params]; the extract name still comes from the
+     standard name mangling (which, for these types, coincides with the builtin
+     name anyway). *)
+  let builtin_info =
+    if Option.is_some builtin_info || not !Config.core_models_lib then
+      builtin_info
+    else
+      match_name_find_opt ctx def.item_meta.name
+        (ExtractBuiltin.builtin_types_keep_params_map ())
+  in
   {
     def_id;
     name;
diff --git a/src/utils/HaxAttributes.ml b/src/utils/HaxAttributes.ml
new file mode 100644
index 000000000..63cc98521
--- /dev/null
+++ b/src/utils/HaxAttributes.ml
@@ -0,0 +1,84 @@
+(** Parsing of hax's [_hax::json(...)] item attributes.
+
+    Hax encodes [#[hax_lib::requires(...)]] / [#[hax_lib::ensures(|r| ...)]]
+    annotations (and several internal markers) as [_hax::json] attributes
+    carrying a JSON payload. This module decodes those payloads; the consumers
+    ({!HaxProducer.produce} and the late-skip pre-pass) decide what to do with
+    them. *)
+
+let log = Logging.translate_log
+
+(** Role carried by an [AssociatedItem] payload. Hax defines more roles
+    ([Decreases], [SmtPat], …); we collapse the ones we don't handle into
+    [Other_role]. *)
+type hax_role = Requires | Ensures | Other_role
+
+(** A parsed [_hax::json(...)] payload. Hax emits several payload shapes (`Uid`,
+    `AssociatedItem`, `ItemStatus`, `NeverErased`, `Language`, …); we act on the
+    three we care about and lump the rest into [Other_payload]. *)
+type hax_payload =
+  | Uid of string  (** [{"Uid":{"uid":"<hex32>"}}] — tags a decoration fn *)
+  | Associated_item of { role : hax_role; uid : string }
+      (** [{"AssociatedItem":{"role":"Requires"|"Ensures","item":{"uid":"<hex32>"}}}]
+          — links a real fn to a decoration fn by uid. *)
+  | Late_skip
+      (** [{"ItemStatus":{"Included":{"late_skip":true}}}] — hax-internal helper
+          (the [const _: () = { … }] wrapper around a decoration, the
+          [fn future] helper inside an [ensures] block, …). These items are not
+          meant to appear in the extracted output. *)
+  | Other_payload
+
+(** Two-step parse of the [args] string charon stores for a [_hax::json] attr.
+
+    Charon records [args] as the verbatim pretty-print of the token stream
+    inside the [(...)], which for hax-emitted attributes is a Rust string
+    literal containing the JSON: e.g. [args] = ["{\"Uid\":{\"uid\":\"...\"}}"].
+    The outer Rust string-literal escapes happen to also be valid JSON string
+    escapes, so we parse twice with [Yojson.Safe.from_string]: first to unwrap
+    the string literal, then to parse the inner JSON. *)
+let parse_args (args : string) : Yojson.Safe.t option =
+  try
+    match Yojson.Safe.from_string args with
+    | `String inner -> Some (Yojson.Safe.from_string inner)
+    | _ -> None
+  with _ -> None
+
+let role_of_string : string -> hax_role = function
+  | "Requires" -> Requires
+  | "Ensures" -> Ensures
+  | _ -> Other_role
+
+let parse_payload (j : Yojson.Safe.t) : hax_payload =
+  match j with
+  | `Assoc [ ("Uid", `Assoc [ ("uid", `String uid) ]) ] -> Uid uid
+  | `Assoc [ ("AssociatedItem", `Assoc fields) ] -> (
+      let role = ref None and uid = ref None in
+      List.iter
+        (fun (k, v) ->
+          match (k, v) with
+          | "role", `String r -> role := Some (role_of_string r)
+          | "item", `Assoc [ ("uid", `String u) ] -> uid := Some u
+          | _ -> ())
+        fields;
+      match (!role, !uid) with
+      | Some role, Some uid -> Associated_item { role; uid }
+      | _ -> Other_payload)
+  | `Assoc
+      [
+        ( "ItemStatus",
+          `Assoc [ ("Included", `Assoc [ ("late_skip", `Bool true) ]) ] );
+      ] -> Late_skip
+  | _ -> Other_payload
+
+(** Parse one [Meta.attribute]; [None] for anything that isn't a recognized
+    [_hax::json] payload. *)
+let parse_attr : Charon.Meta.attribute -> hax_payload option = function
+  | AttrUnknown { path = "_hax::json"; args = Some s } -> (
+      match parse_args s with
+      | Some j -> Some (parse_payload j)
+      | None ->
+          (* A [_hax::json] attribute whose args we couldn't decode as the
+             expected two-step JSON *)
+          [%ltrace Printf.sprintf "failed to parse _hax::json payload: %s" s];
+          None)
+  | _ -> None
diff --git a/tests/lean/BaseTutorial.lean b/tests/lean/BaseTutorial.lean
index 52a9947fe..d9b11240b 100644
--- a/tests/lean/BaseTutorial.lean
+++ b/tests/lean/BaseTutorial.lean
@@ -133,9 +133,9 @@ theorem mul2_add1_spec
      the fact that [2 * x + 1 < U32.max]. In case [step] fails to prove a
      precondition, it leaves it as a subgoal.
    -/
-  step with U32.add_spec as ⟨ x1 ⟩
+  step with U32.add_spec.step_spec as ⟨ x1 ⟩
   /- We can call [step] a second time for the second addition -/
-  step with U32.add_spec as ⟨ x2 ⟩
+  step with U32.add_spec.step_spec as ⟨ x2 ⟩
   /- We are now left with the remaining goal. We do this by calling
      [grind], an automated decision procedure
    -/
diff --git a/tests/lean/HaxSpecs/HaxSpecs.lean b/tests/lean/HaxSpecs/HaxSpecs.lean
new file mode 100644
index 000000000..26c18df78
--- /dev/null
+++ b/tests/lean/HaxSpecs/HaxSpecs.lean
@@ -0,0 +1,389 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hax_specs]
+import Aeneas
+import Hax
+open Aeneas Aeneas.Std Result ControlFlow Error
+open Std.Do
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
+namespace hax_specs
+
+/-- [core::ops::arith::{impl core::ops::arith::Add<&'_0 u32, u32> for &'_1 u32}::add]:
+    Source: '/rustc/library/core/src/internal_macros.rs', lines 49:12-49:68
+    Name pattern: [core::ops::arith::{core::ops::arith::Add<&'1 u32, &'0 u32, u32>}::add]
+    Visibility: public -/
+@[rust_fun
+  "core::ops::arith::{core::ops::arith::Add<&'1 u32, &'0 u32, u32>}::add"]
+axiom Shared1U32.Insts.CoreOpsArithAddShared0U32U32.add
+  : Std.U32 → Std.U32 → Result Std.U32
+
+/-- [hax_specs::basic::only_requires]:
+    Source: 'src/lib.rs', lines 6:4-8:5 -/
+def basic.only_requires (x : Std.U32) : Result Std.U32 := do
+  x + 1#u32
+
+/-- [hax_specs::basic::only_ensures]:
+    Source: 'src/lib.rs', lines 11:4-13:5 -/
+def basic.only_ensures (x : Std.U32) : Result Std.U32 := do
+  ok x
+
+/-- [hax_specs::basic::both]:
+    Source: 'src/lib.rs', lines 17:4-19:5 -/
+def basic.both (x : Std.U32) : Result Std.U32 := do
+  x + 1#u32
+
+/-- [hax_specs::basic::no_args]:
+    Source: 'src/lib.rs', lines 23:4-26:5 -/
+def basic.no_args : Result Unit := do
+  ok ()
+
+/-- [hax_specs::basic::returns_unit]:
+    Source: 'src/lib.rs', lines 31:4-31:30 -/
+def basic.returns_unit (x : Std.U32) : Result Unit := do
+  ok ()
+
+/-- [hax_specs::basic::block_in_requires]:
+    Source: 'src/lib.rs', lines 35:4-37:5 -/
+def basic.block_in_requires (x : Std.U32) : Result Std.U32 := do
+  ok x
+
+/-- [hax_specs::basic::returns_pair]:
+    Source: 'src/lib.rs', lines 41:4-43:5 -/
+def basic.returns_pair (x : Std.U32) : Result (Std.U32 × Std.U32) := do
+  ok (x, x)
+
+/-- [hax_specs::extra_args::generic]:
+    Source: 'src/lib.rs', lines 53:4-55:5 -/
+def extra_args.generic (N : Std.U32) (x : Std.U32) : Result Std.U32 := do
+  N - x
+
+/-- Trait declaration: [hax_specs::extra_args::Val]
+    Source: 'src/lib.rs', lines 58:4-60:5 -/
+structure extra_args.Val (Self : Type) where
+  value : Self → Result Std.U32
+
+/-- [hax_specs::extra_args::{impl hax_specs::extra_args::Val for u32}::value]:
+    Source: 'src/lib.rs', lines 63:8-65:9 -/
+def U32.Insts.Hax_specsExtra_argsVal.value
+  (self : Std.U32) : Result Std.U32 := do
+  ok self
+
+/-- Trait implementation: [hax_specs::extra_args::{impl hax_specs::extra_args::Val for u32}]
+    Source: 'src/lib.rs', lines 62:4-66:5 -/
+@[reducible]
+def U32.Insts.Hax_specsExtra_argsVal : extra_args.Val Std.U32 := {
+  value := U32.Insts.Hax_specsExtra_argsVal.value
+}
+
+/-- [hax_specs::extra_args::traits]:
+    Source: 'src/lib.rs', lines 70:4-72:5 -/
+def extra_args.traits
+  {T : Type} (ValInst : extra_args.Val T) (t : T) (x : Std.U32) :
+  Result Std.U32
+  := do
+  let i ← ValInst.value t
+  i + x
+
+/-- [hax_specs::future::incr]:
+    Source: 'src/lib.rs', lines 81:4-83:5 -/
+def future.incr (x : Std.U32) : Result Std.U32 := do
+  x + 1#u32
+
+/-- [hax_specs::future::incr_i]:
+    Source: 'src/lib.rs', lines 89:4-91:5 -/
+def future.incr_i
+  (x : Slice Std.U32) (i : Std.Usize) : Result (Slice Std.U32) := do
+  let i1 ← Slice.index_usize x i
+  let i2 ← i1 + 1#u32
+  Slice.update x i i2
+
+/-- [hax_specs::future::swap_and_add]:
+    Source: 'src/lib.rs', lines 95:4-101:5 -/
+def future.swap_and_add
+  (x : Std.U32) (y : Std.U32) : Result (Std.U32 × Std.U32 × Std.U32) := do
+  let i ← x + y
+  ok (i, y, x)
+
+
+/-- [hax_specs::basic::only_requires::pre]:
+    Source: 'src/lib.rs', lines 5:4-5:24 -/
+@[reducible]
+def basic.only_requires.pre (x : Std.U32) : Result Bool := do
+  ok (x < 100#u32)
+
+def basic.only_requires.spec (x : Std.U32) : Prop :=
+  (basic.only_requires.pre x).holds →
+  ⦃ ⌜ True ⌝ ⦄
+  basic.only_requires x
+  ⦃ ⇓ res => ⌜ True ⌝ ⦄
+
+
+/-- [hax_specs::basic::only_ensures::post]:
+    Source: 'src/lib.rs', lines 10:4-10:36 -/
+@[reducible]
+def basic.only_ensures.post
+  (x : Std.U32) (result : Std.U32) : Result Bool := do
+  ok (result = x)
+
+def basic.only_ensures.spec (x : Std.U32) : Prop :=
+  ⦃ ⌜ True ⌝ ⦄
+  basic.only_ensures x
+  ⦃ ⇓ res => ⌜ (basic.only_ensures.post x res).holds ⌝ ⦄
+
+
+/-- [hax_specs::basic::both::pre]:
+    Source: 'src/lib.rs', lines 15:4-15:23 -/
+@[reducible]
+def basic.both.pre (x : Std.U32) : Result Bool := do
+  ok (x < 10#u32)
+
+/-- [hax_specs::basic::both::post]:
+    Source: 'src/lib.rs', lines 16:4-16:35 -/
+@[reducible]
+def basic.both.post (x : Std.U32) (result : Std.U32) : Result Bool := do
+  ok (result > x)
+
+def basic.both.spec (x : Std.U32) : Prop :=
+  (basic.both.pre x).holds →
+  ⦃ ⌜ True ⌝ ⦄
+  basic.both x
+  ⦃ ⇓ res => ⌜ (basic.both.post x res).holds ⌝ ⦄
+
+
+/-- [hax_specs::basic::returns_unit::pre]:
+    Source: 'src/lib.rs', lines 29:4-29:23 -/
+@[reducible]
+def basic.returns_unit.pre (x : Std.U32) : Result Bool := do
+  ok (x < 10#u32)
+
+/-- [hax_specs::basic::returns_unit::post]:
+    Source: 'src/lib.rs', lines 30:4-30:24 -/
+@[reducible]
+def basic.returns_unit.post (x : Std.U32) (_ : Unit) : Result Bool := do
+  ok true
+
+def basic.returns_unit.spec (x : Std.U32) : Prop :=
+  (basic.returns_unit.pre x).holds →
+  ⦃ ⌜ True ⌝ ⦄
+  basic.returns_unit x
+  ⦃ ⇓ res => ⌜ (basic.returns_unit.post x res).holds ⌝ ⦄
+
+
+/-- [hax_specs::basic::block_in_requires::pre]:
+    Source: 'src/lib.rs', lines 34:4-34:46 -/
+@[reducible]
+def basic.block_in_requires.pre (x : Std.U32) : Result Bool := do
+  ok (x > 10#u32)
+
+def basic.block_in_requires.spec (x : Std.U32) : Prop :=
+  (basic.block_in_requires.pre x).holds →
+  ⦃ ⌜ True ⌝ ⦄
+  basic.block_in_requires x
+  ⦃ ⇓ res => ⌜ True ⌝ ⦄
+
+
+/-- [hax_specs::basic::returns_pair::post]:
+    Source: 'src/lib.rs', lines 40:4-40:41 -/
+@[reducible]
+def basic.returns_pair.post
+  (x : Std.U32) (p : (Std.U32 × Std.U32)) : Result Bool := do
+  let (a, b) := p
+  if a = x
+  then ok (b = x)
+  else ok false
+
+def basic.returns_pair.spec (x : Std.U32) : Prop :=
+  ⦃ ⌜ True ⌝ ⦄
+  basic.returns_pair x
+  ⦃ ⇓ res => ⌜ (basic.returns_pair.post x res).holds ⌝ ⦄
+
+
+/-- [hax_specs::extra_args::generic::pre]:
+    Source: 'src/lib.rs', lines 51:4-51:31 -/
+@[reducible]
+def extra_args.generic.pre (N : Std.U32) (x : Std.U32) : Result Bool := do
+  if 0#u32 < x
+  then ok (x < N)
+  else ok false
+
+/-- [hax_specs::extra_args::generic::post]:
+    Source: 'src/lib.rs', lines 52:4-52:35 -/
+@[reducible]
+def extra_args.generic.post
+  (N : Std.U32) (x : Std.U32) (result : Std.U32) : Result Bool := do
+  ok (result < N)
+
+def extra_args.generic.spec (N : Std.U32) (x : Std.U32) : Prop :=
+  (extra_args.generic.pre N x).holds →
+  ⦃ ⌜ True ⌝ ⦄
+  extra_args.generic N x
+  ⦃ ⇓ res => ⌜ (extra_args.generic.post N x res).holds ⌝ ⦄
+
+
+/-- [hax_specs::extra_args::traits::pre]:
+    Source: 'src/lib.rs', lines 68:4-68:45 -/
+@[reducible]
+def extra_args.traits.pre
+  {T : Type} (ValInst : extra_args.Val T) (t : T) (x : Std.U32) :
+  Result Bool
+  := do
+  let i ← ValInst.value t
+  if i < 1000#u32
+  then ok (x < 1000#u32)
+  else ok false
+
+/-- [hax_specs::extra_args::traits::post]:
+    Source: 'src/lib.rs', lines 69:4-69:38 -/
+@[reducible]
+def extra_args.traits.post
+  {T : Type} (ValInst : extra_args.Val T) (t : T) (x : Std.U32)
+  (result : Std.U32) :
+  Result Bool
+  := do
+  ok (result < 2000#u32)
+
+def extra_args.traits.spec {T : Type} (ValInst : extra_args.Val T) (t : T)
+  (x : Std.U32) : Prop :=
+  (extra_args.traits.pre ValInst t x).holds →
+  ⦃ ⌜ True ⌝ ⦄
+  extra_args.traits ValInst t x
+  ⦃ ⇓ res => ⌜ (extra_args.traits.post ValInst t x res).holds ⌝ ⦄
+
+
+/-- [hax_specs::future::incr::pre]:
+    Source: 'src/lib.rs', lines 79:4-79:26 -/
+@[reducible]
+def future.incr.pre (x : Std.U32) : Result Bool := do
+  ok (x < 1000#u32)
+
+/-- [hax_specs::future::incr::post]:
+    Source: 'src/lib.rs', lines 80:4-80:41 -/
+@[reducible]
+def future.incr.post (x : Std.U32) (x_future : Std.U32) : Result Bool := do
+  let i ← x + 1#u32
+  ok (x_future = i)
+
+def future.incr.spec (x : Std.U32) : Prop :=
+  (future.incr.pre x).holds →
+  ⦃ ⌜ True ⌝ ⦄
+  future.incr x
+  ⦃ ⇓ res => ⌜ (future.incr.post x res).holds ⌝ ⦄
+
+
+/-- [hax_specs::future::incr_i::pre]:
+    Source: 'src/lib.rs', lines 85:4-85:28 -/
+@[reducible]
+def future.incr_i.pre (x : Slice Std.U32) (i : Std.Usize) : Result Bool := do
+  let i1 := Slice.len x
+  ok (i < i1)
+
+/-- [hax_specs::future::incr_i::post]:
+    Source: 'src/lib.rs', lines 86:4-88:31 -/
+@[reducible]
+def future.incr_i.post
+  (x : Slice Std.U32) (i : Std.Usize) (x_future : Slice Std.U32) :
+  Result Bool
+  := do
+  let i1 ← Slice.index_usize x_future i
+  let i2 ← Slice.index_usize x i
+  let i3 ← i2 + 1#u32
+  ok (i1 = i3)
+
+def future.incr_i.spec (x : Slice Std.U32) (i : Std.Usize) : Prop :=
+  (future.incr_i.pre x i).holds →
+  ⦃ ⌜ True ⌝ ⦄
+  future.incr_i x i
+  ⦃ ⇓ res => ⌜ (future.incr_i.post x i res).holds ⌝ ⦄
+
+
+/-- [hax_specs::future::swap_and_add::pre]:
+    Source: 'src/lib.rs', lines 93:4-93:39 -/
+@[reducible]
+def future.swap_and_add.pre (x : Std.U32) (y : Std.U32) : Result Bool := do
+  if x < 1000#u32
+  then ok (y < 1000#u32)
+  else ok false
+
+/-- [hax_specs::future::swap_and_add::post]:
+    Source: 'src/lib.rs', lines 94:4-94:73 -/
+@[reducible]
+def future.swap_and_add.post
+  (x : Std.U32) (y : Std.U32) (t : (Std.U32 × Std.U32 × Std.U32)) :
+  Result Bool
+  := do
+  let (x_future, y_future, r) := t
+  if y_future = x
+  then
+    if x_future = y
+    then
+      let i ← Shared1U32.Insts.CoreOpsArithAddShared0U32U32.add x y
+      ok (r = i)
+    else ok false
+  else ok false
+
+def future.swap_and_add.spec (x : Std.U32) (y : Std.U32) : Prop :=
+  (future.swap_and_add.pre x y).holds →
+  ⦃ ⌜ True ⌝ ⦄
+  future.swap_and_add x y
+  ⦃ ⇓ res => ⌜ (future.swap_and_add.post x y res).holds ⌝ ⦄
+
+@[spec]
+theorem basic.only_requires.spec.proof (x : Std.U32) :
+  basic.only_requires.spec x
+  := by sorry
+
+@[spec]
+theorem basic.only_ensures.spec.proof (x : Std.U32) : basic.only_ensures.spec x
+  := by sorry
+
+@[spec]
+theorem basic.both.spec.proof (x : Std.U32) : basic.both.spec x := by sorry
+
+@[spec]
+theorem basic.returns_unit.spec.proof (x : Std.U32) : basic.returns_unit.spec x
+  := by sorry
+
+@[spec]
+theorem basic.block_in_requires.spec.proof (x : Std.U32) :
+  basic.block_in_requires.spec x
+  := by sorry
+
+@[spec]
+theorem basic.returns_pair.spec.proof (x : Std.U32) : basic.returns_pair.spec x
+  := by sorry
+
+@[spec]
+theorem extra_args.generic.spec.proof (N : Std.U32) (x : Std.U32) :
+  extra_args.generic.spec N x
+  := by sorry
+
+@[spec]
+theorem extra_args.traits.spec.proof {T : Type} (ValInst : extra_args.Val T)
+  (t : T) (x : Std.U32) : extra_args.traits.spec ValInst t x
+  := by sorry
+
+@[spec]
+theorem future.incr.spec.proof (x : Std.U32) : future.incr.spec x := by sorry
+
+@[spec]
+theorem future.incr_i.spec.proof (x : Slice Std.U32) (i : Std.Usize) :
+  future.incr_i.spec x i
+  := by sorry
+
+@[spec]
+theorem future.swap_and_add.spec.proof (x : Std.U32) (y : Std.U32) :
+  future.swap_and_add.spec x y
+  := by sorry
+
+end hax_specs
diff --git a/tests/lean/HaxSpecsStep/HaxSpecsStep.lean b/tests/lean/HaxSpecsStep/HaxSpecsStep.lean
new file mode 100644
index 000000000..c5f55b962
--- /dev/null
+++ b/tests/lean/HaxSpecsStep/HaxSpecsStep.lean
@@ -0,0 +1,376 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hax_specs]
+import Aeneas
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
+namespace hax_specs
+
+/-- [core::ops::arith::{impl core::ops::arith::Add<&'_0 u32, u32> for &'_1 u32}::add]:
+    Source: '/rustc/library/core/src/internal_macros.rs', lines 49:12-49:68
+    Name pattern: [core::ops::arith::{core::ops::arith::Add<&'1 u32, &'0 u32, u32>}::add]
+    Visibility: public -/
+@[rust_fun
+  "core::ops::arith::{core::ops::arith::Add<&'1 u32, &'0 u32, u32>}::add"]
+axiom Shared1U32.Insts.CoreOpsArithAddShared0U32U32.add
+  : Std.U32 → Std.U32 → Result Std.U32
+
+/-- [hax_specs::basic::only_requires]:
+    Source: 'src/lib.rs', lines 6:4-8:5 -/
+def basic.only_requires (x : Std.U32) : Result Std.U32 := do
+  x + 1#u32
+
+/-- [hax_specs::basic::only_ensures]:
+    Source: 'src/lib.rs', lines 11:4-13:5 -/
+def basic.only_ensures (x : Std.U32) : Result Std.U32 := do
+  ok x
+
+/-- [hax_specs::basic::both]:
+    Source: 'src/lib.rs', lines 17:4-19:5 -/
+def basic.both (x : Std.U32) : Result Std.U32 := do
+  x + 1#u32
+
+/-- [hax_specs::basic::no_args]:
+    Source: 'src/lib.rs', lines 23:4-26:5 -/
+def basic.no_args : Result Unit := do
+  ok ()
+
+/-- [hax_specs::basic::returns_unit]:
+    Source: 'src/lib.rs', lines 31:4-31:30 -/
+def basic.returns_unit (x : Std.U32) : Result Unit := do
+  ok ()
+
+/-- [hax_specs::basic::block_in_requires]:
+    Source: 'src/lib.rs', lines 35:4-37:5 -/
+def basic.block_in_requires (x : Std.U32) : Result Std.U32 := do
+  ok x
+
+/-- [hax_specs::basic::returns_pair]:
+    Source: 'src/lib.rs', lines 41:4-43:5 -/
+def basic.returns_pair (x : Std.U32) : Result (Std.U32 × Std.U32) := do
+  ok (x, x)
+
+/-- [hax_specs::extra_args::generic]:
+    Source: 'src/lib.rs', lines 53:4-55:5 -/
+def extra_args.generic (N : Std.U32) (x : Std.U32) : Result Std.U32 := do
+  N - x
+
+/-- Trait declaration: [hax_specs::extra_args::Val]
+    Source: 'src/lib.rs', lines 58:4-60:5 -/
+structure extra_args.Val (Self : Type) where
+  value : Self → Result Std.U32
+
+/-- [hax_specs::extra_args::{impl hax_specs::extra_args::Val for u32}::value]:
+    Source: 'src/lib.rs', lines 63:8-65:9 -/
+def U32.Insts.Hax_specsExtra_argsVal.value
+  (self : Std.U32) : Result Std.U32 := do
+  ok self
+
+/-- Trait implementation: [hax_specs::extra_args::{impl hax_specs::extra_args::Val for u32}]
+    Source: 'src/lib.rs', lines 62:4-66:5 -/
+@[reducible]
+def U32.Insts.Hax_specsExtra_argsVal : extra_args.Val Std.U32 := {
+  value := U32.Insts.Hax_specsExtra_argsVal.value
+}
+
+/-- [hax_specs::extra_args::traits]:
+    Source: 'src/lib.rs', lines 70:4-72:5 -/
+def extra_args.traits
+  {T : Type} (ValInst : extra_args.Val T) (t : T) (x : Std.U32) :
+  Result Std.U32
+  := do
+  let i ← ValInst.value t
+  i + x
+
+/-- [hax_specs::future::incr]:
+    Source: 'src/lib.rs', lines 81:4-83:5 -/
+def future.incr (x : Std.U32) : Result Std.U32 := do
+  x + 1#u32
+
+/-- [hax_specs::future::incr_i]:
+    Source: 'src/lib.rs', lines 89:4-91:5 -/
+def future.incr_i
+  (x : Slice Std.U32) (i : Std.Usize) : Result (Slice Std.U32) := do
+  let i1 ← Slice.index_usize x i
+  let i2 ← i1 + 1#u32
+  Slice.update x i i2
+
+/-- [hax_specs::future::swap_and_add]:
+    Source: 'src/lib.rs', lines 95:4-101:5 -/
+def future.swap_and_add
+  (x : Std.U32) (y : Std.U32) : Result (Std.U32 × Std.U32 × Std.U32) := do
+  let i ← x + y
+  ok (i, y, x)
+
+
+/-- [hax_specs::basic::only_requires::pre]:
+    Source: 'src/lib.rs', lines 5:4-5:24 -/
+@[reducible]
+def basic.only_requires.pre (x : Std.U32) : Result Bool := do
+  ok (x < 100#u32)
+
+def basic.only_requires.spec (x : Std.U32) : Prop :=
+  (basic.only_requires.pre x).holds →
+  basic.only_requires x
+  ⦃ res => True ⦄
+
+
+/-- [hax_specs::basic::only_ensures::post]:
+    Source: 'src/lib.rs', lines 10:4-10:36 -/
+@[reducible]
+def basic.only_ensures.post
+  (x : Std.U32) (result : Std.U32) : Result Bool := do
+  ok (result = x)
+
+def basic.only_ensures.spec (x : Std.U32) : Prop :=
+  basic.only_ensures x
+  ⦃ res => (basic.only_ensures.post x res).holds ⦄
+
+
+/-- [hax_specs::basic::both::pre]:
+    Source: 'src/lib.rs', lines 15:4-15:23 -/
+@[reducible]
+def basic.both.pre (x : Std.U32) : Result Bool := do
+  ok (x < 10#u32)
+
+/-- [hax_specs::basic::both::post]:
+    Source: 'src/lib.rs', lines 16:4-16:35 -/
+@[reducible]
+def basic.both.post (x : Std.U32) (result : Std.U32) : Result Bool := do
+  ok (result > x)
+
+def basic.both.spec (x : Std.U32) : Prop :=
+  (basic.both.pre x).holds →
+  basic.both x
+  ⦃ res => (basic.both.post x res).holds ⦄
+
+
+/-- [hax_specs::basic::returns_unit::pre]:
+    Source: 'src/lib.rs', lines 29:4-29:23 -/
+@[reducible]
+def basic.returns_unit.pre (x : Std.U32) : Result Bool := do
+  ok (x < 10#u32)
+
+/-- [hax_specs::basic::returns_unit::post]:
+    Source: 'src/lib.rs', lines 30:4-30:24 -/
+@[reducible]
+def basic.returns_unit.post (x : Std.U32) (_ : Unit) : Result Bool := do
+  ok true
+
+def basic.returns_unit.spec (x : Std.U32) : Prop :=
+  (basic.returns_unit.pre x).holds →
+  basic.returns_unit x
+  ⦃ res => (basic.returns_unit.post x res).holds ⦄
+
+
+/-- [hax_specs::basic::block_in_requires::pre]:
+    Source: 'src/lib.rs', lines 34:4-34:46 -/
+@[reducible]
+def basic.block_in_requires.pre (x : Std.U32) : Result Bool := do
+  ok (x > 10#u32)
+
+def basic.block_in_requires.spec (x : Std.U32) : Prop :=
+  (basic.block_in_requires.pre x).holds →
+  basic.block_in_requires x
+  ⦃ res => True ⦄
+
+
+/-- [hax_specs::basic::returns_pair::post]:
+    Source: 'src/lib.rs', lines 40:4-40:41 -/
+@[reducible]
+def basic.returns_pair.post
+  (x : Std.U32) (p : (Std.U32 × Std.U32)) : Result Bool := do
+  let (a, b) := p
+  if a = x
+  then ok (b = x)
+  else ok false
+
+def basic.returns_pair.spec (x : Std.U32) : Prop :=
+  basic.returns_pair x
+  ⦃ res => (basic.returns_pair.post x res).holds ⦄
+
+
+/-- [hax_specs::extra_args::generic::pre]:
+    Source: 'src/lib.rs', lines 51:4-51:31 -/
+@[reducible]
+def extra_args.generic.pre (N : Std.U32) (x : Std.U32) : Result Bool := do
+  if 0#u32 < x
+  then ok (x < N)
+  else ok false
+
+/-- [hax_specs::extra_args::generic::post]:
+    Source: 'src/lib.rs', lines 52:4-52:35 -/
+@[reducible]
+def extra_args.generic.post
+  (N : Std.U32) (x : Std.U32) (result : Std.U32) : Result Bool := do
+  ok (result < N)
+
+def extra_args.generic.spec (N : Std.U32) (x : Std.U32) : Prop :=
+  (extra_args.generic.pre N x).holds →
+  extra_args.generic N x
+  ⦃ res => (extra_args.generic.post N x res).holds ⦄
+
+
+/-- [hax_specs::extra_args::traits::pre]:
+    Source: 'src/lib.rs', lines 68:4-68:45 -/
+@[reducible]
+def extra_args.traits.pre
+  {T : Type} (ValInst : extra_args.Val T) (t : T) (x : Std.U32) :
+  Result Bool
+  := do
+  let i ← ValInst.value t
+  if i < 1000#u32
+  then ok (x < 1000#u32)
+  else ok false
+
+/-- [hax_specs::extra_args::traits::post]:
+    Source: 'src/lib.rs', lines 69:4-69:38 -/
+@[reducible]
+def extra_args.traits.post
+  {T : Type} (ValInst : extra_args.Val T) (t : T) (x : Std.U32)
+  (result : Std.U32) :
+  Result Bool
+  := do
+  ok (result < 2000#u32)
+
+def extra_args.traits.spec {T : Type} (ValInst : extra_args.Val T) (t : T)
+  (x : Std.U32) : Prop :=
+  (extra_args.traits.pre ValInst t x).holds →
+  extra_args.traits ValInst t x
+  ⦃ res => (extra_args.traits.post ValInst t x res).holds ⦄
+
+
+/-- [hax_specs::future::incr::pre]:
+    Source: 'src/lib.rs', lines 79:4-79:26 -/
+@[reducible]
+def future.incr.pre (x : Std.U32) : Result Bool := do
+  ok (x < 1000#u32)
+
+/-- [hax_specs::future::incr::post]:
+    Source: 'src/lib.rs', lines 80:4-80:41 -/
+@[reducible]
+def future.incr.post (x : Std.U32) (x_future : Std.U32) : Result Bool := do
+  let i ← x + 1#u32
+  ok (x_future = i)
+
+def future.incr.spec (x : Std.U32) : Prop :=
+  (future.incr.pre x).holds →
+  future.incr x
+  ⦃ res => (future.incr.post x res).holds ⦄
+
+
+/-- [hax_specs::future::incr_i::pre]:
+    Source: 'src/lib.rs', lines 85:4-85:28 -/
+@[reducible]
+def future.incr_i.pre (x : Slice Std.U32) (i : Std.Usize) : Result Bool := do
+  let i1 := Slice.len x
+  ok (i < i1)
+
+/-- [hax_specs::future::incr_i::post]:
+    Source: 'src/lib.rs', lines 86:4-88:31 -/
+@[reducible]
+def future.incr_i.post
+  (x : Slice Std.U32) (i : Std.Usize) (x_future : Slice Std.U32) :
+  Result Bool
+  := do
+  let i1 ← Slice.index_usize x_future i
+  let i2 ← Slice.index_usize x i
+  let i3 ← i2 + 1#u32
+  ok (i1 = i3)
+
+def future.incr_i.spec (x : Slice Std.U32) (i : Std.Usize) : Prop :=
+  (future.incr_i.pre x i).holds →
+  future.incr_i x i
+  ⦃ res => (future.incr_i.post x i res).holds ⦄
+
+
+/-- [hax_specs::future::swap_and_add::pre]:
+    Source: 'src/lib.rs', lines 93:4-93:39 -/
+@[reducible]
+def future.swap_and_add.pre (x : Std.U32) (y : Std.U32) : Result Bool := do
+  if x < 1000#u32
+  then ok (y < 1000#u32)
+  else ok false
+
+/-- [hax_specs::future::swap_and_add::post]:
+    Source: 'src/lib.rs', lines 94:4-94:73 -/
+@[reducible]
+def future.swap_and_add.post
+  (x : Std.U32) (y : Std.U32) (t : (Std.U32 × Std.U32 × Std.U32)) :
+  Result Bool
+  := do
+  let (x_future, y_future, r) := t
+  if y_future = x
+  then
+    if x_future = y
+    then
+      let i ← Shared1U32.Insts.CoreOpsArithAddShared0U32U32.add x y
+      ok (r = i)
+    else ok false
+  else ok false
+
+def future.swap_and_add.spec (x : Std.U32) (y : Std.U32) : Prop :=
+  (future.swap_and_add.pre x y).holds →
+  future.swap_and_add x y
+  ⦃ res => (future.swap_and_add.post x y res).holds ⦄
+
+@[step]
+theorem basic.only_requires.spec.proof (x : Std.U32) :
+  basic.only_requires.spec x
+  := by sorry
+
+@[step]
+theorem basic.only_ensures.spec.proof (x : Std.U32) : basic.only_ensures.spec x
+  := by sorry
+
+@[step]
+theorem basic.both.spec.proof (x : Std.U32) : basic.both.spec x := by sorry
+
+@[step]
+theorem basic.returns_unit.spec.proof (x : Std.U32) : basic.returns_unit.spec x
+  := by sorry
+
+@[step]
+theorem basic.block_in_requires.spec.proof (x : Std.U32) :
+  basic.block_in_requires.spec x
+  := by sorry
+
+@[step]
+theorem basic.returns_pair.spec.proof (x : Std.U32) : basic.returns_pair.spec x
+  := by sorry
+
+@[step]
+theorem extra_args.generic.spec.proof (N : Std.U32) (x : Std.U32) :
+  extra_args.generic.spec N x
+  := by sorry
+
+@[step]
+theorem extra_args.traits.spec.proof {T : Type} (ValInst : extra_args.Val T)
+  (t : T) (x : Std.U32) : extra_args.traits.spec ValInst t x
+  := by sorry
+
+@[step]
+theorem future.incr.spec.proof (x : Std.U32) : future.incr.spec x := by sorry
+
+@[step]
+theorem future.incr_i.spec.proof (x : Slice Std.U32) (i : Std.Usize) :
+  future.incr_i.spec x i
+  := by sorry
+
+@[step]
+theorem future.swap_and_add.spec.proof (x : Std.U32) (y : Std.U32) :
+  future.swap_and_add.spec x y
+  := by sorry
+
+end hax_specs
diff --git a/tests/lean/Tutorial/Exercises.lean b/tests/lean/Tutorial/Exercises.lean
index e66f1efeb..492a8dc47 100644
--- a/tests/lean/Tutorial/Exercises.lean
+++ b/tests/lean/Tutorial/Exercises.lean
@@ -24,7 +24,7 @@ theorem mul2_add1_spec (x : U32) (h : 2 * x.val + 1 ≤ U32.max)
   : mul2_add1 x ⦃ y => ↑y = 2 * ↑x + (1 : Int) ∧ ↑y = 2 * ↑x + (1 : Int) ⦄
   := by
   unfold mul2_add1
-  step with U32.add_spec as ⟨ x1 ⟩
+  step with U32.add_spec.step_spec as ⟨ x1 ⟩
   step as ⟨ x2 ⟩
   scalar_tac
 
diff --git a/tests/src/hax_specs/Cargo.lock b/tests/src/hax_specs/Cargo.lock
new file mode 100644
index 000000000..a179aba15
--- /dev/null
+++ b/tests/src/hax_specs/Cargo.lock
@@ -0,0 +1,595 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "anyhow"
+version = "1.0.102"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c"
+
+[[package]]
+name = "autocfg"
+version = "1.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53"
+
+[[package]]
+name = "bitflags"
+version = "2.12.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "84d7ced0ae9557296835c32bf1b1e02b44c746701f898460fb000d7eaa84f00a"
+
+[[package]]
+name = "bumpalo"
+version = "3.20.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72f5acc6cb2ba439de613abc23857ec3d78374d8ed5ac84e9d11336e87da8649"
+
+[[package]]
+name = "cfg-if"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
+
+[[package]]
+name = "equivalent"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f"
+
+[[package]]
+name = "foldhash"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2"
+
+[[package]]
+name = "futures-core"
+version = "0.3.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d"
+
+[[package]]
+name = "futures-task"
+version = "0.3.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393"
+
+[[package]]
+name = "futures-util"
+version = "0.3.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6"
+dependencies = [
+ "futures-core",
+ "futures-task",
+ "pin-project-lite",
+ "slab",
+]
+
+[[package]]
+name = "getrandom"
+version = "0.4.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0de51e6874e94e7bf76d726fc5d13ba782deca734ff60d5bb2fb2607c7406555"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "r-efi",
+ "wasip2",
+ "wasip3",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.15.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1"
+dependencies = [
+ "foldhash",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.17.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a"
+
+[[package]]
+name = "hax-lib"
+version = "0.3.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "01a33cb227f97ee5c419064c31d7c55a7d895f28d8019ccdadc311cc036500c4"
+dependencies = [
+ "hax-lib-macros",
+ "num-bigint",
+ "num-traits",
+]
+
+[[package]]
+name = "hax-lib-macros"
+version = "0.3.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "28da835a5f153e9f3d0cc1f42ee605a1cfa9093c93348193793d60a1b0908b51"
+dependencies = [
+ "hax-lib-macros-types",
+ "proc-macro-error2",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "hax-lib-macros-types"
+version = "0.3.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "eed327e9a28d6ee018a4a9ba842d4ee27e378c8a591d2beb6f42f32b24a02fcb"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "serde",
+ "serde_json",
+ "uuid",
+]
+
+[[package]]
+name = "hax_specs"
+version = "0.1.0"
+dependencies = [
+ "hax-lib",
+]
+
+[[package]]
+name = "heck"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
+
+[[package]]
+name = "id-arena"
+version = "2.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954"
+
+[[package]]
+name = "indexmap"
+version = "2.14.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
+dependencies = [
+ "equivalent",
+ "hashbrown 0.17.1",
+ "serde",
+ "serde_core",
+]
+
+[[package]]
+name = "itoa"
+version = "1.0.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682"
+
+[[package]]
+name = "js-sys"
+version = "0.3.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "142bc4740e452c1e57ade0cbc129f139c9093e354346f0872ef985f4f5cf5f11"
+dependencies = [
+ "cfg-if",
+ "futures-util",
+ "once_cell",
+ "wasm-bindgen",
+]
+
+[[package]]
+name = "leb128fmt"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2"
+
+[[package]]
+name = "libc"
+version = "0.2.186"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66"
+
+[[package]]
+name = "log"
+version = "0.4.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "953f07c43838f8e6f9758cab68bf5bed85465e7587ebe0b823f1bcd81978ad3a"
+
+[[package]]
+name = "memchr"
+version = "2.8.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6b947ae49db0d222b1dbc6b113ce7248a3fc3a6ca21b696717bfc000ba4484d8"
+
+[[package]]
+name = "num-bigint"
+version = "0.4.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9"
+dependencies = [
+ "num-integer",
+ "num-traits",
+]
+
+[[package]]
+name = "num-integer"
+version = "0.1.46"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f"
+dependencies = [
+ "num-traits",
+]
+
+[[package]]
+name = "num-traits"
+version = "0.2.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841"
+dependencies = [
+ "autocfg",
+]
+
+[[package]]
+name = "once_cell"
+version = "1.21.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50"
+
+[[package]]
+name = "pin-project-lite"
+version = "0.2.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd"
+
+[[package]]
+name = "prettyplease"
+version = "0.2.37"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b"
+dependencies = [
+ "proc-macro2",
+ "syn",
+]
+
+[[package]]
+name = "proc-macro-error-attr2"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5"
+dependencies = [
+ "proc-macro2",
+ "quote",
+]
+
+[[package]]
+name = "proc-macro-error2"
+version = "2.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802"
+dependencies = [
+ "proc-macro-error-attr2",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.106"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.45"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "r-efi"
+version = "6.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf"
+
+[[package]]
+name = "rustversion"
+version = "1.0.22"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d"
+
+[[package]]
+name = "semver"
+version = "1.0.28"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"
+
+[[package]]
+name = "serde"
+version = "1.0.228"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"
+dependencies = [
+ "serde_core",
+ "serde_derive",
+]
+
+[[package]]
+name = "serde_core"
+version = "1.0.228"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad"
+dependencies = [
+ "serde_derive",
+]
+
+[[package]]
+name = "serde_derive"
+version = "1.0.228"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "serde_json"
+version = "1.0.150"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9"
+dependencies = [
+ "itoa",
+ "memchr",
+ "serde",
+ "serde_core",
+ "zmij",
+]
+
+[[package]]
+name = "slab"
+version = "0.4.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5"
+
+[[package]]
+name = "syn"
+version = "2.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "unicode-xid"
+version = "0.2.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853"
+
+[[package]]
+name = "uuid"
+version = "1.23.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d258b83ceec21034727ecee8c382cfa6c3e133699b0742c64571814fb420c9f7"
+dependencies = [
+ "getrandom",
+ "js-sys",
+ "wasm-bindgen",
+]
+
+[[package]]
+name = "wasip2"
+version = "1.0.3+wasi-0.2.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "20064672db26d7cdc89c7798c48a0fdfac8213434a1186e5ef29fd560ae223d6"
+dependencies = [
+ "wit-bindgen 0.57.1",
+]
+
+[[package]]
+name = "wasip3"
+version = "0.4.0+wasi-0.3.0-rc-2026-01-06"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5428f8bf88ea5ddc08faddef2ac4a67e390b88186c703ce6dbd955e1c145aca5"
+dependencies = [
+ "wit-bindgen 0.51.0",
+]
+
+[[package]]
+name = "wasm-bindgen"
+version = "0.2.122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3ed04576f974d2b2fba0f38c51dbc5518011e38c36bf1143164be765528fd409"
+dependencies = [
+ "cfg-if",
+ "once_cell",
+ "rustversion",
+ "wasm-bindgen-macro",
+ "wasm-bindgen-shared",
+]
+
+[[package]]
+name = "wasm-bindgen-macro"
+version = "0.2.122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "916151b09da36bd82f6615cbf3a419e2f0ba23a03c6160e8e92eb6bd4aa1dec6"
+dependencies = [
+ "quote",
+ "wasm-bindgen-macro-support",
+]
+
+[[package]]
+name = "wasm-bindgen-macro-support"
+version = "0.2.122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "299047362ccbfce148b67ab7e73349f77748e00c8296f9542adfad2ad82c5c5e"
+dependencies = [
+ "bumpalo",
+ "proc-macro2",
+ "quote",
+ "syn",
+ "wasm-bindgen-shared",
+]
+
+[[package]]
+name = "wasm-bindgen-shared"
+version = "0.2.122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9a929b2c61f11ba3e9bc35b50c1f25cb38e0e892c0c231ae2b8cf78d5dad4437"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "wasm-encoder"
+version = "0.244.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "990065f2fe63003fe337b932cfb5e3b80e0b4d0f5ff650e6985b1048f62c8319"
+dependencies = [
+ "leb128fmt",
+ "wasmparser",
+]
+
+[[package]]
+name = "wasm-metadata"
+version = "0.244.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909"
+dependencies = [
+ "anyhow",
+ "indexmap",
+ "wasm-encoder",
+ "wasmparser",
+]
+
+[[package]]
+name = "wasmparser"
+version = "0.244.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe"
+dependencies = [
+ "bitflags",
+ "hashbrown 0.15.5",
+ "indexmap",
+ "semver",
+]
+
+[[package]]
+name = "wit-bindgen"
+version = "0.51.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d7249219f66ced02969388cf2bb044a09756a083d0fab1e566056b04d9fbcaa5"
+dependencies = [
+ "wit-bindgen-rust-macro",
+]
+
+[[package]]
+name = "wit-bindgen"
+version = "0.57.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e"
+
+[[package]]
+name = "wit-bindgen-core"
+version = "0.51.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ea61de684c3ea68cb082b7a88508a8b27fcc8b797d738bfc99a82facf1d752dc"
+dependencies = [
+ "anyhow",
+ "heck",
+ "wit-parser",
+]
+
+[[package]]
+name = "wit-bindgen-rust"
+version = "0.51.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b7c566e0f4b284dd6561c786d9cb0142da491f46a9fbed79ea69cdad5db17f21"
+dependencies = [
+ "anyhow",
+ "heck",
+ "indexmap",
+ "prettyplease",
+ "syn",
+ "wasm-metadata",
+ "wit-bindgen-core",
+ "wit-component",
+]
+
+[[package]]
+name = "wit-bindgen-rust-macro"
+version = "0.51.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0c0f9bfd77e6a48eccf51359e3ae77140a7f50b1e2ebfe62422d8afdaffab17a"
+dependencies = [
+ "anyhow",
+ "prettyplease",
+ "proc-macro2",
+ "quote",
+ "syn",
+ "wit-bindgen-core",
+ "wit-bindgen-rust",
+]
+
+[[package]]
+name = "wit-component"
+version = "0.244.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2"
+dependencies = [
+ "anyhow",
+ "bitflags",
+ "indexmap",
+ "log",
+ "serde",
+ "serde_derive",
+ "serde_json",
+ "wasm-encoder",
+ "wasm-metadata",
+ "wasmparser",
+ "wit-parser",
+]
+
+[[package]]
+name = "wit-parser"
+version = "0.244.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736"
+dependencies = [
+ "anyhow",
+ "id-arena",
+ "indexmap",
+ "log",
+ "semver",
+ "serde",
+ "serde_derive",
+ "serde_json",
+ "unicode-xid",
+ "wasmparser",
+]
+
+[[package]]
+name = "zmij"
+version = "1.0.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b8848ee67ecc8aedbaf3e4122217aff892639231befc6a1b58d29fff4c2cabaa"
diff --git a/tests/src/hax_specs/Cargo.toml b/tests/src/hax_specs/Cargo.toml
new file mode 100644
index 000000000..0e3f602b1
--- /dev/null
+++ b/tests/src/hax_specs/Cargo.toml
@@ -0,0 +1,11 @@
+[package]
+name = "hax_specs"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+name = "hax_specs"
+path = "src/lib.rs"
+
+[dependencies]
+hax-lib = "0.3.6"
diff --git a/tests/src/hax_specs/aeneas-test-options b/tests/src/hax_specs/aeneas-test-options
new file mode 100644
index 000000000..c8e549d09
--- /dev/null
+++ b/tests/src/hax_specs/aeneas-test-options
@@ -0,0 +1,7 @@
+[!lean] skip
+[lean] aeneas-args=-specs hax
+charon-args=--start-from=crate
+charon-args=--rustc-arg=--cfg=hax_compilation
+charon-args=--rustc-arg=-Zcrate-attr=feature(register_tool)
+charon-args=--rustc-arg=-Zcrate-attr=register_tool(_hax)
+charon-args=-- -Zhost-config -Ztarget-applies-to-host --config host.rustflags=["--cfg","hax"]
diff --git a/tests/src/hax_specs/src/lib.rs b/tests/src/hax_specs/src/lib.rs
new file mode 100644
index 000000000..9552d468b
--- /dev/null
+++ b/tests/src/hax_specs/src/lib.rs
@@ -0,0 +1,102 @@
+#[allow(dead_code)]
+mod basic {
+    use hax_lib::*;
+
+    #[requires(x < 100)]
+    fn only_requires(x: u32) -> u32 {
+        x + 1
+    }
+
+    #[ensures(|result| result == x)]
+    fn only_ensures(x: u32) -> u32 {
+        x
+    }
+
+    #[requires(x < 10)]
+    #[ensures(|result| result > x)]
+    fn both(x: u32) -> u32 {
+        x + 1
+    }
+
+    // No arguments
+    #[ensures(|_| true)]
+    fn no_args() {
+        let _x = 0;
+        ()
+    }
+
+    // Unit return with a by-value argument
+    #[requires(x < 10)]
+    #[ensures(|_| true)]
+    fn returns_unit(x: u32) {}
+
+    // Block expression (with a `let`) inside `requires`
+    #[requires({ let bound = x; bound > 10 })]
+    fn block_in_requires(x: u32) -> u32 {
+        x
+    }
+
+    // Pattern directly in the result closure
+    #[ensures(|(a, b)| a == x && b == x)]
+    fn returns_pair(x: u32) -> (u32, u32) {
+        (x, x)
+    }
+}
+
+#[allow(dead_code)]
+mod extra_args {
+    use hax_lib::*;
+
+    // Const generic params
+    #[requires(0 < x && x < N)]
+    #[ensures(|result| result < N)]
+    fn generic<const N: u32>(x: u32) -> u32 {
+        N - x
+    }
+
+    // Trait params
+    trait Val {
+        fn value(&self) -> u32;
+    }
+
+    impl Val for u32 {
+        fn value(&self) -> u32 {
+            *self
+        }
+    }
+
+    #[requires(t.value() < 1000 && x < 1000)]
+    #[ensures(|result| result < 2000)]
+    fn traits<T: Val>(t: T, x: u32) -> u32 {
+        t.value() + x
+    }
+}
+
+#[allow(dead_code)]
+mod future {
+    use hax_lib::*;
+
+    #[requires(*x < 1000)]
+    #[ensures(|_| *future(x) == *x + 1 )]
+    fn incr(x: &mut u32) {
+        *x += 1;
+    }
+
+    #[requires(i < x.len())]
+    #[ensures(|_| {
+            let r = future(x);
+            r[i] == x[i] + 1})]
+    fn incr_i(x: &mut [u32], i: usize) {
+        x[i] += 1
+    }
+
+    #[requires(*x < 1000 && *y < 1000)]
+    #[ensures(|r| { *future(y) == *x && *future(x) == *y && r == x + y})]
+    fn swap_and_add(x: &mut u32, y: &mut u32) -> u32 {
+        let tmp_x = *x;
+        let tmp_y = *y;
+        *x = tmp_y;
+        *y = tmp_x;
+        tmp_x + tmp_y
+    }
+}
diff --git a/tests/src/hax_specs_step/Cargo.lock b/tests/src/hax_specs_step/Cargo.lock
new file mode 120000
index 000000000..8cd0fd3e3
--- /dev/null
+++ b/tests/src/hax_specs_step/Cargo.lock
@@ -0,0 +1 @@
+../hax_specs/Cargo.lock
\ No newline at end of file
diff --git a/tests/src/hax_specs_step/Cargo.toml b/tests/src/hax_specs_step/Cargo.toml
new file mode 120000
index 000000000..45b031597
--- /dev/null
+++ b/tests/src/hax_specs_step/Cargo.toml
@@ -0,0 +1 @@
+../hax_specs/Cargo.toml
\ No newline at end of file
diff --git a/tests/src/hax_specs_step/aeneas-test-options b/tests/src/hax_specs_step/aeneas-test-options
new file mode 100644
index 000000000..d52076ec2
--- /dev/null
+++ b/tests/src/hax_specs_step/aeneas-test-options
@@ -0,0 +1,7 @@
+[!lean] skip
+[lean] aeneas-args=-specs hax-step
+charon-args=--start-from=crate
+charon-args=--rustc-arg=--cfg=hax_compilation
+charon-args=--rustc-arg=-Zcrate-attr=feature(register_tool)
+charon-args=--rustc-arg=-Zcrate-attr=register_tool(_hax)
+charon-args=-- -Zhost-config -Ztarget-applies-to-host --config host.rustflags=["--cfg","hax"]
diff --git a/tests/src/hax_specs_step/src b/tests/src/hax_specs_step/src
new file mode 120000
index 000000000..26216bc06
--- /dev/null
+++ b/tests/src/hax_specs_step/src
@@ -0,0 +1 @@
+../hax_specs/src
\ No newline at end of file