diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml
index 3f3f321..27e0ef6 100644
--- a/.github/workflows/dogfood-gate.yml
+++ b/.github/workflows/dogfood-gate.yml
@@ -71,7 +71,7 @@ jobs:
       - name: Check for K9 files
         id: detect
         run: |
-          COUNT=$(find . \( -name '*.k9' -o -name '*.k9.ncl' \) -not -path './.git/*' | wc -l)
+          COUNT=$(find . \( -name '*.k9' -o -name '*.k9.ncl' \) -not -path './.git/*' -type f | wc -l)
           CONFIG_COUNT=$(find . \( -name '*.toml' -o -name '*.yaml' -o -name '*.yml' -o -name '*.json' \) \
             -not -path './.git/*' -not -path './node_modules/*' -not -path './.deno/*' \
             -not -name 'package-lock.json' -not -name 'Cargo.lock' -not -name 'deno.lock' | wc -l)
@@ -82,11 +82,15 @@ jobs:
           fi
 
       - name: Validate K9 contracts
+        id: validate
         if: steps.detect.outputs.k9_count > 0
         run: bash .github/hooks/validate-k9.sh
       - name: Write summary
         run: |
           K9_COUNT="${{ steps.detect.outputs.k9_count }}"
+          # The hook skips the YAML session bindings, so report the files it
+          # actually validated, not every *.k9 path found.
+          VALIDATED="${{ steps.validate.outputs.files_scanned }}"
           CFG_COUNT="${{ steps.detect.outputs.config_count }}"
           if [ "$K9_COUNT" -eq 0 ]; then
             cat <<'EOF' >> "$GITHUB_STEP_SUMMARY"
@@ -99,7 +103,7 @@ jobs:
           else
             echo "## K9 Contract Validation" >> "$GITHUB_STEP_SUMMARY"
             echo "" >> "$GITHUB_STEP_SUMMARY"
-            echo "Validated **${K9_COUNT}** K9 contract(s) against **${CFG_COUNT}** config file(s)." >> "$GITHUB_STEP_SUMMARY"
+            echo "Validated **${VALIDATED:-0}** of **${K9_COUNT}** K9 file(s) found. Counted **${CFG_COUNT}** config file(s), which K9 validation does not read." >> "$GITHUB_STEP_SUMMARY"
           fi
 
   # ---------------------------------------------------------------------------
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index ef5f17a..df3954f 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -34,6 +34,31 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
   `measured` block), `probe-reachability.sh` and `hosts.txt` (experiment
   X1: reachability probe, HEAD by default, one-byte GET with `--get`).
 
+==== Fixed
+
+Findings from the last review of #98, which merged before they were
+addressed:
+
+* `build/setup.sh` — the Cargo fallback installs `just` into a named root
+  and puts that root's `bin` on `PATH`, so a distro Cargo without
+  `~/.cargo/bin` on `PATH` no longer fails setup after a successful install.
+* `tools/environments/probe-reachability.sh` — `--get` caps a body the
+  server sends despite the byte range (`range-ignored`); a non-GNU `ldd`
+  (FreeBSD) no longer stops the probe. `tests/probe_reachability_test.sh`
+  covers both.
+* `tools/proof-toolchain/toolchain.kyaml` — HOL Light's OCaml switch is a
+  locked runtime entry; Poly/ML takes the newest stable tag, since HOL4
+  names no version; Mizar names the i386 distribution it actually ships
+  (static binaries, needing IA32 emulation on the host).
+* `tools/environments/` and the environment proposal — the measurement adds
+  Cargo's real index and download hosts, which answer, so `cargo install`
+  is no longer reported as blocked by the refused crates.io API.
+* Proposals — PVS has a priority-1 owner (`awesome-hol`); X1 covers every
+  probeable environment class; `DRIFT` fields and the checker's lock hash
+  are named in the cartridge contracts.
+* `Justfile` `container-init` renders the `VERSION` placeholder; the dogfood gate's
+  summary counts the K9 files the hook validated, not every `*.k9` path.
+
 ==== Changed
 
 * `build/setup.sh` — when no system package provides `just`, setup runs
diff --git a/Justfile b/Justfile
index 93a23bf..17dea27 100644
--- a/Justfile
+++ b/Justfile
@@ -385,10 +385,20 @@ container-init:
     read -rp "Container registry [ghcr.io/${OWNER:-hyperpolymath}]: " _REGISTRY
     REGISTRY="${_REGISTRY:-ghcr.io/${OWNER:-hyperpolymath}}"
 
+    read -rp "Service version (the K9 pedigree version) [0.1.0]: " _VERSION
+    VERSION="${_VERSION:-0.1.0}"
+    # The value lands inside quoted TOML and Nickel strings and a sed
+    # replacement, so allow only characters that are safe in all three.
+    if [[ ! "$VERSION" =~ ^[0-9A-Za-z._+-]+$ ]]; then
+        echo "Error: invalid version '$VERSION'. Use letters, digits, '.', '_', '+' or '-'." >&2
+        exit 1
+    fi
+
     echo ""
     echo "  Service: $SERVICE_NAME"
     echo "  Port:    $PORT"
     echo "  Registry: $REGISTRY"
+    echo "  Version: $VERSION"
     echo ""
     read -rp "Proceed? [Y/n] " CONFIRM
     [[ "${CONFIRM:-Y}" =~ ^[Nn] ]] && echo "Aborted." && exit 0
@@ -404,6 +414,7 @@ container-init:
         -e "s|${LB}SERVICE_NAME${RB}|${SERVICE_NAME}|g"
         -e "s|${LB}PORT${RB}|${PORT}|g"
         -e "s|${LB}REGISTRY${RB}|${REGISTRY}|g"
+        -e "s|${LB}VERSION${RB}|${VERSION}|g"
     )
 
     find container/ -type f | while read -r file; do
diff --git a/build/setup.sh b/build/setup.sh
index ab40d83..e5197af 100755
--- a/build/setup.sh
+++ b/build/setup.sh
@@ -132,12 +132,28 @@ detect_platform() {
 # Cargo checks registry package checksums; --locked uses the release lockfile.
 # 1.56.0 matches the estate mise.lock pin and meets the estate floor (just >= 1.42,
 # standards 3-practice/provisioning/PROVISIONING-STANDARD.adoc).
+# The install root is CARGO_INSTALL_ROOT, then CARGO_HOME, then $HOME/.cargo
+# (using the first non-empty value). After a successful install, its bin
+# directory is added to PATH for this process if absent. Returns 1 if Cargo
+# is unavailable or installation fails.
 install_just_with_cargo() {
     if ! command -v cargo >/dev/null 2>&1; then
         fail "Install Cargo or just with your platform's package manager, then rerun setup."
         return 1
     fi
-    cargo install just --version 1.56.0 --locked
+    # Name the install root explicitly, so its bin directory is known: Cargo
+    # installs there but does not add it to this shell's PATH, and a distro
+    # Cargo often runs without ~/.cargo/bin on PATH.
+    cargo_root="${CARGO_INSTALL_ROOT:-${CARGO_HOME:-$HOME/.cargo}}"
+    cargo install just --version 1.56.0 --locked --root "$cargo_root" || return 1
+    case ":$PATH:" in
+        *":$cargo_root/bin:"*) ;;
+        *)
+            PATH="$cargo_root/bin:$PATH"
+            export PATH
+            warn "Added $cargo_root/bin to PATH for this run; add it to your shell profile too."
+            ;;
+    esac
 }
 
 install_just() {
diff --git a/docs/proposals/awesome-estate-maths-proving.adoc b/docs/proposals/awesome-estate-maths-proving.adoc
index b9068a6..66fbbfb 100644
--- a/docs/proposals/awesome-estate-maths-proving.adoc
+++ b/docs/proposals/awesome-estate-maths-proving.adoc
@@ -149,7 +149,8 @@ Isabelle/jEdit and VSCode, Isabelle Zulip, IsaFoL.
 
 |`awesome-hol`
 |HOL4, HOL Light, HOL Zero, ProofPower, Candle, CakeML, OpenTheory, the
-HOL lineage; HOL Light's Flyspeck.
+HOL lineage; HOL Light's Flyspeck. A section on classical higher-order
+logic outside that lineage owns PVS and NASALib.
 |None (`awesome-provable` says "HOL" once).
 |Create
 |1
@@ -249,7 +250,8 @@ echidna's 12 core backends and every PROOF-POLICY route.
 === Where the small families go
 
 Mizar, Metamath, Naproche and Matita fold into
-`awesome-formalised-mathematics`; PVS and the leaner interactive provers
+`awesome-formalised-mathematics`; PVS is owned by `awesome-hol`, so a
+priority-1 list carries every core backend; the leaner interactive provers
 fold into the refreshed `awesome-provable` index; TLA+ is a section of
 `awesome-model-checking`; the hybrid-systems and real-algebra provers
 (KeYmaera X, dReal, QEPCAD, Redlog) appear in `awesome-mathematical-logic`
diff --git a/docs/proposals/boj-prover-solver-cartridges.adoc b/docs/proposals/boj-prover-solver-cartridges.adoc
index 072d8f9..daaf53f 100644
--- a/docs/proposals/boj-prover-solver-cartridges.adoc
+++ b/docs/proposals/boj-prover-solver-cartridges.adoc
@@ -99,7 +99,11 @@ hard-coded count.
 |`provers_check`
 |One prover: `PRESENT` with version and lock hash; `DRIFT` with observed
 version/hash, expected lock version/hash and the mismatch (not
-dispatchable); or `UNAVAILABLE` with the reason it could not run.
+dispatchable); or `UNAVAILABLE` with the reason it could not run. All of it
+comes from `provers.sh doctor --json`, which compares what it ran against
+`toolchain.lock.json`; `provers_check` adds nothing of its own. A `DRIFT`
+result carries `observed_version`, `observed_sha256`, `locked_version` and
+`locked_sha256`, and `mismatch` names which of the two differs.
 
 |`provers_prove`
 |`{file \| goal, prover?, timeout}` → `{verdict, trust_level, prover,
@@ -136,7 +140,9 @@ silently the latter.
 Every `solvers_sat` and `solvers_optimise` response carries `status:
 TESTED or PROVEN`, solver id, version and lock hash. `TESTED` carries the
 bounds and limits used. `PROVEN` requires a certificate reference and
-hash, the input hash, the independent checker's id and version, its
+hash, the input hash, the independent checker's id, version and
+`locked_sha256` (the lock's digest of its installed executable, so the
+exact checker binary is pinned), its
 successful check result, and any axioms used. An emitted certificate or
 unsat core alone does not establish `PROVEN`.
 
diff --git a/docs/proposals/environment-of-environments.adoc b/docs/proposals/environment-of-environments.adoc
index 11c48d6..cdcc969 100644
--- a/docs/proposals/environment-of-environments.adoc
+++ b/docs/proposals/environment-of-environments.adoc
@@ -15,8 +15,8 @@ are specified against the deed; the conversion of this repository's own
 files follows ruling D313.
 
 Status: proposal, 2026-10-27. Nothing here is built. The measured facts in
-<<measured>> were taken in one cloud agent session on that date and are
-reproducible with `tools/environments/probe-reachability.sh`.
+<<measured>> were taken in cloud agent sessions on 2026-10-27 and
+2026-11-04 and are reproducible with `tools/environments/probe-reachability.sh`.
 
 == The claim
 
@@ -43,7 +43,7 @@ report its real capabilities in one machine-readable form.
 |Surface |What it declares |Gap
 
 |`tools/proof-toolchain/toolchain.kyaml`
-|36 tools with roles under PROOF-POLICY, pins and smoke commands
+|37 tools with roles under PROOF-POLICY, pins and smoke commands
 |Declares tools, not environments. Covers the policy provers and their
 backends. Before E6 it covered 7 of echidna's 12 core backends; it now
 covers all 12 (see <<coverage>>).
@@ -77,15 +77,17 @@ so, not pass silently.
 |===
 
 [[measured]]
-== Measured facts from one agent session
-
-Taken 2026-10-27 in a Claude Code cloud session for this repository
-(Ubuntu 24.04.5, glibc 2.39, x86_64, outbound HTTPS through the session's
-agent proxy). The probe ran twice over the 22 URLs in
-`tools/environments/hosts.txt`: once with redirected HEAD requests, once
-with `--get`, a redirected GET for the first byte only. The code is the
-final response the proxy returned. Where the two methods differ, both are
-shown; elsewhere they agreed (200 to HEAD, 200 or 206 to GET).
+== Measured facts from agent sessions
+
+First taken 2026-10-27 and re-taken 2026-11-04 in Claude Code cloud
+sessions for this repository (Ubuntu 24.04.5, glibc 2.39, x86_64, outbound
+HTTPS through the session's agent proxy). The table is the 2026-11-04 run.
+The probe ran twice over the 24 URLs in `tools/environments/hosts.txt`:
+once with redirected HEAD requests, once with `--get`, a redirected GET for
+the first byte only, capped at 64 KiB for servers that ignore the range
+(`range-ignored`). The code is the final response the proxy returned.
+Where the two methods differ, both are shown; elsewhere they agreed (200
+to HEAD, 200 or 206 to GET).
 
 [cols="3,1,3",options="header"]
 |===
@@ -96,14 +98,16 @@ shown; elsewhere they agreed (200 to HEAD, 200 or 206 to GET).
 |`hackage.haskell.org` |200 |Reachable (Agda via cabal is possible in principle).
 |`static.rust-lang.org` (rustup-init) |200 |Reachable.
 |`releases.lean-lang.org` |200 |Reachable (elan toolchains).
-|`isabelle.in.tum.de`, `mizar.uwb.edu.pl`, `pvs.csl.sri.com` |200 |Reachable.
+|`mizar.uwb.edu.pl`, `pvs.csl.sri.com` |200 |Reachable.
+|`isabelle.in.tum.de` |200 (HEAD); 206 or reset (GET) |*Intermittent.* One GET of four succeeded; the others were reset during the TLS handshake. An install from it needs retries.
 |`ftp.gnu.org/gnu/guix` |200 |Reachable.
-|`smt-lib.org`, `www.tptp.org` |200 |Reachable.
+|`smt-lib.org`, `www.tptp.org` |200 |Reachable (TPTP ignores the byte range).
 |`github.com/Z3Prover/z3/releases/download/…/z3-4.13.4-x64-glibc-2.35.zip` |302 then 200 (HEAD), 206 (GET, one byte) |*Reachable.* The request redirects to `release-assets.githubusercontent.com` and succeeds, and the first byte of the asset arrives. A full download was not attempted and no executable was run, so bundle transport is only partly verified.
-|`codeload.github.com`, `raw.githubusercontent.com` |200 |Reachable (source archives and raw files).
+|`codeload.github.com`, `raw.githubusercontent.com` |200 |Reachable (source archives and raw files; codeload ignores the byte range).
 |`github.com/Z3Prover/z3/releases/latest` |403 (HEAD and GET) |*Refused by the proxy.* The release landing page is not available, so "latest" cannot be discovered by scraping.
 |`api.github.com/repos/cvc5/cvc5/releases/latest` |403 (HEAD and GET) |Refused. Release discovery through the API is not available either.
-|`crates.io/api/v1/crates/just` |403 (HEAD and GET) |Refused. The API path cargo resolves through answers 403 to GET as well, so a cargo install from the registry is expected to fail here; one was not attempted.
+|`crates.io/api/v1/crates/just` |403 (HEAD and GET) |Refused. Cargo does not install through this API, so the refusal does not block `cargo install`.
+|`index.crates.io/ju/st/just`, `static.crates.io/crates/just/1.56.0/download` |200 (HEAD); 206 and 200 (GET) |*Reachable.* These are the sparse index and the download route `cargo install` requests (the index's `dl` plus `/{crate}/{version}/download`), so a Cargo install is expected to work here. One was not attempted. The download host ignores the byte range.
 |`ghcr.io/v2/`, `cgr.dev/v2/` |405 (HEAD), 401 (GET) |Registry answered; anonymous token flow not tested. The one case where the methods differ.
 |`cvc5.github.io` |200 |Reachable.
 |`downloads.sourceforge.net` (SBCL x86-64 Linux binary) |200 (HEAD), 206 (GET, one byte) |Reachable: the source the `sbcl` entry fetches.
@@ -215,10 +219,10 @@ sealed-container concern, per the 2026-05-18 packaging ruling.
 |Z3 |`z3` |Covered
 |CVC5 |`cvc5` |Covered
 |Metamath |none needed |Pure-Rust, in-process in echidna
-|HOL Light |`hol-light` |Covered (added 2026-10-27 on the owner's decision; opam)
+|HOL Light |`hol-light` with `hol-light-ocaml` |Covered (added 2026-10-27 on the owner's decision; opam, in a locked OCaml switch)
 |HOL4 |`hol4` with `polyml` |Covered (added 2026-10-27; source build on bundled Poly/ML)
 |ACL2 |`acl2` with `sbcl` |Covered (added 2026-10-27; tagged source from GitHub, built on bundled SBCL)
-|Mizar |`mizar` |Covered (added 2026-10-27; system distribution with its MML)
+|Mizar |`mizar` |Covered (added 2026-10-27; the static i386 distribution with its MML, so the host kernel needs IA32 emulation)
 |PVS |`pvs` with `sbcl` |Covered (added 2026-10-27; BSD-3-Clause source build on bundled SBCL)
 |===
 
@@ -282,9 +286,14 @@ impression.
 |Id |Experiment |Pass criterion
 
 |X1
-|Run `tools/environments/probe-reachability.sh` in each environment class:
-workstation, this session class, a GitHub-hosted runner, the devcontainer.
-|A reachability row per class in `environments.kyaml` `measured`, dated.
+|Run `tools/environments/probe-reachability.sh`, with and without `--get`,
+in each environment class that runs a shell: workstation, this session
+class, a GitHub-hosted runner, the devcontainer, a Guix shell and the
+sealed container (whose `--network=none` run must record every host
+unreachable). `boj-registered` is excluded: it is a server's view of the
+others, not a place a probe runs.
+|A dated `measured` block for each of the six probeable classes in
+`environments.kyaml`; `boj-registered` keeps an empty one.
 The design's host assumptions are replaced by measurements.
 
 |X2
diff --git a/tests/probe_reachability_test.sh b/tests/probe_reachability_test.sh
new file mode 100644
index 0000000..b085369
--- /dev/null
+++ b/tests/probe_reachability_test.sh
@@ -0,0 +1,70 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Test tools/environments/probe-reachability.sh with stub curl and ldd
+# executables, so no network is used. The stub curl reproduces what curl 8.5
+# was measured to do (2026-11-04) against servers that ignore a byte range:
+# with --max-filesize it stops and exits 63, still reporting the status code.
+# Checks: a non-GNU ldd does not stop the probe; --get passes the size cap
+# and reports a capped transfer as range-ignored; outcomes are classified;
+# --json is valid; an unknown argument exits 2. Needs jq.
+set -euo pipefail
+
+repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+probe="$repo_root/tools/environments/probe-reachability.sh"
+work="$(mktemp -d)"
+trap 'rm -rf "$work"' EXIT
+fail() { echo "FAIL: $*" >&2; exit 1; }
+
+mkdir -p "$work/bin"
+cat > "$work/hosts.txt" <<'EOF'
+# comment line
+https://range-ignoring.test/big.bin
+https://honours-range.test/file
+https://refusing.test/api
+https://bad-cert.test/
+EOF
+
+# Stub curl: the URL is the last argument; -w '%{http_code}' output goes to
+# stdout, as with the real curl.
+cat > "$work/bin/curl" <<'SH'
+#!/bin/sh
+args="$*"
+for url in "$@"; do :; done
+case "$args" in *" -r 0-0 "*) mode=get ;; *" -I "*) mode=head ;; *) echo "stub curl: no method in: $args" >&2; exit 97 ;; esac
+if [ "$mode" = get ]; then
+    case "$args" in *"--max-filesize 65536"*) ;; *) echo "stub curl: GET without size cap" >&2; exit 97 ;; esac
+fi
+case "$url" in
+    https://range-ignoring.test/*) printf 200; [ "$mode" = get ] && exit 63; exit 0 ;;
+    https://honours-range.test/*)  [ "$mode" = get ] && printf 206 || printf 200; exit 0 ;;
+    https://refusing.test/*)       printf 403; exit 0 ;;
+    https://bad-cert.test/*)       printf 000; exit 60 ;;
+esac
+printf 000; exit 6
+SH
+# A FreeBSD-style ldd: exists, rejects --version.
+printf '#!/bin/sh\necho "ldd: illegal option -- -" >&2\nexit 1\n' > "$work/bin/ldd"
+chmod +x "$work/bin/curl" "$work/bin/ldd"
+
+run() { PATH="$work/bin:$PATH" HOSTS_FILE="$work/hosts.txt" bash "$probe" "$@"; }
+row() { grep -Eq "^$1 +$2 +$3\$" <<<"$4" || fail "expected '$1 $2 $3' in: $4"; }
+
+head_out="$(run)" || fail "HEAD probe exited non-zero with a non-GNU ldd"
+grep -q 'glibc' <<<"$head_out" && fail "non-GNU ldd reported as glibc"
+row 200 reachable 'https://range-ignoring\.test/big\.bin' "$head_out"
+row 403 refused 'https://refusing\.test/api' "$head_out"
+row 000 tls-failed 'https://bad-cert\.test/' "$head_out"
+
+get_out="$(run --get)" || fail "GET probe exited non-zero"
+row 200 range-ignored 'https://range-ignoring\.test/big\.bin' "$get_out"
+row 206 reachable 'https://honours-range\.test/file' "$get_out"
+
+json="$(run --json --get)" || fail "JSON probe exited non-zero"
+jq -e '.method == "get" and (.hosts | length) == 4 and
+       ([.hosts[].outcome] | sort) == ["range-ignored","reachable","refused","tls-failed"]' \
+    <<<"$json" >/dev/null || fail "JSON output wrong: $json"
+
+rc=0; run --bogus >/dev/null 2>&1 || rc=$?
+[ "$rc" -eq 2 ] || fail "unknown argument exited $rc, expected 2"
+
+echo 'PASS: probe tolerates non-GNU ldd, caps range-ignoring GETs, classifies outcomes'
diff --git a/tests/proof_smoke_wrappers_test.sh b/tests/proof_smoke_wrappers_test.sh
index 497e300..8e89bba 100755
--- a/tests/proof_smoke_wrappers_test.sh
+++ b/tests/proof_smoke_wrappers_test.sh
@@ -17,7 +17,11 @@ for fixture in hol-light-refl.sh hol4-smoke.sml acl2-smoke.lisp smoke.miz \
     mizar-smoke.sh pvs-smoke.sh pvs_smoke.pvs; do
     [ -f "$prefix/share/smoke/$fixture" ] || { echo "FAIL: $fixture not installed" >&2; exit 1; }
 done
-chmod -R a-w "$prefix/share/smoke"  # a wrapper that writes here now fails
+# Record the whole prefix (smoke fixtures and the MML at share/mizar alike), so
+# a write anywhere under it is caught even when running as root, where
+# read-only permissions do not stop writes.
+snapshot() { (cd "$prefix" && find . -print0 | sort -z | xargs -0 stat -c '%n %s %y' 2>/dev/null); }
+before="$(snapshot)"
 
 expect() {  # expect pass|fail <description> <command...>
     local want="$1" what="$2"; shift 2
@@ -73,7 +77,5 @@ expect fail "pvs unproved" pvs unproved
 expect fail "pvs no summary" pvs silent
 expect fail "pvs non-zero exit" pvs crash
 
-[ -z "$(find "$prefix/share/smoke" -newer "$prefix/share/smoke/pvs_smoke.pvs" ! -path "$prefix/share/smoke")" ] ||
-    { echo "FAIL: a wrapper wrote into the prefix" >&2; exit 1; }
-chmod -R u+w "$prefix"
+[ "$(snapshot)" = "$before" ] || { echo "FAIL: a wrapper wrote into the prefix" >&2; exit 1; }
 echo 'PASS: smoke installer and Mizar/PVS wrappers'
diff --git a/tests/setup_install_test.sh b/tests/setup_install_test.sh
index cbde0d5..352af63 100644
--- a/tests/setup_install_test.sh
+++ b/tests/setup_install_test.sh
@@ -2,6 +2,8 @@
 # SPDX-License-Identifier: MPL-2.0
 # Test installer fallback paths without networking or installing dependencies.
 set -euo pipefail
+# install_just_with_cargo prefers CARGO_INSTALL_ROOT; the stub expects CARGO_HOME.
+unset CARGO_INSTALL_ROOT
 
 repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
 fixture_root="$(mktemp -d)"
@@ -10,30 +12,45 @@ trap 'rm -rf "$fixture_root"' EXIT
 # Source the actual functions without running setup's main routine.
 sed '/^main "\$@"$/d' "$repo_root/build/setup.sh" > "$fixture_root/functions.sh"
 
+# Cargo fallback, with stub executables and a real PATH lookup. Cargo's
+# install root is deliberately NOT on PATH, as with a distro Cargo: setup must
+# install into a known root and put its bin directory on PATH itself.
+mkdir -p "$fixture_root/bin"
+cat > "$fixture_root/bin/cargo" <<'SH'
+#!/bin/sh
+expected="install just --version 1.56.0 --locked --root $CARGO_HOME"
+if [ "$*" != "$expected" ]; then
+    echo "Unexpected Cargo arguments: $*" >&2
+    exit 98
+fi
+mkdir -p "$CARGO_HOME/bin"
+printf '#!/bin/sh\necho "just 1.56.0"\n' > "$CARGO_HOME/bin/just"
+chmod +x "$CARGO_HOME/bin/just"
+SH
+printf '#!/bin/sh\nexit 1\n' > "$fixture_root/bin/sudo"  # an apt repository without just
+chmod +x "$fixture_root/bin/cargo" "$fixture_root/bin/sudo"
+
+# The fallback run gets only the utilities it needs, linked into one
+# directory, so a just installed on this machine cannot satisfy the lookup
+# before the Cargo stub runs.
+mkdir -p "$fixture_root/sysbin"
+for tool in sh mkdir chmod head; do
+    ln -s "$(command -v "$tool")" "$fixture_root/sysbin/$tool"
+done
+
 for manager in apt unknown; do
-    FIXTURE_ROOT="$fixture_root" MANAGER="$manager" sh -eu <<'SH'
+    rm -rf "$fixture_root/cargo-home"
+    FIXTURE_ROOT="$fixture_root" MANAGER="$manager" CARGO_HOME="$fixture_root/cargo-home" \
+        PATH="$fixture_root/bin:$fixture_root/sysbin" "$fixture_root/sysbin/sh" -eu <<'SH'
 . "$FIXTURE_ROOT/functions.sh"
 PKG_MGR="$MANAGER"
-installed=false
-command() {
-    case "$2" in
-        just) [ "$installed" = true ] ;;
-        cargo) return 0 ;;
-        *) return 1 ;;
-    esac
-}
-sudo() { return 1; }  # Simulate an apt repository without just.
 curl() { echo 'Unexpected download' >&2; exit 99; }
-cargo() {
-    if [ "$*" != 'install just --version 1.56.0 --locked' ]; then
-        echo "Unexpected Cargo arguments: $*" >&2
-        exit 98
-    fi
-    installed=true
-}
-just() { printf 'just 1.56.0\n'; }
 install_just
-[ "$installed" = true ]
+case ":$PATH:" in
+    *":$CARGO_HOME/bin:"*) ;;
+    *) echo "FAIL: $CARGO_HOME/bin was not added to PATH" >&2; exit 1 ;;
+esac
+[ "$(just --version)" = 'just 1.56.0' ]
 SH
 done
 
diff --git a/tools/environments/README.adoc b/tools/environments/README.adoc
index b77c827..15f9cab 100644
--- a/tools/environments/README.adoc
+++ b/tools/environments/README.adoc
@@ -18,9 +18,12 @@ who reads its capability record, and a `measured` block.
 
 |`probe-reachability.sh`
 |Sends one HEAD request per URL in `hosts.txt` (or, with `--get`, one GET
-for the first byte only) and prints the HTTP status this environment saw,
-as text or as one JSON object. Keeps no body, executes nothing. Its output is what goes into an entry's `measured` block,
-with the date.
+for the first byte only, capped at 64 KiB when the server ignores the
+range) and prints the HTTP status this environment saw, as text or as one
+JSON object. Keeps no body, executes nothing. Its output is what goes
+into an entry's `measured` block, with the date.
+`tests/probe_reachability_test.sh` checks it offline with stub `curl` and
+`ldd` executables.
 
 |`hosts.txt`
 |The hosts the toolchain manifest's `method` column fetches from.
@@ -28,7 +31,14 @@ with the date.
 
 == Reading a `measured` block
 
-`reachable` means the request returned 2xx or 3xx (206 for a ranged GET). `refused` is a 403
+`reachable` means the request returned 2xx or 3xx (206 for a ranged GET).
+`range-ignored` means a `--get` request was answered with the whole body,
+so curl stopped at the 64 KiB cap: the host answered and ignored the
+range. The probe does not inspect the body, so this does not show the
+file is served (an error page over 64 KiB looks the same).
+The probe asks only for the first byte, so it does not show whether the
+host can resume a download. A host that answers some tries and resets
+others is recorded under `intermittent` with the counts seen. `refused` is a 403
 from the environment's proxy. `auth-required` is a 401: the host answered
 and wants a token, which the probe does not supply. `tls-failed` means the
 host's certificate is not in the environment's CA bundle. A container
diff --git a/tools/environments/environments.kyaml b/tools/environments/environments.kyaml
index da6fa40..be0bac3 100644
--- a/tools/environments/environments.kyaml
+++ b/tools/environments/environments.kyaml
@@ -22,7 +22,7 @@
   record: {format: "JCS I-JSON", producer: "provers.sh doctor --json (planned)", schema: "verification/proofs/idris2/EnvCapability.idr (planned)"},
   environments: [
     {id: "workstation", kind: "host", installs: ["guix", "mise", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["echidna", "echidnabot", "proof-burrower", "boj-server"], notes: "tools/workstation/env.sh is the live PATH; versions are unrecorded until doctor runs here", measured: {}},
-    {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-10-27", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (22 URLs, every one probed twice: HEAD, then --get with a one-byte ranged GET)", reachable: ["github.com release asset (HEAD 302 to release-assets.githubusercontent.com then 200; GET bytes 0-0 206)", "codeload.github.com", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "releases.lean-lang.org", "isabelle.in.tum.de", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "downloads.sourceforge.net (SBCL binary)", "ftp.gnu.org", "smt-lib.org", "www.tptp.org"], refused: ["github.com release landing page (/releases/latest; HEAD and GET 403)", "api.github.com (HEAD and GET 403)", "crates.io (HEAD and GET 403)"], registry-answered: ["ghcr.io (HEAD 405, GET 401)", "cgr.dev (HEAD 405, GET 401)"], tls-failed: ["www.cs.utexas.edu (HEAD and GET)"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was therefore not observed. The later one-byte GET shows asset bytes can flow, not that a full download or a run is permitted"}},
+    {id: "agent-session", kind: "cloud-session", installs: ["bundle", "mise"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: "policy", container-runtime: "none", report: ["session .session/ capture", "boj-server"], notes: "network and execution policy differ per session class; measure, never assume", measured: {date: "2026-11-04", platform: "Ubuntu 24.04.5 x86_64 glibc 2.39", hosts-file: "hosts.txt (24 URLs, every one probed twice: HEAD, then --get with a one-byte ranged GET capped at 64 KiB)", reachable: ["github.com release asset (HEAD 302 to release-assets.githubusercontent.com then 200; GET bytes 0-0 206)", "codeload.github.com (GET range-ignored: answers 200 with the whole archive, capped)", "raw.githubusercontent.com", "opam.ocaml.org", "alire.ada.dev", "hackage.haskell.org", "static.rust-lang.org", "index.crates.io (Cargo's sparse index)", "static.crates.io/crates/just/1.56.0/download (the route Cargo downloads from; GET range-ignored, capped)", "releases.lean-lang.org", "mizar.uwb.edu.pl", "pvs.csl.sri.com", "cvc5.github.io", "downloads.sourceforge.net (SBCL binary)", "ftp.gnu.org", "smt-lib.org", "www.tptp.org (GET range-ignored, capped)"], intermittent: ["isabelle.in.tum.de (HEAD 200; GET 206 on 1 of 4 tries, the rest reset during the TLS handshake, curl exit 35)"], refused: ["github.com release landing page (/releases/latest; HEAD and GET 403)", "api.github.com (HEAD and GET 403)", "crates.io/api (HEAD and GET 403; Cargo does not use it to install)"], registry-answered: ["ghcr.io (HEAD 405, GET 401)", "cgr.dev (HEAD 405, GET 401)"], tls-failed: ["www.cs.utexas.edu (HEAD and GET)"], execute-downloaded: "denied-before-download", execute-downloaded-note: "the 2026-10-27 Z3 install experiment was refused by session policy before any bytes moved; whether a fetched binary would run was not observed. One-byte GETs show asset bytes can flow, not that a full download or a run is permitted. On 2026-11-04 the Mizar distribution was downloaded and inspected with file(1) without being run"}},
     {id: "ci-runner", kind: "ci-runner", installs: ["bundle", "guix", "image"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "podman", report: ["workflow summary", "echidnabot"], notes: "full network, limited minutes: a cold opam build is not acceptable here", measured: {}},
     {id: "devcontainer", kind: "container", installs: ["image", "bundle"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: true, container-runtime: "none", report: ["doctor on attach"], notes: ".devcontainer/Containerfile (Wolfi) names no prover today", measured: {}},
     {id: "guix-shell", kind: "guix-shell", installs: ["guix"], prefix: "/opt/hyperpolymath/provers", execute-downloaded: false, container-runtime: "none", report: ["doctor"], notes: "primary packager (ruling 2026-05-18); the bundle covers only the tail Guix does not carry", measured: {}},
diff --git a/tools/environments/hosts.txt b/tools/environments/hosts.txt
index b0719b6..040ba9d 100644
--- a/tools/environments/hosts.txt
+++ b/tools/environments/hosts.txt
@@ -21,6 +21,12 @@ https://alire.ada.dev/
 https://hackage.haskell.org/
 https://static.rust-lang.org/rustup/dist/x86_64-unknown-linux-gnu/rustup-init
 https://crates.io/api/v1/crates/just
+# What `cargo install` actually uses: the sparse index and the crate download.
+# A refusal of the API above says nothing about these.
+https://index.crates.io/ju/st/just
+# The download is the index's "dl" (https://static.crates.io/crates) plus
+# /{crate}/{version}/download, which is the route Cargo requests.
+https://static.crates.io/crates/just/1.56.0/download
 https://releases.lean-lang.org/
 https://ftp.gnu.org/gnu/guix/
 
diff --git a/tools/environments/probe-reachability.sh b/tools/environments/probe-reachability.sh
index cf94992..68d93f1 100755
--- a/tools/environments/probe-reachability.sh
+++ b/tools/environments/probe-reachability.sh
@@ -39,8 +39,13 @@ for arg in "$@"; do
     esac
 done
 if [ "$METHOD" = "get" ]; then
-    # -r 0-0 asks for one byte; the body goes to /dev/null either way.
-    request=(-r 0-0)
+    # -r 0-0 asks for one byte. A server may ignore the range and send the
+    # whole body, so --max-filesize caps the transfer: curl aborts (exit 63)
+    # before reading a body whose length is declared above the cap, or once a
+    # chunked body passes it (measured with curl 8.5.0; an older curl may
+    # enforce the cap only on a declared length, and --max-time still bounds
+    # the transfer). The body goes to /dev/null either way.
+    request=(-r 0-0 --max-filesize 65536)
 else
     request=(-I)
 fi
@@ -56,14 +61,17 @@ fi
 
 # classify <http-code> <curl-exit> — print one outcome label to stdout.
 # Takes the final HTTP status after redirects and curl's exit code. Exit 60
-# yields tls-failed; any other non-zero exit or HTTP 000 yields unreachable,
-# regardless of the HTTP status. With a zero exit, 401 yields auth-required,
+# yields tls-failed; exit 63 with a code other than 000 yields range-ignored.
+# Any remaining non-zero exit or HTTP 000 yields unreachable. With a zero
+# exit, 401 yields auth-required,
 # 403 yields refused, 2xx/3xx yields reachable, and all other codes yield
 # http-<http-code>. A failed probe is reported as a label, not an error status.
 classify() {
     local code="$1" rc="$2"
     if [ "$rc" -eq 60 ]; then
         echo "tls-failed"
+    elif [ "$rc" -eq 63 ] && [ "$code" != "000" ]; then
+        echo "range-ignored"
     elif [ "$rc" -ne 0 ] || [ "$code" = "000" ]; then
         echo "unreachable"
     elif [ "$code" = "401" ]; then
@@ -81,7 +89,12 @@ date_utc="$(date -u +%Y-%m-%dT%H:%M:%SZ)"
 platform="$(uname -s)/$(uname -m)"
 if command -v ldd >/dev/null 2>&1; then
     # awk reads all of ldd's output, so no SIGPIPE under pipefail.
-    platform="$platform glibc $(ldd --version 2>/dev/null | awk 'NR==1{print $NF}')"
+    # Only GNU ldd knows --version (FreeBSD's does not), so the C library
+    # version is optional and its failure must not stop the probe.
+    libc="$(ldd --version 2>/dev/null | awk 'NR==1 && /GNU|GLIBC/{print $NF}')" || libc=""
+    if [ -n "$libc" ]; then
+        platform="$platform glibc $libc"
+    fi
 fi
 
 if [ "$MODE" = "text" ]; then
diff --git a/tools/proof-toolchain/DESIGN.adoc b/tools/proof-toolchain/DESIGN.adoc
index bb7b6cc..9344108 100644
--- a/tools/proof-toolchain/DESIGN.adoc
+++ b/tools/proof-toolchain/DESIGN.adoc
@@ -65,8 +65,10 @@ proves it runs. Roles are listed below.
 
 |`toolchain.lock.json`
 |Tool-owned lock, written only by the bundle build (I-JSON, JCS). Records the
-resolved version, the source URL and the SHA-256 of every input, and the
-SHA-256 of the produced bundle and image digest. Never hand-edited.
+resolved version, the source URL and the SHA-256 of every input, the
+SHA-256 of each tool's installed entry-point executable (the value
+`doctor` compares as `locked_sha256`), and the SHA-256 of the produced
+bundle and image digest. Never hand-edited.
 
 |Bundle build (CI)
 |A workflow on a full-network runner builds every tool into the fixed prefix
@@ -88,7 +90,9 @@ supported target.
 
 |`provers.sh doctor`
 |Reports each manifest entry as `PRESENT <version>`, `DRIFT <have> != <lock>`,
-or `UNAVAILABLE <reason>`, as text and as one JCS object. It never reports a
+or `UNAVAILABLE <reason>`, as text and as one JCS object. In the object a
+`DRIFT` entry carries `observed_version`, `observed_sha256`,
+`locked_version`, `locked_sha256` and `mismatch`. It never reports a
 tool it could not run as present (PROOF-POLICY §6).
 
 |`provers.sh render`
@@ -171,7 +175,7 @@ plus the supporting tools the mapped provers need.
 |`transport` |agda2dedukti, Dedukti (`dkcheck`), Lambdapi. agda2dedukti tracks particular Agda versions; the manifest records which Agda it accepts.
 |`exception:rust` |Kani; Aeneas with Charon (PROOF-POLICY §4.1)
 |`exception:recorded` |TLA+ (`tlc`); Isabelle, HOL Light, HOL4, ACL2, Mizar and PVS (supplementary only). The last five were added 2026-10-27 so a kit-provisioned environment can serve every backend in echidna's default core set. PVS is built from its BSD-3-Clause sources on the bundled SBCL; SRI's click-through licence covers only its Allegro build, which the bundle does not use.
-|`runtime` |Rust toolchains (rustup, the toolchains Creusot and Kani pin), a Java runtime for the `tlc` launcher, Poly/ML for HOL4 and SBCL for ACL2 and PVS, bundled rather than taken from the host
+|`runtime` |Rust toolchains (rustup, the toolchains Creusot and Kani pin), a Java runtime for the `tlc` launcher, the OCaml switch HOL Light runs in, Poly/ML for HOL4 and SBCL for ACL2 and PVS, bundled rather than taken from the host
 |`backend` |Z3, CVC5, Yices, Alt-Ergo, E prover, Vampire
 |===
 
diff --git a/tools/proof-toolchain/toolchain.kyaml b/tools/proof-toolchain/toolchain.kyaml
index ba12637..bb84eaa 100644
--- a/tools/proof-toolchain/toolchain.kyaml
+++ b/tools/proof-toolchain/toolchain.kyaml
@@ -45,12 +45,13 @@
     {id: "tlc", role: "exception:recorded", method: "release asset (tlaplus tla2tools.jar) plus a bundled tlc launcher (java -cp $PREFIX/lib/tla/tla2tools.jar tlc2.TLC, absolute so it runs from any directory)", pin: "resolve-stable", verify: "tlc -h", needs: ["jre"], notes: "pin a stable tagged release with its sha256 in the lock; v1.8.0 is a rolling prerelease rebuilt on every master commit"},
     {id: "jre", role: "runtime", method: "release asset (Eclipse Temurin JRE, Java 17 or later)", pin: "resolve-stable", verify: "java -version", notes: "bundled so the tlc launcher does not depend on a host Java"},
     {id: "isabelle", role: "exception:recorded", method: "release asset", pin: "resolve", verify: "isabelle version", notes: "supplementary evidence only"},
-    {id: "hol-light", role: "exception:recorded", method: "opam (hol_light package) with a bundled hol_light launcher that loads the checkpointed image", pin: "resolve", verify: "sh $PREFIX/share/smoke/hol-light-refl.sh", notes: "added 2026-10-27 (E6: echidna core coverage; owner decision). The script pipes a REFL goal into hol_light and requires a success marker after checking the theorem. Supplementary evidence only, as Isabelle"},
-    {id: "polyml", role: "runtime", method: "source build (polyml/polyml) into the prefix", pin: "from hol4 developers/README", verify: "poly -v", notes: "the Standard ML runtime HOL4 is built on; bundled so hol does not depend on a host Poly/ML"},
+    {id: "hol-light-ocaml", role: "runtime", method: "opam switch at $PREFIX/opam/hol-light holding the OCaml compiler and the camlp5, zarith (or num) and ledit versions that the pinned hol_light opam file selects for that compiler series", pin: "from hol-light opam", verify: "$PREFIX/opam/hol-light/bin/ocaml -version", notes: "HOL Light's launcher starts this OCaml toplevel with the checkpointed image, so the switch is part of the closure: every package in it is locked with its version and hash, and camlp5 stays inside the cap the hol_light opam file sets for the chosen OCaml series"},
+    {id: "hol-light", role: "exception:recorded", method: "opam (hol_light package) into the hol-light-ocaml switch, with a bundled hol_light launcher that loads the checkpointed image", pin: "resolve", verify: "sh $PREFIX/share/smoke/hol-light-refl.sh", needs: ["hol-light-ocaml"], notes: "added 2026-10-27 (E6: echidna core coverage; owner decision). The script pipes a REFL goal into hol_light and requires a success marker after checking the theorem. Supplementary evidence only, as Isabelle"},
+    {id: "polyml", role: "runtime", method: "source build (polyml/polyml, tagged release) into the prefix, with libpolyml and libpolymain found through the bundle's run path", pin: "resolve-stable", verify: "poly -v", notes: "the Standard ML runtime HOL4 is built on; bundled so hol does not depend on a host Poly/ML. HOL4 recommends Poly/ML but names no version, so the newest stable tag is taken and the lock records the version HOL4 was built and smoke-tested with"},
     {id: "hol4", role: "exception:recorded", method: "source build (HOL-Theorem-Prover/HOL, tagged release) on the bundled Poly/ML, exposed as bin/hol and bin/Holmake", pin: "resolve-stable", verify: "hol < $PREFIX/share/smoke/hol4-smoke.sml", needs: ["polyml"], notes: "added 2026-10-27 (E6). The smoke file proves a trivial theorem and exits non-zero on failure. Supplementary evidence only"},
     {id: "sbcl", role: "runtime", method: "release archive (the official x86-64 Linux binary distribution that sbcl.org's platform table links, served from downloads.sourceforge.net; sbcl/sbcl on GitHub carries source tags only)", pin: "resolve-stable", verify: "sbcl --version", notes: "the Common Lisp ACL2 and PVS are built on; bundled so neither depends on a host Lisp. One pin serves both, and the lock records the version each was built with"},
     {id: "acl2", role: "exception:recorded", method: "tagged source archive (acl2/acl2 on GitHub, fetched from codeload.github.com) built with the bundled SBCL into a saved image, exposed as bin/acl2", pin: "resolve-stable", verify: "acl2 < $PREFIX/share/smoke/acl2-smoke.lisp", needs: ["sbcl"], notes: "added 2026-10-27 (E6). Community books (books/, licensed separately) are not bundled; a consumer that needs them records that as its own entry. The entry never fetches from the legacy www.cs.utexas.edu home. Supplementary evidence only"},
-    {id: "mizar", role: "exception:recorded", method: "release asset (Mizar system distribution for Linux x86_64 from mizar.uwb.edu.pl, which carries the matching MML), with the MML installed at $PREFIX/share/mizar", pin: "resolve-stable", verify: "sh $PREFIX/share/smoke/mizar-smoke.sh $PREFIX", notes: "added 2026-10-27 (E6). The MML version is coupled to the system release and is recorded in the lock with it; the exact `verifier` and `makeenv` binaries are what echidna's Mizar backend spawns. The smoke script sets MIZFILES to the bundled MML, works in a scratch directory and fails on a non-empty .err file. Supplementary evidence only"},
+    {id: "mizar", role: "exception:recorded", method: "release archive (the i386-linux system distribution from mizar.uwb.edu.pl/~softadm/current, which carries the matching MML; Mizar publishes no x86_64 Linux build), with the MML installed at $PREFIX/share/mizar", pin: "resolve-stable", verify: "sh $PREFIX/share/smoke/mizar-smoke.sh $PREFIX", notes: "added 2026-10-27 (E6). The MML version is coupled to the system release and is recorded in the lock with it; the exact `verifier` and `makeenv` binaries are what echidna's Mizar backend spawns. The smoke script sets MIZFILES to the bundled MML, works in a scratch directory and fails on a non-empty .err file. Its binaries are statically linked 32-bit i386 executables (checked with file(1) on 8.1.15: no shared libraries), so no 32-bit userland is bundled, but the host kernel must run i386 code (IA32 emulation); where it cannot, the smoke check fails and doctor reports UNAVAILABLE. Supplementary evidence only"},
     {id: "pvs", role: "exception:recorded", method: "source build (SRI-CSL/PVS tagged release, BSD-3-Clause) on the bundled SBCL, headless, exposed as bin/pvs and bin/proveit", pin: "resolve-stable", verify: "sh $PREFIX/share/smoke/pvs-smoke.sh", needs: ["sbcl"], notes: "added 2026-10-27 (E6, completing echidna's core twelve). The SBCL source build is redistributable; SRI's click-through licence covers only its Allegro build, which is not used. NASALib is not bundled; a consumer that needs it records it as its own entry. The smoke script proves one lemma with proveit in a scratch directory and requires the summary to report it succeeded. Supplementary evidence only"},
     {id: "z3", role: "backend", method: "release asset", pin: "resolve", verify: "z3 --version"},
     {id: "cvc5", role: "backend", method: "release asset", pin: "resolve", verify: "cvc5 --version"},