diff --git a/Cslib/Languages/Boole/examples/euclid_gcd.lean b/Cslib/Languages/Boole/examples/euclid_gcd.lean
new file mode 100644
index 000000000..e8a866568
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/euclid_gcd.lean
@@ -0,0 +1,75 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- Euclid's algorithm for GCD, with a spec stated via a helper function/predicate.
+--
+-- We use the subtraction-based variant of Euclid's algorithm to avoid `mod`, which currently
+-- tends to produce large verification conditions.
+--
+-- Divisibility/maximality are stated as axioms about `GCDSpec`.
+private def euclidGcdPgm : Strata.Program :=
+#strata
+program Boole;
+
+function GCDSpec(a : int, b : int) : int;
+function Divides(d : int, a : int) : bool;
+
+// Subtraction-based Euclid facts for `GCDSpec`.
+axiom (forall x : int :: GCDSpec(x, x) == x);
+axiom (forall x : int, y : int :: x > y && y > 0 ==> GCDSpec(x, y) == GCDSpec(x - y, y));
+axiom (forall x : int, y : int :: y > x && x > 0 ==> GCDSpec(x, y) == GCDSpec(x, y - x));
+
+// Spec helper: divisibility and maximality properties of the computed `d`.
+// The key idea is that callers can assume `free ensures` without having to verify them here.
+procedure GCDProperties(a : int, b : int, d : int) returns ()
+spec
+{
+  requires d == GCDSpec(a, b);
+  free ensures Divides(d, a) && Divides(d, b);
+  free ensures forall e : int :: (e >= 0 && Divides(e, a) && Divides(e, b)) ==> e <= d;
+}
+{};
+
+procedure EuclidGCD(a : int, b : int) returns (d : int)
+spec
+{
+  requires a > 0;
+  requires b > 0;
+  ensures d == GCDSpec(a, b);
+  ensures Divides(d, a) && Divides(d, b);
+  ensures forall e : int :: (e >= 0 && Divides(e, a) && Divides(e, b)) ==> e <= d;
+}
+{
+  var x : int;
+  var y : int;
+
+  x := a;
+  y := b;
+
+  while (x != y)
+    invariant x > 0
+    invariant y > 0
+    invariant GCDSpec(x, y) == GCDSpec(a, b)
+  {
+    if (x > y) {
+      x := x - y;
+    } else {
+      y := y - x;
+    }
+  }
+
+  d := x;
+
+  // Discharge the divisibility/maximality postconditions via the spec helper.
+  call GCDProperties(a, b, d);
+};
+#end
+
+set_option maxHeartbeats 1000000 in
+example : Strata.smtVCsCorrect euclidGcdPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata
diff --git a/Cslib/Languages/Boole/examples/insertion_sort.lean b/Cslib/Languages/Boole/examples/insertion_sort.lean
new file mode 100644
index 000000000..6561b15ea
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/insertion_sort.lean
@@ -0,0 +1,103 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- CLRS Chapter 1: Insertion Sort
+-- Pseudo-code adapted from CLRS book (3rd edition), page 18
+
+-- Pseudo-code:
+-- INSERTION-SORT(A)
+-- 1  for j = 2 to A.length
+-- 2      key = A[j]
+-- 3      // Insert A[j] into the sorted sequence A[1..j-1]
+-- 4      i = j - 1
+-- 5      while i > 0 and A[i] > key
+-- 6          A[i + 1] = A[i]
+-- 7          i = i - 1
+-- 8      A[i + 1] = key
+
+private def insertionSortPgm :=
+#strata
+program Boole;
+
+// An "array of ints" is a map from int to int
+type Array := Map int int;
+
+// Global array we'll sort
+var A : Array;
+var n : int; // length of A
+
+// Add axiom for length of A
+// function array_length(a: Array) : int { n }
+// axiom (array_length(A) == n);
+// [FEATURE REQUEST] Support native arrays
+
+
+procedure InsertionSort() returns ()
+spec
+{
+  modifies A;
+  // Adjacent-order formulation of sortedness (simpler VCs than ∀ i j, ...).
+  ensures forall k:int ::
+    0 <= k && k < n - 1 ==> A[k] <= A[k + 1];
+  // [FEATURE REQUEST] Support for Lean 4-style quantifiers
+  // -- ∀ k: int, 0 ≤ k ∧ k < n - 1 → A[k] ≤ A[k + 1]
+}
+{
+  var i : int;
+  var j : int;
+  var key : int;
+
+  if (n > 1) {
+    // CLRS-style insertion sort (0-based):
+    // for i = 1 to n-1
+    // [FEATURE REQUEST] For loop construct
+    i := 1;
+    while (i < n)
+      invariant 1 <= i && i <= n
+      invariant (
+        forall k:int ::
+          0 <= k && k < i - 1 ==> A[k] <= A[k + 1]
+      )
+    {
+      key := A[i];
+      j := i - 1;
+
+      // We do one shift outside the loop so that, inside the loop,
+      // the prefix `A[0..i]` is sorted (with `key` stored separately).
+      if (A[j] > key) {
+        A := A[j + 1 := A[j]];
+        j := j - 1;
+
+        while (j >= 0 && A[j] > key)
+          invariant -1 <= j && j < i
+          invariant (
+            forall k:int ::
+              0 <= k && k < i ==> A[k] <= A[k + 1]
+          )
+          invariant (
+            forall k:int :: j < k && k <= i ==> A[k] > key
+          )
+        {
+          A := A[j + 1 := A[j]];
+          j := j - 1;
+        }
+      }
+
+      A := A[j + 1 := key];
+      i := i + 1;
+    }
+  }
+};
+#end
+
+-- Optional: run the SMT-based pipeline if `cvc5` is on your `PATH`.
+-- Note: use `#eval!` if your dependency graph contains `sorry`.
+-- #eval! Strata.Boole.verify "cvc5" insertionSortPgm
+
+example : Strata.smtVCsCorrect insertionSortPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata
diff --git a/Cslib/Languages/Boole/examples/linear_search.lean b/Cslib/Languages/Boole/examples/linear_search.lean
new file mode 100644
index 000000000..cac9f8613
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/linear_search.lean
@@ -0,0 +1,45 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- Linear search: return an index where `A[idx] == x`, or `-1` if not found.
+private def linearSearchPgm : Strata.Program :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+procedure LinearSearch(A : Array, n : int, x : int) returns (idx : int)
+spec
+{
+  requires n >= 0;
+  ensures (idx == -1 ==> forall k:int :: 0 <= k && k < n ==> A[k] != x);
+  ensures (idx != -1 ==> 0 <= idx && idx < n && A[idx] == x);
+}
+{
+  var i : int;
+
+  i := 0;
+  idx := -1;
+
+  while (i < n && idx == -1)
+    invariant 0 <= i && i <= n
+    invariant (idx == -1 ==> forall k:int :: 0 <= k && k < i ==> A[k] != x)
+    invariant (idx != -1 ==> 0 <= idx && idx < i && A[idx] == x)
+  {
+    if (A[i] == x) {
+      idx := i;
+    }
+    i := i + 1;
+  }
+};
+#end
+
+set_option maxHeartbeats 500000 in
+example : Strata.smtVCsCorrect linearSearchPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata
+
diff --git a/Cslib/Languages/Boole/examples/prefix_sums.lean b/Cslib/Languages/Boole/examples/prefix_sums.lean
new file mode 100644
index 000000000..45c73c35e
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/prefix_sums.lean
@@ -0,0 +1,50 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- Prefix sums.
+--
+-- Intended spec: `S[i] = Σ_{k<i} A[k]`. In Boole, we encode the summation via an
+-- uninterpreted function with recursive axioms.
+private def prefixSumsPgm : Strata.Program :=
+#strata
+program Boole;
+
+// Sum of the first `i` elements: `PrefixSum(A, i) = Σ_{k<i} A[k]`.
+function PrefixSum(A : Map int int, i : int) : int;
+
+axiom (forall A : Map int int :: PrefixSum(A, 0) == 0);
+axiom (forall A : Map int int, i : int ::
+  i > 0 ==> PrefixSum(A, i) == PrefixSum(A, i - 1) + A[i - 1]);
+
+procedure PrefixSums(A : Map int int, n : int) returns (S : Map int int)
+spec
+{
+  requires n >= 0;
+  ensures forall i : int :: 0 <= i && i <= n ==> S[i] == PrefixSum(A, i);
+}
+{
+  var i : int;
+
+  // Initialize S[0] = 0.
+  S := S[0 := 0];
+
+  i := 0;
+  while (i < n)
+    invariant 0 <= i && i <= n
+    invariant forall k : int :: 0 <= k && k <= i ==> S[k] == PrefixSum(A, k)
+  {
+    // Step: S[i+1] = S[i] + A[i].
+    S := S[i + 1 := S[i] + A[i]];
+    i := i + 1;
+  }
+};
+#end
+
+set_option maxHeartbeats 1000000 in
+example : Strata.smtVCsCorrect prefixSumsPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata
diff --git a/Cslib/Languages/Boole/examples/selection_sort.lean b/Cslib/Languages/Boole/examples/selection_sort.lean
new file mode 100644
index 000000000..05017b80f
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/selection_sort.lean
@@ -0,0 +1,76 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- Selection sort.
+--
+-- This example uses a lightweight sortedness spec:
+--   `∀ k, 0 ≤ k ∧ k < n-1 → A[k] ≤ A[k+1]`
+-- instead of `∀ i j, i ≤ j → A[i] ≤ A[j]`, because it tends to generate
+-- simpler verification conditions.
+private def selectionSortPgm : Strata.Program :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+var A : Array;
+var n : int;
+
+procedure SelectionSort() returns ()
+spec
+{
+  modifies A;
+  // Adjacent-order sortedness.
+  ensures forall k:int :: 0 <= k && k < n - 1 ==> A[k] <= A[k + 1];
+}
+{
+  var i : int;
+  var j : int;
+  var m : int;
+  var tmp : int;
+
+  if (n > 1) {
+    i := 0;
+
+    while (i < n - 1)
+      invariant 0 <= i && i <= n - 1
+      // Prefix `A[0..i]` is sorted.
+      invariant forall k:int :: 0 <= k && k < i ==> A[k] <= A[k + 1]
+      // Every element already placed in the prefix is <= every element remaining in the suffix.
+      invariant forall p:int, q:int :: 0 <= p && p < i && i <= q && q < n ==> A[p] <= A[q]
+    {
+      m := i;
+      j := i + 1;
+
+      // Find an index `m` holding a minimum of `A[i..n-1]`.
+      while (j < n)
+        invariant i <= m && m < n
+        invariant i < j && j <= n
+        invariant forall k:int :: i <= k && k < j ==> A[m] <= A[k]
+      {
+        if (A[j] < A[m]) {
+          m := j;
+        }
+        j := j + 1;
+      }
+
+      if (m != i) {
+        tmp := A[i];
+        A := A[i := A[m]];
+        A := A[m := tmp];
+      }
+
+      i := i + 1;
+    }
+  }
+};
+#end
+
+set_option maxHeartbeats 1000000 in
+example : Strata.smtVCsCorrect selectionSortPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata
diff --git a/Cslib/Languages/Boole/examples/two_sum.lean b/Cslib/Languages/Boole/examples/two_sum.lean
new file mode 100644
index 000000000..fdac7ec45
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/two_sum.lean
@@ -0,0 +1,69 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- Two-sum (quadratic scan).
+--
+-- Returns `(i, j)` with `0 ≤ i < j < n` and `A[i] + A[j] == t`, or `(-1, -1)` if no pair is found.
+--
+-- Note: this example proves *soundness* of the returned indices, not *completeness*
+-- (i.e. it does not prove that `(-1, -1)` implies there is no solution).
+private def twoSumPgm : Strata.Program :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+procedure TwoSum(A : Array, n : int, t : int) returns (ri : int, rj : int)
+spec
+{
+  requires n >= 0;
+
+  // Soundness: if we return indices, they denote a valid solution.
+  ensures (ri != -1) ==> 0 <= ri && ri < rj && rj < n && A[ri] + A[rj] == t;
+  // "Not found" is represented as (-1, -1).
+  ensures (ri == -1) ==> rj == -1;
+  ensures (rj == -1) ==> ri == -1;
+}
+{
+  var i : int;
+  var j : int;
+  var found : bool;
+
+  ri := -1;
+  rj := -1;
+  found := false;
+
+  i := 0;
+  while (i < n)
+    invariant 0 <= i && i <= n
+    invariant (found == false) ==> (ri == -1 && rj == -1)
+    invariant (found == true) ==> 0 <= ri && ri < rj && rj < n && A[ri] + A[rj] == t
+  {
+    if (found == false) {
+      j := i + 1;
+      while (j < n)
+        invariant i + 1 <= j && j <= n
+        invariant (found == false) ==> (ri == -1 && rj == -1)
+        invariant (found == true) ==> 0 <= ri && ri < rj && rj < n && A[ri] + A[rj] == t
+      {
+        if (found == false && A[i] + A[j] == t) {
+          ri := i;
+          rj := j;
+          found := true;
+        }
+        j := j + 1;
+      }
+    }
+    i := i + 1;
+  }
+};
+#end
+
+set_option maxHeartbeats 1000000 in
+example : Strata.smtVCsCorrect twoSumPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata
diff --git a/Cslib/Languages/Boole/feature_requests/quantifier_syntax/insertion_sort.lean b/Cslib/Languages/Boole/feature_requests/quantifier_syntax/insertion_sort.lean
deleted file mode 100644
index 163dec6aa..000000000
--- a/Cslib/Languages/Boole/feature_requests/quantifier_syntax/insertion_sort.lean
+++ /dev/null
@@ -1,87 +0,0 @@
-import Strata.MetaVerifier
-import Smt
-
----------------------------------------------------------------------
-namespace Strata
-
--- CLRS Chapter 1: Insertion Sort
--- Pseudo-code adapted from CLRS book (3rd edition), page 18
-
--- Pseudo-code:
--- INSERTION-SORT(A)
--- 1  for j = 2 to A.length
--- 2      key = A[j]
--- 3      // Insert A[j] into the sorted sequence A[1..j-1]
--- 4      i = j - 1
--- 5      while i > 0 and A[i] > key
--- 6          A[i + 1] = A[i]
--- 7          i = i - 1
--- 8      A[i + 1] = key
-
-private def insertionSortPgm :=
-#strata
-program Boole;
-
-// An "array of ints" is a map from int to int
-type Array := Map int int;
-
-// Global array we'll sort
-var A : Array;
-var n : int; // length of A
-
-// Add axiom for length of A
-// function array_length(a: Array) : int { n }
-// axiom (array_length(A) == n);
-// [FEATURE REQUEST] Support native arrays
-
-
-procedure InsertionSort() returns ()
-spec
-{
-  modifies A;
-  modifies n;
-  ensures forall i:int, j: int ::
-  0 <= i && i <= j && j < n ==> A[i] <= A[j];
-  // [FEATURE REQUEST] Support for Lean 4-style quantifiers
-  // -- ∀ i, j: int, 0 ≤ i ∧ i ≤ j ∧ j < n → A[i] ≤ A[j]
-}
-{
-  var i : int;
-  var j : int;
-  var key : int;
-
-  // CLRS-style insertion sort (0-based):
-  // for i = 1 to n-1
-  // [FEATURE REQUEST] For loop construct
-  i := 1;
-  while (i < n) {
-    key := A[i];
-    j := i - 1;
-
-    while (j >= 0 && A[j] > key)
-     invariant (
-      forall p:int, q:int ::
-        0 <= p && p <= q && q < i ==> A[p] <= A[q]
-     )
-    {
-      // map update: A[j+1] := A[j]
-      A := A[j + 1 := A[j]];
-      // [FEATURE REQUEST] Support for array updates
-      // like A[j+1] := A[j]
-      j := j - 1;
-    }
-
-    // A[j+1] := key
-    A := A[j + 1 := key];
-
-    i := i + 1;
-  }
-};
-#end
-
--- TODO: cvc5 is finding counter-examples... fix wrong VCs
-#eval Strata.Boole.verify "cvc5" insertionSortPgm
-
-example : Strata.smtVCsCorrect insertionSortPgm := by
-  gen_smt_vcs
-  all_goals grind
diff --git a/lake-manifest.json b/lake-manifest.json
index ff8eecb60..7748e2cdb 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "68cf0a7e14add81c9a41c0ecfefdbca58a4504fb",
+   "rev": "3aba61f308be6b197ef1ebafc88d7e564144cd53",
    "name": "Strata",
    "manifestFile": "lake-manifest.json",
    "inputRev": "boole-clean",