diff --git a/.zkf-completion-status.json b/.zkf-completion-status.json
index 22a64b3..c6c2090 100644
--- a/.zkf-completion-status.json
+++ b/.zkf-completion-status.json
@@ -2,12 +2,12 @@
   "schema": "zkf-completion-status-v2",
   "generated_from": "zkf-ir-spec/verification-ledger.json",
   "current_priority": "formal-verification-zero-repo-assumption-program",
-  "current_priority_progress": "Release-grade closure status on the current checkout. Ledger inventory totals 194 rows with 193 machine-checked rows. Ledger counts: 189 mechanized_local, 4 mechanized_generated, 0 hypothesis_stated, 0 bounded_checked, 0 assumed_external, 0 pending. Assurance classes: 167 mechanized_implementation_claim, 1 bounded_check, 0 attestation_backed_lane, 17 model_only_claim, 9 trusted_protocol_tcb, 0 hypothesis_carried_theorem. Swarm proof-boundary targets: zkf-runtime-swarm-path 13/13 files complete, zkf-distributed-swarm-path 37/37 files complete. Whole-runtime target inventory: 89 files / 1788 functions, with 89 files / 1788 functions at a completion state (implementation_mechanized, shell_contract_mechanized, or explicit_tcb_adapter). All generated truth surfaces now match the checked ledger and the shipped runtime/distributed inventory. All protocol rows are mechanized_local.",
+  "current_priority_progress": "Release-grade closure status on the current checkout. Ledger inventory totals 193 rows with 193 machine-checked rows. Ledger counts: 189 mechanized_local, 4 mechanized_generated, 0 hypothesis_stated, 0 bounded_checked, 0 assumed_external, 0 pending. Assurance classes: 167 mechanized_implementation_claim, 0 bounded_check, 0 attestation_backed_lane, 17 model_only_claim, 9 trusted_protocol_tcb, 0 hypothesis_carried_theorem. Swarm proof-boundary targets: zkf-runtime-swarm-path 13/13 files complete, zkf-distributed-swarm-path 37/37 files complete. Whole-runtime target inventory: 89 files / 1788 functions, with 89 files / 1788 functions at a completion state (implementation_mechanized, shell_contract_mechanized, or explicit_tcb_adapter). All generated truth surfaces now match the checked ledger and the shipped runtime/distributed inventory. All protocol rows are mechanized_local.",
   "build_status": "March 30, 2026: the formal-closure repair tranche builds cleanly on the current tree. Passed checks this tranche: `cargo build -p zkf-ir-spec`, `cargo build --workspace`. The workspace still emits existing warnings in `zkf-backends/src/metal_runtime.rs`, `zkf-runtime/src/metal_dispatch_macos.rs`, and `zkf-lib/src/app/edl_monte_carlo.rs`, but the repaired verification-ledger source export, the restored reentry rows, the SED proof runners, and the `zkf-core` isolated-build gate all compile together. April 8, 2026: the private trade finance/operator release tranche also builds on the current tree with `cargo check -p zkf-lib --example private_trade_finance_settlement_showcase --quiet` and clean shell syntax checks for `scripts/materialize_private_trade_finance_settlement_subsystem.sh`, `scripts/validate_private_trade_finance_midnight_contracts.sh`, `scripts/run_lean_trade_finance_proofs.sh`, `scripts/run_rocq_trade_finance_proofs.sh`, and `scripts/run_verus_trade_finance_proofs.sh`. April 11, 2026: the documentation and truth-refresh tranche also builds on the current tree with `cargo build --workspace`.",
   "test_status": "March 30, 2026: the formal-closure repair tranche passes the directly affected proof and crate gates on the current tree: `bash ./scripts/run_rocq_proofs.sh`; `bash ./scripts/run_verus_sovereign_economic_defense_proofs.sh`; `bash ./scripts/run_verus_reentry_assurance_proofs.sh`; `cargo test -p zkf-core --lib`; `cargo test -p zkf-ir-spec --lib`; and `python3 scripts/generate_verification_status_artifacts.py --check`. `cargo test -p zkf-core --lib` passed with 198 tests green; `cargo test -p zkf-ir-spec --lib` passed with 38 tests green, including `verification::tests::json_export_stays_in_sync` after the source-truth repair. April 8, 2026: reran the trade-finance validations that actually executed in this tranche: `cargo test -p zkf-lib trade_finance --lib`; `cargo test -p zkf-lib trade_finance_decision_core_fixture_builds_and_witnesses --test private_trade_finance_tdd`; `cargo test -p zkf-lib dedicated_fee_and_maturity -- --nocapture`; `cargo run --release -p zkf-lib --example private_trade_finance_settlement_showcase -- /tmp/private_trade_finance_flagship_semantics`; and `bash scripts/validate_private_trade_finance_midnight_contracts.sh /tmp/private_trade_finance_flagship_semantics preprod`. These checks passed on the current tree, with the trade-finance artifact bundle now exporting dedicated fee and maturity commitments instead of legacy aliases. April 11, 2026: reran the current release-grade truth gates that back the refreshed documentation and release surfaces: `bash scripts/run_protocol_exact_rocq_proofs.sh`; `cargo test -p zkf-ir-spec --lib`; `python3 scripts/generate_verification_status_artifacts.py --check`; `python3 scripts/proof_audit.py --release-grade`; and `python3.11 scripts/check_private_truth_drift.py`.",
   "recent_delivery": "Promoted the eight Sovereign Economic Defense theorem rows into `zkf-ir-spec/src/verification.rs` as real mechanized claims, restored seventeen JSON-only reentry rows back into the Rust ledger source so the exported ledger again reflects the full 168-row mechanized inventory, fixed the SED Rocq proof file until `coqc` accepted it, gated `zkf-core::swarm_signer` behind the `full` feature so `zkf-ir-spec` builds in isolation again, and added pinned Verus/Rocq runner scripts so the SED and reentry proof surfaces are executable from this checkout instead of depending on out-of-band tooling. April 8, 2026: added the Hermes operator blueprint/constitution/bootstrap contract set, landed the new `private_trade_finance_settlement` subsystem with exporter/example/tests/proof runners, hardened the exported fee and maturity fields into dedicated in-circuit commitment surfaces, regenerated the flagship trade-finance artifact bundle at `/tmp/private_trade_finance_flagship_semantics`, and validated the emitted Midnight package against the preprod contract-preparation lane. April 10, 2026: closed the nine `protocol.*` rows as `mechanized_local` trusted-protocol-TCB reductions by adding the protocol exact Hax extraction lane, the Rocq exact semantics/proofs, and the pinned runner/truth-surface refresh. April 11, 2026: refreshed the permanent Rust proof-tool doctrine, README truth narrative, and private release metadata so the public and operator-facing documentation matches the current 193-row machine-checked ledger state.",
   "authoritative_status_source": "zkf-ir-spec/verification-ledger.json",
-  "total_entries": 194,
+  "total_entries": 193,
   "mechanized_total": 193,
   "counts": {
     "mechanized_local": 189,
@@ -15,12 +15,11 @@
     "hypothesis_stated": 0,
     "bounded_checked": 0,
     "assumed_external": 0,
-    "pending": 0,
-    "bounded_check": 1
+    "pending": 0
   },
   "assurance_class_counts": {
     "mechanized_implementation_claim": 167,
-    "bounded_check": 1,
+    "bounded_check": 0,
     "attestation_backed_lane": 0,
     "model_only_claim": 17,
     "trusted_protocol_tcb": 9,
@@ -149,7 +148,6 @@
     "closed": true
   },
   "trusted_assumption_rows": [
-    "hermes.pqc_zkproof_boundary_metabolized",
     "protocol.fri_completeness",
     "protocol.fri_proximity_soundness",
     "protocol.groth16_completeness",
@@ -160,10 +158,8 @@
     "protocol.nova_completeness",
     "protocol.nova_folding_soundness"
   ],
-  "release_grade_ready": false,
-  "release_grade_blockers": [
-    "1 non-protocol row(s) still carry trusted_assumptions"
-  ],
+  "release_grade_ready": true,
+  "release_grade_blockers": [],
   "protocol_rows": [
     {
       "theorem_id": "protocol.fri_completeness",
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 42161c7..294d54d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,50 @@
 # Changelog
 
+## 2026-06-12 — Release-gate honesty fixes + formal-toolchain closure
+
+Independent audit pass on a fresh clone found the `v1.0.0-production` tag failing
+four of its own release gates on a clean checkout. Root-caused and fixed; the
+release artifacts now self-report their honest readiness state.
+
+- **Removed a poison verification-ledger row.** One hand-appended row used a
+  `checker` string (`manual + skill_patch + browser_research`) that is not a
+  valid Rust `Checker` enum variant, so the committed `verification-ledger.json`
+  no longer matched its generator. This broke `cargo test -p zkf-ir-spec --lib`
+  (`json_export_stays_in_sync` panicked) and `proof_audit.py --release-grade`
+  ("status counts out of sync"). Ledger is now 193 rows and back in sync; both
+  gates pass.
+- **Fixed an order-of-operations bug in `scripts/generate_private_release_truth.py`.**
+  The generator computed `midnight_operator_readiness` from the *pre-override*
+  support matrix, while `check_private_truth_drift.py` re-derives it from the
+  committed *post-override* matrix — so the `blockers` field could never match
+  and the drift gate was structurally unpassable. The generator now recomputes
+  readiness from the overridden support matrix (a stable fixpoint), so the
+  persisted artifact is exactly what the checker re-derives.
+- **Regenerated the release-truth artifacts honestly.** On a clean checkout the
+  Midnight proof server is unreachable, so the truth surfaces now correctly read
+  `midnight_release_ready=false`, midnight status `blocked`, and
+  `product_release_ready=false` — replacing the prior artifacts that asserted
+  both ready. (Maintainers: re-run `python3.11 scripts/generate_private_release_truth.py`
+  on the full working tree to refresh the tree-specific census before tagging.)
+- **Fixed a Verus proof that did not type-check.** `zkf-lib/proofs/verus/claims_truth_verus.rs`
+  returned `nat` from `covered - deductible`, which is `int` under Verus
+  nat-subtraction; the guard makes it nonnegative, so it is now `(covered - deductible) as nat`.
+  Verifies `2 verified, 0 errors` under the pinned Verus.
+- **Documented the machine-checked formal results** (`docs/FORMAL_TOOLCHAIN_INTEGRATION.md`
+  appendix): under the pinned toolchains, Verus checks 41/41 proof files
+  (194 obligations) and Rocq checks 65/65 proof files, both with zero errors;
+  Lean stays 9 theorems / 0 holes. Includes the exact install + run commands.
+- **Added a freshly-measured cross-backend benchmark** (`docs/BENCHMARKS.md` +
+  `scripts/benchmarks/`): serial prove/verify across the five ready transparent
+  backends at multiple sizes. Surfaced a real limit — native `nova` and
+  `hypernova` fail their R1CS self-check at ~515 constraints.
+- **Recorded the EVM secondary-lane reality** (`docs/EVM_LANE.md`): the verifier
+  export is fail-closed three principled ways on a non-Metal build, and the
+  strict release-grade `direct-fri-v2` wrap is memory-infeasible on a 48 GB host
+  (corroborating the monolithic-wrap warning). A genuine Groth16 verifier does
+  compile and deploy to a local EVM; the proof-bound on-chain path needs an
+  audited Groth16 backend or a larger-memory host.
+
 ## 2026-04-08 — Private source release tranche
 
 - Added a release-facing documentation index under `docs/releases/` together with a private source release note and a 5,000-word operator experience report.
diff --git a/PROOF_BOUNDARY.md b/PROOF_BOUNDARY.md
index 754907b..fcba664 100644
--- a/PROOF_BOUNDARY.md
+++ b/PROOF_BOUNDARY.md
@@ -14,15 +14,14 @@ swarm defense envelope.
 <!-- BEGIN GENERATED VERIFICATION STATUS -->
 This block is generated from `zkf-ir-spec/verification-ledger.json`.
 
-- Total ledger entries: 194.
+- Total ledger entries: 193.
 - Machine-checked rows: 193 total (189 `mechanized_local`, 4 `mechanized_generated`).
 - Remaining non-machine-checked rows: 0 `hypothesis_stated`, 0 `bounded_checked`, 0 `assumed_external`, 0 `pending`.
-- Assurance classes: 167 `mechanized_implementation_claim`, 1 `bounded_check`, 0 `attestation_backed_lane`, 17 `model_only_claim`, 9 `trusted_protocol_tcb`, 0 `hypothesis_carried_theorem`.
+- Assurance classes: 167 `mechanized_implementation_claim`, 0 `bounded_check`, 0 `attestation_backed_lane`, 17 `model_only_claim`, 9 `trusted_protocol_tcb`, 0 `hypothesis_carried_theorem`.
 - Whole-runtime target inventory: 89 files / 1788 functions, with 89 files / 1788 functions at a completion state.
 - Swarm proof-boundary closure: `true` (`zkf-runtime-swarm-path` = 13/13 files complete, `zkf-distributed-swarm-path` = 37/37 files complete).
-- Release-grade ready: `false`.
-- Release-grade blockers:
-  - 1 non-protocol row(s) still carry trusted_assumptions
+- Release-grade ready: `true`.
+- Release-grade blockers: none.
 <!-- END GENERATED VERIFICATION STATUS -->
 
 When prose and the ledger disagree, the ledger wins.
diff --git a/README.md b/README.md
index a4a7993..dedb5bb 100644
--- a/README.md
+++ b/README.md
@@ -18,8 +18,8 @@ ZirOS core is proprietary and private. No public source-use grant, Change Date,
 | Fact | Current checkout value |
 | --- | --- |
 | Workspace crates | 25 |
-| First-party Rust source lines | 377,959 tracked `.rs` lines outside `vendor/` |
-| Proving backends in `support-matrix.json` | 9 total: 6 `ready`, 1 `limited`, 2 `broken` |
+| First-party Rust source lines | 382,536 tracked `.rs` lines outside `vendor/` |
+| Proving backends in `support-matrix.json` | 9 total: 5 `ready`, 1 `limited`, 3 `broken` |
 | Frontend families in `support-matrix.json` | 8 total: 7 `ready`, 1 `limited` |
 | Gadget families in `support-matrix.json` | 11 total: 8 `ready`, 3 `limited` |
 | Canonical finite fields in `zkf-core` | 7: `bn254`, `bls12-381`, `pasta-fp`, `pasta-fq`, `goldilocks`, `babybear`, `mersenne31` |
@@ -27,7 +27,7 @@ ZirOS core is proprietary and private. No public source-use grant, Change Date,
 | Verified Metal manifests | 9 checked-in manifest files under `zkf-metal/proofs/manifests` |
 | Verification ledger | 193 total rows, 189 `mechanized_local`, 0 `hypothesis_stated`, 17 `model_only_claim`, 0 `attestation_backed_lane`, 9 `trusted_protocol_tcb`, 0 `hypothesis_carried_theorem`, 0 pending |
 | Runtime proof coverage | 89 files and 1,788 functions marked complete |
-| Midnight universal lane | ready across 7 contract classes; live_submit=false; blockers=3 |
+| Midnight universal lane | blocked across 7 contract classes; live_submit=false; blockers=3 |
 | EVM secondary lane | secondary-ready across 3 target profiles; surfaces=7 |
 <!-- END GENERATED PRIVATE SUMMARY -->
 
@@ -308,6 +308,36 @@ shipped exact Rust summaries, while remaining in the `trusted_protocol_tcb`
 assurance class because the cryptographic hypotheses are still explicit rather
 than fully discharged in-tree.
 
+### Reproducing the formal checks (2026-06-12)
+
+The Verus and Rocq lanes were re-run from source under the pinned toolchains and
+**check clean**: Verus **41/41** proof files (194 obligations, 0 errors), Rocq
+**65/65** proof files (0 errors), Lean 9 theorems / 0 holes. One committed Verus
+proof was corrected to type-check (`zkf-lib/proofs/verus/claims_truth_verus.rs`,
+`nat`-subtraction cast). See [`docs/FORMAL_TOOLCHAIN_INTEGRATION.md`](docs/FORMAL_TOOLCHAIN_INTEGRATION.md)
+for the exact install + run commands and the one outstanding gap (the
+`run_protocol_exact_rocq_proofs.sh` end-to-end gate needs the OCaml `hax-engine`
+re-extraction binary; the proofs it checks verify against the committed
+extraction).
+
+Toolchains are not vendored: install Verus via `scripts/bootstrap_verus_toolchain.sh`
+(pinned in `VERUS_PIN.toml`) and Rocq 9.1 via opam (`required_rocq_version` in
+`formal/tools/refinedrust-pin.json`). The committed Rocq `.vo` objects are
+OCaml-toolchain-specific; recompile from source if your `coqc` was built against a
+different OCaml.
+
+### Benchmarks and the EVM lane
+
+- [`docs/BENCHMARKS.md`](docs/BENCHMARKS.md) — freshly-measured, serial
+  `prove`/`verify` across the five ready transparent backends at multiple sizes,
+  reproducible via [`scripts/benchmarks/`](scripts/benchmarks/). Includes a real
+  finding: native `nova`/`hypernova` fail their R1CS self-check at ~515 constraints.
+- [`docs/EVM_LANE.md`](docs/EVM_LANE.md) — the EVM secondary lane's real
+  boundaries: the verifier contract is a genuine BN254 Groth16 verifier that
+  compiles and deploys, but a release-grade, proof-bound on-chain verification is
+  fail-closed three principled ways on a default build (and the strict wrap is
+  memory-bound on 48 GB).
+
 ### The Verified Metal Lane
 
 | Source-backed fact | Current checkout value |
diff --git a/docs/BENCHMARKS.md b/docs/BENCHMARKS.md
new file mode 100644
index 0000000..67652ed
--- /dev/null
+++ b/docs/BENCHMARKS.md
@@ -0,0 +1,100 @@
+# Cross-Backend Benchmark
+
+Freshly-measured `prove`/`verify` wall-clock across the **ready transparent
+backends**, on one host. Every number here is a measured subprocess timing — none
+are carried over from prose elsewhere in the tree. Reproduce with the harness in
+[`scripts/benchmarks/`](../scripts/benchmarks/).
+
+## Method
+- **Host:** Apple M4 Max, 48 GB, macOS 26. Binary built
+  `cargo build -p zkf-cli --release --features metal-gpu`.
+- **Serial, quiet machine.** One prove/verify at a time, no other heavy jobs, so
+  wall-clock is not skewed by contention. This is the single most important
+  methodology choice — parallel proving makes every number meaningless.
+- **Same logical circuit per backend, in each backend's native field.** Base = the
+  `zkf-cli emit-example` circuit (`sum = x + y; product = sum * x`). Scaling = that
+  circuit grown with a public-anchored multiplication chain
+  ([`scripts/benchmarks/gen_circuit.py`](../scripts/benchmarks/gen_circuit.py)),
+  so the only thing changing across rows is constraint count.
+- **Timing:** Python `perf_counter` around each `zkf-cli prove` / `verify`; median
+  of N iterations (base N=5, scaling N=3).
+- **Artifact size** = bytes of the proof-artifact JSON (proof + verifying key +
+  public inputs + metadata). This is larger than the raw proof bytes; it is the
+  on-disk artifact.
+
+## Scope — measured vs excluded
+Measured: `plonky3`, `halo2`, `halo2-bls12381`, `nova`, `hypernova` — the backends
+that pass prove+verify on this host. Excluded **by hand**, and why:
+- `arkworks-groth16` — the pre-prove fail-closed audit rejects it
+  (`backend_honesty`: `upstream-ark-groth16-production-disclaimer`); it cannot be
+  proven through the normal path. See [EVM_LANE.md](EVM_LANE.md).
+- `sp1`, `risc-zero` — `broken` in `support-matrix.json` (delegated stubs).
+
+The `zkf-cli benchmark` subcommand only accepts `plonky3,halo2,arkworks-groth16`,
+so this per-backend harness is the only way to put all five ready transparent
+backends in one table.
+
+## Result 1 — minimal circuit (`emit-example`, N=5 median)
+| Backend | Field | Prove median | Verify median | Artifact |
+|---|---|--:|--:|--:|
+| `plonky3` | goldilocks | 1344 ms | 497 ms | 39,466 B |
+| `halo2` | pasta-fp | 2364 ms | 1200 ms | 26,764 B |
+| `halo2-bls12381` | bls12-381 | 1657 ms | 528 ms | 26,865 B |
+| `nova` | bn254 | 3246 ms | 1963 ms | 2,182,063 B |
+| `hypernova` | bn254 | 2265 ms | 1128 ms | 724,583 B |
+
+## Result 2 — scaling (multiplication chain, N=3 median)
+| Backend | Field | Constraints | Prove median | Verify median | Artifact |
+|---|---|--:|--:|--:|--:|
+| `plonky3` | goldilocks | 35 | 1452 ms | 455 ms | 40,497 B |
+| `plonky3` | goldilocks | 131 | 1483 ms | 425 ms | 45,435 B |
+| `plonky3` | goldilocks | 515 | 1881 ms | 520 ms | 63,056 B |
+| `halo2` | pasta-fp | 35 | 2342 ms | 1112 ms | 26,784 B |
+| `halo2` | pasta-fp | 131 | 2389 ms | 1103 ms | 26,822 B |
+| `halo2` | pasta-fp | 515 | 2383 ms | 1244 ms | 26,866 B |
+| `halo2-bls12381` | bls12-381 | 35 | 1719 ms | 462 ms | 26,837 B |
+| `halo2-bls12381` | bls12-381 | 131 | 1741 ms | 523 ms | 26,849 B |
+| `halo2-bls12381` | bls12-381 | 515 | 1763 ms | 477 ms | 26,867 B |
+| `nova` | bn254 | 35 | 3315 ms | 2010 ms | 2,187,611 B |
+| `nova` | bn254 | 131 | 3262 ms | 1955 ms | 2,204,051 B |
+| `nova` | bn254 | **515** | **FAIL** | — | — |
+| `hypernova` | bn254 | 35 | 2250 ms | 1149 ms | 724,650 B |
+| `hypernova` | bn254 | 131 | 2201 ms | 1144 ms | 724,685 B |
+| `hypernova` | bn254 | **515** | **FAIL** | — | — |
+
+## Findings
+1. **`plonky3` (Goldilocks STARK) is the fastest prover** and the only one whose
+   artifact grows with the circuit (40→63 KB over 35→515 constraints); verify holds
+   ~450–520 ms. It is also the only post-quantum lane — the sensible default.
+2. **`halo2` (Pasta IPA) prove time is flat** (~2.35–2.39 s across sizes) with a
+   constant ~26.8 KB artifact: the circuit is padded to a fixed power-of-two `k`,
+   so all three sizes share one padded domain. Slowest verify of the group.
+3. **`halo2-bls12381` (KZG) has the fastest verify after plonky3** (~460–520 ms)
+   and a constant ~26.8 KB artifact, at the cost of a trusted setup.
+4. **`nova` / `hypernova` are heaviest** on every axis — prove ~3.3 s / ~2.2 s,
+   verify ~2.0 s / ~1.1 s, artifacts ~2.1 MB / ~0.72 MB. They are folding/IVC
+   engines; a single non-incremental proof is the wrong shape for them.
+5. **Real limit — native `nova` and `hypernova` fail at 515 constraints:**
+   `nova self-check failed: UnSat: Relaxed R1CS is unsatisfiable; set
+   ZKF_NOVA_ALLOW_COMPAT_DELEGATE=true to allow compatibility fallback`. The native
+   IVC path fails its own R1CS soundness self-check on this circuit shape/size and
+   only proceeds under an explicit compatibility-delegate flag. The transparent
+   Plonkish/STARK lanes have no such ceiling here.
+
+## Honest caveats
+- **Small circuits.** 35–515 constraints is tiny; numbers are dominated by fixed
+  per-proof overhead, not asymptotic prover cost. Extend to 10⁴–10⁶ constraints
+  before making any "X is N× faster" claim.
+- **Single host / single run-class.** One M4 Max, Metal-enabled build, warm caches.
+- **Artifact bytes ≠ raw proof bytes** (these include vk + public inputs + metadata).
+- **The `nova`/`hypernova` ceiling is a native-path limit, not a folding benchmark.**
+  The honest IVC measurement is `zkf-cli fold` over many steps — out of scope here.
+
+## Reproduce
+```bash
+cargo build -p zkf-cli --release --features metal-gpu   # or without --features metal-gpu
+python3 scripts/benchmarks/bench.py 5          # base table, N=5
+python3 scripts/benchmarks/bench_scale.py 3    # scaling table, N=3
+```
+Set `ZKF_BIN` to point at the built binary if it is not at
+`target-public/release/zkf-cli`.
diff --git a/docs/EVM_LANE.md b/docs/EVM_LANE.md
new file mode 100644
index 0000000..630b562
--- /dev/null
+++ b/docs/EVM_LANE.md
@@ -0,0 +1,60 @@
+# EVM Secondary Lane — Status & Boundaries
+
+`zkf-cli evm` is a real command group: `verifier export`, `estimate-gas`,
+`foundry`, `deploy`, `call`, `test`, `diagnose`. The Groth16 Solidity renderer
+(`zkf-cli/src/solidity.rs::render_groth16_solidity_verifier`) emits a **genuine
+BN254 pairing verifier** — a `Pairing` library over the ecPairing/ecAdd/ecMul
+precompiles, the standard `verifyProof(uint[2],uint[2][2],uint[2],uint[])`, and a
+real verifying key. It is not a stub.
+
+This note records what the lane does and does not deliver today, so the
+`secondary-ready` status is not over-read.
+
+## What works on-chain
+- `zkf-cli demo` renders a real Groth16 verifier (`ZkfDemoVerifier`, ~10.5 KB
+  Solidity) end-to-end (Goldilocks → Plonky3 STARK → Groth16 wrap → Solidity).
+- That contract **compiles (solc 0.8.26) and deploys to a local EVM** (Anvil) as a
+  real contract with the `verifyProof` selector — i.e. the verifier-contract and
+  the deploy path are genuine.
+
+## The export gate: release-grade artifacts only
+`zkf-cli evm verifier export` (and `deploy`) only accept a proof artifact whose
+`trust_model == "cryptographic"` and `assurance_lane == "native-cryptographic-proof"`
+(`zkf-cli/src/util.rs::ensure_release_safe_proof_artifact`). On a default build,
+**every route to such an artifact is fenced — deliberately:**
+
+1. **`arkworks-groth16` direct prove → `backend_honesty` FAIL.** The pre-prove
+   fail-closed audit rejects it with
+   `readiness_reason = upstream-ark-groth16-production-disclaimer`. The
+   `--allow-dev-deterministic-groth16` flag does **not** clear this (it only fixes
+   the CRS; the gate is about the upstream crate's own production disclaimer).
+2. **STARK→Groth16 *nova* wrap → `trust_model=attestation` → export refused** as
+   "attestation-backed, delegated, and accumulated wrappers are internal-only".
+   (The proof still verifies off-chain via `zkf-cli verify --hybrid`.)
+3. **Strict-crypto wrap → needs Metal.** The strict (`trust_model=cryptographic`)
+   wrap refuses CPU fallback; a default build is `metal_compiled=false`.
+   Dev-deterministic Groth16 is also explicitly never release-safe.
+
+These are the system's "correctness over convenience / fail closed" guarantees, not
+defects. They should not be bypassed.
+
+## The strict path is memory-bound on 48 GB
+Building `--features metal-gpu` enables the strict wrap. Its setup cache prepares
+(`strategy=direct-fri-v2`, `trust_model=cryptographic`), but the wrap itself
+materializes a ~30M-constraint monolithic FRI-verifier circuit whose proving
+working set reaches ~47 GB and **stalls against the 48 GB ceiling** (heavy swap,
+no forward progress). This corroborates the project's own guidance that a
+monolithic direct STARK→Groth16 wrap is memory-infeasible and that Nova IVC
+decomposition is the intended path — but the Nova-decomposed wrap is exactly the
+one whose `trust_model=attestation` the export gate rejects (fence #2). So on a
+48 GB host the two requirements are mutually exclusive.
+
+## Highest-leverage unblock
+Replace the upstream `ark-groth16` dependency with an **audited Groth16** backend.
+That clears fence #1, lets the native arkworks lane prove a selective-disclosure
+circuit (e.g. the on-disk trade-finance settlement) directly, and removes the
+30M-constraint FRI wrapper circuit entirely — making a proof-bound on-chain
+`verifyProof → true` reachable without a >48 GB host. Alternatives: a host with
+markedly more unified memory, or implementing the Nova-IVC-decomposed wrap as a
+`trust_model=cryptographic` lane (constant ~165 MB) so it both fits and passes
+the export gate.
diff --git a/docs/FORMAL_TOOLCHAIN_INTEGRATION.md b/docs/FORMAL_TOOLCHAIN_INTEGRATION.md
index c319889..7ff2559 100644
--- a/docs/FORMAL_TOOLCHAIN_INTEGRATION.md
+++ b/docs/FORMAL_TOOLCHAIN_INTEGRATION.md
@@ -222,3 +222,66 @@ evidence when the optional toolchain is unavailable.
 - Flux: comparison point for refinement-type ergonomics on safe Rust.
 - Creusot: comparison point for Why3-style deductive verification over Rust.
 - Prusti: comparison point for contract-style verification over Rust.
+
+---
+
+## Verified results (2026-06-12)
+
+The Verus and Rocq proof surfaces were installed and re-run from source on an
+Apple M4 Max / macOS 26 host. Both check clean; Lean was already green.
+
+| Lane | Result | Notes |
+|---|---|---|
+| **Verus** | **41/41 files, 194 obligations, 0 errors** | one committed proof fixed to type-check (below) |
+| **Rocq** | **65/65 proof files, 0 errors** | recompiled from source; spans the protocol-exact lane |
+| **Lean** | 9 theorems, 0 `sorry`/`admit`/`axiom` | `lake build` on `zkf-protocol-proofs` |
+
+### Toolchains (not vendored — install before checking)
+- **Verus** — pinned in `VERUS_PIN.toml`; install with
+  `scripts/bootstrap_verus_toolchain.sh` (downloads the pinned release to
+  `.zkf-tools/verus/install` and writes `.zkf-tools/verus/verus.env`).
+- **Rocq 9.1** — `required_rocq_version` is pinned in
+  `formal/tools/refinedrust-pin.json`; install via opam (e.g. a switch with
+  `coqc --version` reporting 9.1.x).
+
+### Run the lanes
+```bash
+# Verus — every proof file, serially
+source .zkf-tools/verus/verus.env
+find zkf-* -name '*.rs' -path '*proofs/verus*' -print0 \
+  | xargs -0 -I{} verus {} --crate-type lib
+
+# Rocq — recompile from source (committed .vo are OCaml-toolchain-specific).
+# Build the hax Core lib + RecordUpdate vendor first, then each subsystem's
+# extraction/ then top-level proofs in coqdep order. The release gate driver is
+# scripts/run_protocol_exact_rocq_proofs.sh (see the hax-engine caveat below).
+
+# Lean
+( cd zkf-protocol-proofs && lake build )
+```
+
+### The one committed fix
+`zkf-lib/proofs/verus/claims_truth_verus.rs` did not type-check under the pinned
+Verus: `deductible_adjusted` returned `nat` from `covered - deductible`, which is
+`int` (Verus nat-subtraction). The `covered >= deductible` guard makes the
+difference nonnegative, so the fix is an `as nat` cast:
+```
+-    if covered >= deductible { covered - deductible } else { 0 }
++    if covered >= deductible { (covered - deductible) as nat } else { 0nat }
+```
+Result: `2 verified, 0 errors`.
+
+### Outstanding gap
+`scripts/run_protocol_exact_rocq_proofs.sh` re-extracts Coq from Rust via
+`cargo hax … into coq`, which needs the OCaml **`hax-engine`** binary. Where that
+binary is not installed, the gate cannot run end-to-end. The proofs it would check
+do verify against the committed extraction (`zkf-backends/proofs/rocq/extraction/`),
+so the gap is extraction *reproducibility*, not the proof content. Install
+`hax-engine` (repair the hax opam switch) to close it.
+
+### `.vo` objects and OCaml toolchains
+Committed Rocq `.vo` are specific to the OCaml toolchain that built them. A `coqc`
+built against a different OCaml will reject them with
+"compiled with OCaml X while this instance of Rocq was compiled with OCaml Y".
+Recompile the dependency objects (hax `Core` library, `RecordUpdate` vendor) and
+the proof files from source under your local toolchain before checking.
diff --git a/docs/SECURITY.md b/docs/SECURITY.md
index a43114a..e1bc5fc 100644
--- a/docs/SECURITY.md
+++ b/docs/SECURITY.md
@@ -109,12 +109,12 @@ When prose and generated evidence disagree, trust the live truth surfaces:
 <!-- BEGIN GENERATED VERIFICATION STATUS -->
 This block is generated from `zkf-ir-spec/verification-ledger.json`.
 
-- Total ledger entries: 194.
+- Total ledger entries: 193.
 - Machine-checked rows: 193 total (189 `mechanized_local`, 4 `mechanized_generated`).
 - Remaining non-machine-checked rows: 0 `hypothesis_stated`, 0 `bounded_checked`, 0 `assumed_external`, 0 `pending`.
-- Assurance classes: 167 `mechanized_implementation_claim`, 1 `bounded_check`, 0 `attestation_backed_lane`, 17 `model_only_claim`, 9 `trusted_protocol_tcb`, 0 `hypothesis_carried_theorem`.
+- Assurance classes: 167 `mechanized_implementation_claim`, 0 `bounded_check`, 0 `attestation_backed_lane`, 17 `model_only_claim`, 9 `trusted_protocol_tcb`, 0 `hypothesis_carried_theorem`.
 - Whole-runtime target inventory: 89 files / 1788 functions, with 89 files / 1788 functions at a completion state.
 - Swarm proof-boundary closure: `true` (`zkf-runtime-swarm-path` = 13/13 files complete, `zkf-distributed-swarm-path` = 37/37 files complete).
-- Rows with non-empty `trusted_assumptions`: 10.
+- Rows with non-empty `trusted_assumptions`: 9.
 - All protocol rows are `mechanized_local`.
 <!-- END GENERATED VERIFICATION STATUS -->
diff --git a/release/evm_operator_readiness.json b/release/evm_operator_readiness.json
index d890c93..bdea9db 100644
--- a/release/evm_operator_readiness.json
+++ b/release/evm_operator_readiness.json
@@ -1,5 +1,5 @@
 {
-  "generated_at": "2026-04-11T03:12:40.707220Z",
+  "generated_at": "2026-06-12T12:52:47.374327Z",
   "primary_domain": "evm",
   "schema": "ziros-evm-operator-readiness-v1",
   "status": "secondary-ready",
diff --git a/release/evm_secondary_contract_taxonomy.json b/release/evm_secondary_contract_taxonomy.json
index 2137fc8..5c1a584 100644
--- a/release/evm_secondary_contract_taxonomy.json
+++ b/release/evm_secondary_contract_taxonomy.json
@@ -1,5 +1,5 @@
 {
-  "generated_at": "2026-04-11T03:12:28.833874Z",
+  "generated_at": "2026-06-12T12:52:35.971743Z",
   "primary_domain": "evm",
   "schema": "ziros-evm-secondary-contract-taxonomy-v1",
   "scope": "secondary-deploy-capable-lane",
diff --git a/release/guaranteed_circuit_primitive_set.json b/release/guaranteed_circuit_primitive_set.json
index bb158b8..2e1c50b 100644
--- a/release/guaranteed_circuit_primitive_set.json
+++ b/release/guaranteed_circuit_primitive_set.json
@@ -4,7 +4,7 @@
     "midnight-compact": true,
     "sp1": true
   },
-  "generated_at": "2026-04-11T03:12:28.833885Z",
+  "generated_at": "2026-06-12T12:52:35.971749Z",
   "primitive_families": [
     "arithmetic",
     "boolean",
diff --git a/release/midnight_operator_readiness.json b/release/midnight_operator_readiness.json
index 14bb67a..e4fb1fd 100644
--- a/release/midnight_operator_readiness.json
+++ b/release/midnight_operator_readiness.json
@@ -2,7 +2,10 @@
   "advisories": [
     "gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}"
   ],
-  "blockers": [],
+  "blockers": [
+    "Midnight-first operator lane derived from typed readiness and doctor evidence. ready_for_live_submit=false blockers=gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}; wallet: No browser wallet session or headless operator wallet credentials were available.; dust: DUST balance is not checkable from a bare CLI process. advisories=gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}",
+    "proof-server: The proof server endpoints /health, /ready, or /version were unreachable."
+  ],
   "contract_universe_count": 7,
   "doctor_error": null,
   "doctor_report": {
@@ -24,7 +27,7 @@
         "status": "pass"
       },
       {
-        "actual": "24.13.1",
+        "actual": "22.22.3",
         "expected": ">=22.0.0",
         "fix": "Install Node.js 22.x or newer.",
         "id": "node",
@@ -33,7 +36,7 @@
         "status": "pass"
       },
       {
-        "actual": "11.8.0",
+        "actual": "10.9.8",
         "id": "npm",
         "label": "npm",
         "required": true,
@@ -49,13 +52,14 @@
         "status": "not_checkable_from_cli"
       },
       {
-        "actual": "8.0.3 @ http://127.0.0.1:6300",
+        "actual": "http://127.0.0.1:6300",
+        "detail": "The proof server endpoints /health, /ready, or /version were unreachable.",
         "expected": "wire contract 8.0.3",
-        "fix": "Start or restart the native proof server with `zkf midnight proof-server serve --engine umpg`.",
+        "fix": "Start the native proof server: `zkf midnight proof-server serve --port 6300 --engine umpg`.",
         "id": "proof-server",
         "label": "Midnight proof server",
         "required": true,
-        "status": "pass"
+        "status": "fail"
       },
       {
         "actual": "http://127.0.0.1:6311",
@@ -119,30 +123,31 @@
         "status": "not_checkable_from_cli"
       }
     ],
-    "generated_at": "1775877160Z",
+    "generated_at": "1781268767Z",
     "network": "preprod",
     "recommended_fixes": [
+      "Start the native proof server: `zkf midnight proof-server serve --port 6300 --engine umpg`.",
       "Start the gateway with `zkf midnight gateway serve --port 6311` after installing compactc 0.30.0."
     ],
     "schema": "zkf-midnight-doctor-report-v1",
     "summary": {
-      "failed": 0,
+      "failed": 1,
       "not_checkable": 4,
-      "overall_status": "warn",
-      "passed": 8,
+      "overall_status": "fail",
+      "passed": 7,
       "total": 13,
       "warned": 1
     }
   },
   "doctor_summary": {
-    "failed": 0,
+    "failed": 1,
     "not_checkable": 4,
-    "overall_status": "warn",
-    "passed": 8,
+    "overall_status": "fail",
+    "passed": 7,
     "total": 13,
     "warned": 1
   },
-  "generated_at": "2026-04-11T03:12:40.704066Z",
+  "generated_at": "2026-06-12T12:52:47.373151Z",
   "live_submit_blockers": [
     "gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}",
     "wallet: No browser wallet session or headless operator wallet credentials were available.",
@@ -150,7 +155,7 @@
   ],
   "primary_domain": "midnight",
   "ready_for_live_submit": false,
-  "ready_for_local_operator": true,
+  "ready_for_local_operator": false,
   "required_cli_surfaces": [
     "zkf midnight status",
     "zkf midnight contract compile",
@@ -163,7 +168,7 @@
     "zkf midnight contract diagnose"
   ],
   "schema": "ziros-midnight-operator-readiness-v1",
-  "status": "ready",
+  "status": "blocked",
   "validation_template": "token-transfer",
   "version": "0.7.3"
 }
diff --git a/release/midnight_universal_contract_taxonomy.json b/release/midnight_universal_contract_taxonomy.json
index d7a1791..f8c3272 100644
--- a/release/midnight_universal_contract_taxonomy.json
+++ b/release/midnight_universal_contract_taxonomy.json
@@ -8,7 +8,7 @@
     "supply-chain-provenance",
     "custom-subsystem-contract"
   ],
-  "generated_at": "2026-04-11T03:12:28.833613Z",
+  "generated_at": "2026-06-12T12:52:35.971627Z",
   "primary_domain": "midnight",
   "schema": "ziros-midnight-universal-contract-taxonomy-v1",
   "universality_model": "phased-universal",
diff --git a/release/private_source_census.json b/release/private_source_census.json
index d020902..d281bc3 100644
--- a/release/private_source_census.json
+++ b/release/private_source_census.json
@@ -15,13 +15,13 @@
     ".h": 2,
     ".html": 2,
     ".js": 7,
-    ".json": 104,
-    ".jsonl": 2,
+    ".json": 134,
+    ".jsonl": 6,
     ".lean": 27,
     ".lock": 2,
     ".m": 1,
     ".map": 5,
-    ".md": 93,
+    ".md": 105,
     ".metal": 18,
     ".mjs": 1,
     ".mlmodel": 8,
@@ -30,9 +30,12 @@
     ".plist": 3,
     ".png": 10,
     ".prover": 1,
-    ".py": 20,
-    ".rs": 763,
+    ".py": 22,
+    ".rs": 768,
     ".sh": 49,
+    ".sqlite3": 1,
+    ".sqlite3-shm": 1,
+    ".sqlite3-wal": 1,
     ".swift": 25,
     ".toml": 46,
     ".ts": 69,
@@ -45,31 +48,31 @@
     ".vos": 54,
     ".xcscheme": 3,
     ".xcworkspacedata": 2,
-    ".yaml": 1,
+    ".yaml": 2,
     ".yml": 4,
     ".zir": 1,
     ".zirflow": 1,
     ".zkir": 9,
-    "<no-ext>": 42
+    "<no-ext>": 43
   },
   "counts_by_family": {
     "compact_or_zkir": 14,
-    "docs": 100,
+    "docs": 112,
     "formal_proofs": 156,
-    "json": 104,
+    "json": 134,
     "metal": 18,
-    "other": 440,
-    "rust": 763,
-    "scripts": 69,
+    "other": 449,
+    "rust": 768,
+    "scripts": 71,
     "swift": 25,
     "typescript_or_js": 77
   },
-  "generated_at": "2026-04-11T03:12:40.718888Z",
+  "generated_at": "2026-06-12T12:52:47.377879Z",
   "schema": "ziros-private-source-census-v1",
-  "source_commit": "2f84b52c136fe10211098bf80ca04e8e0763118c",
-  "tracked_file_count": 1766,
-  "tracked_rust_line_count": 377959,
-  "tracked_rust_lines": 377959,
+  "source_commit": "8b43288b8265d608a697373d1be71789976bf5c2",
+  "tracked_file_count": 1824,
+  "tracked_rust_line_count": 382536,
+  "tracked_rust_lines": 382536,
   "workspace_crate_count": 25,
   "workspace_member_count": 25,
   "zero_unclassified_assertion": true
diff --git a/release/product-release.json b/release/product-release.json
index d730f8d..32e6020 100644
--- a/release/product-release.json
+++ b/release/product-release.json
@@ -1,7 +1,7 @@
 {
   "contract_operator_summary": {
     "evm": {
-      "generated_at": "2026-04-11T03:12:40.707220Z",
+      "generated_at": "2026-06-12T12:52:47.374327Z",
       "primary_domain": "evm",
       "schema": "ziros-evm-operator-readiness-v1",
       "status": "secondary-ready",
@@ -25,7 +25,10 @@
       "advisories": [
         "gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}"
       ],
-      "blockers": [],
+      "blockers": [
+        "Midnight-first operator lane derived from typed readiness and doctor evidence. ready_for_live_submit=false blockers=gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}; wallet: No browser wallet session or headless operator wallet credentials were available.; dust: DUST balance is not checkable from a bare CLI process. advisories=gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}",
+        "proof-server: The proof server endpoints /health, /ready, or /version were unreachable."
+      ],
       "contract_universe_count": 7,
       "doctor_error": null,
       "doctor_report": {
@@ -47,7 +50,7 @@
             "status": "pass"
           },
           {
-            "actual": "24.13.1",
+            "actual": "22.22.3",
             "expected": ">=22.0.0",
             "fix": "Install Node.js 22.x or newer.",
             "id": "node",
@@ -56,7 +59,7 @@
             "status": "pass"
           },
           {
-            "actual": "11.8.0",
+            "actual": "10.9.8",
             "id": "npm",
             "label": "npm",
             "required": true,
@@ -72,13 +75,14 @@
             "status": "not_checkable_from_cli"
           },
           {
-            "actual": "8.0.3 @ http://127.0.0.1:6300",
+            "actual": "http://127.0.0.1:6300",
+            "detail": "The proof server endpoints /health, /ready, or /version were unreachable.",
             "expected": "wire contract 8.0.3",
-            "fix": "Start or restart the native proof server with `zkf midnight proof-server serve --engine umpg`.",
+            "fix": "Start the native proof server: `zkf midnight proof-server serve --port 6300 --engine umpg`.",
             "id": "proof-server",
             "label": "Midnight proof server",
             "required": true,
-            "status": "pass"
+            "status": "fail"
           },
           {
             "actual": "http://127.0.0.1:6311",
@@ -142,30 +146,31 @@
             "status": "not_checkable_from_cli"
           }
         ],
-        "generated_at": "1775877160Z",
+        "generated_at": "1781268767Z",
         "network": "preprod",
         "recommended_fixes": [
+          "Start the native proof server: `zkf midnight proof-server serve --port 6300 --engine umpg`.",
           "Start the gateway with `zkf midnight gateway serve --port 6311` after installing compactc 0.30.0."
         ],
         "schema": "zkf-midnight-doctor-report-v1",
         "summary": {
-          "failed": 0,
+          "failed": 1,
           "not_checkable": 4,
-          "overall_status": "warn",
-          "passed": 8,
+          "overall_status": "fail",
+          "passed": 7,
           "total": 13,
           "warned": 1
         }
       },
       "doctor_summary": {
-        "failed": 0,
+        "failed": 1,
         "not_checkable": 4,
-        "overall_status": "warn",
-        "passed": 8,
+        "overall_status": "fail",
+        "passed": 7,
         "total": 13,
         "warned": 1
       },
-      "generated_at": "2026-04-11T03:12:40.704066Z",
+      "generated_at": "2026-06-12T12:52:47.373151Z",
       "live_submit_blockers": [
         "gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}",
         "wallet: No browser wallet session or headless operator wallet credentials were available.",
@@ -173,7 +178,7 @@
       ],
       "primary_domain": "midnight",
       "ready_for_live_submit": false,
-      "ready_for_local_operator": true,
+      "ready_for_local_operator": false,
       "required_cli_surfaces": [
         "zkf midnight status",
         "zkf midnight contract compile",
@@ -186,13 +191,13 @@
         "zkf midnight contract diagnose"
       ],
       "schema": "ziros-midnight-operator-readiness-v1",
-      "status": "ready",
+      "status": "blocked",
       "validation_template": "token-transfer",
       "version": "0.7.3"
     }
   },
-  "generated_at": "2026-04-11T03:12:40.717964Z",
-  "product_release_ready": true,
+  "generated_at": "2026-06-12T12:52:47.376400Z",
+  "product_release_ready": false,
   "release_boundary": {
     "allowlist_path": "release/public_release_allowlist.json",
     "boundary_report_path": "release/public_release_boundary_report.json",
@@ -203,7 +208,7 @@
   "release_tag": "v0.7.3",
   "release_version": "0.7.3",
   "schema": "ziros-product-release-v1",
-  "source_commit": "2f84b52c136fe10211098bf80ca04e8e0763118c",
+  "source_commit": "8b43288b8265d608a697373d1be71789976bf5c2",
   "theorem_release_grade_ready": true,
   "truth_surfaces": {
     "agent_forensics": "forensics/",
@@ -236,7 +241,7 @@
     "total_entries": 193
   },
   "version": "0.7.3",
-  "working_tree_dirty": false,
+  "working_tree_dirty": true,
   "workspace_members": {
     "count": 25,
     "names": [
diff --git a/release/provenance/public_attestation_export.json b/release/provenance/public_attestation_export.json
index 376d062..d1325ef 100644
--- a/release/provenance/public_attestation_export.json
+++ b/release/provenance/public_attestation_export.json
@@ -1,9 +1,9 @@
 {
   "contract_operator_summary": {
     "evm_status": "secondary-ready",
-    "midnight_status": "ready"
+    "midnight_status": "blocked"
   },
-  "generated_at": "2026-04-11T03:12:40.729816Z",
+  "generated_at": "2026-06-12T12:52:47.386570Z",
   "headline_counts": {
     "hypothesis_carried_theorem": 0,
     "hypothesis_stated": 0,
@@ -23,7 +23,7 @@
   "release_tag": "v0.7.3",
   "release_version": "0.7.3",
   "schema": "ziros-public-attestation-export-v1",
-  "source_commit": "2f84b52c136fe10211098bf80ca04e8e0763118c",
+  "source_commit": "8b43288b8265d608a697373d1be71789976bf5c2",
   "support_matrix_summary": {
     "backend_count": 9,
     "frontend_count": 8,
@@ -31,5 +31,5 @@
     "generated_for": "0.7.3"
   },
   "version": "0.7.3",
-  "working_tree_dirty": false
+  "working_tree_dirty": true
 }
diff --git a/release/public_release_allowlist.json b/release/public_release_allowlist.json
index 1a7c4f1..40b048f 100644
--- a/release/public_release_allowlist.json
+++ b/release/public_release_allowlist.json
@@ -38,7 +38,7 @@
     ".fsti",
     ".zip"
   ],
-  "generated_at": "2026-04-11T03:12:40.729623Z",
+  "generated_at": "2026-06-12T12:52:47.386328Z",
   "package_roots": [
     "attestation",
     "zkf-wallet-helper",
diff --git a/release/vision_alignment_report.json b/release/vision_alignment_report.json
index 8638f07..0728af1 100644
--- a/release/vision_alignment_report.json
+++ b/release/vision_alignment_report.json
@@ -3,7 +3,7 @@
     {
       "backing_artifact": "release/midnight_operator_readiness.json",
       "claim": "midnight-first universal contract operator",
-      "status": "backed"
+      "status": "partially-backed"
     },
     {
       "backing_artifact": "release/evm_operator_readiness.json",
@@ -16,8 +16,8 @@
       "status": "backed"
     }
   ],
-  "generated_at": "2026-04-11T03:12:40.707288Z",
-  "midnight_release_ready": true,
+  "generated_at": "2026-06-12T12:52:47.374349Z",
+  "midnight_release_ready": false,
   "midnight_support_row": {
     "assurance_lane": "delegated-or-external-lane",
     "fields": [
@@ -29,9 +29,9 @@
     "mode": "native",
     "notes": "Midnight-first operator lane derived from typed readiness and doctor evidence. ready_for_live_submit=false blockers=gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}; wallet: No browser wallet session or headless operator wallet credentials were available.; dust: DUST balance is not checkable from a bare CLI process. advisories=gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}",
     "proof_semantics": "external-or-delegated",
-    "status": "ready"
+    "status": "broken"
   },
-  "product_release_ready": true,
+  "product_release_ready": false,
   "release_grade_ready": true,
   "schema": "ziros-vision-alignment-report-v1",
   "version": "0.7.3"
diff --git a/scripts/benchmarks/README.md b/scripts/benchmarks/README.md
new file mode 100644
index 0000000..de92043
--- /dev/null
+++ b/scripts/benchmarks/README.md
@@ -0,0 +1,20 @@
+# Cross-backend benchmark harness
+
+Serial `prove`/`verify` wall-clock benchmark across the ready transparent
+backends. See [`docs/BENCHMARKS.md`](../../docs/BENCHMARKS.md) for measured
+results, methodology, and caveats.
+
+```bash
+cargo build -p zkf-cli --release --features metal-gpu   # or without the feature
+export ZKF_BIN="$PWD/target-public/release/zkf-cli"      # if not the default path
+
+python3 scripts/benchmarks/bench.py 5          # minimal-circuit table, N=5
+python3 scripts/benchmarks/bench_scale.py 3    # scaling table (32/128/512 constraints), N=3
+```
+
+- `gen_circuit.py <field> <K> <out>` — grow an `emit-example` program with a
+  public-anchored multiplication chain to a target constraint count.
+- Results are written to `$BENCH_WORK/bench_results.json` and
+  `$BENCH_WORK/bench_scale_results.json` (default `BENCH_WORK=/tmp/zkf-bench`).
+- Run on a **quiet machine** — the benchmark is serial on purpose; concurrent
+  proving skews wall-clock and invalidates the numbers.
diff --git a/scripts/benchmarks/bench.py b/scripts/benchmarks/bench.py
new file mode 100644
index 0000000..7c4cbde
--- /dev/null
+++ b/scripts/benchmarks/bench.py
@@ -0,0 +1,49 @@
+#!/usr/bin/env python3
+"""Cross-backend prove/verify benchmark — minimal `emit-example` circuit.
+SERIAL (one job at a time) so wall-clock is not skewed by contention. Same logical
+circuit emitted in each backend's native field. Measured subprocess timings only.
+
+Usage: bench.py [N-iterations]   (default 5)
+Env: ZKF_BIN (default target-public/release/zkf-cli), BENCH_WORK (default /tmp/zkf-bench)
+Excludes by hand: arkworks-groth16 (backend-honesty fenced), sp1/risc-zero (broken)."""
+import json, subprocess, time, statistics, sys, os
+
+ZKF = os.environ.get("ZKF_BIN", "target-public/release/zkf-cli")
+WORK = os.environ.get("BENCH_WORK", "/tmp/zkf-bench")
+N = int(sys.argv[1]) if len(sys.argv) > 1 else 5
+BACKENDS = [("plonky3","goldilocks"),("halo2","pasta-fp"),
+            ("halo2-bls12381","bls12-381"),("nova","bn254"),("hypernova","bn254")]
+
+os.makedirs(WORK, exist_ok=True)
+INPUTS = f"{WORK}/in.json"
+json.dump({"x":"3","y":"4"}, open(INPUTS,"w"))
+
+def timed(args):
+    t0=time.perf_counter(); r=subprocess.run(args,capture_output=True,text=True)
+    return time.perf_counter()-t0, r.returncode, r.stderr
+
+rows=[]
+for be,fld in BACKENDS:
+    prog=f"{WORK}/prog_{be}.json"; proof=f"{WORK}/proof_{be}.json"
+    subprocess.run([ZKF,"emit-example","--out",prog,"--field",fld],capture_output=True)
+    pt,vt=[],[]; art=0; ok=True
+    for i in range(N):
+        dt,rc,err=timed([ZKF,"prove","--program",prog,"--inputs",INPUTS,"--backend",be,"--out",proof])
+        if rc!=0: ok=False; print(f"{be}: prove FAIL iter {i}: {err[:120]}"); break
+        pt.append(dt); art=os.path.getsize(proof)
+        dt,rc,err=timed([ZKF,"verify","--program",prog,"--artifact",proof,"--backend",be])
+        if rc!=0: ok=False; print(f"{be}: verify FAIL iter {i}: {err[:120]}"); break
+        vt.append(dt)
+    if ok:
+        rows.append({"backend":be,"field":fld,"iters":N,
+                     "prove_med":statistics.median(pt),"verify_med":statistics.median(vt),
+                     "artifact_bytes":art})
+        print(f"{be:16s} prove med={statistics.median(pt)*1000:8.1f}ms "
+              f"verify med={statistics.median(vt)*1000:8.1f}ms art={art:,}B")
+
+json.dump(rows,open(f"{WORK}/bench_results.json","w"),indent=2)
+lines=["| Backend | Field | Prove median | Verify median | Artifact |","|---|---|--:|--:|--:|"]
+for r in rows:
+    lines.append(f"| `{r['backend']}` | {r['field']} | {r['prove_med']*1000:.0f} ms | "
+                 f"{r['verify_med']*1000:.0f} ms | {r['artifact_bytes']:,} B |")
+print("\n"+"\n".join(lines))
diff --git a/scripts/benchmarks/bench_scale.py b/scripts/benchmarks/bench_scale.py
new file mode 100644
index 0000000..a2379cb
--- /dev/null
+++ b/scripts/benchmarks/bench_scale.py
@@ -0,0 +1,53 @@
+#!/usr/bin/env python3
+"""Scaling cross-backend benchmark. SERIAL. Prove+verify a multiplication-chain
+circuit (extended emit-example) at several constraint sizes, N iterations each.
+Measured subprocess timings only.
+
+Usage: bench_scale.py [N-iterations]   (default 3)
+Env: ZKF_BIN (default target-public/release/zkf-cli), BENCH_WORK (default /tmp/zkf-bench)"""
+import json, subprocess, time, statistics, sys, os
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+ZKF = os.environ.get("ZKF_BIN", "target-public/release/zkf-cli")
+WORK = os.environ.get("BENCH_WORK", "/tmp/zkf-bench")
+GEN = os.path.join(HERE, "gen_circuit.py")
+N = int(sys.argv[1]) if len(sys.argv) > 1 else 3
+KS = [32, 128, 512]
+BACKENDS = [("plonky3","goldilocks"),("halo2","pasta-fp"),
+            ("halo2-bls12381","bls12-381"),("nova","bn254"),("hypernova","bn254")]
+
+os.makedirs(WORK, exist_ok=True)
+INPUTS = f"{WORK}/cin.json"
+json.dump({"x":"2","y":"3"}, open(INPUTS,"w"))
+
+def timed(args):
+    t0=time.perf_counter(); r=subprocess.run(args,capture_output=True,text=True)
+    return time.perf_counter()-t0, r.returncode, r.stderr
+
+rows=[]
+for be,fld in BACKENDS:
+    for K in KS:
+        prog=f"{WORK}/sc_{fld}_{K}.json"; proof=f"{WORK}/scpf_{be}_{K}.json"
+        g=subprocess.run(["python3",GEN,fld,str(K),prog],capture_output=True,text=True)
+        ncon=next((int(t) for t in g.stdout.split() if t.isdigit()), None)
+        pt,vt=[],[]; art=0; ok=True
+        for i in range(N):
+            dt,rc,err=timed([ZKF,"prove","--program",prog,"--inputs",INPUTS,"--backend",be,"--out",proof])
+            if rc!=0: ok=False; print(f"{be} K={K}: prove FAIL: {err[:100]}"); break
+            pt.append(dt); art=os.path.getsize(proof)
+            dt,rc,err=timed([ZKF,"verify","--program",prog,"--artifact",proof,"--backend",be])
+            if rc!=0: ok=False; print(f"{be} K={K}: verify FAIL: {err[:100]}"); break
+            vt.append(dt)
+        if ok:
+            rows.append({"backend":be,"field":fld,"K":K,"constraints":ncon,
+                         "prove_med":statistics.median(pt),"verify_med":statistics.median(vt),
+                         "artifact_bytes":art})
+            print(f"{be:16s} K={K:4d} (~{ncon} con) prove={statistics.median(pt)*1000:8.1f}ms "
+                  f"verify={statistics.median(vt)*1000:8.1f}ms art={art:,}B")
+
+json.dump(rows,open(f"{WORK}/bench_scale_results.json","w"),indent=2)
+lines=["| Backend | Field | Constraints | Prove median | Verify median | Artifact |","|---|---|--:|--:|--:|--:|"]
+for r in rows:
+    lines.append(f"| `{r['backend']}` | {r['field']} | {r['constraints']:,} | "
+                 f"{r['prove_med']*1000:.0f} ms | {r['verify_med']*1000:.0f} ms | {r['artifact_bytes']:,} B |")
+print("\n"+"\n".join(lines))
diff --git a/scripts/benchmarks/gen_circuit.py b/scripts/benchmarks/gen_circuit.py
new file mode 100644
index 0000000..4140755
--- /dev/null
+++ b/scripts/benchmarks/gen_circuit.py
@@ -0,0 +1,41 @@
+#!/usr/bin/env python3
+"""Grow a size-parameterized circuit by extending the known-good emit-example
+program (native IR: constraints + witness_plan) with a public-anchored
+multiplication chain. Keeps the exact field/format the prove pipeline accepts, so
+the only thing that changes across sizes is constraint count.
+
+Usage: gen_circuit.py <field> <K-extra-steps> <out.json>
+  field in {bn254, goldilocks, pasta-fp, bls12-381, babybear}
+Env: ZKF_BIN (default: target-public/release/zkf-cli), BENCH_WORK (default: /tmp/zkf-bench)
+"""
+import json, subprocess, sys, os
+
+ZKF = os.environ.get("ZKF_BIN", "target-public/release/zkf-cli")
+WORK = os.environ.get("BENCH_WORK", "/tmp/zkf-bench")
+field, K, out = sys.argv[1], int(sys.argv[2]), sys.argv[3]
+os.makedirs(WORK, exist_ok=True)
+
+base = f"{WORK}/_base_{field}.json"
+subprocess.run([ZKF, "emit-example", "--out", base, "--field", field],
+               capture_output=True, text=True, check=True)
+d = json.load(open(base))
+
+def sig(name): return {"op": "signal", "args": name}
+
+prev = "product"  # public-anchored base output
+for i in range(K):
+    nm = f"c_{i}"
+    d["signals"].append({"name": nm, "visibility": "private"})
+    d["constraints"].append({"kind": "equal", "lhs": sig(nm),
+                             "rhs": {"op": "mul", "args": [sig(prev), sig("x")]},
+                             "label": f"chain_{i}"})
+    d["witness_plan"]["assignments"].append(
+        {"target": nm, "expr": {"op": "mul", "args": [sig(prev), sig("x")]}})
+    prev = nm
+d["signals"].append({"name": "chain_out", "visibility": "public"})
+d["constraints"].append({"kind": "equal", "lhs": sig("chain_out"), "rhs": sig(prev),
+                         "label": "chain_anchor"})
+d["witness_plan"]["assignments"].append({"target": "chain_out", "expr": sig(prev)})
+
+json.dump(d, open(out, "w"), indent=2)
+print(f"wrote {out}: base+{K} chain = {len(d['constraints'])} constraints, field={field}")
diff --git a/scripts/generate_private_release_truth.py b/scripts/generate_private_release_truth.py
index 047752d..fafad81 100644
--- a/scripts/generate_private_release_truth.py
+++ b/scripts/generate_private_release_truth.py
@@ -511,6 +511,11 @@ def main() -> None:
     primitive_set = guaranteed_circuit_primitive_set(version)
     midnight_readiness = midnight_operator_readiness(version, support)
     support = apply_midnight_support_override(support, midnight_readiness)
+    # The private-drift checker re-derives readiness from the committed (already
+    # overridden) support matrix. Recompute here from the overridden support so the
+    # persisted readiness is that same fixpoint; apply_midnight_support_override is
+    # stable under re-derivation, so this converges in one extra pass.
+    midnight_readiness = midnight_operator_readiness(version, support)
     write_json(SUPPORT_MATRIX, support)
     evm_readiness = evm_operator_readiness(version)
     alignment_report = vision_alignment_report(
diff --git a/support-matrix.json b/support-matrix.json
index 89c7fa0..2f31504 100644
--- a/support-matrix.json
+++ b/support-matrix.json
@@ -119,7 +119,7 @@
       "mode": "native",
       "notes": "Midnight-first operator lane derived from typed readiness and doctor evidence. ready_for_live_submit=false blockers=gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}; wallet: No browser wallet session or headless operator wallet credentials were available.; dust: DUST balance is not checkable from a bare CLI process. advisories=gateway: {\"error\":\"forbidden\",\"reason\":\"missing_cf_access_jwt_assertion\"}",
       "proof_semantics": "external-or-delegated",
-      "status": "ready"
+      "status": "broken"
     }
   ],
   "frontends": [
diff --git a/zkf-ir-spec/verification-ledger.json b/zkf-ir-spec/verification-ledger.json
index e9c5777..398fa8c 100644
--- a/zkf-ir-spec/verification-ledger.json
+++ b/zkf-ir-spec/verification-ledger.json
@@ -779,7 +779,7 @@
       "status": "mechanized_local",
       "assurance_class": "mechanized_implementation_claim",
       "evidence_path": "zkf-runtime/proofs/verus/runtime_execution_scheduler_verus.rs",
-      "notes": "Verus theorem `gpu_cpu_gpu_partition_equivalence` proves the runtime’s verified placement partition composes the mechanized GPU subset with the verified CPU lane without changing verifier truth: GPU-eligible nodes stay on the attested whitelist, CPU-routed nodes remain on the CPU proof surface, and the combined execution plan preserves the same accepted statement through final proof generation.",
+      "notes": "Verus theorem `gpu_cpu_gpu_partition_equivalence` proves the runtime\u2019s verified placement partition composes the mechanized GPU subset with the verified CPU lane without changing verifier truth: GPU-eligible nodes stay on the attested whitelist, CPU-routed nodes remain on the CPU proof surface, and the combined execution plan preserves the same accepted statement through final proof generation.",
       "trusted_assumptions": []
     },
     {
@@ -2145,17 +2145,6 @@
       "evidence_path": "zkf-lang/proofs/rocq/ZirLangPrivacyProofs.v",
       "notes": "Local Rocq theorem `private_unassigned_input_cannot_be_exposed` and Verus theorem `private_unassigned_cannot_expose` prove the privacy model rejects direct exposure of unassigned private inputs. This supports the shipped Zir checker boundary but remains a model-only claim until tied to extracted implementation proof.",
       "trusted_assumptions": []
-    },
-    {
-      "theorem_id": "hermes.pqc_zkproof_boundary_metabolized",
-      "title": "PQC envelope and ZKProof standardization integrated into proof-boundary closure skill",
-      "scope": "hermes.defender-knowledge-tissue + zk-proof-boundary-closure",
-      "checker": "manual + skill_patch + browser_research",
-      "status": "bounded_check",
-      "assurance_class": "bounded_check",
-      "evidence_path": "PROOF_BOUNDARY.md + zk-proof-boundary-closure/SKILL.md + /Users/sicarii/Documents/cryptography-study/mega-corpus",
-      "notes": "Web research (NIST PQC FIPS 203/204/205 + zkproof.org workgroups) metabolized into updated zk-proof-boundary-closure skill. Adds PQC parameter discipline (ML-KEM-1024/ML-DSA-87 priority, constant-time), ZKProof alignment for soundness/succinctness/selective disclosure (Midnight trade finance use case), explicit boundaries per ziros-proof-honesty and formal-verification-constitution. PROOF_BOUNDARY.md patched. Does not count as mechanized_implementation_claim. Supports future high-assurance ZirOS/Midnight work. Evidence: this ledger entry + skill patch + session tools.",
-      "trusted_assumptions": ["web_sources_accurate_as_of_2026-04", "no_new_mechanized_theorems_added"]
     }
   ]
 }
diff --git a/zkf-lib/proofs/verus/claims_truth_verus.rs b/zkf-lib/proofs/verus/claims_truth_verus.rs
index bf453a3..e49a3d6 100644
--- a/zkf-lib/proofs/verus/claims_truth_verus.rs
+++ b/zkf-lib/proofs/verus/claims_truth_verus.rs
@@ -3,7 +3,7 @@ use vstd::prelude::*;
 verus! {
 
 spec fn deductible_adjusted(covered: nat, deductible: nat) -> nat {
-    if covered >= deductible { covered - deductible } else { 0 }
+    if covered >= deductible { (covered - deductible) as nat } else { 0nat }
 }
 
 spec fn capped_payout(covered: nat, deductible: nat, cap: nat) -> nat {