docs(wave3): reconcile human + machine docs to verified backend reality

The Wave-3 fixes/verification were recorded in PR comments + commit
messages but the repo's own canonical docs still carried stale claims
(ProVerif 'OCaml via opam', Tamarin 'Haskell Stack', Metamath
'in-process pure-Rust', SCIP 'scipopt.org .deb'). Per CLAUDE.md
('record decisions there, not in chat') reconcile both:

- docs/handover/TODO.md (human): install-strategy table -> strategy
  *of record as shipped & verified*, +Status column, +Wave-3
  verification note (#74 resolved, imandra intentional).
- .machine_readable/6a2/STATE.a2ml (machine): wave-3-handover-hints +
  l3-status Wave-3 line rewritten to the verified reality with the
  exact at-source strategy per backend + 'VERIFIED REAL' markers.

No behaviour change; documentation only.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -834,7 +834,7 @@ changes = [
 l3-status-after-wave-2 = [
   "Wave-1 (Tier-1, every PR, 9 backends): DONE — landed in b022bf4.",
   "Wave-2 (Tier-2, nightly, 10 backends): DONE for 9; hol-light deferred to Wave-3.",
-  "Wave-3 (Tier-3, weekly, 9 backends: Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath): LANDED. All 9 Containerfiles in .containerization/ (Imandra is proprietary-gated stub). Justfile: container-build-tier3 + per-backend recipes. container-ci.yml: weekly tier3-container matrix job, 8 non-proprietary images, allow-fail, 90 min timeout for HOL4/ACL2.",
+  "Wave-3 (Tier-3, weekly, 9 backends: Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath): LANDED + RUNTIME-SMOKE-VERIFIED 2026-05-18 (PR #73, consolidated Containerfile.wave3). 8/8 non-proprietary backends confirmed REAL by exercising the binary in the built image — NOT trusting the build log (a green build had been hiding silent stubs: scip/tamarin dead-download, metamath missing libc6-dev, or-tools missing build-number, twelf/acl2 baked build paths, proverif opam-solve fail). All fixed at-source; #74 (proverif) resolved. Imandra is an INTENTIONAL honest licence-gated fail-loud stub (real adapter + Idris2 ABI proofs retained; KEEP decision). Justfile: container-build-tier3 + per-backend recipes. container-ci.yml: weekly tier3-container matrix job, 8 non-proprietary images, allow-fail, 90 min timeout for HOL4/ACL2.",
   "Wave-4 (Tier-4, quarterly, 19 backends): SCAFFOLD ONLY — placeholder tier4 job in live-provers.yml announces list. See wave-4-rationale for per-backend mock-only justification.",
 ]
 wave-4-rationale = {
@@ -858,16 +858,21 @@ wave-4-rationale = {
   Kissat = "SAT solver; binary available from GitHub; deferred pending DIMACS fixture set",
   Alloy = "Java-based relational model finder; no headless CLI mode without Alloy API; deferred",
 }
+# Strategy OF RECORD as actually shipped & runtime-smoke-verified in
+# .containerization/Containerfile.wave3 (2026-05-18; PR #73 commits
+# 63bacf0/6032f2e/981389a/faf05e9/ea2ce4b). 8/8 non-proprietary backends
+# verified REAL by exercising the binary in the built image (NOT the
+# build log); imandra is an intentional honest licence-gated stub.
 wave-3-handover-hints = [
-  "Tamarin: Haskell Stack build; prebuilt binaries from github.com/tamarin-prover/tamarin-prover/releases may work.",
-  "ProVerif: OCaml build via opam; consider the Docker image from INRIA.",
-  "Imandra: proprietary binary; needs signed registration before download.",
-  "SCIP: academic license now lifted; prebuilt .deb from scipopt.org.",
-  "OR-Tools: large C++ build; use the official ortools Python wheel's bundled binaries or the official .tar.gz release.",
-  "HOL4: Poly/ML + Moscow ML build; tractable but slow.",
-  "ACL2: Common Lisp (SBCL/CCL); prebuilt SBCL image + `make` is easiest.",
-  "Twelf: SML/NJ build.",
-  "Metamath: in-process pure-Rust verifier per stub-audit-result; external metamath binary is optional smoke-test scope only.",
+  "Tamarin: official SRI-CSL Maude 3.5.1 prebuilt (bookworm apt maude is 3.2, which tamarin-prover 1.12.0 REJECTS) + tamarin-prover prebuilt; both stages. VERIFIED REAL.",
+  "ProVerif: official INRIA source tarball proverif2.05 (bblanche.gitlabpages.inria.fr/proverif/), built with bookworm ocaml/ocaml-findlib/ocamlbuild + liblablgtk2-ocaml-dev (./build hard-fails without it), tar --no-same-owner (tarball numeric uid/gid vs container userns). NO opam. Resolves #74. VERIFIED REAL (Horn-clause resolution executed).",
+  "Imandra: proprietary binary; needs signed registration. INTENTIONAL honest fail-loud stub + documented IMANDRA_TOKEN-secret real-install path; real Rust adapter + Idris2 ABI proofs retained. KEEP (decision 2026-05-18). NOT counted as verified.",
+  "SCIP: official scipopt/scip GitHub portable bundle (scipopt.org download 403s anonymous). VERIFIED REAL (MIP solve).",
+  "OR-Tools: official C++ .tar.gz; asset name carries the build number — ARG ORTOOLS_BUILD must track it (v9.12 -> 4544). VERIFIED REAL (libortools present).",
+  "HOL4: Poly/ML build (trindemossen-2; kananaskis-15 was a phantom tag). VERIFIED REAL.",
+  "ACL2: Common Lisp (SBCL); build-in-place (not relocatable). VERIFIED REAL.",
+  "Twelf: SML/NJ build; build-in-place (heap path baked). VERIFIED REAL.",
+  "Metamath: official metamath-exe v0.198 source, gcc m*.c — REQUIRES libc6-dev (bookworm-slim gcc lacks libc headers). VERIFIED REAL.",
 ]
 
 [session-2026-04-24-pkg5-close]

docs/handover/TODO.md

@@ -57,17 +57,33 @@ licence-gated. Table below kept for the per-backend install strategy of record.
 
 Handover hints live in `.machine_readable/6a2/STATE.a2ml [wave-3-handover-hints]`.
 
-| Backend | Install strategy |
-|---------|------------------|
-| Tamarin | Haskell Stack build; try prebuilt binaries from `tamarin-prover/tamarin-prover/releases` first |
-| ProVerif | OCaml via opam; consider INRIA Docker image |
-| Imandra | Proprietary — needs signed registration. Gate on Imandra licence decision (see open questions). |
-| SCIP | Academic licence lifted; prebuilt `.deb` from scipopt.org |
-| OR-Tools | Large C++ build; use official ortools Python wheel's bundled binaries |
-| HOL4 | Poly/ML + Moscow ML build; tractable but slow |
-| ACL2 | Common Lisp (SBCL/CCL); prebuilt SBCL image + `make` |
-| Twelf | SML/NJ build |
-| Metamath | In-process pure-Rust verifier per `stub-audit-result`; external binary optional |
+Strategy of record below = **as actually shipped & runtime-smoke-verified
+in `.containerization/Containerfile.wave3`** (2026-05-18, PR #73). Every
+non-proprietary backend was confirmed real by running its binary in the
+built image, not by trusting the build log — see "Wave-3 verification"
+note after the table.
+
+| Backend | Install strategy (verified) | Status |
+|---------|------------------|--------|
+| Tamarin | Official `tamarin-prover` prebuilt + **official SRI-CSL Maude 3.5.1 prebuilt** (bookworm apt `maude` is 3.2, which tamarin-prover 1.12.0 rejects) | ✅ REAL |
+| ProVerif | **Official INRIA source tarball `proverif2.05`**, built with bookworm `ocaml`/`ocaml-findlib`/`ocamlbuild` + `liblablgtk2-ocaml-dev` (`./build` hard-fails without it), `tar --no-same-owner`. **No opam** (resolves #74) | ✅ REAL |
+| Imandra | Proprietary — signed registration required. **Intentional honest fail-loud stub** + documented `IMANDRA_TOKEN`-secret real-install path; real Rust adapter + Idris2 ABI proofs retained. Kept by decision 2026-05-18 | ⏸ stub (by design) |
+| SCIP | Official `scipopt/scip` GitHub portable bundle (scipopt.org download 403s anonymous) | ✅ REAL |
+| OR-Tools | Official C++ `.tar.gz`; asset name carries the build number — `ARG ORTOOLS_BUILD` must track it (v9.12 → 4544) | ✅ REAL |
+| HOL4 | Poly/ML build (`trindemossen-2`; `kananaskis-15` was a phantom tag) | ✅ REAL |
+| ACL2 | Common Lisp (SBCL); build-in-place (not relocatable) | ✅ REAL |
+| Twelf | SML/NJ build; build-in-place (heap path baked) | ✅ REAL |
+| Metamath | Official `metamath-exe` v0.198 source, `gcc m*.c` — **requires `libc6-dev`** (bookworm-slim `gcc` lacks libc headers) | ✅ REAL |
+
+**Wave-3 verification (2026-05-18, PR #73, `ea2ce4b`):** all 8
+non-proprietary backends runtime-smoke-verified REAL by exercising the
+binary in the built image — *not* trusting the build log. A green Wave-3
+build had been masking silent stubs (scip/tamarin dead-download,
+metamath missing `libc6-dev`, or-tools missing build-number,
+twelf/acl2 baked build paths, proverif opam-solve failure); all fixed
+at-source. **#74 (proverif opam) resolved.** Imandra remains the only
+stub — genuinely proprietary, honestly fail-loud, kept by decision
+(real adapter + Idris2 ABI proofs retained). No stub-theatre.
 
 ### Wave-4 (Tier-4 quarterly, 19 backends, allow-fail placeholder)