diff --git a/.bcr/presubmit.yml b/.bcr/presubmit.yml
index 837e942..a1ac32a 100644
--- a/.bcr/presubmit.yml
+++ b/.bcr/presubmit.yml
@@ -1,12 +1,21 @@
 bcr_test_module:
   module_path: "examples/rust_to_rocq"
   matrix:
-    platform: ["debian11", "macos", "ubuntu2204"]
-    bazel: ["7.x", "8.x"]
+    platform: ["ubuntu2204"]
+    bazel: ["8.x"]
   tasks:
     run_tests:
       name: "Build rust_to_rocq example"
       platform: ${{ platform }}
       bazel: ${{ bazel }}
+      environment:
+        # Nix installer updates ~/.profile but Buildkite CI disregards it.
+        # Cargo/rustup installed to ~/.cargo/bin.
+        PATH: /var/lib/buildkite-agent/.nix-profile/bin:/var/lib/buildkite-agent/.cargo/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
+        # Rust nightly sysroot lib needed for linking rustc_private crates
+        LIBRARY_PATH: /var/lib/buildkite-agent/.rustup/toolchains/nightly-2024-12-07-x86_64-unknown-linux-gnu/lib
+      shell_commands:
+        - curl -L https://nixos.org/nix/install | sh -s -- --no-daemon
+        - curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain nightly-2024-12-07 -c rustc-dev,rust-src,llvm-tools-preview
       build_targets:
-        - "//:all"
+        - "//:point_proofs"
diff --git a/examples/rust_to_rocq/MODULE.bazel b/examples/rust_to_rocq/MODULE.bazel
new file mode 100644
index 0000000..a25da9e
--- /dev/null
+++ b/examples/rust_to_rocq/MODULE.bazel
@@ -0,0 +1,52 @@
+"""BCR test module for rules_rocq_rust.
+
+This standalone module exercises the full Rust-to-Rocq verification pipeline:
+translate Rust to Rocq, compile the Rocq code, and verify proofs.
+"""
+
+module(
+    name = "rules_rocq_rust_example",
+    version = "0.1.0",
+)
+
+# Depend on rules_rocq_rust (local_path_override for dev, BCR resolves it in presubmit)
+bazel_dep(name = "rules_rocq_rust")
+local_path_override(
+    module_name = "rules_rocq_rust",
+    path = "../..",
+)
+
+# Nix integration (transitive dep from rules_rocq_rust, but root module must configure repo)
+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
+    commit = "aca4d95fce4914b3892661bcb80b8087293536c6",
+    sha256 = "",
+)
+use_repo(nix_repo, "nixpkgs")
+
+# Rocq toolchain
+rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq")
+rocq.toolchain(
+    version = "9.0",
+    strategy = "nix",
+    with_rocq_of_rust_deps = True,
+)
+use_repo(rocq, "rocq_toolchains", "rocq_stdlib", "rocq_coqutil", "rocq_hammer", "rocq_hammer_tactics", "rocq_smpl")
+register_toolchains("@rocq_toolchains//:all")
+
+# rocq-of-rust toolchain
+rocq_of_rust = use_extension("@rules_rocq_rust//coq_of_rust:extensions.bzl", "rocq_of_rust")
+rocq_of_rust.toolchain(
+    use_real_library = True,
+)
+use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_source")
+register_toolchains("@rocq_of_rust_toolchains//:toolchain")