diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a66e5ef..a7242da 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -249,3 +249,35 @@ jobs:
         working-directory: tests/charon_llbc
         run: bazel test //:hello_verified --test_output=errors
         timeout-minutes: 30
+
+  relay-coverage:
+    name: Aeneas coverage — real relay primitive (Linux)
+    runs-on: [self-hosted, linux, x64, rust-cpu]
+    steps:
+      - uses: actions/checkout@v4
+      - uses: bazelbuild/setup-bazelisk@v3
+      - uses: actions/cache@v4
+        with:
+          path: ~/.cache/bazel
+          key: bazel-relaycov-${{ runner.os }}-${{ hashFiles('tests/relay_coverage/MODULE.bazel') }}
+          restore-keys: bazel-relaycov-${{ runner.os }}-
+      # Translate a real relay `plain` primitive (CRC32) to Lean and print it —
+      # coverage discovery for relay's verification-oriented Rust.
+      - name: Translate relay CRC32 (Rust -> LLBC -> Lean)
+        id: translate
+        working-directory: tests/relay_coverage
+        run: bazel build //:crc32_lean_check
+        timeout-minutes: 20
+        continue-on-error: true
+      - name: Show Aeneas output (full on success, partial on error)
+        working-directory: tests/relay_coverage
+        run: |
+          echo "===== Aeneas-generated Lean (may be partial if it errored) ====="
+          # no-sandbox action writes into out_dir even when it errors mid-way.
+          f=$(find bazel-bin bazel-out -name 'Crc32Llbc.lean' 2>/dev/null | head -1)
+          [ -n "$f" ] && cat "$f" || echo "(no output produced)"
+      - name: Fail if translation failed
+        if: steps.translate.outcome != 'success'
+        run: |
+          echo "Aeneas translation of relay CRC32 did not succeed (see partial output above)."
+          exit 1
diff --git a/tests/relay_coverage/BUILD.bazel b/tests/relay_coverage/BUILD.bazel
new file mode 100644
index 0000000..5698c38
--- /dev/null
+++ b/tests/relay_coverage/BUILD.bazel
@@ -0,0 +1,34 @@
+load("@rules_lean//aeneas:defs.bzl", "aeneas_translate", "charon_llbc")
+
+# Aeneas coverage experiment on a real relay primitive (CRC32).
+# Rust -> LLBC (Charon) -> Lean (Aeneas). Translate-only: reveals what Aeneas
+# can handle from relay's `plain` verification code, without the heavy compile.
+charon_llbc(
+    name = "crc32_llbc",
+    srcs = ["src/lib.rs"],
+    crate_name = "crc32",
+    crate_root = "src/lib.rs",
+)
+
+aeneas_translate(
+    name = "crc32_lean",
+    srcs = [":crc32_llbc"],
+)
+
+# Assert Aeneas produced a non-empty module.
+genrule(
+    name = "crc32_lean_check",
+    srcs = [":crc32_lean"],
+    outs = ["crc32_lean_check.stamp"],
+    cmd = """
+set -euo pipefail
+LEAN=$(SRCS)
+if [ ! -s "$$LEAN" ]; then
+    echo "ERROR: aeneas produced an empty module at $$LEAN" >&2
+    exit 1
+fi
+echo "aeneas translated relay CRC32 -> $$LEAN ($$(wc -c < "$$LEAN") bytes)"
+echo "OK" > $@
+""",
+    testonly = True,
+)
diff --git a/tests/relay_coverage/MODULE.bazel b/tests/relay_coverage/MODULE.bazel
new file mode 100644
index 0000000..6d26e5a
--- /dev/null
+++ b/tests/relay_coverage/MODULE.bazel
@@ -0,0 +1,46 @@
+module(name = "test_relay_coverage", version = "0.0.0")
+
+bazel_dep(name = "rules_lean", version = "0.1.0")
+local_path_override(
+    module_name = "rules_lean",
+    path = "../..",
+)
+
+bazel_dep(name = "bazel_skylib", version = "1.7.1")
+bazel_dep(name = "platforms", version = "0.0.11")
+bazel_dep(name = "rules_shell", version = "0.3.0")
+
+# Charon + Aeneas binary toolchains (translate-only; no lean toolchain needed).
+aeneas = use_extension("@rules_lean//aeneas:extensions.bzl", "aeneas")
+aeneas.charon_toolchain(
+    version = "build-2026.04.22.081730-2d35584fb79ef804c50f106d8c40bd3728284f8d",
+)
+aeneas.toolchain(
+    version = "build-2026.04.22.084123-1a8946778f0934266d63564c2aac74ec1fff4b68",
+    rev = "1a8946778f0934266d63564c2aac74ec1fff4b68",
+    lean_version = "4.28.0-rc1",
+    sha256 = {
+        "macos_aarch64": "62393cd005c67290fc38cf0e4361f9bf242b73e695aa1777bd7685023a60db09",
+        "macos_x86_64": "6320148064af0c98c556f27c66077309869e585da449776c53dde65d21da6ae2",
+        "linux_x86_64": "f0b9e245c11eae567ab57317e91fca3fc090a246d2ebdb8d618d8d70b90c8ecc",
+    },
+)
+
+use_repo(
+    aeneas,
+    "charon_toolchains",
+    "charon_macos_aarch64",
+    "charon_macos_x86_64",
+    "charon_linux_x86_64",
+    "charon_linux_aarch64",
+    "aeneas_toolchains",
+    "aeneas_macos_aarch64",
+    "aeneas_macos_x86_64",
+    "aeneas_linux_x86_64",
+    "aeneas_lean_lib",
+)
+
+register_toolchains(
+    "@charon_toolchains//:all",
+    "@aeneas_toolchains//:all",
+)
diff --git a/tests/relay_coverage/src/lib.rs b/tests/relay_coverage/src/lib.rs
new file mode 100644
index 0000000..491ea0c
--- /dev/null
+++ b/tests/relay_coverage/src/lib.rs
@@ -0,0 +1,46 @@
+//! Aeneas coverage experiment: a REAL relay primitive translated verbatim.
+//!
+//! Source: pulseengine/relay `crates/relay-primitives/plain/src/crc32.rs`
+//! (test module stripped). Exercises features beyond the trivial example:
+//! a const-eval array, `&[u8]` slices, indexing, `as` casts, `%`, bit ops,
+//! `while` loops. The point is to discover what Aeneas can translate from
+//! relay's verification-oriented `plain` code.
+
+/// CRC32 lookup table for polynomial 0xEDB88320 (standard reflected).
+///
+/// WORKAROUND: computed by a runtime fn instead of a `const`. Aeneas
+/// (build-2026.04.22) hits an internal error translating the const-eval'd
+/// global array form (the identical body as a `const` fails at src/lib.rs:10).
+pub fn crc32_table() -> [u32; 256] {
+    let mut table = [0u32; 256];
+    let mut i: usize = 0;
+    while i < 256 {
+        let mut crc: u32 = i as u32;
+        let mut j: usize = 0;
+        while j < 8 {
+            if crc & 1 != 0 {
+                crc = (crc >> 1) ^ 0xEDB8_8320u32;
+            } else {
+                crc = crc >> 1;
+            }
+            j = j + 1;
+        }
+        table[i] = crc;
+        i = i + 1;
+    }
+    table
+}
+
+/// Compute CRC32 over a byte slice. Pure, deterministic, total.
+pub fn crc32_compute(data: &[u8]) -> u32 {
+    let table = crc32_table();
+    let mut crc: u32 = 0xFFFF_FFFFu32;
+    let mut i: usize = 0;
+    while i < data.len() {
+        let byte = data[i];
+        let raw_index = ((crc ^ (byte as u32)) % 256u32) as usize;
+        crc = (crc >> 8) ^ table[raw_index];
+        i = i + 1;
+    }
+    crc ^ 0xFFFF_FFFFu32
+}