diff --git a/MODULE.bazel b/MODULE.bazel
index 94ca14d..2a4ee8f 100644
--- a/MODULE.bazel
+++ b/MODULE.bazel
@@ -112,7 +112,7 @@ bazel_dep(name = "rules_verus", version = "0.1.0")
 
 git_override(
     module_name = "rules_verus",
-    commit = "e2c1600",
+    commit = "8a2bbf6",
     remote = "https://github.com/pulseengine/rules_verus.git",
 )
 
diff --git a/src/lib/src/verus_proofs/BUILD.bazel b/src/lib/src/verus_proofs/BUILD.bazel
index b9c3d04..e07be31 100644
--- a/src/lib/src/verus_proofs/BUILD.bazel
+++ b/src/lib/src/verus_proofs/BUILD.bazel
@@ -1,6 +1,8 @@
-load("@rules_verus//verus:defs.bzl", "verus_library", "verus_test")
+load("@rules_verus//verus:defs.bzl", "verus_library", "verus_strip", "verus_test")
+
+# ── Track 1: Verus SMT verification (CV-20, CV-21, CV-22) ──────────
+# Fully hermetic — bundled Rust sysroot, no rustup needed.
 
-# Merkle tree inclusion proof soundness (CV-20) and anti-rollback (CV-21)
 verus_library(
     name = "wsc_merkle_proofs",
     srcs = [
@@ -23,3 +25,15 @@ verus_test(
     crate_root = "mod.rs",
     crate_name = "wsc_verus_proofs",
 )
+
+# ── Track 2: Strip Verus → plain Rust for coq-of-rust pipeline ─────
+
+verus_strip(
+    name = "wsc_proofs_stripped",
+    srcs = [
+        "mod.rs",
+        "merkle_proofs.rs",
+        "dsse_proofs.rs",
+    ],
+    visibility = ["//visibility:public"],
+)