diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index d5ca8cefa..997cf991c 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -14,14 +14,24 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - name: Set TEST_ARGS manually
-        run: |
-          echo "TEST_ARGS='--wfail --iofail'" >> $GITHUB_ENV
-        shell: bash
       - uses: leanprover/lean-action@v1
         with:
-          build-args: "--wfail --iofail"
-          test-args: "--wfail --iofail"
+          build: false
+          test: false
+          lint: false
+      - name: Set up cvc5
+        run: |
+          lake update cvc5
+          lake build @cvc5
+          cvc5_bin="$(find .lake/packages/cvc5 -maxdepth 5 -type f -name cvc5 -path '*/bin/cvc5' -print -quit)"
+          test -n "$cvc5_bin"
+          echo "$(dirname "$cvc5_bin")" >> "$GITHUB_PATH"
+      - name: Build
+        run: lake build --wfail --iofail
+      - name: Test
+        run: lake test --wfail --iofail
+      - name: Lint
+        run: lake lint
       - name: "lake exe mk_all --check"
         run: |
           set -e
diff --git a/Cslib/Languages/Boole/examples/circular_queue.lean b/Cslib/Languages/Boole/examples/circular_queue.lean
new file mode 100644
index 000000000..09b403aa9
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/circular_queue.lean
@@ -0,0 +1,141 @@
+import StrataBoole.MetaVerifier
+import Smt
+
+------------------------------------------------------------
+namespace Strata
+
+-- Circular-buffer queue.
+--
+-- The queue is represented by an array `Q`, a capacity `n`, a head pointer, a
+-- tail pointer, and a live element count.  Unlike `queue_array_based.lean`,
+-- `head` and `tail` wrap back to zero when they reach the capacity.  We model
+-- that wraparound with a small `NextIndex` function instead of `mod`, so the
+-- verification conditions remain simple arithmetic plus map-update reasoning.
+private def circularQueuePgm :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+// `NextIndex(i, n)` is the usual circular-buffer successor:
+// `if i + 1 == n then 0 else i + 1`.
+//
+function NextIndex(i : int, n : int) : int {
+  if i + 1 == n then 0 else i + 1
+}
+
+var Q     : Array;
+var n     : int;
+var head  : int;
+var tail  : int;
+var count : int;
+
+// Initialize an empty circular queue.
+procedure CircularQueueInit(cap : int) returns ()
+spec
+{
+  requires cap > 0;
+  modifies n;
+  modifies head;
+  modifies tail;
+  modifies count;
+
+  ensures n == cap;
+  ensures head == 0;
+  ensures tail == 0;
+  ensures count == 0;
+}
+{
+  n := cap;
+  head := 0;
+  tail := 0;
+  count := 0;
+};
+
+// Return whether the circular queue is empty.
+procedure CircularQueueEmpty() returns (b : bool)
+spec
+{
+  ensures (b ==> count == 0);
+  ensures (count == 0 ==> b);
+}
+{
+  if (count == 0) {
+    b := true;
+  } else {
+    b := false;
+  }
+};
+
+// Return whether the circular queue is full.
+procedure CircularQueueFull() returns (b : bool)
+spec
+{
+  ensures (b ==> count == n);
+  ensures (count == n ==> b);
+}
+{
+  if (count == n) {
+    b := true;
+  } else {
+    b := false;
+  }
+};
+
+// Add `x` at the current tail position and advance the tail pointer, wrapping
+// to zero when the insertion occurs at the last array slot.
+procedure CircularEnqueue(x : int) returns ()
+spec
+{
+  requires n > 0;
+  requires 0 <= head && head < n;
+  requires 0 <= tail && tail < n;
+  requires 0 <= count && count < n;
+  modifies Q;
+  modifies tail;
+  modifies count;
+
+  ensures count == old(count) + 1;
+  ensures Q[old(tail)] == x;
+  ensures 0 <= tail && tail < n;
+  ensures (
+    ∀ i:int .
+      0 <= i && i < n && i != old(tail) ==> Q[i] == old(Q[i])
+  );
+}
+{
+  Q := Q[tail := x];
+  tail := NextIndex(tail, n);
+  count := count + 1;
+};
+
+// Remove and return the current head element, then advance the head pointer
+// with the same wraparound convention.
+procedure CircularDequeue() returns (x : int)
+spec
+{
+  requires n > 0;
+  requires 0 <= head && head < n;
+  requires 0 <= tail && tail < n;
+  requires 0 < count && count <= n;
+  modifies head;
+  modifies count;
+
+  ensures x == old(Q[old(head)]);
+  ensures count == old(count) - 1;
+  ensures 0 <= head && head < n;
+}
+{
+  x := Q[head];
+  head := NextIndex(head, n);
+  count := count - 1;
+};
+
+#end
+
+theorem circularQueuePgm_smtVCsCorrect :
+    Strata.smtVCsCorrectBoole circularQueuePgm := by
+  gen_smt_vcs_boole
+  all_goals (first | smt +mono | omega | trivial | grind)
+
+end Strata
diff --git a/Cslib/Languages/Boole/examples/deque_array_based.lean b/Cslib/Languages/Boole/examples/deque_array_based.lean
new file mode 100644
index 000000000..de97c2456
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/deque_array_based.lean
@@ -0,0 +1,146 @@
+import StrataBoole.MetaVerifier
+import Smt
+
+------------------------------------------------------------
+namespace Strata
+
+-- Array-backed double-ended queue.
+--
+-- A deque supports insertion and removal at both ends.  This example uses a
+-- bounded, non-circular array model: live elements occupy indices
+-- `front .. back - 1`, with `front == back` meaning empty.  The front can move
+-- left and the back can move right, so `PushFront` requires spare space before
+-- `front` and `PushBack` requires spare space after `back`.
+--
+-- The circular-buffer queue example covers wraparound behavior separately.
+-- Keeping this deque non-circular makes the specifications direct and lets the
+-- example focus on four endpoint operations, `old(...)`, and frame properties.
+private def dequeArrayPgm :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+var D     : Array;
+var n     : int;
+var front : int;
+var back  : int;
+
+// Initialize an empty deque.  Starting both endpoints at `start` leaves room
+// to grow in either direction if `0 < start < cap`.
+procedure DequeInit(cap : int, start : int) returns ()
+spec
+{
+  requires cap > 0;
+  requires 0 <= start && start <= cap;
+  modifies n;
+  modifies front;
+  modifies back;
+
+  ensures n == cap;
+  ensures front == start;
+  ensures back == start;
+}
+{
+  n := cap;
+  front := start;
+  back := start;
+};
+
+// Return whether the deque has no live elements.
+procedure DequeEmpty() returns (b : bool)
+spec
+{
+  ensures (b ==> front == back);
+  ensures (front == back ==> b);
+}
+{
+  if (front == back) {
+    b := true;
+  } else {
+    b := false;
+  }
+};
+
+// Add `x` to the back of the deque.
+procedure PushBack(x : int) returns ()
+spec
+{
+  requires 0 <= front && front <= back;
+  requires back < n;
+  modifies D;
+  modifies back;
+
+  ensures back == old(back) + 1;
+  ensures D[old(back)] == x;
+  ensures (
+    ∀ i:int .
+      old(front) <= i && i < old(back) ==> D[i] == old(D[i])
+  );
+}
+{
+  D := D[back := x];
+  back := back + 1;
+};
+
+// Remove and return the last element of the deque.
+procedure PopBack() returns (x : int)
+spec
+{
+  requires front < back;
+  modifies back;
+
+  ensures back == old(back) - 1;
+  ensures x == old(D[old(back) - 1]);
+  ensures front <= back;
+}
+{
+  back := back - 1;
+  x := D[back];
+};
+
+// Add `x` to the front of the deque.
+procedure PushFront(x : int) returns ()
+spec
+{
+  requires 0 < front && front <= back;
+  requires back <= n;
+  modifies D;
+  modifies front;
+
+  ensures front == old(front) - 1;
+  ensures D[front] == x;
+  ensures (
+    ∀ i:int .
+      old(front) <= i && i < old(back) ==> D[i] == old(D[i])
+  );
+}
+{
+  front := front - 1;
+  D := D[front := x];
+};
+
+// Remove and return the first element of the deque.
+procedure PopFront() returns (x : int)
+spec
+{
+  requires front < back;
+  modifies front;
+
+  ensures front == old(front) + 1;
+  ensures x == old(D[old(front)]);
+  ensures front <= back;
+}
+{
+  x := D[front];
+  front := front + 1;
+};
+
+#end
+
+theorem dequeArrayPgm_smtVCsCorrect :
+    Strata.smtVCsCorrectBoole dequeArrayPgm := by
+  gen_smt_vcs_boole
+  all_goals (first | smt +mono | omega | trivial | grind)
+
+end Strata
diff --git a/Cslib/Languages/Boole/examples/queue_array_based.lean b/Cslib/Languages/Boole/examples/queue_array_based.lean
new file mode 100644
index 000000000..bdc6d80fa
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/queue_array_based.lean
@@ -0,0 +1,126 @@
+import StrataBoole.MetaVerifier
+import Smt
+
+------------------------------------------------------------
+namespace Strata
+
+-- CLRS Chapter 10: Queues (array implementation).
+--
+-- This version models a bounded, non-circular FIFO queue.  The queue contents
+-- occupy indices `head .. tail - 1`; `head == tail` means empty.  Unlike a
+-- circular-buffer implementation, this example does not wrap `head` or `tail`
+-- modulo the capacity.  That keeps the arithmetic simple and focuses the
+-- verification on global variables, `modifies` clauses, and `old(...)`
+-- postconditions.
+private def queueArrayPgm :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+// Global queue storage, capacity, and head/tail pointers.
+//
+// Valid live elements are stored in Q[head], Q[head + 1], ..., Q[tail - 1].
+// The next enqueue writes at Q[tail].  The next dequeue reads from Q[head].
+var Q    : Array;
+var n    : int;
+var head : int;
+var tail : int;
+
+// Initialize an empty queue with capacity `cap`.
+procedure QueueInit(cap : int) returns ()
+spec
+{
+  requires cap >= 0;
+  modifies n;
+  modifies head;
+  modifies tail;
+  ensures n == cap;
+  ensures head == 0;
+  ensures tail == 0;
+}
+{
+  n := cap;
+  head := 0;
+  tail := 0;
+};
+
+// Return whether the queue is empty.
+//
+// The postconditions state both directions of the Boolean result:
+// if `b` is true then the queue is empty, and if the queue is empty then `b`
+// is true.  Together these characterize `b` as `(head == tail)`.
+procedure QueueEmpty() returns (b : bool)
+spec
+{
+  ensures (b ==> head == tail);
+  ensures (head == tail ==> b);
+}
+{
+  if (head == tail) {
+    b := true;
+  } else {
+    b := false;
+  }
+};
+
+// Add `x` to the back of the queue.
+//
+// Preconditions require a well-formed, non-full queue segment:
+// `0 <= head <= tail < n`.  The `modifies` clause records that this operation
+// changes the queue array and the tail pointer, but not the head pointer or
+// capacity.  The postconditions use `old(...)` to relate the post-state to the
+// pre-state:
+// * `tail` advances by one;
+// * the old tail slot now stores `x`;
+// * all previously live elements are preserved.
+procedure Enqueue(x : int) returns ()
+spec
+{
+  requires 0 <= head;
+  requires head <= tail;
+  requires tail < n;
+  modifies Q;
+  modifies tail;
+
+  ensures tail == old(tail) + 1;
+  ensures Q[old(tail)] == x;
+  ensures (
+    ∀ i:int .
+      old(head) <= i && i < old(tail) ==> Q[i] == old(Q[i])
+  );
+}
+{
+  Q := Q[tail := x];
+  tail := tail + 1;
+};
+
+// Remove and return the front element of the queue.
+//
+// The non-empty precondition `head < tail` guarantees that `Q[head]` is a live
+// element.  Dequeue changes only the head pointer: the array contents and tail
+// are not modified.  The returned value is the element that was at the old head,
+// and the post-state head advances by one.
+procedure Dequeue() returns (x : int)
+spec
+{
+  requires head < tail;
+  modifies head;
+
+  ensures head == old(head) + 1;
+  ensures x == old(Q[old(head)]);
+  ensures head <= tail;
+}
+{
+  x := Q[head];
+  head := head + 1;
+};
+
+#end
+
+theorem queueArrayPgm_smtVCsCorrect :
+    Strata.smtVCsCorrectBoole queueArrayPgm := by
+  gen_smt_vcs_boole
+  all_goals (first | smt +mono | omega | trivial | grind)
+
+end Strata
diff --git a/Cslib/Languages/Boole/examples/seq_slicing.lean b/Cslib/Languages/Boole/examples/seq_slicing.lean
index f0a6f2606..cf2615ed5 100644
--- a/Cslib/Languages/Boole/examples/seq_slicing.lean
+++ b/Cslib/Languages/Boole/examples/seq_slicing.lean
@@ -144,6 +144,8 @@ Result: ✅ pass-/
 #guard_msgs in
 #eval Strata.Boole.verify "cvc5" seqSlicingSeed (options := .quiet)
 
+-- `smt`/`smt +mono` trigger a kernel application type mismatch here (not just a tactic
+-- failure) on the `Sequence` obligations, so they're deliberately excluded.
 theorem seqSlicingSeed_smtVCsCorrect : Strata.smtVCsCorrectBoole seqSlicingSeed := by
   gen_smt_vcs_boole
   all_goals (first | omega | trivial | grind)
diff --git a/Cslib/Languages/Boole/examples/two_sum.lean b/Cslib/Languages/Boole/examples/two_sum.lean
index 00d4bd3bb..054f50524 100644
--- a/Cslib/Languages/Boole/examples/two_sum.lean
+++ b/Cslib/Languages/Boole/examples/two_sum.lean
@@ -124,6 +124,8 @@ Result: ✅ pass-/
 #guard_msgs in
 #eval Strata.Boole.verify "cvc5" twoSumPgm (options := .quiet)
 
+-- `smt`/`smt +mono` trigger a kernel application type mismatch here (not just a tactic
+-- failure), so they're deliberately excluded from the fallback chain.
 set_option maxHeartbeats 1000000 in
 theorem twoSumPgm_smtVCsCorrect : Strata.smtVCsCorrectBoole twoSumPgm := by
   gen_smt_vcs_boole