diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 6c93a7c..ad4274b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -23,6 +23,11 @@ env:
   # resolve under actions/checkout's default shallow strategy.
   RELAY_REF: 178ffd479ad863c91ece4f580379a9207c36a530
   RIVET_REF: 78f001e23d595ba816f7a7be59282194dedfdc12
+  # Pinned rules_wasm_component for Bazel-running jobs (verus, future
+  # bazel build //...). wohl's MODULE.bazel uses local_path_override
+  # for local dev; CI checks out the pinned ref into a sibling path so
+  # the override resolves.
+  RULES_WASM_COMPONENT_REF: fbe20571eee9bd05687c95e7a43f6c236d9b2428
 
 jobs:
   lint:
@@ -182,3 +187,30 @@ jobs:
       - name: rivet validate
         working-directory: wohl
         run: rivet validate
+
+  verus:
+    name: Verus (bazel test //proofs/verus)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          path: wohl
+      - uses: actions/checkout@v4
+        with:
+          repository: pulseengine/rules_wasm_component
+          path: rules_wasm_component
+          ref: ${{ env.RULES_WASM_COMPONENT_REF }}
+          fetch-depth: 0
+      # rules_rocq_rust's module extension eagerly creates a
+      # nixpkgs-backed rocq_toolchains repo at Bazel analysis time,
+      # so every Bazel job needs nix-build on PATH (see MODULE.bazel
+      # comment). Pinned to cachix/install-nix-action v31.10.6.
+      - uses: cachix/install-nix-action@8aa03977d8d733052d78f4e008a241fd1dbf36b3
+      - uses: bazel-contrib/setup-bazel@0.15.0
+        with:
+          bazelisk-cache: true
+          disk-cache: ${{ github.workflow }}-verus
+          repository-cache: true
+      - name: bazel test //proofs/verus:alert_dedup_verify
+        working-directory: wohl
+        run: bazel test //proofs/verus:alert_dedup_verify --test_output=summary
diff --git a/MODULE.bazel b/MODULE.bazel
index dcf9ebe..4b8582b 100644
--- a/MODULE.bazel
+++ b/MODULE.bazel
@@ -39,6 +39,28 @@ git_override(
     commit = "e4660cc1b06fc4c0aefb49401fa2e2184cf804e3",
 )
 
+# rules_rocq_rust's module extension unconditionally creates the
+# rocq_toolchains repo via a nixpkgs package, even before any rocq rule
+# is loaded. That requires `nix-build` on PATH (local dev: install nix;
+# CI: see the install step in the verus job). The nixpkgs commit below
+# mirrors rivet — keep them in lock-step until we have a reason to
+# diverge.
+bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0")
+
+nix_repo = use_extension(
+    "@rules_nixpkgs_core//extensions:repository.bzl",
+    "nix_repo",
+)
+nix_repo.github(
+    name = "nixpkgs",
+    org = "NixOS",
+    repo = "nixpkgs",
+    # nixos-unstable with Rocq 9.0.1 (matches pulseengine/rivet's pin).
+    commit = "aca4d95fce4914b3892661bcb80b8087293536c6",
+    sha256 = "",
+)
+use_repo(nix_repo, "nixpkgs")
+
 local_path_override(
     module_name = "rules_wasm_component",
     path = "../rules_wasm_component",
diff --git a/MODULE.bazel.lock b/MODULE.bazel.lock
index 5f665ee..46abca8 100644
--- a/MODULE.bazel.lock
+++ b/MODULE.bazel.lock
@@ -339,7 +339,7 @@
     "@@rules_nixpkgs_core+//extensions:repository.bzl%nix_repo": {
       "general": {
         "bzlTransitiveDigest": "dTTtWNdwe7E4j77oKh1mHI1qtdxfaVSGSZa1oPf2QjU=",
-        "usagesDigest": "ZjI2xoiQBaRz3qc721Gc+tXJ9FrSWkJDOJeEXWOvz4Q=",
+        "usagesDigest": "+xvGwqDhVmiuZ2ymH5G9SDGZMpTkU5ccxmwXBQjvdtY=",
         "recordedInputs": [
           "REPO_MAPPING:rules_nixpkgs_core+,bazel_skylib bazel_skylib+"
         ],
@@ -348,15 +348,17 @@
             "repoRuleId": "@@rules_nixpkgs_core+//:nixpkgs.bzl%_nixpkgs_http_repository",
             "attributes": {
               "unmangled_name": "nixpkgs",
-              "url": "https://github.com/NixOS/nixpkgs/archive/refs/tags/24.05.tar.gz",
-              "strip_prefix": "nixpkgs-24.05",
+              "url": "https://github.com/NixOS/nixpkgs/archive/aca4d95fce4914b3892661bcb80b8087293536c6.tar.gz",
+              "strip_prefix": "nixpkgs-aca4d95fce4914b3892661bcb80b8087293536c6",
               "integrity": "",
-              "sha256": "911314b81780f26fdaf87e17174210bdbd40c86bac1795212f257cdc236a1e78"
+              "sha256": ""
             }
           }
         },
         "moduleExtensionMetadata": {
-          "explicitRootModuleDirectDeps": [],
+          "explicitRootModuleDirectDeps": [
+            "nixpkgs"
+          ],
           "explicitRootModuleDirectDevDeps": [],
           "useAllRepos": "NO",
           "reproducible": false