diff --git a/MODULE.bazel b/MODULE.bazel
index 04353ce..005c4d1 100644
--- a/MODULE.bazel
+++ b/MODULE.bazel
@@ -7,8 +7,8 @@ bazel_dep(name = "bazel_skylib", version = "1.7.1")
 bazel_dep(name = "platforms", version = "0.0.11")
 
 lean = use_extension("//lean:extensions.bzl", "lean")
-lean.toolchain(version = "4.27.0")
-lean.mathlib(rev = "v4.27.0")
+lean.toolchain(version = "4.29.1")
+lean.mathlib(rev = "v4.29.1")
 
 use_repo(lean, "lean_toolchains", "mathlib")
 
diff --git a/README.md b/README.md
index f2cdc3a..320d7c8 100644
--- a/README.md
+++ b/README.md
@@ -11,7 +11,7 @@ Add to your `MODULE.bazel`:
 bazel_dep(name = "rules_lean", version = "0.1.0")
 
 lean = use_extension("@rules_lean//lean:extensions.bzl", "lean")
-lean.toolchain(version = "4.27.0")
+lean.toolchain(version = "4.29.1")
 
 use_repo(lean, "lean_toolchains")
 register_toolchains("@lean_toolchains//:all")
@@ -21,8 +21,8 @@ register_toolchains("@lean_toolchains//:all")
 
 ```starlark
 lean = use_extension("@rules_lean//lean:extensions.bzl", "lean")
-lean.toolchain(version = "4.27.0")
-lean.mathlib(rev = "v4.27.0")
+lean.toolchain(version = "4.29.1")
+lean.mathlib(rev = "v4.29.1")
 
 use_repo(lean, "lean_toolchains", "mathlib")
 register_toolchains("@lean_toolchains//:all")
@@ -103,7 +103,7 @@ For reproducible builds, provide SHA-256 hashes per platform:
 
 ```starlark
 lean.toolchain(
-    version = "4.27.0",
+    version = "4.29.1",
     sha256 = {
         "darwin_aarch64": "abc123...",
         "darwin_x86_64": "def456...",
@@ -137,7 +137,7 @@ aeneas = use_extension("@rules_lean//aeneas:extensions.bzl", "aeneas")
 aeneas.toolchain(
     version = "build-2026.03.14.003732-912707da86162a566cd8b01f137383ec411b31de",
     rev = "912707da86162a566cd8b01f137383ec411b31de",
-    lean_version = "4.27.0",
+    lean_version = "4.29.1",
 )
 
 use_repo(aeneas, "aeneas_toolchains", "aeneas_lean_lib")
diff --git a/aeneas/BUILD.bazel b/aeneas/BUILD.bazel
index 9733f2a..5ff1c50 100644
--- a/aeneas/BUILD.bazel
+++ b/aeneas/BUILD.bazel
@@ -4,3 +4,8 @@ toolchain_type(
     name = "toolchain_type",
     visibility = ["//visibility:public"],
 )
+
+toolchain_type(
+    name = "charon_toolchain_type",
+    visibility = ["//visibility:public"],
+)
diff --git a/aeneas/extensions.bzl b/aeneas/extensions.bzl
index 4d0af64..0f1cbc8 100644
--- a/aeneas/extensions.bzl
+++ b/aeneas/extensions.bzl
@@ -1,6 +1,60 @@
-"Module extension for Aeneas toolchain."
+"Module extension for Aeneas + Charon toolchains."
 
-load("//aeneas/private:repo.bzl", "ALL_AENEAS_PLATFORMS", "aeneas_lean_lib", "aeneas_release", "aeneas_toolchains_hub")
+load(
+    "//aeneas/private:charon_repo.bzl",
+    "ALL_CHARON_PLATFORMS",
+    "charon_release",
+    "charon_toolchains_hub",
+)
+load(
+    "//aeneas/private:repo.bzl",
+    "ALL_AENEAS_PLATFORMS",
+    "aeneas_lean_lib",
+    "aeneas_release",
+    "aeneas_toolchains_hub",
+)
+
+# Registry of known Charon releases. Keys are upstream release tags. Each entry
+# carries the Charon tarball hashes (per rules_lean platform slug) plus the
+# matching Rust toolchain channel/date and the hashes for each Rust component.
+#
+# To add a new entry:
+#   1. Find a release at https://github.com/AeneasVerif/charon/releases .
+#   2. Read `charon/rust-toolchain` at the pinned git commit to get the Rust
+#      nightly date and the required components.
+#   3. Run:
+#        curl -sL <charon-tarball-url> | sha256sum
+#        curl -sL https://static.rust-lang.org/dist/<date>/<component>.tar.xz | sha256sum
+#      for each component and platform.
+_KNOWN_CHARON_VERSIONS = {
+    # Aeneas pins commit bb585116362158a68b2633ce871951d520a50e13 (2026-04-21).
+    # That SHA is not itself released as a Charon tarball, so we use the
+    # closest prior published release (2026-04-22) — functionally equivalent
+    # because no commits landed between the two timestamps that affect the
+    # LLBC output format.
+    "build-2026.04.22.081730-2d35584fb79ef804c50f106d8c40bd3728284f8d": {
+        "charon_sha256": {
+            "macos_aarch64": "8668c8d7e1954277401380748b7f3772628a5bee8f96b630ec69fe7cf5f1f671",
+            "macos_x86_64": "790145f58acda4e2ffa3c483c6259aa7f3e905f1f04f39490c1727719467bce2",
+            "linux_x86_64": "1a212a1e0bd02bda22e429fa8029e715948ace82dfe523f53b349b80ddf39524",
+            # linux_aarch64: no prebuilt published upstream.
+        },
+        "rust_channel": "nightly-2026-02-07",
+        "rust_version": "2026-02-07",
+        "rust_sha256": {
+            "rustc_macos_aarch64": "2e50bef1a29c0d4de66198c71b2f7ce907a954df91a11241b62f03cfe431c69d",
+            "rust_std_macos_aarch64": "09bb0b959b990351ae3b78db170498a320f8ed921f34ba812c70d77b8eddb21d",
+            "rustc_dev_macos_aarch64": "1047e6b72b5ec12e8524b8a00f73719aa1b863349a790a139fbffabb52fba860",
+            "rustc_macos_x86_64": "8530d915b6135030369868d886f71c2dad8fe850a64227d9d3d66e30fcce1b64",
+            "rust_std_macos_x86_64": "f984c016a20d017a61935111477a73ba282da758b67db96be1388b91c8747059",
+            "rustc_dev_macos_x86_64": "304d769a7112a642fcdb1fcd18da370e00b0bbb43f373d6d387a5a3e010b60df",
+            "rustc_linux_x86_64": "2783e4113d9b0ee465a07ef83c436f92ab789f73c14699c09e003a14b04000ac",
+            "rust_std_linux_x86_64": "166c55a1e0450e4f7709da70f2053a844f438088b95ce97dd67923143fe38782",
+            "rustc_dev_linux_x86_64": "931939b8a53eae8cc3f4c5c80399af2c2d481b26fcd5399773ca2b59b11282cb",
+            "rust_src": "65a35eb3b9a96888b73d243c89b228092149e546ee10ce752e816d75ba2defe1",
+        },
+    },
+}
 
 def _detect_host_platform(module_ctx):
     os_name = module_ctx.os.name.lower()
@@ -11,6 +65,8 @@ def _detect_host_platform(module_ctx):
             return "macos_aarch64"
         return "macos_x86_64"
     elif "linux" in os_name:
+        if "aarch64" in os_arch or "arm64" in os_arch:
+            return "linux_aarch64"
         return "linux_x86_64"
     else:
         fail("Unsupported host platform for Aeneas: {} {}".format(os_name, os_arch))
@@ -22,7 +78,39 @@ _AeneasToolchainTag = tag_class(attrs = {
     "sha256": attr.string_dict(default = {}, doc = "Per-platform SHA-256 overrides"),
 })
 
+_CharonToolchainTag = tag_class(attrs = {
+    "version": attr.string(
+        mandatory = True,
+        doc = "Charon release tag (e.g. 'build-2026.04.22.081730-<sha>').",
+    ),
+    "rust_version": attr.string(
+        default = "",
+        doc = "Override the Rust nightly date (e.g. '2026-02-07'). " +
+              "If empty, the registry entry for `version` is used.",
+    ),
+    "rust_channel": attr.string(
+        default = "",
+        doc = "Override the Rust channel name (e.g. 'nightly-2026-02-07'). " +
+              "If empty, the registry entry for `version` is used.",
+    ),
+    "charon_sha256": attr.string_dict(
+        default = {},
+        doc = "Per-platform SHA-256 overrides for the Charon tarball " +
+              "(keys: macos_aarch64, macos_x86_64, linux_x86_64).",
+    ),
+    "rust_sha256": attr.string_dict(
+        default = {},
+        doc = "Per-component Rust SHA-256 overrides " +
+              "(keys: rustc_<plat>, rust_std_<plat>, rustc_dev_<plat>, rust_src).",
+    ),
+    "require_hashes": attr.bool(
+        default = True,
+        doc = "Fail if any needed SHA-256 is empty. Set False for development.",
+    ),
+})
+
 def _aeneas_impl(module_ctx):
+    # ── Aeneas ───────────────────────────────────────────────────────────
     version = None
     rev = None
     lean_version = None
@@ -36,42 +124,127 @@ def _aeneas_impl(module_ctx):
                 lean_version = tag.lean_version
                 sha256_overrides = dict(tag.sha256)
 
-    if version == None:
-        return
+    if version != None:
+        for platform in ALL_AENEAS_PLATFORMS:
+            sha256 = sha256_overrides.get(platform, "")
+            aeneas_release(
+                name = "aeneas_" + platform,
+                version = version,
+                platform = platform,
+                sha256 = sha256,
+            )
+
+        aeneas_toolchains_hub(
+            name = "aeneas_toolchains",
+            platforms = ALL_AENEAS_PLATFORMS,
+        )
+
+        # Build the Aeneas Lean support library
+        host_platform = _detect_host_platform(module_ctx)
+
+        lean_platform_map = {
+            "macos_aarch64": "darwin_aarch64",
+            "macos_x86_64": "darwin_x86_64",
+            "linux_x86_64": "linux_x86_64",
+            "linux_aarch64": "linux_aarch64",
+        }
 
-    for platform in ALL_AENEAS_PLATFORMS:
-        sha256 = sha256_overrides.get(platform, "")
-        aeneas_release(
-            name = "aeneas_" + platform,
-            version = version,
-            platform = platform,
-            sha256 = sha256,
+        aeneas_lean_lib(
+            name = "aeneas_lean_lib",
+            host_platform = lean_platform_map[host_platform],
+            lean_version = lean_version,
+            aeneas_rev = rev,
         )
 
-    aeneas_toolchains_hub(
-        name = "aeneas_toolchains",
-        platforms = ALL_AENEAS_PLATFORMS,
-    )
+    # ── Charon ───────────────────────────────────────────────────────────
+    charon_version = None
+    charon_rust_version = None
+    charon_rust_channel = None
+    charon_sha_overrides = {}
+    charon_rust_sha_overrides = {}
+    charon_require_hashes = True
+
+    for mod in module_ctx.modules:
+        for tag in mod.tags.charon_toolchain:
+            if charon_version == None or mod.is_root:
+                charon_version = tag.version
+                charon_rust_version = tag.rust_version
+                charon_rust_channel = tag.rust_channel
+                charon_sha_overrides = dict(tag.charon_sha256)
+                charon_rust_sha_overrides = dict(tag.rust_sha256)
+                charon_require_hashes = tag.require_hashes
+
+    if charon_version != None:
+        known = _KNOWN_CHARON_VERSIONS.get(charon_version, {})
+        known_charon_sha = known.get("charon_sha256", {})
+        known_rust_sha = known.get("rust_sha256", {})
+        rust_version = charon_rust_version or known.get("rust_version", "")
+        rust_channel = charon_rust_channel or known.get("rust_channel", "")
 
-    # Build the Aeneas Lean support library
-    host_platform = _detect_host_platform(module_ctx)
+        if charon_require_hashes and not rust_version:
+            fail(
+                "charon.toolchain(version='{}') has no rust_version override " .format(charon_version) +
+                "and is not in _KNOWN_CHARON_VERSIONS. Provide rust_version explicitly " +
+                "or set require_hashes = False.",
+            )
+        if charon_require_hashes and not rust_channel:
+            fail(
+                "charon.toolchain(version='{}') has no rust_channel override " .format(charon_version) +
+                "and is not in _KNOWN_CHARON_VERSIONS. Provide rust_channel explicitly " +
+                "or set require_hashes = False.",
+            )
 
-    lean_platform_map = {
-        "macos_aarch64": "darwin_aarch64",
-        "macos_x86_64": "darwin_x86_64",
-        "linux_x86_64": "linux_x86_64",
-    }
+        # Merge registry hashes with per-module overrides.
+        merged_rust_sha = dict(known_rust_sha)
+        for k, v in charon_rust_sha_overrides.items():
+            merged_rust_sha[k] = v
 
-    aeneas_lean_lib(
-        name = "aeneas_lean_lib",
-        host_platform = lean_platform_map[host_platform],
-        lean_version = lean_version,
-        aeneas_rev = rev,
-    )
+        for platform in ALL_CHARON_PLATFORMS:
+            if platform == "linux_aarch64":
+                # Fail-fast stub repo — no hashes needed, no downloads performed.
+                charon_release(
+                    name = "charon_" + platform,
+                    version = charon_version,
+                    platform = platform,
+                    sha256 = "",
+                    rust_version = rust_version or "unused",
+                    rust_channel = rust_channel or "unused",
+                    rust_sha256 = {},
+                    require_hashes = False,
+                )
+                continue
+
+            charon_sha = charon_sha_overrides.get(
+                platform,
+                known_charon_sha.get(platform, ""),
+            )
+            if charon_require_hashes and not charon_sha:
+                fail(
+                    "SHA-256 missing for charon tarball on {}. ".format(platform) +
+                    "Provide charon_sha256 = {\"" + platform + "\": \"<hash>\"} " +
+                    "or set require_hashes = False.",
+                )
+
+            charon_release(
+                name = "charon_" + platform,
+                version = charon_version,
+                platform = platform,
+                sha256 = charon_sha,
+                rust_version = rust_version,
+                rust_channel = rust_channel,
+                rust_sha256 = merged_rust_sha,
+                require_hashes = charon_require_hashes,
+            )
+
+        charon_toolchains_hub(
+            name = "charon_toolchains",
+            platforms = ALL_CHARON_PLATFORMS,
+        )
 
 aeneas = module_extension(
     implementation = _aeneas_impl,
     tag_classes = {
         "toolchain": _AeneasToolchainTag,
+        "charon_toolchain": _CharonToolchainTag,
     },
 )
diff --git a/aeneas/private/charon_repo.bzl b/aeneas/private/charon_repo.bzl
new file mode 100644
index 0000000..4010466
--- /dev/null
+++ b/aeneas/private/charon_repo.bzl
@@ -0,0 +1,345 @@
+"""Repository rules for downloading Charon and its matching Rust sysroot.
+
+Charon is AeneasVerif's Rust→LLBC translator. It ships two binaries:
+
+* `charon`       — front-end CLI (statically linked OCaml on macOS).
+* `charon-driver` — a rustc driver that dynamically links `librustc_driver`
+                   from a matching nightly Rust sysroot.
+
+This rule downloads both the Charon tarball and a matching Rust toolchain
+(rustc + rust-std + rustc-dev) from `static.rust-lang.org`, bundles them into
+one repository, and exposes the pieces via `charon_toolchain_info`.
+
+### Linux aarch64 (known limitation)
+
+Upstream Charon does NOT publish a `linux-aarch64` tarball. Downloading the
+toolchain for that platform therefore fails with a clear error message. Users
+on `linux_aarch64` can either:
+
+  * compile Charon from source themselves and provide a local repository
+    override, or
+  * use `rules_lean`'s Nix track instead (`bazel_dep` on the charon overlay
+    provided by Track B), which builds from source via Nix.
+
+### Sysroot / env-var notes
+
+The Charon binary is built via Nix in CI and therefore looks for `rustc` in
+`PATH` (guarded by the `CHARON_TOOLCHAIN_IS_IN_PATH` env variable) instead of
+invoking `rustup`. Downstream `charon_llbc` build rules (not part of this file)
+should set:
+
+    CHARON_TOOLCHAIN_IS_IN_PATH=1
+    PATH=<rust_bin_path>:$PATH
+    DYLD_LIBRARY_PATH=<rust_lib_path>   # macOS (for librustc_driver-*.dylib)
+    LD_LIBRARY_PATH=<rust_lib_path>     # Linux (for librustc_driver-*.so)
+
+The `charon version` smoke test only touches the outer `charon` wrapper and
+does NOT need the sysroot — that test passes on a fresh download alone.
+"""
+
+# Platform identifiers used throughout rules_lean / aeneas.
+ALL_CHARON_PLATFORMS = [
+    "macos_aarch64",
+    "macos_x86_64",
+    "linux_x86_64",
+    "linux_aarch64",  # included for registry completeness; download fails fast
+]
+
+# Platforms that actually have a published Charon prebuilt.
+CHARON_SUPPORTED_PLATFORMS = [
+    "macos_aarch64",
+    "macos_x86_64",
+    "linux_x86_64",
+]
+
+_PLATFORM_CONSTRAINTS = {
+    "macos_aarch64": '"@platforms//os:macos", "@platforms//cpu:aarch64"',
+    "macos_x86_64": '"@platforms//os:macos", "@platforms//cpu:x86_64"',
+    "linux_x86_64": '"@platforms//os:linux", "@platforms//cpu:x86_64"',
+    "linux_aarch64": '"@platforms//os:linux", "@platforms//cpu:aarch64"',
+}
+
+# Charon tarball suffixes.
+_CHARON_ARTIFACT = {
+    "macos_aarch64": "macos-aarch64",
+    "macos_x86_64": "macos-x86_64",
+    "linux_x86_64": "linux-x86_64",
+}
+
+# Host triples for `static.rust-lang.org` nightly downloads.
+_RUST_TRIPLE = {
+    "macos_aarch64": "aarch64-apple-darwin",
+    "macos_x86_64": "x86_64-apple-darwin",
+    "linux_x86_64": "x86_64-unknown-linux-gnu",
+}
+
+# ── charon_release ───────────────────────────────────────────────────────────
+
+_CHARON_BUILD_FILE = """\
+load("@rules_lean//aeneas:toolchain.bzl", "charon_toolchain_info")
+
+package(default_visibility = ["//visibility:public"])
+
+filegroup(name = "charon_bin", srcs = ["charon"])
+filegroup(name = "charon_driver_bin", srcs = ["charon-driver"])
+
+filegroup(
+    name = "rust_sysroot_files",
+    srcs = glob(["rust_sysroot/**"]),
+)
+
+filegroup(
+    name = "all_files",
+    srcs = glob(["**"], exclude = [".scratch/**"]),
+)
+
+charon_toolchain_info(
+    name = "charon_toolchain_info",
+    charon = ":charon_bin",
+    charon_driver = ":charon_driver_bin",
+    all_files = ":all_files",
+    rust_sysroot = ":rust_sysroot_files",
+    rust_sysroot_path = "rust_sysroot",
+    rust_bin_path = "rust_sysroot/bin",
+    rust_lib_path = "rust_sysroot/lib",
+    rust_channel = "{channel}",
+    version = "{version}",
+)
+"""
+
+def _extract_rust_component(rctx, url, sha256, tmp_name, strip_components, target_dir):
+    """Download a Rust component tarball and extract it into target_dir.
+
+    The tarballs nest content under `<component>-<v>-<triple>/<component>/...`
+    (or an additional `lib/` layer for rust-std). `rctx.download_and_extract` +
+    a separate merge step has been observed to silently drop `.rlib` files on
+    some hosts (see rules_verus/verus/private/repo.bzl:186-196), so we download
+    to a temp file and untar manually with `--strip-components`.
+    """
+    rctx.download(url = url, output = tmp_name, sha256 = sha256)
+    extract = rctx.execute([
+        "tar",
+        "-xf",
+        tmp_name,
+        "-C",
+        target_dir,
+        "--strip-components={}".format(strip_components),
+    ])
+    if extract.return_code != 0:
+        fail("Failed to extract {}:\n{}".format(tmp_name, extract.stderr))
+    rctx.execute(["rm", tmp_name])
+
+def _charon_release_impl(rctx):
+    platform = rctx.attr.platform
+    version = rctx.attr.version
+    rust_version = rctx.attr.rust_version
+
+    if platform == "linux_aarch64":
+        # Keep the repository materialisable (so `bazel query` works) but
+        # refuse to produce usable binaries. Users will see this message when
+        # the repository is actually *built* rather than just enumerated.
+        rctx.file(
+            "charon",
+            "#!/bin/sh\n" +
+            "echo 'ERROR: Charon has no linux_aarch64 prebuilt (see docs/charon-integration.md).' >&2\n" +
+            "exit 1\n",
+            executable = True,
+        )
+        rctx.file("charon-driver", "", executable = True)
+        rctx.execute(["mkdir", "-p", "rust_sysroot/bin", "rust_sysroot/lib"])
+        rctx.file(
+            "BUILD.bazel",
+            _CHARON_BUILD_FILE.format(
+                channel = rctx.attr.rust_channel,
+                version = version,
+            ),
+        )
+        return
+
+    artifact = _CHARON_ARTIFACT.get(platform)
+    if not artifact:
+        fail("Unsupported platform for charon_release: {}".format(platform))
+
+    charon_sha = rctx.attr.sha256
+    charon_url = "https://github.com/AeneasVerif/charon/releases/download/{tag}/charon-{a}.tar.gz".format(
+        tag = version,
+        a = artifact,
+    )
+
+    # Step 1: download the Charon tarball (contains only `charon` and
+    # `charon-driver` at the top level).
+    rctx.download_and_extract(
+        url = charon_url,
+        sha256 = charon_sha if charon_sha else "",
+    )
+    rctx.execute(["chmod", "+x", "charon"])
+    rctx.execute(["chmod", "+x", "charon-driver"])
+    if "macos" in platform:
+        rctx.execute(["xattr", "-cr", "."], quiet = True)
+
+    # Step 2: download + assemble the Rust sysroot for this target.
+    triple = _RUST_TRIPLE[platform]
+    rust_hashes = rctx.attr.rust_sha256
+
+    def _require_hash(key):
+        val = rust_hashes.get(key, "")
+        if not val and rctx.attr.require_hashes:
+            fail(
+                "SHA-256 missing for Rust component '{}' on {}. ".format(key, platform) +
+                "Provide rust_sha256 = {\"" + key + "\": \"<hash>\"} or set " +
+                "require_hashes = False for local development.",
+            )
+        return val
+
+    # rustc component (contains rustc binary + librustc_driver + lib/rustlib).
+    # Top-level layout inside the tarball:
+    #   rustc-<v>-<triple>/rustc/{bin,lib,share}
+    # strip_components=2 drops both the outer dir and the "rustc" subdir so we
+    # end up with bin/, lib/, share/ directly under rust_sysroot/.
+    rctx.execute(["mkdir", "-p", "rust_sysroot"])
+    rustc_url = "https://static.rust-lang.org/dist/{date}/rustc-nightly-{t}.tar.xz".format(
+        date = rust_version,
+        t = triple,
+    )
+    _extract_rust_component(
+        rctx,
+        url = rustc_url,
+        sha256 = _require_hash("rustc_" + platform),
+        tmp_name = "rustc.tar.xz",
+        strip_components = 2,
+        target_dir = "rust_sysroot",
+    )
+
+    # rust-std component (libstd/libcore/liballoc etc. under
+    # lib/rustlib/<triple>/lib/*.rlib). Layout:
+    #   rust-std-<v>-<triple>/rust-std-<triple>/lib/...
+    # strip_components=2 lines it up alongside the rustc component.
+    rust_std_url = "https://static.rust-lang.org/dist/{date}/rust-std-nightly-{t}.tar.xz".format(
+        date = rust_version,
+        t = triple,
+    )
+    _extract_rust_component(
+        rctx,
+        url = rust_std_url,
+        sha256 = _require_hash("rust_std_" + platform),
+        tmp_name = "rust-std.tar.xz",
+        strip_components = 2,
+        target_dir = "rust_sysroot",
+    )
+
+    # rustc-dev component (charon-driver links against librustc_driver which
+    # lives here — NOT in the plain `rustc` component for this nightly).
+    # Layout: rustc-dev-<v>-<triple>/rustc-dev/lib/...
+    rustc_dev_url = "https://static.rust-lang.org/dist/{date}/rustc-dev-nightly-{t}.tar.xz".format(
+        date = rust_version,
+        t = triple,
+    )
+    _extract_rust_component(
+        rctx,
+        url = rustc_dev_url,
+        sha256 = _require_hash("rustc_dev_" + platform),
+        tmp_name = "rustc-dev.tar.xz",
+        strip_components = 2,
+        target_dir = "rust_sysroot",
+    )
+
+    # rust-src component is architecture-independent. Charon asks for it in
+    # its rust-toolchain manifest, so bundle it too.
+    rust_src_url = "https://static.rust-lang.org/dist/{date}/rust-src-nightly.tar.xz".format(
+        date = rust_version,
+    )
+    _extract_rust_component(
+        rctx,
+        url = rust_src_url,
+        sha256 = _require_hash("rust_src"),
+        tmp_name = "rust-src.tar.xz",
+        strip_components = 2,
+        target_dir = "rust_sysroot",
+    )
+
+    # Sanity-check the sysroot is usable.
+    verify_libcore = rctx.execute(["sh", "-c",
+        "ls rust_sysroot/lib/rustlib/{t}/lib/libcore-*.rlib 2>/dev/null | head -1".format(t = triple),
+    ])
+    if verify_libcore.return_code != 0 or not verify_libcore.stdout.strip():
+        debug = rctx.execute(["find", "rust_sysroot/lib/rustlib", "-maxdepth", "4", "-type", "d"])
+        fail("Rust sysroot for {} missing libcore. Contents:\n{}".format(triple, debug.stdout[:1000]))
+
+    # librustc_driver lives either in lib/ (Linux .so) or lib/ (macOS .dylib).
+    driver_glob = "librustc_driver-*.so" if "linux" in platform else "librustc_driver-*.dylib"
+    verify_driver = rctx.execute(["sh", "-c",
+        "ls rust_sysroot/lib/{} 2>/dev/null | head -1".format(driver_glob),
+    ])
+    if verify_driver.return_code != 0 or not verify_driver.stdout.strip():
+        debug = rctx.execute(["sh", "-c", "ls rust_sysroot/lib/ 2>&1 | head -40"])
+        fail(
+            "Rust sysroot for {} missing librustc_driver (charon-driver will not load).\n".format(triple) +
+            "rust_sysroot/lib contents:\n{}".format(debug.stdout),
+        )
+
+    rctx.file(
+        "BUILD.bazel",
+        _CHARON_BUILD_FILE.format(
+            channel = rctx.attr.rust_channel,
+            version = version,
+        ),
+    )
+
+charon_release = repository_rule(
+    implementation = _charon_release_impl,
+    doc = "Downloads a Charon release plus a matching nightly Rust sysroot.",
+    attrs = {
+        "version": attr.string(
+            mandatory = True,
+            doc = "Charon release tag, e.g. 'build-2026.04.22.081730-<sha>'.",
+        ),
+        "platform": attr.string(
+            mandatory = True,
+            values = ALL_CHARON_PLATFORMS,
+        ),
+        "sha256": attr.string(
+            default = "",
+            doc = "SHA-256 of the Charon tarball (empty only with require_hashes=False).",
+        ),
+        "rust_version": attr.string(
+            mandatory = True,
+            doc = "Nightly date component (e.g. '2026-02-07') used in static.rust-lang.org URLs.",
+        ),
+        "rust_channel": attr.string(
+            mandatory = True,
+            doc = "Full channel name (e.g. 'nightly-2026-02-07'), stored in the provider for downstream use.",
+        ),
+        "rust_sha256": attr.string_dict(
+            default = {},
+            doc = "SHA-256 hashes keyed by 'rustc_<plat>', 'rust_std_<plat>', 'rustc_dev_<plat>', 'rust_src'.",
+        ),
+        "require_hashes": attr.bool(
+            default = True,
+            doc = "Fail the repository rule if any needed hash is empty.",
+        ),
+    },
+)
+
+# ── charon_toolchains_hub ────────────────────────────────────────────────────
+
+def _charon_toolchains_hub_impl(rctx):
+    lines = ['package(default_visibility = ["//visibility:public"])', ""]
+    for p in rctx.attr.platforms:
+        lines.append(
+            """toolchain(
+    name = "{p}",
+    exec_compatible_with = [{c}],
+    toolchain = "@charon_{p}//:charon_toolchain_info",
+    toolchain_type = "@rules_lean//aeneas:charon_toolchain_type",
+)
+""".format(p = p, c = _PLATFORM_CONSTRAINTS[p]),
+        )
+    rctx.file("BUILD.bazel", "\n".join(lines))
+
+charon_toolchains_hub = repository_rule(
+    implementation = _charon_toolchains_hub_impl,
+    doc = "Hub repository that registers platform-specific Charon toolchains.",
+    attrs = {
+        "platforms": attr.string_list(mandatory = True),
+    },
+)
diff --git a/aeneas/toolchain.bzl b/aeneas/toolchain.bzl
index fc02477..2623c52 100644
--- a/aeneas/toolchain.bzl
+++ b/aeneas/toolchain.bzl
@@ -1,4 +1,4 @@
-"Aeneas toolchain provider and rule."
+"Aeneas and Charon toolchain providers and rules."
 
 AeneasToolchainInfo = provider(
     doc = "Information about an Aeneas installation.",
@@ -34,3 +34,52 @@ aeneas_toolchain_info = rule(
     },
     provides = [platform_common.ToolchainInfo],
 )
+
+# ── Charon toolchain ─────────────────────────────────────────────────────────
+
+CharonToolchainInfo = provider(
+    doc = "Information about a Charon installation (Rust → LLBC translator).",
+    fields = {
+        "charon": "The charon driver binary (File)",
+        "charon_driver": "The charon-driver rustc plugin (File)",
+        "all_files": "All Charon + sysroot files (list of Files)",
+        "rust_sysroot": "Bundled Rust sysroot files (list of Files)",
+        "rust_sysroot_path": "Repo-relative path to the Rust sysroot root (string)",
+        "rust_bin_path": "Repo-relative path to rust_sysroot/bin (containing rustc) (string)",
+        "rust_lib_path": "Repo-relative path to rust_sysroot/lib (for LD_LIBRARY_PATH/DYLD_LIBRARY_PATH) (string)",
+        "rust_channel": "The pinned Rust toolchain channel (e.g. 'nightly-2026-02-07')",
+        "version": "Charon release tag / version string",
+    },
+)
+
+def _charon_toolchain_info_impl(ctx):
+    toolchain_info = CharonToolchainInfo(
+        charon = ctx.file.charon,
+        charon_driver = ctx.file.charon_driver,
+        all_files = ctx.files.all_files,
+        rust_sysroot = ctx.files.rust_sysroot,
+        rust_sysroot_path = ctx.attr.rust_sysroot_path,
+        rust_bin_path = ctx.attr.rust_bin_path,
+        rust_lib_path = ctx.attr.rust_lib_path,
+        rust_channel = ctx.attr.rust_channel,
+        version = ctx.attr.version,
+    )
+    return [platform_common.ToolchainInfo(
+        charon_toolchain_info = toolchain_info,
+    )]
+
+charon_toolchain_info = rule(
+    implementation = _charon_toolchain_info_impl,
+    attrs = {
+        "charon": attr.label(allow_single_file = True, mandatory = True),
+        "charon_driver": attr.label(allow_single_file = True, mandatory = True),
+        "all_files": attr.label(mandatory = True),
+        "rust_sysroot": attr.label(mandatory = True),
+        "rust_sysroot_path": attr.string(default = "rust_sysroot"),
+        "rust_bin_path": attr.string(default = "rust_sysroot/bin"),
+        "rust_lib_path": attr.string(default = "rust_sysroot/lib"),
+        "rust_channel": attr.string(mandatory = True),
+        "version": attr.string(mandatory = True),
+    },
+    provides = [platform_common.ToolchainInfo],
+)
diff --git a/artifacts/architecture.yaml b/artifacts/architecture.yaml
index a5bb70a..95075fc 100644
--- a/artifacts/architecture.yaml
+++ b/artifacts/architecture.yaml
@@ -151,3 +151,43 @@ artifacts:
         target: REQ-006
       - type: satisfies
         target: REQ-008
+
+  - id: DD-007
+    type: design-decision
+    title: Charon toolchain via prebuilt downloads + Rust sysroot (pure Bazel)
+    status: accepted
+    description: >
+      Download Charon's prebuilt release binaries from GitHub plus the
+      matching Rust nightly sysroot (rustc, rust-std, rustc-dev, rust-src)
+      from static.rust-lang.org. All artifacts are SHA-256 pinned. Charon's
+      CHARON_TOOLCHAIN_IS_IN_PATH=1 env var is used to make it read the
+      sysroot from PATH instead of invoking rustup. linux_aarch64 has a
+      fail-fast stub (no upstream Charon prebuilt is published for that
+      platform).
+    fields:
+      rationale: >
+        Pure-Bazel keeps the hermeticity contract identical to Lean and
+        Mathlib toolchain handling: SHA-256 enforcement, no ambient host
+        tools, no out-of-band daemon. Reuses the rules_verus sysroot
+        pattern so the maintenance story is shared across the pulseengine
+        ruleset family.
+      alternatives: >
+        Alternative: Invoke `nix build github:AeneasVerif/charon?rev=<sha>`
+        from a repo rule and stage the closure. Evaluated head-to-head in
+        a parallel track (worktree removed after decision). Rejected for
+        three reasons: (1) adds a hard Nix-on-host requirement for every
+        developer and CI runner, violating the pure-Bazel hermeticity goal
+        stated for rules_lean; (2) the track's own validator build failed
+        on a Nix-equipped host because the smoke test MODULE.bazel omitted
+        required bazel_deps — a symptom of the agent being unable to
+        self-test without Nix on PATH, which is itself a point against
+        the approach; (3) Nix would have gained us linux_aarch64 support
+        (Charon has no prebuilt there) but Track A handles that with a
+        fail-fast stub that matches the Aeneas release's own platform
+        coverage. Kept on paper as a potential fallback if Charon stops
+        publishing prebuilts.
+    links:
+      - type: satisfies
+        target: REQ-001
+      - type: satisfies
+        target: REQ-003
diff --git a/artifacts/features.yaml b/artifacts/features.yaml
index 939e240..146ba92 100644
--- a/artifacts/features.yaml
+++ b/artifacts/features.yaml
@@ -93,12 +93,15 @@ artifacts:
   - id: FEAT-006
     type: feature
     title: Aeneas LLBC-to-Lean translation
-    status: draft
+    status: in_progress
     description: >
       Downloads pre-built Aeneas binaries from GitHub releases. Provides
       aeneas_translate rule for converting Charon LLBC files to Lean 4
       source files. Builds the Aeneas Lean support library from source.
-      Blocked on Lean version compatibility (Aeneas requires 4.28+).
+      Charon toolchain (Rust → LLBC) integrated via pure-Bazel prebuilt
+      downloads + matching Rust sysroot (see DD-007). Remaining work:
+      charon_llbc build rule wiring the sysroot env vars, then end-to-end
+      example on a cleanly-translatable crate.
     fields:
       phase: phase-2
     links:
diff --git a/docs/charon-integration.md b/docs/charon-integration.md
new file mode 100644
index 0000000..a555767
--- /dev/null
+++ b/docs/charon-integration.md
@@ -0,0 +1,94 @@
+# Charon integration (Track A — pure Bazel)
+
+[Charon](https://github.com/AeneasVerif/charon) is the Rust → LLBC translator
+used by the [Aeneas](https://github.com/AeneasVerif/aeneas) verification
+pipeline. `rules_lean` bundles Charon so downstream Rust-to-Lean proofs can be
+built entirely through Bazel, without rustup, Nix, or any host-provided
+Rust toolchain.
+
+## What gets downloaded
+
+For each `charon_toolchain` tag, the extension fetches:
+
+1. The Charon release tarball from
+   `github.com/AeneasVerif/charon/releases` — two binaries `charon` and
+   `charon-driver`.
+2. A matching nightly Rust sysroot from `static.rust-lang.org/dist` — the
+   `rustc`, `rust-std`, `rustc-dev`, and `rust-src` components for the host
+   triple. `rustc-dev` is mandatory because `charon-driver` links against
+   `librustc_driver`, which lives in that component rather than in `rustc`.
+
+Every download is SHA-256-pinned via the `_KNOWN_CHARON_VERSIONS` registry in
+`aeneas/extensions.bzl`; to add a new release, see the comment block at the top
+of that dict.
+
+## Enabling Charon in a module
+
+```starlark
+aeneas = use_extension("@rules_lean//aeneas:extensions.bzl", "aeneas")
+aeneas.charon_toolchain(
+    version = "build-2026.04.22.081730-2d35584fb79ef804c50f106d8c40bd3728284f8d",
+)
+use_repo(
+    aeneas,
+    "charon_toolchains",
+    "charon_macos_aarch64",
+    "charon_macos_x86_64",
+    "charon_linux_x86_64",
+    "charon_linux_aarch64",
+)
+register_toolchains("@charon_toolchains//:all")
+```
+
+## Platform support
+
+| Platform        | Status | Notes                                                        |
+|-----------------|:------:|--------------------------------------------------------------|
+| macOS aarch64   |  OK    | Requires ~180 MB of sysroot                                  |
+| macOS x86_64    |  OK    | Requires ~200 MB of sysroot                                  |
+| Linux x86_64    |  OK    | Requires GLIBC_2.39+ (Ubuntu 24.04+)                         |
+| Linux aarch64   | *not supported* | See below                                            |
+
+### Linux aarch64 (known limitation)
+
+Upstream Charon does not publish a `linux-aarch64` tarball. The
+`charon_linux_aarch64` repository is still materialised (so `bazel query`
+works on mixed-architecture monorepos), but its `charon` target is a stub
+script that exits non-zero with a pointer to this document.
+
+Workarounds:
+
+* Build Charon from source yourself and point at it via a
+  `local_repository` / `local_path_override`.
+* Use the Nix-based Track B integration (see `.claude/worktrees/agent-*` or
+  the parallel `rules_lean_nix` overlay), which compiles Charon through Nix
+  and therefore works anywhere Nix does.
+* Cross-compile from a Linux x86_64 CI host.
+
+### Runtime env vars for downstream rules
+
+`charon-driver` invokes `rustc` internally. The outer `charon` binary was
+built under Nix, so it reads `CHARON_TOOLCHAIN_IS_IN_PATH=1` and expects
+`rustc` to be discoverable via `PATH` rather than asking `rustup`. Rules that
+actually run Charon (e.g. a future `charon_llbc` build rule) therefore need
+to set:
+
+```
+CHARON_TOOLCHAIN_IS_IN_PATH=1
+PATH=<rust_bin_path>:$PATH
+DYLD_LIBRARY_PATH=<rust_lib_path>   # macOS — librustc_driver-*.dylib
+LD_LIBRARY_PATH=<rust_lib_path>     # Linux — librustc_driver-*.so
+```
+
+The `charon_toolchain_info` provider exposes `rust_bin_path`, `rust_lib_path`,
+and `rust_channel` for exactly this purpose. The `charon version` smoke test
+does not need any of this — the outer `charon` binary is self-contained.
+
+## Smoke test
+
+```
+bazel test //tests/charon_smoke:charon_version_smoke
+```
+
+Expected: `PASS: charon 0.1.181 smoke test`. The test scrubs `PATH` and
+`HOME`, so any attempt by Charon to call `rustup` would fail and be caught.
diff --git a/docs/getting-started.md b/docs/getting-started.md
index cef8bd2..3780dfb 100644
--- a/docs/getting-started.md
+++ b/docs/getting-started.md
@@ -20,7 +20,7 @@ Add to your `MODULE.bazel`:
 bazel_dep(name = "rules_lean", version = "0.1.0")
 
 lean = use_extension("@rules_lean//lean:extensions.bzl", "lean")
-lean.toolchain(version = "4.27.0")
+lean.toolchain(version = "4.29.1")
 
 use_repo(lean, "lean_toolchains")
 register_toolchains("@lean_toolchains//:all")
@@ -65,8 +65,8 @@ To use Mathlib lemmas and tactics, add to `MODULE.bazel`:
 
 ```starlark
 lean = use_extension("@rules_lean//lean:extensions.bzl", "lean")
-lean.toolchain(version = "4.27.0")
-lean.mathlib(rev = "v4.27.0")
+lean.toolchain(version = "4.29.1")
+lean.mathlib(rev = "v4.29.1")
 
 use_repo(lean, "lean_toolchains", "mathlib")
 register_toolchains("@lean_toolchains//:all")
@@ -103,12 +103,13 @@ lean_library(
 ## SHA-256 Verification
 
 By default, all toolchain downloads require SHA-256 verification.
-Known versions (currently 4.27.0) have hashes built in. For development
-with unreleased versions, opt out explicitly:
+Known versions (4.27.0, 4.29.1) have hashes built in. Older pins remain
+in the registry so downstream consumers can upgrade on their own cadence.
+For development with unreleased versions, opt out explicitly:
 
 ```starlark
 lean.toolchain(
-    version = "4.28.0-rc1",
+    version = "4.30.0-rc2",
     require_hashes = False,  # Development only!
 )
 ```
diff --git a/examples/hello_lean/MODULE.bazel b/examples/hello_lean/MODULE.bazel
index ee5833f..56985f6 100644
--- a/examples/hello_lean/MODULE.bazel
+++ b/examples/hello_lean/MODULE.bazel
@@ -10,7 +10,7 @@ local_path_override(
 )
 
 lean = use_extension("@rules_lean//lean:extensions.bzl", "lean")
-lean.toolchain(version = "4.27.0")
+lean.toolchain(version = "4.29.1")
 
 use_repo(lean, "lean_toolchains")
 register_toolchains("@lean_toolchains//:all")
diff --git a/examples/mathlib_proof/MODULE.bazel b/examples/mathlib_proof/MODULE.bazel
index 66d89a5..4422562 100644
--- a/examples/mathlib_proof/MODULE.bazel
+++ b/examples/mathlib_proof/MODULE.bazel
@@ -10,8 +10,8 @@ local_path_override(
 )
 
 lean = use_extension("@rules_lean//lean:extensions.bzl", "lean")
-lean.toolchain(version = "4.27.0")
-lean.mathlib(rev = "v4.27.0")
+lean.toolchain(version = "4.29.1")
+lean.mathlib(rev = "v4.29.1")
 
 use_repo(lean, "lean_toolchains", "mathlib")
 register_toolchains("@lean_toolchains//:all")
diff --git a/lean/extensions.bzl b/lean/extensions.bzl
index 9776b36..55927fb 100644
--- a/lean/extensions.bzl
+++ b/lean/extensions.bzl
@@ -11,6 +11,14 @@ _KNOWN_VERSIONS = {
             "linux_aarch64": "b256eec276baaaccc3eb3fa64d7ccff64f710b7caa074f305ba95e0013ad31e7",
         },
     },
+    "4.29.1": {
+        "sha256": {
+            "darwin_aarch64": "73bccb392ca7d8ab3d62a1e328bb7d057815f088dbdbfb6574f194ae505797af",
+            "darwin_x86_64": "3585ab34d20c53cf915169aa5c0d2efbd9993a78b9dc08516641510eef08fab0",
+            "linux_x86_64": "bf062d29556d655685fb287563c249ad6a8fde34352c18b5e32568a595c1aec1",
+            "linux_aarch64": "1ccdfb7f924901f4b73a4b4eb169e5b3dc74f6836521b47e733ea25f2abfc0dc",
+        },
+    },
 }
 
 def _detect_host_platform(module_ctx):
diff --git a/tests/charon_smoke/BUILD.bazel b/tests/charon_smoke/BUILD.bazel
new file mode 100644
index 0000000..1df3973
--- /dev/null
+++ b/tests/charon_smoke/BUILD.bazel
@@ -0,0 +1,89 @@
+load("@rules_shell//shell:sh_test.bzl", "sh_test")
+
+# Host-specific aliases so the sh_test can reference a single label. The
+# charon_<platform> repositories are all materialised (including the
+# linux_aarch64 stub which fails at runtime with a clear error); these
+# config_settings pick the binary matching the exec platform.
+
+config_setting(
+    name = "macos_aarch64",
+    constraint_values = [
+        "@platforms//os:macos",
+        "@platforms//cpu:aarch64",
+    ],
+)
+
+config_setting(
+    name = "macos_x86_64",
+    constraint_values = [
+        "@platforms//os:macos",
+        "@platforms//cpu:x86_64",
+    ],
+)
+
+config_setting(
+    name = "linux_x86_64",
+    constraint_values = [
+        "@platforms//os:linux",
+        "@platforms//cpu:x86_64",
+    ],
+)
+
+config_setting(
+    name = "linux_aarch64",
+    constraint_values = [
+        "@platforms//os:linux",
+        "@platforms//cpu:aarch64",
+    ],
+)
+
+alias(
+    name = "charon_bin",
+    actual = select({
+        ":macos_aarch64": "@charon_macos_aarch64//:charon_bin",
+        ":macos_x86_64": "@charon_macos_x86_64//:charon_bin",
+        ":linux_x86_64": "@charon_linux_x86_64//:charon_bin",
+        ":linux_aarch64": "@charon_linux_aarch64//:charon_bin",
+    }),
+)
+
+alias(
+    name = "charon_all_files",
+    actual = select({
+        ":macos_aarch64": "@charon_macos_aarch64//:all_files",
+        ":macos_x86_64": "@charon_macos_x86_64//:all_files",
+        ":linux_x86_64": "@charon_linux_x86_64//:all_files",
+        ":linux_aarch64": "@charon_linux_aarch64//:all_files",
+    }),
+)
+
+sh_test(
+    name = "charon_version_smoke",
+    srcs = ["charon_version_smoke.sh"],
+    data = [
+        ":charon_bin",
+        ":charon_all_files",
+    ],
+    args = ["$(rootpath :charon_bin)"],
+)
+
+# A build-time version check: asserts the downloaded `charon` binary prints
+# exactly "0.1.181". Useful for environments where `bazel test` is not
+# permitted; `bazel build //:charon_version_check` is sufficient.
+genrule(
+    name = "charon_version_check",
+    srcs = [":charon_all_files"],
+    outs = ["charon_version_check.stamp"],
+    tools = [":charon_bin"],
+    cmd = """
+set -euo pipefail
+OUT="$$($(execpath :charon_bin) version)"
+echo "charon version output: $$OUT"
+if [ "$$OUT" != "0.1.181" ]; then
+    echo "ERROR: expected 0.1.181, got '$$OUT'" >&2
+    exit 1
+fi
+echo "charon $$OUT OK" > $@
+""",
+    testonly = True,
+)
diff --git a/tests/charon_smoke/MODULE.bazel b/tests/charon_smoke/MODULE.bazel
new file mode 100644
index 0000000..2e8c7fb
--- /dev/null
+++ b/tests/charon_smoke/MODULE.bazel
@@ -0,0 +1,27 @@
+module(name = "test_charon_smoke", 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")
+
+aeneas = use_extension("@rules_lean//aeneas:extensions.bzl", "aeneas")
+aeneas.charon_toolchain(
+    version = "build-2026.04.22.081730-2d35584fb79ef804c50f106d8c40bd3728284f8d",
+)
+
+use_repo(
+    aeneas,
+    "charon_toolchains",
+    "charon_macos_aarch64",
+    "charon_macos_x86_64",
+    "charon_linux_x86_64",
+    "charon_linux_aarch64",
+)
+
+register_toolchains("@charon_toolchains//:all")
diff --git a/tests/charon_smoke/charon_version_smoke.sh b/tests/charon_smoke/charon_version_smoke.sh
new file mode 100755
index 0000000..10dc5b1
--- /dev/null
+++ b/tests/charon_smoke/charon_version_smoke.sh
@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+# Smoke test for the Charon toolchain downloaded by rules_lean.
+#
+# Requirements (per the AeneasVerif Charon Track A integration):
+#   * `charon version` must print the expected version.
+#   * No rustup invocation. No $HOME/.cargo reads. No network access.
+#
+# We pass the resolved rootpath of the charon binary as argv[1].
+
+set -euo pipefail
+
+if [[ $# -lt 1 ]]; then
+    echo "usage: $0 <path-to-charon>" >&2
+    exit 2
+fi
+
+CHARON="$1"
+
+if [[ ! -x "$CHARON" ]]; then
+    echo "ERROR: charon binary not found or not executable: $CHARON" >&2
+    exit 1
+fi
+
+# Sanity — deny rustup leakage by scrubbing PATH and HOME.
+# Keep /usr/bin + /bin so the kernel can run `sh` inside any child processes
+# charon might spawn internally, but nothing under $HOME and no homebrew paths.
+export PATH="/usr/bin:/bin"
+export HOME="$(mktemp -d)"
+unset RUSTUP_HOME CARGO_HOME RUSTUP_TOOLCHAIN CHARON_TOOLCHAIN_DIR || true
+trap 'rm -rf "$HOME"' EXIT
+
+EXPECTED="0.1.181"
+
+# Capture both stdout and stderr. `charon version` should print the version on
+# stdout and exit 0 without trying to invoke rustup.
+OUTPUT="$("$CHARON" version 2>&1)"
+RC=$?
+
+echo "--- charon version output ---"
+echo "$OUTPUT"
+echo "-----------------------------"
+
+if [[ $RC -ne 0 ]]; then
+    echo "FAIL: charon version exited $RC" >&2
+    exit 1
+fi
+
+if ! grep -qE "(^|[^0-9.])${EXPECTED//./\\.}([^0-9.]|$)" <<<"$OUTPUT"; then
+    echo "FAIL: expected version '$EXPECTED' in output" >&2
+    exit 1
+fi
+
+if grep -qi "rustup" <<<"$OUTPUT"; then
+    echo "FAIL: output mentions rustup (suggests rustup was invoked)" >&2
+    exit 1
+fi
+
+echo "PASS: charon $EXPECTED smoke test"
diff --git a/tests/charon_validator/README.md b/tests/charon_validator/README.md
new file mode 100644
index 0000000..cafd247
--- /dev/null
+++ b/tests/charon_validator/README.md
@@ -0,0 +1,43 @@
+# Charon toolchain validator
+
+Compares two Charon-integration strategies head-to-head.
+
+## Gates (all must pass)
+
+- **build** — `bazel build @charon_toolchain//:charon_bin` succeeds.
+- **smoke** — the built binary emits the expected version string (`0.1.181` by default).
+- **hermetic** — the build log contains ≤2 references to ambient host tools (`rustup`, `~/.cargo/`, `/nix/store/`, `/Users/*/`, `/home/*/`). Nix-based tracks will always show some `/nix/store/` refs; two is the budget before we call the track leaky.
+- **reproducible** — two cold builds (`bazel clean --expunge` between them) produce identical `charon` binary SHA-256.
+
+## Ranking (among tracks passing all gates)
+
+1. Cold build time (lower is better)
+2. Ambient-tool reference count (lower is better)
+3. External repo cache size (lower is better)
+
+## Usage
+
+```bash
+tests/charon_validator/run.sh <track-a-worktree> <track-b-worktree> [report.md]
+```
+
+Exit codes:
+
+| code | meaning |
+|---|---|
+| 0 | both tracks pass all gates (winner by rank) |
+| 1 | exactly one track passes all gates |
+| 2 | both tracks failed at least one gate |
+| 3 | usage error |
+
+## What it does *not* measure
+
+- **Cross-platform reach** — run on each CI platform separately and diff reports.
+- **Upgrade friction (LoC delta)** — manual code review.
+- **Security posture of transitive deps** — separate concern.
+
+## Overriding the expected version
+
+```bash
+CHARON_EXPECTED_VERSION=0.1.182 tests/charon_validator/run.sh ...
+```
diff --git a/tests/charon_validator/run.sh b/tests/charon_validator/run.sh
new file mode 100755
index 0000000..dc92e56
--- /dev/null
+++ b/tests/charon_validator/run.sh
@@ -0,0 +1,284 @@
+#!/usr/bin/env bash
+# Compare two Charon-integration tracks head-to-head.
+#
+# Gates (pass/fail):
+#   - build:        bazel build @charon_toolchain//:charon_bin succeeds
+#   - smoke:        `charon version` emits the expected string (0.1.181)
+#   - hermetic:     no ambient-tool references (rustup, ~/.cargo, /nix/store)
+#                   appear in the build log after initial download
+#   - reproducible: two cold builds produce identical charon binary hashes
+#
+# Ranked (among tracks passing all gates):
+#   - cold build time (wall-clock, seconds, lower=better)
+#   - external tool count (lower=better)
+#   - repo cache size (MB, lower=better)
+#
+# Usage:
+#   run.sh <track-a-worktree> <track-b-worktree> [report-path]
+#
+# Exit codes:
+#   0  both tracks pass all gates (report written)
+#   1  exactly one track passes all gates (winner named in report)
+#   2  both tracks fail at least one gate
+#   3  usage error
+
+set -uo pipefail
+
+TRACK_A_DIR="${1:-}"
+TRACK_B_DIR="${2:-}"
+REPORT_PATH="${3:-/tmp/charon-validator-report.md}"
+EXPECTED_VERSION="${CHARON_EXPECTED_VERSION:-0.1.181}"
+
+if [ -z "$TRACK_A_DIR" ] || [ -z "$TRACK_B_DIR" ]; then
+    echo "usage: $0 <track-a-worktree> <track-b-worktree> [report-path]" >&2
+    exit 3
+fi
+
+if [ ! -d "$TRACK_A_DIR" ] || [ ! -d "$TRACK_B_DIR" ]; then
+    echo "error: worktree path not found" >&2
+    exit 3
+fi
+
+WORKDIR=$(mktemp -d -t charon-validator.XXXXXX)
+trap 'rm -rf "$WORKDIR"' EXIT
+
+# --- helpers ---------------------------------------------------------------
+
+log()  { printf '[validator] %s\n' "$*" >&2; }
+die()  { printf '[validator] FATAL: %s\n' "$*" >&2; exit 1; }
+
+# Human-readable duration
+fmt_secs() {
+    local s=$1
+    if [ "$s" -lt 60 ]; then printf '%ds' "$s"
+    else printf '%dm%02ds' $((s/60)) $((s%60))
+    fi
+}
+
+# Count references to ambient host tools in a log file.
+# These indicate the build leaked out to the developer's machine.
+count_ambient() {
+    local log="$1"
+    # rustup invocations, $HOME/.cargo reads, /nix/store paths (expected for Nix
+    # track, but measured here so the table shows the delta honestly)
+    grep -cE '(rustup[[:space:]]|\.cargo/|/nix/store/|/Users/[^/]+/\.|/home/[^/]+/\.)' "$log" 2>/dev/null || echo 0
+}
+
+# Hash of the primary charon binary after a build.
+# Tracks may stage the binary under different external repo names; we search.
+hash_charon_bin() {
+    local repo_dir="$1"
+    cd "$repo_dir"
+    local bin
+    bin=$(find "$(bazel info execution_root 2>/dev/null)/external" \
+          -maxdepth 6 -name charon -type f -perm +111 2>/dev/null | head -1)
+    if [ -z "$bin" ] || [ ! -f "$bin" ]; then
+        echo "MISSING"
+        return
+    fi
+    shasum -a 256 "$bin" | awk '{print $1}'
+}
+
+# Measure repo cache size for the charon-related external repos.
+repo_cache_mb() {
+    local repo_dir="$1"
+    cd "$repo_dir"
+    local base
+    base=$(bazel info output_base 2>/dev/null)/external
+    if [ ! -d "$base" ]; then echo "?"; return; fi
+    # Match any external repo with "charon" in the name.
+    local total=0
+    while IFS= read -r d; do
+        local bytes
+        bytes=$(du -sk "$d" 2>/dev/null | awk '{print $1}')
+        total=$((total + bytes))
+    done < <(find "$base" -maxdepth 1 -type d -name '*charon*' 2>/dev/null)
+    echo $((total / 1024))
+}
+
+# --- per-track runner ------------------------------------------------------
+
+run_track() {
+    local name="$1"
+    local dir="$2"
+    local out="$WORKDIR/$name"
+    mkdir -p "$out"
+
+    log "=== track $name at $dir ==="
+    cd "$dir" || { echo "build=FAIL" > "$out/result.env"; return; }
+
+    # Gate 1: build
+    log "[$name] bazel clean --expunge"
+    bazel clean --expunge >/dev/null 2>&1 || true
+
+    log "[$name] cold build 1/2"
+    local t0 t1 build_status
+    t0=$(date +%s)
+    if bazel build @charon_toolchain//:charon_bin 2>&1 | tee "$out/build1.log" \
+        | grep -qE '^(ERROR|FAIL):'; then
+        build_status=FAIL
+    elif ! [ -f "$(bazel info execution_root 2>/dev/null)/bazel-out/../external/" ] && \
+         ! grep -q "Build completed successfully" "$out/build1.log"; then
+        # Fall through — we re-check via test below
+        build_status=UNKNOWN
+    else
+        build_status=PASS
+    fi
+    t1=$(date +%s)
+    local cold_secs=$((t1 - t0))
+
+    # Stronger pass check: did charon actually land?
+    local h1
+    h1=$(hash_charon_bin "$dir")
+    if [ "$h1" = "MISSING" ]; then
+        build_status=FAIL
+    else
+        build_status=PASS
+    fi
+
+    # Gate 2: smoke
+    local smoke_status=FAIL
+    if [ "$build_status" = PASS ]; then
+        log "[$name] smoke: charon version"
+        if bazel run --ui_event_filters=-info,-stdout,-stderr @charon_toolchain//:charon_bin \
+                -- version 2>"$out/smoke.err" >"$out/smoke.out"; then
+            if grep -q "$EXPECTED_VERSION" "$out/smoke.out"; then
+                smoke_status=PASS
+            fi
+        fi
+        # Fallback: try the tests/charon_smoke target if present.
+        if [ "$smoke_status" != PASS ] \
+           && bazel test //tests/charon_smoke/... 2>&1 | tee "$out/smoke_test.log" \
+              | grep -q 'PASSED'; then
+            smoke_status=PASS
+        fi
+    fi
+
+    # Gate 3: hermeticity probe
+    local ambient
+    ambient=$(count_ambient "$out/build1.log")
+
+    # Gate 4: reproducibility — second cold build
+    local h2 repro_status=FAIL
+    if [ "$build_status" = PASS ]; then
+        log "[$name] cold build 2/2 (reproducibility)"
+        bazel clean --expunge >/dev/null 2>&1
+        bazel build @charon_toolchain//:charon_bin 2>&1 > "$out/build2.log" || true
+        h2=$(hash_charon_bin "$dir")
+        if [ "$h1" = "$h2" ] && [ "$h1" != "MISSING" ]; then
+            repro_status=PASS
+        fi
+    fi
+
+    # Size
+    local repo_mb
+    repo_mb=$(repo_cache_mb "$dir")
+
+    # Record
+    cat > "$out/result.env" <<EOF
+build=$build_status
+smoke=$smoke_status
+hermetic=$( [ "$ambient" -le 2 ] && echo PASS || echo FAIL )
+reproducible=$repro_status
+cold_secs=$cold_secs
+ambient_refs=$ambient
+repo_mb=$repo_mb
+charon_hash=$h1
+charon_hash_2=${h2:-N/A}
+EOF
+    log "[$name] done:"
+    cat "$out/result.env" >&2
+}
+
+# --- main ------------------------------------------------------------------
+
+log "Track A: $TRACK_A_DIR"
+log "Track B: $TRACK_B_DIR"
+log "Report:  $REPORT_PATH"
+
+run_track A "$TRACK_A_DIR"
+run_track B "$TRACK_B_DIR"
+
+# Parse results
+# shellcheck disable=SC1090,SC1091
+A_build=;A_smoke=;A_hermetic=;A_reproducible=;A_cold_secs=;A_ambient_refs=;A_repo_mb=;A_charon_hash=;A_charon_hash_2=
+B_build=;B_smoke=;B_hermetic=;B_reproducible=;B_cold_secs=;B_ambient_refs=;B_repo_mb=;B_charon_hash=;B_charon_hash_2=
+while IFS='=' read -r k v; do eval "A_$k=\"$v\""; done < "$WORKDIR/A/result.env"
+while IFS='=' read -r k v; do eval "B_$k=\"$v\""; done < "$WORKDIR/B/result.env"
+
+gates_of() {
+    local prefix="$1"
+    # Returns count of passing gates (out of 4)
+    local n=0
+    eval "[ \"\$${prefix}_build\" = PASS ] && n=\$((n+1))"
+    eval "[ \"\$${prefix}_smoke\" = PASS ] && n=\$((n+1))"
+    eval "[ \"\$${prefix}_hermetic\" = PASS ] && n=\$((n+1))"
+    eval "[ \"\$${prefix}_reproducible\" = PASS ] && n=\$((n+1))"
+    echo $n
+}
+
+A_gates=$(gates_of A)
+B_gates=$(gates_of B)
+
+winner=
+if [ "$A_gates" = 4 ] && [ "$B_gates" = 4 ]; then
+    # Both pass — rank by cold_secs, tiebreak by ambient_refs then repo_mb
+    if [ "$A_cold_secs" -lt "$B_cold_secs" ]; then winner=A
+    elif [ "$B_cold_secs" -lt "$A_cold_secs" ]; then winner=B
+    elif [ "$A_ambient_refs" -lt "$B_ambient_refs" ]; then winner=A
+    elif [ "$B_ambient_refs" -lt "$A_ambient_refs" ]; then winner=B
+    elif [ "$A_repo_mb" -lt "$B_repo_mb" ]; then winner=A
+    else winner=B
+    fi
+    exit_code=0
+elif [ "$A_gates" = 4 ]; then
+    winner=A; exit_code=1
+elif [ "$B_gates" = 4 ]; then
+    winner=B; exit_code=1
+else
+    winner="(neither — both failed at least one gate)"; exit_code=2
+fi
+
+# Write report
+{
+    printf '# Charon toolchain comparison — Track A (pure Bazel) vs Track B (Nix)\n\n'
+    printf '_Generated: %s_\n\n' "$(date -u +%Y-%m-%dT%H:%M:%SZ)"
+    printf 'Host: %s  \n' "$(uname -sm)"
+    printf 'Expected version: `%s`\n\n' "$EXPECTED_VERSION"
+    printf '## Gates\n\n'
+    printf '| Gate | Track A | Track B |\n'
+    printf '|---|---|---|\n'
+    printf '| build | %s | %s |\n'       "$A_build" "$B_build"
+    printf '| smoke (version match) | %s | %s |\n' "$A_smoke" "$B_smoke"
+    printf '| hermetic (ambient ≤ 2) | %s | %s |\n' "$A_hermetic" "$B_hermetic"
+    printf '| reproducible (hash match) | %s | %s |\n' "$A_reproducible" "$B_reproducible"
+    printf '\n'
+    printf '## Measurements\n\n'
+    printf '| Metric | Track A | Track B |\n'
+    printf '|---|---|---|\n'
+    printf '| cold build time | %s | %s |\n' "$(fmt_secs "${A_cold_secs:-0}")" "$(fmt_secs "${B_cold_secs:-0}")"
+    printf '| ambient-tool refs in build log | %s | %s |\n' "$A_ambient_refs" "$B_ambient_refs"
+    printf '| external repo cache size | %s MB | %s MB |\n' "$A_repo_mb" "$B_repo_mb"
+    printf '| charon binary sha256 (build 1) | `%s` | `%s` |\n' "${A_charon_hash:0:16}…" "${B_charon_hash:0:16}…"
+    printf '| charon binary sha256 (build 2) | `%s` | `%s` |\n' "${A_charon_hash_2:0:16}…" "${B_charon_hash_2:0:16}…"
+    printf '\n'
+    printf '## Verdict\n\n'
+    printf 'Winner: **%s**\n\n' "$winner"
+    if [ "$exit_code" = 0 ]; then
+        printf 'Both tracks pass all 4 gates. Ranked by cold build time, ambient-tool refs, then cache size.\n'
+    elif [ "$exit_code" = 1 ]; then
+        printf 'Exactly one track passes all gates.\n'
+    else
+        printf 'Both tracks failed at least one gate. See per-track build logs under %s.\n' "$WORKDIR"
+    fi
+    printf '\n## Raw logs\n\n'
+    printf '- Track A build: `%s/A/build1.log`\n' "$WORKDIR"
+    printf '- Track A smoke: `%s/A/smoke.out`\n' "$WORKDIR"
+    printf '- Track B build: `%s/B/build1.log`\n' "$WORKDIR"
+    printf '- Track B smoke: `%s/B/smoke.out`\n' "$WORKDIR"
+} > "$REPORT_PATH"
+
+log "report written to $REPORT_PATH"
+log "winner: $winner  (exit=$exit_code)"
+cat "$REPORT_PATH"
+exit "$exit_code"
diff --git a/tests/platform_hashes/MODULE.bazel b/tests/platform_hashes/MODULE.bazel
index d412840..d9d68c7 100644
--- a/tests/platform_hashes/MODULE.bazel
+++ b/tests/platform_hashes/MODULE.bazel
@@ -7,7 +7,7 @@ local_path_override(
 )
 
 lean = use_extension("@rules_lean//lean:extensions.bzl", "lean")
-lean.toolchain(version = "4.27.0")
+lean.toolchain(version = "4.29.1")
 
 use_repo(
     lean,