diff --git a/.github/workflows/live-provers.yml b/.github/workflows/live-provers.yml
index e17aaefd..06f4b272 100644
--- a/.github/workflows/live-provers.yml
+++ b/.github/workflows/live-provers.yml
@@ -226,21 +226,127 @@ jobs:
         run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
 
   # ============================================================================
-  # Tier 3 — weekly.  Container-provisioned provers.  Wave-3 placeholder.
+  # Tier 3 — weekly.  Heavier upstream provers, best-effort provisioning.
+  #
+  # Backends grouped as:
+  #   A — live-provisioned today via apt / upstream tarball (tamarin, proverif,
+  #       metamath, twelf, ortools).  Version-check runs, skip-if-absent.
+  #   B — heavy-build deferred (hol4, acl2, scip) and proprietary (imandra).
+  #       Provisioning step emits a skip note; test step runs the suite with
+  #       continue-on-error so the matrix stays green and the binary's absence
+  #       is logged as SKIP by the suite's `which` probe.
   # ============================================================================
   tier3:
-    name: T3 container provers
+    name: T3 / ${{ matrix.backend }}
     if: github.event_name == 'schedule' && github.event.schedule == '0 5 * * 0' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '3' || inputs.tier == 'all'))
     runs-on: ubuntu-latest
     continue-on-error: true
+    strategy:
+      fail-fast: false
+      matrix:
+        backend:
+          - tamarin
+          - proverif
+          - metamath
+          - twelf
+          - ortools
+          - hol4
+          - acl2
+          - scip
+          - imandra
     steps:
       - name: Checkout
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
-      - name: Announce Wave-3 TODO
+      - name: Install Rust
+        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
+      - name: Cache Cargo
+        uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
+      - name: Provision ${{ matrix.backend }} (best-effort)
+        continue-on-error: true
         run: |
-          echo "Tier-3 backends (Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath)"
-          echo "are provisioned via per-backend Containerfiles in Wave-3 of L3."
-          echo "See ~/Desktop/ECHIDNA-L3-LIVE-PROVER-CI-PROMPT.md for scope."
+          set -euo pipefail
+          sudo apt-get update
+          case "${{ matrix.backend }}" in
+            tamarin)
+              # Tamarin publishes prebuilt Linux x86_64 tarballs.
+              curl -fsSL -o /tmp/tamarin.tar.gz \
+                https://github.com/tamarin-prover/tamarin-prover/releases/latest/download/tamarin-prover-linux64-ubuntu.tar.gz || \
+                curl -fsSL -o /tmp/tamarin.tar.gz \
+                https://github.com/tamarin-prover/tamarin-prover/releases/download/1.10.0/tamarin-prover-1.10.0-linux64-ubuntu.tar.gz
+              sudo mkdir -p /opt/tamarin
+              sudo tar xzf /tmp/tamarin.tar.gz -C /opt/tamarin
+              # The tarball lays down tamarin-prover directly or in a version dir; link whichever we find.
+              TAMARIN_BIN="$(find /opt/tamarin -type f -name tamarin-prover | head -n 1)"
+              [ -n "$TAMARIN_BIN" ] && sudo ln -sf "$TAMARIN_BIN" /usr/local/bin/tamarin-prover
+              ;;
+            proverif)
+              # ProVerif is in the Ubuntu/Debian main repos.
+              sudo apt-get install -y proverif
+              ;;
+            metamath)
+              # metamath-exe is small; apt-installable on Ubuntu with build fallback.
+              sudo apt-get install -y metamath || {
+                sudo apt-get install -y build-essential git autoconf automake
+                git clone --depth=1 https://github.com/metamath/metamath-exe.git /tmp/mm
+                (cd /tmp/mm && ./build.sh) || \
+                  (cd /tmp/mm && autoreconf -i && ./configure && make)
+                sudo install -m 0755 /tmp/mm/metamath /usr/local/bin/metamath
+              }
+              ;;
+            twelf)
+              # Twelf is in Debian with SML/NJ; on Ubuntu it may live in universe.
+              sudo apt-get install -y twelf || \
+                echo "twelf unavailable via apt on this runner; test will SKIP."
+              ;;
+            ortools)
+              # Google OR-Tools ships prebuilt Linux tarballs.  The binary we
+              # expose to echidna is a small wrapper that invokes the solver CLI.
+              OR_URL="https://github.com/google/or-tools/releases/latest/download/or-tools_amd64_ubuntu-22.04_cpp_v9.11.4210.tar.gz"
+              curl -fsSL -o /tmp/ortools.tar.gz "$OR_URL" || {
+                echo "OR-Tools tarball unavailable at expected URL; test will SKIP."
+                exit 0
+              }
+              sudo mkdir -p /opt/ortools
+              sudo tar xzf /tmp/ortools.tar.gz -C /opt/ortools --strip-components=1
+              # Echidna's ORTools backend invokes `ortools_solve`.  The release
+              # ships `bin/solve` or similar; create the expected symlink.
+              OR_BIN="$(find /opt/ortools -type f \( -name ortools_solve -o -name solve \) | head -n 1)"
+              [ -n "$OR_BIN" ] && sudo ln -sf "$OR_BIN" /usr/local/bin/ortools_solve
+              ;;
+            hol4)
+              # HOL4 requires Poly/ML and a full tree build (~15min+); defer to
+              # container provisioning.  Test step will SKIP on this runner.
+              echo "hol4: heavy Poly/ML build deferred to Containerfile provisioning."
+              ;;
+            acl2)
+              # ACL2 requires a Common Lisp image (CCL/SBCL) and a 10min+ build;
+              # defer to container provisioning.  Test step will SKIP.
+              echo "acl2: heavy SBCL+image build deferred to Containerfile."
+              ;;
+            scip)
+              # SCIP Optimization Suite needs a full cmake build (~10min).  The
+              # upstream tarball requires a form-gated download, so CI defers to
+              # Containerfile provisioning.  Test step will SKIP.
+              echo "scip: form-gated upstream tarball; deferred to Containerfile."
+              ;;
+            imandra)
+              # Imandra is proprietary; no public Linux binary.  Handled via
+              # vendor-supplied container where a licence is available.
+              echo "imandra: proprietary; no public CI provisioning available."
+              ;;
+          esac
+          # Best-effort version probe for the matrix log.
+          case "${{ matrix.backend }}" in
+            tamarin)    tamarin-prover --version 2>&1 | head -n 1 || true ;;
+            proverif)   proverif --version 2>&1 | head -n 1 || true ;;
+            metamath)   echo exit | metamath 2>&1 | head -n 1 || true ;;
+            twelf)      twelf-server --help 2>&1 | head -n 1 || true ;;
+            ortools)    ortools_solve --help 2>&1 | head -n 1 || true ;;
+            hol4|acl2|scip|imandra) true ;;
+          esac
+      - name: Run live test for ${{ matrix.backend }} (allow-fail while Wave-3 wires up)
+        continue-on-error: true
+        run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
 
   # ============================================================================
   # Tier 4 — quarterly, best-effort / allow-fail.
diff --git a/Justfile b/Justfile
index a34e4b0f..0c6b4370 100644
--- a/Justfile
+++ b/Justfile
@@ -74,6 +74,40 @@ vocab-canon:
     julia scripts/vocabulary_mine_corpus.jl
     julia scripts/vocabulary_canonicalize.jl
 
+# ── Corpus / training pipeline ─────────────────────────────────
+#
+# Three steps in order: provision upstream mirrors, run every extractor,
+# then retrain.  Each step is idempotent; re-running only touches what
+# has changed.  See scripts/provision_corpora.sh --list for the source
+# catalogue.
+
+# Clone every upstream prover corpus into external_corpora/.
+# Pass specific names to provision a subset: `just provision-corpora metamath mathlib4`.
+provision-corpora *NAMES:
+    @if [ -z "{{NAMES}}" ]; then \
+        scripts/provision_corpora.sh --all; \
+    else \
+        scripts/provision_corpora.sh {{NAMES}}; \
+    fi
+
+# Report which upstream corpora are on disk and their sizes.
+corpora-status:
+    scripts/provision_corpora.sh --status
+
+# Run every scripts/extract_*.jl against the provisioned corpora.
+# Pass names to run a subset: `just extract-corpora metamath mathlib4`.
+extract-corpora *NAMES:
+    scripts/extract_all.sh {{NAMES}}
+
+# Full retrain from provisioned corpora.  Honours ECHIDNA_MAX_PROOF_STATES
+# (0 = unlimited), ECHIDNA_NUM_EPOCHS, ECHIDNA_NUM_NEGATIVES.
+retrain:
+    julia --project=src/julia src/julia/run_training.jl
+
+# End-to-end pipeline: provision → extract → retrain.
+# Use `ECHIDNA_MAX_PROOF_STATES=0 just corpus-refresh` to lift the sample cap.
+corpus-refresh: provision-corpora extract-corpora retrain
+
 # Run the eight-axis metrics suite against the current corpus and post
 # results to VeriSimDB. Falls back to training_data/metrics_<run_id>.jsonl
 # if VERISIM_URL is unreachable. Target values are documented in
diff --git a/scripts/extract_all.sh b/scripts/extract_all.sh
new file mode 100755
index 00000000..43ef598c
--- /dev/null
+++ b/scripts/extract_all.sh
@@ -0,0 +1,89 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# ECHIDNA — run every scripts/extract_*.jl once, non-interactively.
+#
+# Assumes scripts/provision_corpora.sh has already populated
+# external_corpora/; extractors whose upstream is absent short-circuit
+# with a print line (they already handle missing inputs gracefully).
+#
+# Usage
+# -----
+#   scripts/extract_all.sh                    # run every extractor
+#   scripts/extract_all.sh NAME ...           # run only the named extractors
+#                                             # (matches scripts/extract_<NAME>.jl)
+#   scripts/extract_all.sh --list             # list available extractors
+#
+# Environment
+#   ECHIDNA_JULIA_PROJECT — path passed to `julia --project=`
+#     (default: src/julia).
+#
+# Exit code is the number of extractors that failed (0 on clean run,
+# N on partial failure).  Suitable for a nightly cron.
+
+set -uo pipefail  # NOTE: not `set -e` — we want to collect failures, not abort.
+
+ECHIDNA_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+JULIA_PROJECT="${ECHIDNA_JULIA_PROJECT:-$ECHIDNA_ROOT/src/julia}"
+
+list_extractors() {
+    ( cd "$ECHIDNA_ROOT/scripts" && ls extract_*.jl 2>/dev/null | sed 's/^extract_//; s/\.jl$//' )
+}
+
+# Handle info flags before probing the environment.
+case "${1:-}" in
+    --list)
+        list_extractors
+        exit 0
+        ;;
+    -h|--help)
+        sed -n '4,22p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//'
+        exit 0
+        ;;
+esac
+
+if ! command -v julia >/dev/null 2>&1; then
+    echo "error: julia not on PATH; install Julia to run the extractors." >&2
+    exit 127
+fi
+
+# Build the list of extractors to run.
+if [[ $# -gt 0 ]]; then
+    targets=()
+    for name in "$@"; do
+        path="$ECHIDNA_ROOT/scripts/extract_${name}.jl"
+        if [[ ! -f "$path" ]]; then
+            echo "error: no such extractor: extract_${name}.jl" >&2
+            exit 2
+        fi
+        targets+=("$path")
+    done
+else
+    mapfile -t targets < <(find "$ECHIDNA_ROOT/scripts" -maxdepth 1 -name 'extract_*.jl' | sort)
+fi
+
+echo "Running ${#targets[@]} extractor(s) with --project=$JULIA_PROJECT"
+echo
+
+failed=()
+for script in "${targets[@]}"; do
+    name="$(basename "$script" .jl)"
+    echo "========================================"
+    echo "  $name"
+    echo "========================================"
+    if julia --project="$JULIA_PROJECT" "$script"; then
+        echo "  [ok] $name"
+    else
+        echo "  [FAIL] $name"
+        failed+=("$name")
+    fi
+    echo
+done
+
+if [[ ${#failed[@]} -gt 0 ]]; then
+    echo "Extractors that failed: ${failed[*]}"
+    exit "${#failed[@]}"
+fi
+
+echo "All extractors completed."
diff --git a/scripts/provision_corpora.sh b/scripts/provision_corpora.sh
new file mode 100755
index 00000000..4f3f1bc0
--- /dev/null
+++ b/scripts/provision_corpora.sh
@@ -0,0 +1,281 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# ECHIDNA — Non-interactive upstream corpus provisioning.
+#
+# Clones the upstream mirror of every theorem-prover corpus the extractors
+# under scripts/extract_*.jl expect at external_corpora/<name>/.  Each
+# clone uses --depth=1 to keep the bandwidth bill finite (~4-8 GB total
+# when all sources are selected).
+#
+# Usage
+# -----
+#   scripts/provision_corpora.sh [NAME ...]     # provision the named sources
+#   scripts/provision_corpora.sh --all          # provision every source
+#   scripts/provision_corpora.sh --list         # print the source catalogue
+#   scripts/provision_corpora.sh --status       # show which sources are on disk
+#
+# Selection names match the external_corpora/<name>/ directory each extractor
+# expects.  Unknown names exit non-zero so typos fail loudly in CI.
+#
+# Behaviour
+#   * If external_corpora/<name>/ already exists the source is skipped
+#     (idempotent; safe to re-run).  Pass --force to re-clone into a
+#     fresh directory.
+#   * Network failures are retried once; a failure after that is logged
+#     and the script continues to the next source (so a single offline
+#     mirror doesn't abort a 40-source provisioning).
+#   * Designed to be callable from a Justfile recipe or a nightly CI
+#     workflow.  No interactive prompts, ever.
+
+set -euo pipefail
+
+ECHIDNA_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+CORPORA_DIR="${ECHIDNA_CORPORA_DIR:-$ECHIDNA_ROOT/external_corpora}"
+FORCE=0
+
+# ------------------------------------------------------------------
+# Upstream catalogue
+#
+# Each entry: "<name>|<kind>|<url>|<subpath?>"
+#   kind = git   — `git clone --depth=1 <url> <CORPORA_DIR>/<name>`
+#   kind = tar   — `curl <url> | tar xz` into <CORPORA_DIR>/<name>
+#   kind = skip  — metadata only (proprietary / form-gated / non-public)
+#
+# Adding a source:
+#   1. Add a row here with the real upstream URL.
+#   2. Update scripts/extract_<name>.jl to read from external_corpora/<name>.
+# ------------------------------------------------------------------
+CATALOGUE=(
+    # Interactive proof assistants
+    "abella|git|https://github.com/abella-prover/abella"
+    "agda-stdlib|git|https://github.com/agda/agda-stdlib"
+    "agda-cubical|git|https://github.com/agda/cubical"
+    "agda-unimath|git|https://github.com/UniMath/agda-unimath"
+    "arend|git|https://github.com/JetBrains/Arend"
+    "CoqGym|git|https://github.com/princeton-vl/CoqGym"
+    "mathcomp|git|https://github.com/math-comp/math-comp"
+    "mathcomp-analysis|git|https://github.com/math-comp/analysis"
+    "mathcomp-finmap|git|https://github.com/math-comp/finmap"
+    "mathcomp-algebra-tactics|git|https://github.com/math-comp/algebra-tactics"
+    "mathlib3|git|https://github.com/leanprover-community/mathlib"
+    "mathlib4|git|https://github.com/leanprover-community/mathlib4"
+    "hol4|git|https://github.com/HOL-Theorem-Prover/HOL"
+    "hol_light|git|https://github.com/jrh13/hol-light"
+    "fstar|git|https://github.com/FStarLang/FStar"
+    "idris2|git|https://github.com/idris-lang/Idris2"
+    "matita|git|https://github.com/rocq-prover/matita"
+    "mizar|git|https://github.com/MizarProject/mml"
+    "metamath|git|https://github.com/metamath/set.mm"
+    "opentheory|git|https://github.com/gilith/opentheory"
+    "pvs|git|https://github.com/nasa/pvslib"
+    "afp|git|https://foss.heptapod.net/isa-afp/afp-devel.git"
+
+    # ACL2 family
+    "acl2|git|https://github.com/acl2/acl2"
+    "acl2s|git|https://github.com/acl2s/acl2s"
+
+    # Auto-active verifiers
+    "dafny|git|https://github.com/dafny-lang/dafny"
+    "why3|git|https://gitlab.inria.fr/why3/why3"
+    "boogie|git|https://github.com/boogie-org/boogie"
+    "cameleer|git|https://github.com/ocaml-gospel/cameleer"
+    "framac|git|https://git.frama-c.com/pub/frama-c"
+    "viper|git|https://github.com/viperproject/silver"
+    "key|git|https://github.com/KeYProject/key"
+
+    # Model checkers / CI verifiers
+    "cbmc|git|https://github.com/diffblue/cbmc"
+    "seahorn|git|https://github.com/seahorn/seahorn"
+    "spin|git|https://github.com/nimble-code/Spin"
+    "prism|git|https://github.com/prismmodelchecker/prism-examples"
+    "nusmv|skip|http://nusmv.fbk.eu/distrib/" # distro ships examples
+    "uppaal|skip|https://uppaal.org/documentation/" # commercial; examples gated
+    "tlaplus_examples|git|https://github.com/tlaplus/Examples"
+
+    # SAT / SMT / FO-ATP benchmarks
+    "abc|git|https://github.com/berkeley-abc/abc"
+    "dreal4|git|https://github.com/dreal/dreal4"
+    "smtlib|skip|https://smtlib.cs.uiowa.edu/benchmarks.shtml" # tarball index
+    "sat_benchmarks|skip|https://www.satcompetition.org/" # annual tarballs
+    "tptp|skip|https://www.tptp.org/" # form-free tarball
+
+    # Security protocol verifiers
+    "tamarin|git|https://github.com/tamarin-prover/tamarin-prover"
+    "proverif|git|https://gitlab.inria.fr/bblanche/proverif"
+
+    # Constraint / optimisation
+    "alloy|git|https://github.com/AlloyTools/models"
+    "minizinc|git|https://github.com/MiniZinc/minizinc-benchmarks"
+
+    # Logic frameworks / misc
+    "dedukti|git|https://github.com/Deducteam/Libraries"
+    "elpi-lang|git|https://github.com/LPCIC/elpi"
+    "naproche|git|https://github.com/naproche/naproche"
+    "mercury-lang|git|https://github.com/Mercury-Language/mercury"
+    "nunchaku|git|https://github.com/nunchaku-inria/nunchaku"
+    "athena|git|https://github.com/AthenaFoundation/athena"
+)
+
+# ------------------------------------------------------------------
+
+usage() {
+    sed -n '4,25p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//'
+}
+
+list_catalogue() {
+    printf "%-28s %-5s %s\n" "NAME" "KIND" "URL"
+    printf "%-28s %-5s %s\n" "----" "----" "---"
+    for entry in "${CATALOGUE[@]}"; do
+        IFS='|' read -r name kind url _ <<<"$entry"
+        printf "%-28s %-5s %s\n" "$name" "$kind" "$url"
+    done
+}
+
+show_status() {
+    local present=0
+    local missing=0
+    printf "%-28s %-9s %s\n" "NAME" "STATUS" "SIZE"
+    printf "%-28s %-9s %s\n" "----" "------" "----"
+    for entry in "${CATALOGUE[@]}"; do
+        IFS='|' read -r name kind _ _ <<<"$entry"
+        local path="$CORPORA_DIR/$name"
+        if [[ -d "$path" ]]; then
+            local size
+            size="$(du -sh "$path" 2>/dev/null | awk '{print $1}')"
+            printf "%-28s %-9s %s\n" "$name" "present" "$size"
+            present=$((present + 1))
+        elif [[ "$kind" == "skip" ]]; then
+            printf "%-28s %-9s %s\n" "$name" "manual" "(gated upstream)"
+        else
+            printf "%-28s %-9s %s\n" "$name" "missing" "-"
+            missing=$((missing + 1))
+        fi
+    done
+    echo
+    echo "Summary: $present present, $missing missing, $(( ${#CATALOGUE[@]} - present - missing )) manual."
+    echo "Root:    $CORPORA_DIR"
+}
+
+find_entry() {
+    local want="$1"
+    for entry in "${CATALOGUE[@]}"; do
+        IFS='|' read -r name _ _ _ <<<"$entry"
+        if [[ "$name" == "$want" ]]; then
+            echo "$entry"
+            return 0
+        fi
+    done
+    return 1
+}
+
+provision_one() {
+    local entry="$1"
+    IFS='|' read -r name kind url _ <<<"$entry"
+    local dest="$CORPORA_DIR/$name"
+
+    if [[ "$kind" == "skip" ]]; then
+        echo "  [skip]   $name: provision manually from $url"
+        return 0
+    fi
+
+    if [[ -d "$dest" && $FORCE -eq 0 ]]; then
+        echo "  [ok]     $name: already present at $dest"
+        return 0
+    fi
+
+    if [[ -d "$dest" && $FORCE -eq 1 ]]; then
+        echo "  [force]  removing $dest"
+        rm -rf "$dest"
+    fi
+
+    mkdir -p "$CORPORA_DIR"
+
+    case "$kind" in
+        git)
+            echo "  [clone]  $name  <-  $url"
+            if ! git clone --depth=1 --filter=blob:none "$url" "$dest" 2>&1 | tail -n 3; then
+                echo "  [retry]  $name"
+                sleep 2
+                if ! git clone --depth=1 "$url" "$dest" 2>&1 | tail -n 3; then
+                    echo "  [FAIL]   $name: clone failed; continuing"
+                    return 1
+                fi
+            fi
+            ;;
+        tar)
+            echo "  [tar]    $name  <-  $url"
+            mkdir -p "$dest"
+            if ! curl -fsSL "$url" | tar xz -C "$dest" --strip-components=1; then
+                echo "  [FAIL]   $name: tarball extraction failed; continuing"
+                return 1
+            fi
+            ;;
+        *)
+            echo "  [WARN]   unknown kind '$kind' for $name"
+            return 1
+            ;;
+    esac
+    echo "  [done]   $name"
+}
+
+provision_all() {
+    local ok=0 fail=0 skip=0
+    for entry in "${CATALOGUE[@]}"; do
+        IFS='|' read -r _ kind _ _ <<<"$entry"
+        if [[ "$kind" == "skip" ]]; then
+            skip=$((skip + 1))
+            provision_one "$entry" || true
+            continue
+        fi
+        if provision_one "$entry"; then
+            ok=$((ok + 1))
+        else
+            fail=$((fail + 1))
+        fi
+    done
+    echo
+    echo "Provisioning complete: $ok ok, $fail failed, $skip manual."
+}
+
+# ------------------------------------------------------------------
+
+case "${1:-}" in
+    ""|--help|-h)
+        usage
+        exit 0
+        ;;
+    --list)
+        list_catalogue
+        exit 0
+        ;;
+    --status)
+        show_status
+        exit 0
+        ;;
+    --all)
+        shift
+        [[ "${1:-}" == "--force" ]] && { FORCE=1; shift; }
+        provision_all
+        ;;
+    --force)
+        FORCE=1
+        shift
+        if [[ "${1:-}" == "--all" ]]; then
+            shift
+            provision_all
+        else
+            for name in "$@"; do
+                entry="$(find_entry "$name")" || { echo "unknown source: $name (run --list)"; exit 2; }
+                provision_one "$entry" || true
+            done
+        fi
+        ;;
+    *)
+        for name in "$@"; do
+            entry="$(find_entry "$name")" || { echo "unknown source: $name (run --list)"; exit 2; }
+            provision_one "$entry" || true
+        done
+        ;;
+esac
diff --git a/src/julia/run_training.jl b/src/julia/run_training.jl
index 7c38652b..93c8f54b 100644
--- a/src/julia/run_training.jl
+++ b/src/julia/run_training.jl
@@ -10,6 +10,14 @@
 #   data_dir  = training_data/
 #   save_dir  = models/neural/
 #
+# Environment overrides (see below):
+#   ECHIDNA_MAX_PROOF_STATES — cap on proof states loaded (default 200000 on
+#     GPU, 50000 on CPU).  Set to 0 to disable the cap and consume the entire
+#     expanded corpus; required when re-baselining after corpus growth.
+#   ECHIDNA_NUM_EPOCHS      — training epochs (default 30).
+#   ECHIDNA_NUM_NEGATIVES   — hard-negative premise samples per example
+#     (default 20).
+#
 # This script:
 #   1. Loads JSONL training data (proof states + premises)
 #   2. Builds vocabulary from the corpus
@@ -74,10 +82,24 @@ println("═══════════════════════
 println("Loading training data...")
 println("═══════════════════════════════════════════════════════════")
 
+# Default cap: 200k on GPU (enough to exercise the expanded corpus without
+# OOM on a 24GB card), 50k on CPU (keeps wall-clock finite).  An operator
+# re-baselining after corpus growth sets ECHIDNA_MAX_PROOF_STATES=0 to lift
+# the cap entirely.
+default_cap = has_gpu ? 200_000 : 50_000
+cap_env = get(ENV, "ECHIDNA_MAX_PROOF_STATES", "")
+max_proof_states = isempty(cap_env) ? default_cap : parse(Int, cap_env)
+# `load_training_data` treats any value `<= 0` as "load everything".
+cap_label = max_proof_states <= 0 ? "unlimited" : string(max_proof_states)
+println("  max_proof_states = $cap_label")
+
+num_negatives = parse(Int, get(ENV, "ECHIDNA_NUM_NEGATIVES", "20"))
+println("  num_negatives    = $num_negatives")
+
 train_data, val_data, vocab = load_training_data(data_dir;
     train_split=0.8f0,
-    max_proof_states=50000,  # Cap for reasonable training time
-    num_negatives=20
+    max_proof_states=max_proof_states,
+    num_negatives=num_negatives,
 )
 
 if isempty(train_data.examples)
@@ -101,8 +123,9 @@ println("Model created successfully")
 println()
 
 # Configure training
+num_epochs = parse(Int, get(ENV, "ECHIDNA_NUM_EPOCHS", "30"))
 training_config = TrainingConfig(
-    num_epochs=30,
+    num_epochs=num_epochs,
     learning_rate=1f-4,
     lr_schedule=:cosine,
     weight_decay=1f-5,
diff --git a/tests/live_prover_suite.rs b/tests/live_prover_suite.rs
index b613802b..3ab4cf8d 100644
--- a/tests/live_prover_suite.rs
+++ b/tests/live_prover_suite.rs
@@ -110,6 +110,15 @@ fn kind_label(kind: ProverKind) -> &'static str {
         ProverKind::Dafny => "Dafny",
         ProverKind::FStar => "F*",
         ProverKind::TLAPS => "TLAPS",
+        ProverKind::Tamarin => "Tamarin",
+        ProverKind::ProVerif => "ProVerif",
+        ProverKind::Metamath => "Metamath",
+        ProverKind::Twelf => "Twelf",
+        ProverKind::ORTools => "OR-Tools",
+        ProverKind::HOL4 => "HOL4",
+        ProverKind::ACL2 => "ACL2",
+        ProverKind::SCIP => "SCIP",
+        ProverKind::Imandra => "Imandra",
         _ => "<other>",
     }
 }
@@ -214,3 +223,65 @@ async fn live_tlaps_version() {
     // TLA+ Proof System's prover is `tlapm` (per provers/mod.rs).
     assert_version_reachable(ProverKind::TLAPS, "tlapm").await;
 }
+
+// ==========================================================================
+// Tier 3 — weekly.  Upstream-tarball or heavier-build provers.  Most of
+// these SKIP locally and in PR CI; the weekly tier3 matrix in
+// live-provers.yml provisions each binary in its own job before running
+// `cargo test ... <backend>`, so only the matching test runs per job.
+// ==========================================================================
+
+#[tokio::test]
+async fn live_tamarin_version() {
+    assert_version_reachable(ProverKind::Tamarin, "tamarin-prover").await;
+}
+
+#[tokio::test]
+async fn live_proverif_version() {
+    assert_version_reachable(ProverKind::ProVerif, "proverif").await;
+}
+
+#[tokio::test]
+async fn live_metamath_version() {
+    assert_version_reachable(ProverKind::Metamath, "metamath").await;
+}
+
+#[tokio::test]
+async fn live_twelf_version() {
+    // Twelf's CLI entry is `twelf-server` per provers/mod.rs.
+    assert_version_reachable(ProverKind::Twelf, "twelf-server").await;
+}
+
+#[tokio::test]
+async fn live_ortools_version() {
+    // Echidna's ORTools backend invokes `ortools_solve` (wrapper around the
+    // OR-Tools C++ solve CLI).  Provisioned via upstream tarball.
+    assert_version_reachable(ProverKind::ORTools, "ortools_solve").await;
+}
+
+#[tokio::test]
+async fn live_hol4_version() {
+    // HOL4 requires Poly/ML + a tree build; provisioning is deferred to
+    // Containerfile.  Test SKIPs on runners without `hol` on PATH.
+    assert_version_reachable(ProverKind::HOL4, "hol").await;
+}
+
+#[tokio::test]
+async fn live_acl2_version() {
+    // ACL2 requires a Common Lisp image; provisioning deferred to Containerfile.
+    assert_version_reachable(ProverKind::ACL2, "acl2").await;
+}
+
+#[tokio::test]
+async fn live_scip_version() {
+    // SCIP requires a cmake build of SCIP Optimization Suite; deferred to
+    // Containerfile.  Test SKIPs until provisioned.
+    assert_version_reachable(ProverKind::SCIP, "scip").await;
+}
+
+#[tokio::test]
+async fn live_imandra_version() {
+    // Imandra is proprietary; handled via vendor-supplied container where a
+    // licence is available.  Test SKIPs on public CI.
+    assert_version_reachable(ProverKind::Imandra, "imandra").await;
+}