From 39fa68b470837b945003664d594ad7273150964f Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 7 Sep 2026 02:26:48 +0100
Subject: [PATCH 1/5] fix(proof): reject satisfiable obligations and verify
 live Coq submissions

---
 .github/workflows/actions.lock     |   3 +
 .github/workflows/proof-safety.yml |  33 +++++++
 src/rust/provers/coq.rs            |   2 +-
 src/rust/server.rs                 |   7 +-
 tests/live_service_regressions.rs  | 147 +++++++++++++++++++++++++++++
 5 files changed, 189 insertions(+), 3 deletions(-)
 create mode 100644 .github/workflows/proof-safety.yml
 create mode 100644 tests/live_service_regressions.rs

diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
index 45419472..d24cbdbe 100644
--- a/.github/workflows/actions.lock
+++ b/.github/workflows/actions.lock
@@ -63,6 +63,9 @@ workflows:
         - 'actions/checkout@v7.0.1'
         - 'actions/deploy-pages@v5.0.0'
         - 'actions/upload-pages-artifact@v5.0.0'
+    '.github/workflows/proof-safety.yml':
+        - 'actions/checkout@v7.0.1'
+        - 'swatinem/rust-cache@v2.9.2'
     '.github/workflows/rust-ci.yml': []
     '.github/workflows/s4-loop.yml':
         - 'actions/checkout@v7.0.1'
diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
new file mode 100644
index 00000000..b7811e36
--- /dev/null
+++ b/.github/workflows/proof-safety.yml
@@ -0,0 +1,33 @@
+# This workflow is managed by gh actions-lock.
+# SPDX-License-Identifier: AGPL-3.0-or-later
+name: Proof Safety
+on:
+  pull_request:
+  push:
+    branches: [main]
+permissions:
+  contents: read
+concurrency:
+  group: proof-safety-${{ github.ref }}
+  cancel-in-progress: true
+jobs:
+  proof-safety:
+    name: Proof safety regressions
+    runs-on: ubuntu-24.04
+    timeout-minutes: 25
+    env:
+      VERISIMDB_URL: http://127.0.0.1:17799
+    steps:
+      - uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+      - uses: Swatinem/rust-cache@v2.9.2
+      - name: Install required native provers
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y coq z3 cvc5 capnproto pkg-config libssl-dev
+          command -v coqc
+          command -v z3
+          command -v cvc5
+      - name: Require accepted and rejected proofs through the live service
+        run: cargo test --locked --features live-provers --test live_service_regressions -- --nocapture
diff --git a/src/rust/provers/coq.rs b/src/rust/provers/coq.rs
index 3a9c4c7d..940aecbe 100644
--- a/src/rust/provers/coq.rs
+++ b/src/rust/provers/coq.rs
@@ -946,7 +946,7 @@ impl ProverBackend for CoqBackend {
         }
         if let Some(source) = state.metadata.get("coq_source").and_then(|v| v.as_str()) {
             let temp_file =
-                std::env::temp_dir().join(format!("echidna_coq_verify_{}.v", uuid::Uuid::new_v4()));
+                std::env::temp_dir().join(format!("echidna_coq_verify_{}.v", uuid::Uuid::new_v4().simple()));
             tokio::fs::write(&temp_file, source)
                 .await
                 .context("Failed to write temp file")?;
diff --git a/src/rust/server.rs b/src/rust/server.rs
index 7580679b..2c41e1eb 100644
--- a/src/rust/server.rs
+++ b/src/rust/server.rs
@@ -531,13 +531,16 @@ async fn verify_handler(Json(req): Json<VerifyRequest>) -> Result<Json<VerifyRes
             1
         };
 
-        let outcome_str = if raw.valid {
+        // A completed SMT query is not necessarily a discharged obligation.
+        // Only unsat closes a query interpreted as the negated obligation.
+        let verified = raw.valid && matches!(smt_status.as_deref(), Some("unsat"));
+        let outcome_str = if verified {
             "PROVED"
         } else {
             "NO_PROOF_FOUND"
         };
         return Ok(Json(VerifyResponse {
-            valid: raw.valid,
+            valid: verified,
             outcome: outcome_str.to_string(),
             goals_remaining,
             tactics_used: 0,
diff --git a/tests/live_service_regressions.rs b/tests/live_service_regressions.rs
new file mode 100644
index 00000000..be87a0b9
--- /dev/null
+++ b/tests/live_service_regressions.rs
@@ -0,0 +1,147 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+//! Opt-in checks for the parse_string path used by the HTTP service.
+#![cfg(feature = "live-provers")]
+
+use echidna::provers::{ProverConfig, ProverFactory, ProverKind};
+
+#[tokio::test]
+async fn http_verification_requires_a_discharged_obligation() {
+    use serde_json::{json, Value};
+    use std::time::Duration;
+    // Missing binaries are a failure here, not a successful skipped test.
+    for executable in ["coqc", "z3", "cvc5"] {
+        which::which(executable)
+            .unwrap_or_else(|_| panic!("required prover missing: {executable}"));
+    }
+    let socket = std::net::TcpListener::bind("127.0.0.1:0").unwrap();
+    let port = socket.local_addr().unwrap().port();
+    drop(socket);
+    let mut server = tokio::process::Command::new(env!("CARGO_BIN_EXE_echidna"))
+        .args(["server", "--host", "127.0.0.1", "--port", &port.to_string()])
+        .kill_on_drop(true)
+        .spawn()
+        .unwrap();
+    let client = reqwest::Client::builder()
+        .timeout(Duration::from_secs(15))
+        .build()
+        .unwrap();
+    let base = format!("http://127.0.0.1:{port}");
+    let mut ready = false;
+    for _ in 0..100 {
+        assert!(
+            server.try_wait().unwrap().is_none(),
+            "server exited before becoming ready"
+        );
+        if client
+            .get(format!("{base}/api/health"))
+            .send()
+            .await
+            .is_ok()
+        {
+            ready = true;
+            break;
+        }
+        tokio::time::sleep(Duration::from_millis(100)).await;
+    }
+    assert!(ready, "server never became ready");
+    for prover in ["Z3", "CVC5"] {
+        for (assertion, expected_status, expected_valid) in
+            [("false", "unsat", true), ("true", "sat", false)]
+        {
+            let response = client.post(format!("{base}/api/verify"))
+                .json(&json!({"prover": prover, "content": format!("(set-logic QF_LIA)\n(assert {assertion})\n(check-sat)\n")}))
+                .send().await.unwrap().error_for_status().unwrap();
+            let result: Value = response.json().await.unwrap();
+            assert_eq!(result["smt_status"], expected_status, "{prover}: {result}");
+            assert_eq!(result["valid"], expected_valid, "{prover}: {result}");
+            assert_eq!(
+                result["outcome"] == "PROVED",
+                expected_valid,
+                "{prover}: {result}"
+            );
+        }
+    }
+    for (content, expected) in [
+        (
+            "Theorem identity : forall P : Prop, P -> P. Proof. intros P H. exact H. Qed.",
+            true,
+        ),
+        ("Theorem impossible : False. Proof. exact I. Qed.", false),
+    ] {
+        let result: Value = client
+            .post(format!("{base}/api/verify"))
+            .json(&json!({"prover":"Coq", "content":content}))
+            .send()
+            .await
+            .unwrap()
+            .error_for_status()
+            .unwrap()
+            .json()
+            .await
+            .unwrap();
+        assert_eq!(result["valid"], expected, "Coq: {result}");
+    }
+    server.kill().await.unwrap();
+    server.wait().await.unwrap();
+}
+
+#[tokio::test]
+async fn coq_string_submission_accepts_proof_and_rejects_falsehood() {
+    // This test deliberately fails when Coq is unavailable: skips are not proof evidence.
+    let executable = which::which("coqc").expect("this live regression requires coqc");
+    let prover = ProverFactory::create(
+        ProverKind::Coq,
+        ProverConfig {
+            executable,
+            ..Default::default()
+        },
+    )
+    .unwrap();
+    for (source, expected) in [
+        (
+            "Theorem identity : forall P : Prop, P -> P.\nProof. intros P H. exact H. Qed.\n",
+            true,
+        ),
+        ("Theorem impossible : False.\nProof. exact I. Qed.\n", false),
+    ] {
+        let state = prover.parse_string(source).await.unwrap();
+        assert_eq!(prover.verify_proof(&state).await.unwrap(), expected);
+    }
+}
+
+#[test]
+fn report_actual_backend_inventory() {
+    // Ask the compiled serde implementation for its accepted variants. This
+    // includes variants omitted by ProverKind::all(), unlike the CLI listing.
+    let error = serde_json::from_str::<ProverKind>("\"_inventory_probe_\"")
+        .unwrap_err()
+        .to_string();
+    let expected = error
+        .split("expected one of ")
+        .nth(1)
+        .expect("serde variant list");
+    let variants: Vec<_> = expected
+        .split('`')
+        .enumerate()
+        .filter_map(|(index, value)| (index % 2 == 1).then_some(value))
+        .collect();
+    let advertised = ProverKind::all();
+    let mut records = Vec::new();
+    for name in variants {
+        let kind: ProverKind = serde_json::from_value(serde_json::json!(name)).unwrap();
+        let executable = kind.default_executable();
+        let path = which::which(executable).ok();
+        records.push(serde_json::json!({
+            "backend": name,
+            "listed_by_cli": advertised.contains(&kind),
+            "default_executable": executable,
+            "executable_on_path": path,
+            "proof_validation": "not established by inventory",
+        }));
+    }
+    assert!(records.len() >= advertised.len());
+    println!(
+        "BACKEND_INVENTORY={}",
+        serde_json::to_string(&records).unwrap()
+    );
+}

From 8b0b2fa2d524b67b775faf9a4c74d2178d4d2fb6 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 7 Sep 2026 02:48:23 +0100
Subject: [PATCH 2/5] fix(ci): install native build tools and patch vulnerable
 dependencies

---
 .github/workflows/actions.lock                |  30 +-
 .github/workflows/agda-meta-checker.yml       |   1 +
 .github/workflows/boj-build.yml               |   1 +
 .github/workflows/bridge-gate.yml             |   1 +
 .github/workflows/cargo-audit.yml             |   5 +-
 .github/workflows/cflite_batch.yml            |   1 +
 .github/workflows/cflite_pr.yml               |   1 +
 .github/workflows/chapel-ci.yml               |   5 +-
 .github/workflows/codeql.yml                  |   1 +
 .github/workflows/container-ci.yml            |   1 +
 .github/workflows/dogfood-gate.yml            |   1 +
 .github/workflows/dogfood-proofs-ci.yml       |   1 +
 .github/workflows/formal-verification.yml     |   5 +-
 .../generator-generic-ossf-slsa3-publish.yml  |   1 +
 .github/workflows/ghcr-publish.yml            |   1 +
 .github/workflows/governance.yml              |   1 +
 .github/workflows/hypatia-scan.yml            |   1 +
 .github/workflows/idris2-abi-ci.yml           |   1 +
 .github/workflows/label-triage.yml            |   1 +
 .github/workflows/labels.yml                  |   1 +
 .github/workflows/live-provers.yml            |  17 +-
 .github/workflows/mirror.yml                  |   1 +
 .github/workflows/mvp-smoke.yml               |   3 +-
 .github/workflows/pages.yml                   |   1 +
 .github/workflows/proof-safety.yml            |   2 +-
 .github/workflows/rust-ci.yml                 |   4 +-
 .github/workflows/rust-native-reusable.yml    | 360 ++++++++++
 .github/workflows/s4-loop.yml                 |   3 +-
 .github/workflows/scorecard.yml               |   1 +
 .github/workflows/secret-scanner.yml          |   1 +
 .github/workflows/security-scan.yml           |   1 +
 .github/workflows/server-boot-gate.yml        |   3 +-
 .github/workflows/spark-theatre-gate.yml      |   1 +
 .../workflows/verification-proofs-cron.yml    |   1 +
 .github/workflows/workflow-linter.yml         |   1 +
 .../contractiles/intend/intend.k9.ncl         |   9 +-
 Cargo.lock                                    |  28 +-
 fuzz/Cargo.lock                               | 655 +++++++++++++++---
 src/rust/provers/coq.rs                       |   6 +-
 src/rust/provers/dafny.rs                     |   3 +-
 src/rust/server.rs                            |   6 +-
 41 files changed, 1012 insertions(+), 156 deletions(-)
 create mode 100644 .github/workflows/rust-native-reusable.yml

diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
index d24cbdbe..91e8b1d8 100644
--- a/.github/workflows/actions.lock
+++ b/.github/workflows/actions.lock
@@ -13,7 +13,7 @@ workflows:
         - 'actions/checkout@v7.0.1'
     '.github/workflows/cargo-audit.yml':
         - 'actions/checkout@v7.0.1'
-        - 'dtolnay/rust-toolchain@stable'
+        - 'dtolnay/rust-toolchain@master'
     '.github/workflows/cflite_batch.yml':
         - 'google/clusterfuzzlite@v1'
     '.github/workflows/cflite_pr.yml':
@@ -22,7 +22,7 @@ workflows:
         - 'actions/checkout@v7.0.1'
         - 'actions/download-artifact@v8.0.1'
         - 'actions/upload-artifact@v7.0.1'
-        - 'dtolnay/rust-toolchain@stable'
+        - 'dtolnay/rust-toolchain@master'
         - 'mlugg/setup-zig@v2.2.1'
         - 'swatinem/rust-cache@v2.9.2'
     '.github/workflows/codeql.yml':
@@ -36,7 +36,7 @@ workflows:
         - 'actions/checkout@v7.0.1'
     '.github/workflows/formal-verification.yml':
         - 'actions/checkout@v7.0.1'
-        - 'dtolnay/rust-toolchain@stable'
+        - 'dtolnay/rust-toolchain@master'
         - 'swatinem/rust-cache@v2.9.2'
     '.github/workflows/generator-generic-ossf-slsa3-publish.yml':
         - 'actions/checkout@v7.0.1'
@@ -51,12 +51,12 @@ workflows:
     '.github/workflows/labels.yml': []
     '.github/workflows/live-provers.yml':
         - 'actions/checkout@v7.0.1'
-        - 'dtolnay/rust-toolchain@stable'
+        - 'dtolnay/rust-toolchain@master'
         - 'swatinem/rust-cache@v2.9.2'
     '.github/workflows/mirror.yml': []
     '.github/workflows/mvp-smoke.yml':
         - 'actions/checkout@v7.0.1'
-        - 'dtolnay/rust-toolchain@stable'
+        - 'dtolnay/rust-toolchain@master'
         - 'swatinem/rust-cache@v2.9.2'
         - 'taiki-e/install-action@v2.86.4'
     '.github/workflows/pages.yml':
@@ -67,9 +67,14 @@ workflows:
         - 'actions/checkout@v7.0.1'
         - 'swatinem/rust-cache@v2.9.2'
     '.github/workflows/rust-ci.yml': []
+    '.github/workflows/rust-native-reusable.yml':
+        - 'actions/checkout@v7.0.1'
+        - 'dtolnay/rust-toolchain@master'
+        - 'goto-bus-stop/setup-zig@v2.2.1'
+        - 'swatinem/rust-cache@v2.9.2'
     '.github/workflows/s4-loop.yml':
         - 'actions/checkout@v7.0.1'
-        - 'dtolnay/rust-toolchain@stable'
+        - 'dtolnay/rust-toolchain@master'
         - 'swatinem/rust-cache@v2.9.2'
         - 'taiki-e/install-action@v2.86.4'
     '.github/workflows/scorecard.yml': []
@@ -77,7 +82,7 @@ workflows:
     '.github/workflows/security-scan.yml': []
     '.github/workflows/server-boot-gate.yml':
         - 'actions/checkout@v7.0.1'
-        - 'dtolnay/rust-toolchain@stable'
+        - 'dtolnay/rust-toolchain@master'
         - 'swatinem/rust-cache@v2.9.2'
     '.github/workflows/spark-theatre-gate.yml': []
     '.github/workflows/verification-proofs-cron.yml':
@@ -134,9 +139,9 @@ dependencies:
         repo_id: 496012378
         uses:
             - 'actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f'
-    'dtolnay/rust-toolchain@stable':
-        ref: 'stable'
-        commit: 'sha1-4360b52568e2003a75bf9bc1d59f33a8e3fc893c'
+    'dtolnay/rust-toolchain@master':
+        ref: 'master'
+        commit: 'sha1-d1031067263f94b142dd6c0ce24c5eb9d02d52a0'
         owner_id: 1940490
         repo_id: 260749683
     'github/codeql-action@v4.37.7':
@@ -149,6 +154,11 @@ dependencies:
         commit: 'sha1-884713a6c30a92e5e8544c39945cd7cb630abcd1'
         owner_id: 1342004
         repo_id: 400046858
+    'goto-bus-stop/setup-zig@v2.2.1':
+        ref: 'v2.2.1'
+        commit: 'sha1-abea47f85e598557f500fa1fd2ab7464fcb39406'
+        owner_id: 1006268
+        repo_id: 212984112
     'haskell-actions/setup@v2.12.0':
         ref: 'v2.12.0'
         commit: 'sha1-6037f33647c3f17758a2356c80fc4a53d7e0685d'
diff --git a/.github/workflows/agda-meta-checker.yml b/.github/workflows/agda-meta-checker.yml
index 8a32aca5..70a5da04 100644
--- a/.github/workflows/agda-meta-checker.yml
+++ b/.github/workflows/agda-meta-checker.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # CI workflow for ECHIDNA Agda meta-checker
 # Type-checks all formal proofs verifying trust pipeline correctness
 
diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml
index d2c956d4..1d269aa5 100644
--- a/.github/workflows/boj-build.yml
+++ b/.github/workflows/boj-build.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: BoJ Server Build Trigger
 on:
   push:
diff --git a/.github/workflows/bridge-gate.yml b/.github/workflows/bridge-gate.yml
index 2e65025a..63213b4f 100644
--- a/.github/workflows/bridge-gate.yml
+++ b/.github/workflows/bridge-gate.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
 # bridge-gate.yml -- merge-orchestration CVE/bump gate.
diff --git a/.github/workflows/cargo-audit.yml b/.github/workflows/cargo-audit.yml
index 937fed86..b94dadf4 100644
--- a/.github/workflows/cargo-audit.yml
+++ b/.github/workflows/cargo-audit.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # cargo-audit.yml — Dependency vulnerability scanning for Rust projects.
@@ -47,7 +48,9 @@ jobs:
 
       - name: Install Rust toolchain
         if: steps.detect.outputs.present == 'true'
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: stable
 
       - name: Install cargo-audit
         if: steps.detect.outputs.present == 'true'
diff --git a/.github/workflows/cflite_batch.yml b/.github/workflows/cflite_batch.yml
index c6ecee72..d42f9964 100644
--- a/.github/workflows/cflite_batch.yml
+++ b/.github/workflows/cflite_batch.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: ClusterFuzzLite batch fuzzing
 on:
   schedule:
diff --git a/.github/workflows/cflite_pr.yml b/.github/workflows/cflite_pr.yml
index 656ba57c..98b9fe85 100644
--- a/.github/workflows/cflite_pr.yml
+++ b/.github/workflows/cflite_pr.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: ClusterFuzzLite PR fuzzing
 on:
   pull_request:
diff --git a/.github/workflows/chapel-ci.yml b/.github/workflows/chapel-ci.yml
index 9147d7a6..1d8b017b 100644
--- a/.github/workflows/chapel-ci.yml
+++ b/.github/workflows/chapel-ci.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: Chapel Accelerator CI
 
 on:
@@ -149,7 +150,7 @@ jobs:
       - uses: actions/checkout@v7.0.1
 
       - name: Install Rust toolchain
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
         with:
           toolchain: stable
 
@@ -203,7 +204,7 @@ jobs:
           version: 0.14.0
 
       - name: Install Rust
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
         with:
           toolchain: stable
 
diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml
index 4554278c..a49bf739 100644
--- a/.github/workflows/codeql.yml
+++ b/.github/workflows/codeql.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: CodeQL Security Analysis
 
 on:
diff --git a/.github/workflows/container-ci.yml b/.github/workflows/container-ci.yml
index 4df1a280..c1e101ce 100644
--- a/.github/workflows/container-ci.yml
+++ b/.github/workflows/container-ci.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 #
 # container-ci.yml — Container build verification.
 #
diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml
index 74c1ee4e..f0fd1fff 100644
--- a/.github/workflows/dogfood-gate.yml
+++ b/.github/workflows/dogfood-gate.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # dogfood-gate.yml — Hyperpolymath Dogfooding Quality Gate
diff --git a/.github/workflows/dogfood-proofs-ci.yml b/.github/workflows/dogfood-proofs-ci.yml
index 5e367e50..16ef05e0 100644
--- a/.github/workflows/dogfood-proofs-ci.yml
+++ b/.github/workflows/dogfood-proofs-ci.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # Gates the ECHIDNA dogfood proof corpus: every theorem under proofs/{coq,lean,agda}
 # must type-check. These proofs had no CI coverage before this workflow -- the other
 # proof workflows are path-filtered to meta-checker/** (agda-meta-checker) and
diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml
index c1a32c0b..5c2ed2b2 100644
--- a/.github/workflows/formal-verification.yml
+++ b/.github/workflows/formal-verification.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # formal-verification.yml — Creusot formal verification of the trust-pipeline kernel.
@@ -52,7 +53,7 @@ jobs:
         uses: actions/checkout@v7.0.1
 
       - name: Install stable Rust toolchain
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
         with:
           toolchain: stable
 
@@ -83,7 +84,7 @@ jobs:
         uses: actions/checkout@v7.0.1
 
       - name: Install nightly Rust toolchain (Creusot pin)
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
         with:
           # Pin matches crates/echidna-core-spark/rust-toolchain.toml.
           # Update both files together when bumping.
diff --git a/.github/workflows/generator-generic-ossf-slsa3-publish.yml b/.github/workflows/generator-generic-ossf-slsa3-publish.yml
index ac570fdf..3ff3b460 100644
--- a/.github/workflows/generator-generic-ossf-slsa3-publish.yml
+++ b/.github/workflows/generator-generic-ossf-slsa3-publish.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # This workflow uses actions that are not certified by GitHub.
 # They are provided by a third-party and are governed by
 # separate terms of service, privacy policy, and support
diff --git a/.github/workflows/ghcr-publish.yml b/.github/workflows/ghcr-publish.yml
index 5b3e6b85..d41787a0 100644
--- a/.github/workflows/ghcr-publish.yml
+++ b/.github/workflows/ghcr-publish.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: Publish to GHCR
 
 permissions:
diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml
index b5055a0e..c83309e2 100644
--- a/.github/workflows/governance.yml
+++ b/.github/workflows/governance.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: Governance
 
 on:
diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
index 90d3b3c4..17482cf9 100644
--- a/.github/workflows/hypatia-scan.yml
+++ b/.github/workflows/hypatia-scan.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: Hypatia Security Scan
 
 on:
diff --git a/.github/workflows/idris2-abi-ci.yml b/.github/workflows/idris2-abi-ci.yml
index b3c001f1..7fff30d0 100644
--- a/.github/workflows/idris2-abi-ci.yml
+++ b/.github/workflows/idris2-abi-ci.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: Idris2 ABI Type-Check
 
 on:
diff --git a/.github/workflows/label-triage.yml b/.github/workflows/label-triage.yml
index 9886e920..fc799478 100644
--- a/.github/workflows/label-triage.yml
+++ b/.github/workflows/label-triage.yml
@@ -1,4 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
+# This workflow is managed by gh actions-lock.
 name: Label Triage
 
 # Classify newly-filed issues against the estate label taxonomy.
diff --git a/.github/workflows/labels.yml b/.github/workflows/labels.yml
index c80b676c..af34c6b2 100644
--- a/.github/workflows/labels.yml
+++ b/.github/workflows/labels.yml
@@ -1,4 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
+# This workflow is managed by gh actions-lock.
 name: Labels
 
 # Applies the canonical estate label set from .github/labels.json.
diff --git a/.github/workflows/live-provers.yml b/.github/workflows/live-provers.yml
index 6759c565..0441c9ec 100644
--- a/.github/workflows/live-provers.yml
+++ b/.github/workflows/live-provers.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # ECHIDNA — Live-Prover CI
 #
 # Exercises real prover binaries against canonical micro-goals. Complements
@@ -79,7 +80,9 @@ jobs:
         uses: actions/checkout@v7.0.1
 
       - name: Install Rust
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: stable
 
       - name: Cache Cargo
         uses: Swatinem/rust-cache@v2.9.2
@@ -172,7 +175,9 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v7.0.1
       - name: Install Rust
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: stable
       - name: Cache Cargo
         uses: Swatinem/rust-cache@v2.9.2
       - name: Provision ${{ matrix.backend }} (best-effort via apt / upstream release)
@@ -320,7 +325,9 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v7.0.1
       - name: Install Rust
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: stable
       - name: Cache Cargo
         uses: Swatinem/rust-cache@v2.9.2
       - name: Provision ${{ matrix.backend }} (best-effort)
@@ -448,7 +455,9 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v7.0.1
       - name: Install Rust
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: stable
       - name: Cache Cargo
         uses: Swatinem/rust-cache@v2.9.2
       - name: Provision ${{ matrix.backend }} (best-effort, CUDA/OpenCL required)
diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml
index 70f3f271..5c73f975 100644
--- a/.github/workflows/mirror.yml
+++ b/.github/workflows/mirror.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: Mirror to Git Forges
 
 on:
diff --git a/.github/workflows/mvp-smoke.yml b/.github/workflows/mvp-smoke.yml
index 43e30c68..2df68dd1 100644
--- a/.github/workflows/mvp-smoke.yml
+++ b/.github/workflows/mvp-smoke.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: MVP Smoke (Best Effort)
 
 on:
@@ -33,7 +34,7 @@ jobs:
         uses: actions/checkout@v7.0.1
 
       - name: Setup Rust toolchain
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
         with:
           toolchain: stable
 
diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml
index bb10ea65..cf06fcd5 100644
--- a/.github/workflows/pages.yml
+++ b/.github/workflows/pages.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: GitHub Pages (Ddraig SSG)
 on:
   push:
diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index b7811e36..5b91710e 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -1,5 +1,5 @@
-# This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: AGPL-3.0-or-later
+# This workflow is managed by gh actions-lock.
 name: Proof Safety
 on:
   pull_request:
diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml
index 426478db..f8fbe1ae 100644
--- a/.github/workflows/rust-ci.yml
+++ b/.github/workflows/rust-ci.yml
@@ -1,6 +1,8 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # Rust CI — thin wrapper calling the shared estate reusable in
 # hyperpolymath/standards. Configure once, propagate everywhere.
 # See: docs/CI-REUSABLE-WORKFLOWS.adoc in standards.
@@ -17,7 +19,7 @@ permissions:
 
 jobs:
   rust-ci:
-    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd # main 2026-08-04 (lockfile-bearing ref: actions.lock required by caller-side enforcement, standards#570)
+    uses: ./.github/workflows/rust-native-reusable.yml # main 2026-08-04 (lockfile-bearing ref: actions.lock required by caller-side enforcement, standards#570)
     with:
       enable_audit: true
       enable_coverage: true
diff --git a/.github/workflows/rust-native-reusable.yml b/.github/workflows/rust-native-reusable.yml
new file mode 100644
index 00000000..498c4183
--- /dev/null
+++ b/.github/workflows/rust-native-reusable.yml
@@ -0,0 +1,360 @@
+# SPDX-License-Identifier: MPL-2.0
+# This workflow is managed by gh actions-lock.
+# Derived from hyperpolymath/standards@571cc734cd69fb846032ec77a662aa8ee4fc32cd.
+# Native workspace variant installs schema compilers before check/test/coverage.
+# This workflow is managed by gh actions-lock.
+# rust-ci-reusable.yml — Reusable Rust CI bundle (RSR).
+#
+# Replaces the per-repo `rust-ci.yml` template that copy-drifted across
+# the estate. Estate audit (2026-05-26) found:
+#
+#   * 137 repos shipping their own copy of rust-ci.yml
+#   * 30 unique SHAs — same logical workflow, drifted independently
+#   * Recurring failure modes across PRs: missing top-level
+#     `permissions:`, inconsistent `if: hashFiles('Cargo.toml')`
+#     guards, `cargo audit` re-installing every run, license-header
+#     drift (PMPL/MPL/AGPL), inconsistent SHA pins.
+#
+# The reusable bundles the union of features observed across the
+# variants and gates the slow extras (audit, coverage) behind opt-in
+# inputs so consumers only pay for what they want.
+#
+# Caller example (single wrapper, mirrors governance.yml + deno-ci.yml):
+#
+#   jobs:
+#     rust-ci:
+#       uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@70cdad0e95bb2366a9b2ae9789c0e377fef6e3ef
+#
+# With audit + coverage enabled:
+#
+#   jobs:
+#     rust-ci:
+#       uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@70cdad0e95bb2366a9b2ae9789c0e377fef6e3ef
+#       with:
+#         enable_audit: true
+#         enable_coverage: true
+#         zig_version: "0.15.2" # for Rust crates with a Zig-native build
+#
+# Sub-crate / monorepo workspace (Cargo.toml lives in a subdirectory):
+#
+#   jobs:
+#     rust-ci-cli:
+#       uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@70cdad0e95bb2366a9b2ae9789c0e377fef6e3ef
+#       with:
+#         working_directory: crates/cli
+#     rust-ci-server:
+#       uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@70cdad0e95bb2366a9b2ae9789c0e377fef6e3ef
+#       with:
+#         working_directory: crates/server
+#
+# Out-of-scope (left bespoke per-repo): multi-OS matrices, cross-compile
+# (`cross build`), multi-Rust-version matrices. Each has too much per-repo
+# variance to share a single abstraction cleanly (verified against the 5
+# matrix-using repos as of 2026-05-26: julia-the-viper / verisimdb /
+# verisimiser / reasonably-good-token-vault use four different matrix
+# dimensions).
+
+name: Rust CI (native workspace)
+
+on:
+  workflow_call:
+    inputs:
+      runs-on:
+        description: Runner label for all Rust CI jobs
+        type: string
+        required: false
+        default: ubuntu-latest
+      enable_audit:
+        description: Run `cargo audit` (slow — installs each run; off by default)
+        type: boolean
+        required: false
+        default: false
+      enable_coverage:
+        description: Measure line coverage with cargo-llvm-cov and enforce `coverage_floor` (off by default)
+        type: boolean
+        required: false
+        default: false
+      coverage_floor:
+        description: Minimum line-coverage percent when enable_coverage is set; ratchet upward, never lower.
+        type: string
+        required: false
+        default: "0"
+      clippy_args:
+        description: Args appended to `cargo clippy`
+        type: string
+        required: false
+        default: "--all-targets -- -D warnings"
+      test_args:
+        description: Args appended to `cargo test`
+        type: string
+        required: false
+        default: "--all-targets"
+      check_args:
+        description: Args appended to `cargo check`
+        type: string
+        required: false
+        default: "--all-targets"
+      working_directory:
+        description: |
+          Directory containing `Cargo.toml` (relative to the repo root). All
+          cargo invocations cd into this directory; `hashFiles()` guards also
+          consult it. Default `.` keeps single-crate repos unchanged. Set
+          to e.g. `crates/server` for a sub-crate, or pass a different
+          value per wrapper call when running the reusable in a workspace
+          via separate jobs.
+        type: string
+        required: false
+        default: "."
+      zig_version:
+        description: |
+          Exact Zig version required by a Rust crate's native build. Leave
+          empty for pure-Rust workspaces. When set, check, test, and coverage
+          jobs install the same compiler before invoking Cargo.
+        type: string
+        required: false
+        default: ""
+
+# Only `contents: read` is requested. A reusable workflow may narrow the
+# caller's permissions but never widen them: requesting a permission the
+# caller has not granted aborts the run as `startup_failure` with ZERO
+# jobs — no logs, no red step, just an empty run. The previous
+# `actions: read` here was used by no job in this file, so every caller
+# granting only `contents: read` (the estate default) failed to start.
+permissions:
+  contents: read
+
+jobs:
+  # Skip the whole reusable when the repo has no Cargo.toml — lets consumers
+  # add the wrapper unconditionally without worrying about repos that don't
+  # ship Rust code yet. This MUST be a checked-out step, NOT a job-level
+  # `if: hashFiles(...)`: job `if:` is evaluated server-side before any
+  # checkout, so hashFiles() sees an empty workspace and always returns ''
+  # — which silently skipped every job on EVERY repo, Rust or not. The
+  # detect job checks out and exposes a real boolean the others gate on.
+  detect:
+    timeout-minutes: 5
+    name: Detect Cargo.toml
+    runs-on: ${{ inputs.runs-on }}
+    permissions:
+      contents: read
+    outputs:
+      has_cargo: ${{ steps.detect.outputs.has_cargo }}
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          repository: ${{ github.repository }}
+          ref: ${{ github.ref }}
+      - name: Detect Cargo.toml
+        id: detect
+        run: |
+          if [ -f "${{ inputs.working_directory }}/Cargo.toml" ]; then
+            echo "has_cargo=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "has_cargo=false" >> "$GITHUB_OUTPUT"
+          fi
+
+  check:
+    timeout-minutes: 20
+    name: Cargo check + clippy + fmt
+    runs-on: ${{ inputs.runs-on }}
+    needs: detect
+    if: ${{ needs.detect.outputs.has_cargo == 'true' }}
+    permissions:
+      contents: read
+    defaults:
+      run:
+        working-directory: ${{ inputs.working_directory }}
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          repository: ${{ github.repository }}
+          ref: ${{ github.ref }}
+
+      - name: Install Rust toolchain
+        # `toolchain:` is mandatory because the action is pinned by commit SHA:
+        # dtolnay/rust-toolchain infers the toolchain from the `@`-ref (e.g.
+        # `@stable`), but a SHA ref carries no version, so the action's "parse
+        # toolchain version" step fails with `'toolchain' is a required input`.
+        # See standards estate-wide rust-ci red.
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: stable
+          components: clippy, rustfmt
+
+      - name: Install native schema compilers
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y capnproto protobuf-compiler pkg-config libssl-dev
+
+      - name: Install Zig for native build
+        if: ${{ inputs.zig_version != '' }}
+        uses: goto-bus-stop/setup-zig@v2.2.1
+        with:
+          version: ${{ inputs.zig_version }}
+
+      - name: Cache cargo registry and build
+        uses: Swatinem/rust-cache@v2.9.2
+        with:
+          workspaces: ${{ inputs.working_directory }}
+
+      - name: Cargo check
+        # `--locked` so CI honours `Cargo.lock` and surfaces dep drift the
+        # first push it happens, instead of silently re-resolving (which
+        # masked the echidna#92 / echidna PR #128 dependabot major-bump
+        # break for 24h). See standards#295.
+        run: cargo check --locked ${{ inputs.check_args }}
+
+      - name: Cargo fmt
+        run: cargo fmt --all -- --check
+
+      - name: Cargo clippy
+        run: cargo clippy --locked ${{ inputs.clippy_args }}
+
+  test:
+    timeout-minutes: 20
+    name: Cargo test
+    runs-on: ${{ inputs.runs-on }}
+    needs: [detect, check]
+    if: ${{ needs.detect.outputs.has_cargo == 'true' }}
+    permissions:
+      contents: read
+    defaults:
+      run:
+        working-directory: ${{ inputs.working_directory }}
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          repository: ${{ github.repository }}
+          ref: ${{ github.ref }}
+
+      - name: Install Rust toolchain
+        # `toolchain:` mandatory under SHA pin — see Cargo check job above.
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: stable
+
+      - name: Install native schema compilers
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y capnproto protobuf-compiler pkg-config libssl-dev
+
+      - name: Install Zig for native build
+        if: ${{ inputs.zig_version != '' }}
+        uses: goto-bus-stop/setup-zig@v2.2.1
+        with:
+          version: ${{ inputs.zig_version }}
+
+      - name: Cache cargo registry and build
+        uses: Swatinem/rust-cache@v2.9.2
+        with:
+          workspaces: ${{ inputs.working_directory }}
+
+      - name: Run tests
+        # `--locked` — see Cargo check above.
+        run: cargo test --locked ${{ inputs.test_args }}
+
+      - name: Write summary
+        if: always()
+        run: |
+          {
+            echo "## Rust CI Results"
+            echo ""
+            echo "- **cargo check**: ${{ needs.check.result }}"
+            echo "- **cargo test**: completed"
+          } >> "$GITHUB_STEP_SUMMARY"
+
+  audit:
+    timeout-minutes: 20
+    name: Cargo audit (security)
+    runs-on: ${{ inputs.runs-on }}
+    needs: detect
+    if: ${{ inputs.enable_audit && needs.detect.outputs.has_cargo == 'true' }}
+    permissions:
+      contents: read
+    defaults:
+      run:
+        working-directory: ${{ inputs.working_directory }}
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          repository: ${{ github.repository }}
+          ref: ${{ github.ref }}
+
+      - name: Install Rust toolchain
+        # `toolchain:` mandatory under SHA pin — see Cargo check job above.
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: stable
+
+      - name: Install cargo-audit
+        # Use the binstall path when available to skip a from-source rebuild
+        # on every run — was the single biggest contributor to slow CI on
+        # repos that opted in to audit (~3–4 minute install).
+        run: cargo install cargo-audit --locked
+
+      - name: Security audit
+        run: cargo audit
+
+  coverage:
+    timeout-minutes: 25
+    name: llvm-cov line coverage
+    runs-on: ${{ inputs.runs-on }}
+    needs: detect
+    if: ${{ inputs.enable_coverage && needs.detect.outputs.has_cargo == 'true' }}
+    permissions:
+      contents: read
+    defaults:
+      run:
+        working-directory: ${{ inputs.working_directory }}
+    env:
+      # Ratcheted line-coverage floor (from the caller). Raise toward target; never lower.
+      FLOOR: ${{ inputs.coverage_floor }}
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          repository: ${{ github.repository }}
+          ref: ${{ github.ref }}
+
+      - name: Install Rust toolchain
+        # `toolchain:` mandatory under SHA pin — see Cargo check job above.
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: stable
+          components: llvm-tools-preview
+
+      - name: Install native schema compilers
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y capnproto protobuf-compiler pkg-config libssl-dev
+
+      - name: Install Zig for native build
+        if: ${{ inputs.zig_version != '' }}
+        uses: goto-bus-stop/setup-zig@v2.2.1
+        with:
+          version: ${{ inputs.zig_version }}
+
+      - name: Install cargo-llvm-cov
+        run: cargo install cargo-llvm-cov --locked
+
+      - name: Measure line coverage
+        id: cov
+        # Self-contained: no external coverage service. Own the gate on our runner.
+        run: |
+          set -euo pipefail
+          cargo llvm-cov --workspace --locked --json --output-path cov.json
+          PCT=$(jq -r '.data[0].totals.lines.percent' cov.json)
+          printf '### Line coverage: %.2f%% (floor %s%%)\n' "$PCT" "$FLOOR" >> "$GITHUB_STEP_SUMMARY"
+          echo "pct=$PCT" >> "$GITHUB_OUTPUT"
+
+      - name: Enforce ratchet floor
+        run: |
+          set -euo pipefail
+          awk -v p="${{ steps.cov.outputs.pct }}" -v f="$FLOOR" 'BEGIN {
+            if (p + 0 < f + 0) { printf "FAIL: line coverage %.2f%% is below floor %s%%\n", p, f; exit 1 }
+            printf "OK: line coverage %.2f%% >= floor %s%%\n", p, f
+          }'
diff --git a/.github/workflows/s4-loop.yml b/.github/workflows/s4-loop.yml
index cbf413fd..195e2ca5 100644
--- a/.github/workflows/s4-loop.yml
+++ b/.github/workflows/s4-loop.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # S4 loop-closure CI — brings up verisim-api as a service container and
 # runs the echidna s4_loop_closure integration test.  Filed once
 # ghcr.io/hyperpolymath/verisimdb-api:latest became available (PR #121).
@@ -36,7 +37,7 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v7.0.1
       - name: Setup Rust toolchain
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
         with:
           toolchain: stable
       - name: Cache Cargo
diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml
index dda49f8b..2a86ea21 100644
--- a/.github/workflows/scorecard.yml
+++ b/.github/workflows/scorecard.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: OSSF Scorecard
 
 on:
diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml
index d44fcdc6..e4a727cc 100644
--- a/.github/workflows/secret-scanner.yml
+++ b/.github/workflows/secret-scanner.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 name: Secret Scanner
 
 on:
diff --git a/.github/workflows/security-scan.yml b/.github/workflows/security-scan.yml
index dea6bdd6..3f08f5f2 100644
--- a/.github/workflows/security-scan.yml
+++ b/.github/workflows/security-scan.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 
 name: Security Scan
 
diff --git a/.github/workflows/server-boot-gate.yml b/.github/workflows/server-boot-gate.yml
index 8a0ab3bf..9234df5f 100644
--- a/.github/workflows/server-boot-gate.yml
+++ b/.github/workflows/server-boot-gate.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # Server boot gate — builds the echidna binary, boots the server, and
 # verifies that /api/health, /api/provers, and a session {id} route all
 # respond.  Exists so "compiles" can never again mean "boots" — the
@@ -28,7 +29,7 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v7.0.1
       - name: Setup Rust toolchain
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@master
         with:
           toolchain: stable
       - name: Cache Cargo
diff --git a/.github/workflows/spark-theatre-gate.yml b/.github/workflows/spark-theatre-gate.yml
index 230c6458..e1958317 100644
--- a/.github/workflows/spark-theatre-gate.yml
+++ b/.github/workflows/spark-theatre-gate.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # Estate SPARK Theatre Gate — thin caller of the reusable workflow in
 # hyperpolymath/standards (#135 / #141). Pinned by commit SHA per the
 # estate action-pinning policy. Regenerate the pin only when the reusable
diff --git a/.github/workflows/verification-proofs-cron.yml b/.github/workflows/verification-proofs-cron.yml
index abfb7c93..06513f7c 100644
--- a/.github/workflows/verification-proofs-cron.yml
+++ b/.github/workflows/verification-proofs-cron.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # Weekly verification of the heavier self-proof corpora that are too slow and too
 # network-heavy to gate on every PR: currently Isabelle/HOL (proofs/isabelle). The
 # Isabelle toolchain is a large, non-apt download (~500MB tarball), so this runs on
diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml
index c3cf64db..2e3180cb 100644
--- a/.github/workflows/workflow-linter.yml
+++ b/.github/workflows/workflow-linter.yml
@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
+# This workflow is managed by gh actions-lock.
 # Prevention workflow - validates all workflows have proper security config
 name: Workflow Security Linter
 
diff --git a/.machine_readable/contractiles/intend/intend.k9.ncl b/.machine_readable/contractiles/intend/intend.k9.ncl
index 59c4d48e..6c7d454a 100644
--- a/.machine_readable/contractiles/intend/intend.k9.ncl
+++ b/.machine_readable/contractiles/intend/intend.k9.ncl
@@ -30,7 +30,7 @@ K9!
 #   (feedback_audit_tool_suppression_design.md — structural > markers).
 # * Sessional drift detection hooks (on_close, on_open).
 # * Ratification at session open; drift log at session close.
-# * Evidence sinks: VeriSimDB (queryable) + 6a2/DRIFT.a2ml (repo-local).
+# * Evidence sinks: VeriSimDB (queryable) + descriptiles/DRIFT.a2ml (repo-local).
 # * Failure-mode defenses cross-referenced to the AI failure catalog.
 
 let base_k9 = import "../k9/template-hunt.k9.ncl" in
@@ -66,6 +66,7 @@ let base    = import "../_base.ncl" in
 
     security = {
       leash = 'Hunt,
+      signature_required = true,
       trust_level = "subprocess + filesystem-read",
       allow_network = false,
       allow_filesystem_write = false,   # evidence sinks are indirected
@@ -120,7 +121,7 @@ let base    = import "../_base.ncl" in
     # VeriSimDB = queryable machine record (feedback_verisimdb_policy.md);
     # ECHIDNA records every proof attempt to VeriSimDB, so contractile
     # executions land in the same store for cross-query.
-    # 6a2/DRIFT.a2ml = repo-local append-only drift log (feedback_sessional_
+    # descriptiles/DRIFT.a2ml = repo-local append-only drift log (feedback_sessional_
     # drift_detection.md + user_6a2_is_contractile_ought.md descriptive role).
     evidence_sinks = [
       {
@@ -130,7 +131,7 @@ let base    = import "../_base.ncl" in
       },
       {
         kind        = 'drift_log,
-        path        = ".machine_readable/6a2/DRIFT.a2ml",
+        path        = ".machine_readable/descriptiles/DRIFT.a2ml",
         append_only = true,
       },
     ],
@@ -222,7 +223,7 @@ let base    = import "../_base.ncl" in
             # the AI is the holder of the line against enthusiasm drift.
           },
         ],
-        signed_record_destination = ".machine_readable/6a2/ratification-<session-id>.a2ml",
+        signed_record_destination = ".machine_readable/descriptiles/ratification-<session-id>.a2ml",
         must_precede_work = true,
       },
 
diff --git a/Cargo.lock b/Cargo.lock
index e544b40f..dcb0ed11 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -155,9 +155,9 @@ dependencies = [
 
 [[package]]
 name = "anyhow"
-version = "1.0.102"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c"
+checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"
 
 [[package]]
 name = "approx"
@@ -544,9 +544,9 @@ checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724"
 
 [[package]]
 name = "chacha20"
-version = "0.10.0"
+version = "0.10.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6f8d983286843e49675a4b7a2d174efe136dc93a18d69130dd18198a6c167601"
+checksum = "65c35e4b699c7e15ccbe7ee35c005e4fc0a278d22238a2857e6ce2dadeda1b06"
 dependencies = [
  "cfg-if",
  "cpufeatures 0.3.0",
@@ -1097,7 +1097,7 @@ dependencies = [
  "lazy_static",
  "nalgebra",
  "nom",
- "num-bigint 0.5.0",
+ "num-bigint 0.5.1",
  "num-integer",
  "num-traits",
  "pretty_assertions",
@@ -1558,9 +1558,9 @@ checksum = "8fb167719045debebe9f532320accc7b5c993c5a3b813f5696a11d5ca7bdc57b"
 
 [[package]]
 name = "h2"
-version = "0.4.14"
+version = "0.4.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "171fefbc92fe4a4de27e0698d6a5b392d6a0e333506bc49133760b3bcf948733"
+checksum = "a9f37a958b41b3b19ee2707c06439c0e9e547e847223eb791ecb0cb821c65e27"
 dependencies = [
  "atomic-waker",
  "bytes",
@@ -2227,9 +2227,9 @@ dependencies = [
 
 [[package]]
 name = "num-bigint"
-version = "0.4.7"
+version = "0.4.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c863e9ab5e7bf9c99ba75e1050f1e4d624ae87ed3532d6238ffbdc7b585dbbe6"
+checksum = "c89e69e7e0f03bea5ef08013795c25018e101932225a656383bd384495ecc367"
 dependencies = [
  "num-integer",
  "num-traits",
@@ -2237,9 +2237,9 @@ dependencies = [
 
 [[package]]
 name = "num-bigint"
-version = "0.5.0"
+version = "0.5.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7032fbb7ef662c18e806aa75b311f68ddf5c94e8fc62832c0039d79095ab6abf"
+checksum = "93e7820bc0a80a0238e650327316f929ba18d5be054b647490a3a6a339f3e7c0"
 dependencies = [
  "num-integer",
  "num-traits",
@@ -2284,7 +2284,7 @@ version = "0.4.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f83d14da390562dca69fc84082e73e548e1ad308d24accdedd2720017cb37824"
 dependencies = [
- "num-bigint 0.4.7",
+ "num-bigint 0.4.8",
  "num-integer",
  "num-traits",
 ]
@@ -3484,9 +3484,9 @@ dependencies = [
 
 [[package]]
 name = "spin"
-version = "0.9.8"
+version = "0.9.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6980e8d7511241f8acf4aebddbb1ff938df5eebe98691418c4468d0b72a96a67"
+checksum = "3763264f6b73151db08c50ff20d7d8a0b8796e021cdea7ceedad07b80155fa0e"
 
 [[package]]
 name = "spki"
diff --git a/fuzz/Cargo.lock b/fuzz/Cargo.lock
index 37b3e1fc..0cf3a9c3 100644
--- a/fuzz/Cargo.lock
+++ b/fuzz/Cargo.lock
@@ -128,9 +128,18 @@ dependencies = [
 
 [[package]]
 name = "anyhow"
-version = "1.0.102"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c"
+checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"
+
+[[package]]
+name = "approx"
+version = "0.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cab112f0a86d568ea0e627cc1d6be74a1e9cd55214684db5561995f6dad897c6"
+dependencies = [
+ "num-traits",
+]
 
 [[package]]
 name = "arbitrary"
@@ -178,14 +187,14 @@ checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8"
 
 [[package]]
 name = "axum"
-version = "0.7.9"
+version = "0.8.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "edca88bc138befd0323b20752846e6587272d3b03b0343c8ea28a6f819e6e71f"
+checksum = "31b698c5f9a010f6573133b09e0de5408834d0c82f8d7475a89fc1867a71cd90"
 dependencies = [
- "async-trait",
  "axum-core",
  "axum-macros",
  "bytes",
+ "form_urlencoded",
  "futures-util",
  "http",
  "http-body",
@@ -198,8 +207,7 @@ dependencies = [
  "mime",
  "percent-encoding",
  "pin-project-lite",
- "rustversion",
- "serde",
+ "serde_core",
  "serde_json",
  "serde_path_to_error",
  "serde_urlencoded",
@@ -213,19 +221,17 @@ dependencies = [
 
 [[package]]
 name = "axum-core"
-version = "0.4.5"
+version = "0.5.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09f2bd6146b97ae3359fa0cc6d6b376d9539582c7b4220f041a33ec24c226199"
+checksum = "08c78f31d7b1291f7ee735c1c6780ccde7785daae9a9206026862dab7d8792d1"
 dependencies = [
- "async-trait",
  "bytes",
- "futures-util",
+ "futures-core",
  "http",
  "http-body",
  "http-body-util",
  "mime",
  "pin-project-lite",
- "rustversion",
  "sync_wrapper",
  "tower-layer",
  "tower-service",
@@ -234,9 +240,9 @@ dependencies = [
 
 [[package]]
 name = "axum-macros"
-version = "0.4.2"
+version = "0.5.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "57d123550fa8d071b7255cb0cc04dc302baa6c8c4a79f55701552684d8399bce"
+checksum = "7aa268c23bfbbd2c4363b9cd302a4f504fb2a9dfe7e3451d66f35dd392e20aca"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -249,6 +255,12 @@ version = "0.22.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6"
 
+[[package]]
+name = "base64ct"
+version = "1.8.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2af50177e190e07a26ab74f8b1efbfe2ef87da2116221318cb1c2e82baf7de06"
+
 [[package]]
 name = "bitflags"
 version = "2.11.1"
@@ -266,7 +278,25 @@ dependencies = [
  "cc",
  "cfg-if",
  "constant_time_eq",
- "cpufeatures",
+ "cpufeatures 0.3.0",
+]
+
+[[package]]
+name = "block-buffer"
+version = "0.10.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3078c7629b62d3f0439517fa394996acacc5cbc91c5a20d8c658e77abd503a71"
+dependencies = [
+ "generic-array",
+]
+
+[[package]]
+name = "block-buffer"
+version = "0.12.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d2f6c7dbe95a6ed67ad9f18e57daf93a2f034c524b99fd2b76d18fdfeb6660aa"
+dependencies = [
+ "hybrid-array",
 ]
 
 [[package]]
@@ -275,6 +305,12 @@ version = "3.20.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5d20789868f4b01b2f2caec9f5c4e0213b41e3e5702a50157d699ae31ced2fcb"
 
+[[package]]
+name = "bytemuck"
+version = "1.25.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "95832e849adfb21180ccb6826a99da14e5d266ae5c2e668e1602cf234f153797"
+
 [[package]]
 name = "bytes"
 version = "1.11.1"
@@ -305,6 +341,17 @@ version = "0.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724"
 
+[[package]]
+name = "chacha20"
+version = "0.10.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "65c35e4b699c7e15ccbe7ee35c005e4fc0a278d22238a2857e6ce2dadeda1b06"
+dependencies = [
+ "cfg-if",
+ "cpufeatures 0.3.0",
+ "rand_core 0.10.1",
+]
+
 [[package]]
 name = "chrono"
 version = "0.4.44"
@@ -395,6 +442,18 @@ dependencies = [
  "windows-sys 0.61.2",
 ]
 
+[[package]]
+name = "const-oid"
+version = "0.9.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c2459377285ad874054d797f3ccebf984978aa39129f6eafde5cdc8315b612f8"
+
+[[package]]
+name = "const-oid"
+version = "0.10.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a6ef517f0926dd24a1582492c791b6a4818a4d94e789a334894aa15b0d12f55c"
+
 [[package]]
 name = "constant_time_eq"
 version = "0.4.2"
@@ -407,6 +466,15 @@ version = "0.8.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b"
 
+[[package]]
+name = "cpufeatures"
+version = "0.2.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "59ed5838eebb26a2bb2e58f6d5b5316989ae9d08bab10e0e6d103e656d1b0280"
+dependencies = [
+ "libc",
+]
+
 [[package]]
 name = "cpufeatures"
 version = "0.3.0"
@@ -437,6 +505,62 @@ version = "0.2.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "460fbee9c2c2f33933d720630a6a0bac33ba7053db5344fac858d4b8952d77d5"
 
+[[package]]
+name = "crypto-common"
+version = "0.1.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "78c8292055d1c1df0cce5d180393dc8cce0abec0a7102adb6c7b1eef6016d60a"
+dependencies = [
+ "generic-array",
+ "typenum",
+]
+
+[[package]]
+name = "crypto-common"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ce6e4c961d6cd6c9a86db418387425e8bdeaf05b3c8bc1411e6dca4c252f1453"
+dependencies = [
+ "hybrid-array",
+]
+
+[[package]]
+name = "curve25519-dalek"
+version = "4.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "97fb8b7c4503de7d6ae7b42ab72a5a59857b4c937ec27a3d4539dba95b5ab2be"
+dependencies = [
+ "cfg-if",
+ "cpufeatures 0.2.17",
+ "curve25519-dalek-derive",
+ "digest 0.10.7",
+ "fiat-crypto",
+ "rustc_version",
+ "subtle",
+ "zeroize",
+]
+
+[[package]]
+name = "curve25519-dalek-derive"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f46882e17999c6cc590af592290432be3bce0428cb0d5f8b6715e4dc7b383eb3"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "der"
+version = "0.7.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e7c1832837b905bbfb5101e07cc24c8deddf52f93225eee6ead5f4d63d53ddcb"
+dependencies = [
+ "const-oid 0.9.6",
+ "zeroize",
+]
+
 [[package]]
 name = "derive_arbitrary"
 version = "1.4.2"
@@ -448,6 +572,27 @@ dependencies = [
  "syn",
 ]
 
+[[package]]
+name = "digest"
+version = "0.10.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292"
+dependencies = [
+ "block-buffer 0.10.4",
+ "crypto-common 0.1.7",
+]
+
+[[package]]
+name = "digest"
+version = "0.11.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f1dd6dbb5841937940781866fa1281a1ff7bd3bf827091440879f9994983d5c2"
+dependencies = [
+ "block-buffer 0.12.1",
+ "const-oid 0.10.2",
+ "crypto-common 0.2.2",
+]
+
 [[package]]
 name = "displaydoc"
 version = "0.2.5"
@@ -461,7 +606,7 @@ dependencies = [
 
 [[package]]
 name = "echidna"
-version = "2.1.0"
+version = "2.3.0"
 dependencies = [
  "actix",
  "anyhow",
@@ -472,22 +617,29 @@ dependencies = [
  "clap",
  "colored",
  "echidna-core",
+ "ed25519-dalek",
  "futures",
  "indicatif",
  "lazy_static",
+ "nalgebra",
  "nom",
- "rand 0.8.6",
+ "num-bigint 0.5.1",
+ "num-integer",
+ "num-traits",
+ "rand 0.10.2",
  "reqwest",
+ "rustfft",
  "rustyline",
  "serde",
  "serde_json",
+ "sha2 0.11.0",
  "tempfile",
  "thiserror",
  "tiny-keccak",
  "tokio",
  "toml",
  "tower",
- "tower-http",
+ "tower-http 0.7.1",
  "tracing",
  "tracing-subscriber",
  "typed-wasm",
@@ -512,6 +664,30 @@ dependencies = [
  "serde_json",
 ]
 
+[[package]]
+name = "ed25519"
+version = "2.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "115531babc129696a58c64a4fef0a8bf9e9698629fb97e9e40767d235cfbcd53"
+dependencies = [
+ "pkcs8",
+ "signature",
+]
+
+[[package]]
+name = "ed25519-dalek"
+version = "2.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "70e796c081cee67dc755e1a36a0a172b897fab85fc3f6bc48307991f64e4eca9"
+dependencies = [
+ "curve25519-dalek",
+ "ed25519",
+ "serde",
+ "sha2 0.10.9",
+ "subtle",
+ "zeroize",
+]
+
 [[package]]
 name = "encode_unicode"
 version = "1.0.0"
@@ -520,9 +696,9 @@ checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0"
 
 [[package]]
 name = "endian-type"
-version = "0.1.2"
+version = "0.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c34f04666d835ff5d62e058c3995147c06f42fe86ff053337632bca83e42702d"
+checksum = "869b0adbda23651a9c5c0c3d270aac9fcb52e8622a8f2b17e57802d7791962f2"
 
 [[package]]
 name = "equivalent"
@@ -553,15 +729,10 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9f1f227452a390804cdb637b74a86990f2a7d7ba4b7d5693aac9b4dd6defd8d6"
 
 [[package]]
-name = "fd-lock"
-version = "4.0.4"
+name = "fiat-crypto"
+version = "0.2.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0ce92ff622d6dadf7349484f42c93271a0d49b7cc4d466a936405bacbe10aa78"
-dependencies = [
- "cfg-if",
- "rustix",
- "windows-sys 0.59.0",
-]
+checksum = "28dea519a9695b9977216879a3ebfddf92f1c08c05d984f8996aecd6ecdc811d"
 
 [[package]]
 name = "find-msvc-tools"
@@ -672,6 +843,16 @@ dependencies = [
  "slab",
 ]
 
+[[package]]
+name = "generic-array"
+version = "0.14.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "85649ca51fd72272d7821adaf274ad91c288277713d9c18820d8499a7ff69e9a"
+dependencies = [
+ "typenum",
+ "version_check",
+]
+
 [[package]]
 name = "getrandom"
 version = "0.2.17"
@@ -708,10 +889,35 @@ dependencies = [
  "cfg-if",
  "libc",
  "r-efi 6.0.0",
+ "rand_core 0.10.1",
  "wasip2",
  "wasip3",
 ]
 
+[[package]]
+name = "glam"
+version = "0.30.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "19fc433e8437a212d1b6f1e68c7824af3aed907da60afa994e7f542d18d12aa9"
+
+[[package]]
+name = "glam"
+version = "0.31.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "556f6b2ea90b8d15a74e0e7bb41671c9bdf38cd9f78c284d750b9ce58a2b5be7"
+
+[[package]]
+name = "glam"
+version = "0.32.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f70749695b063ecbf6b62949ccccde2e733ec3ecbbd71d467dca4e5c6c97cca0"
+
+[[package]]
+name = "glam"
+version = "0.33.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "21fef0953c54fd3de2f44b743fbf77e044c81a25faee03636dfccc0d35135e23"
+
 [[package]]
 name = "hashbrown"
 version = "0.15.5"
@@ -787,6 +993,15 @@ version = "1.0.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "df3b46402a9d5adb4c86a0cf463f42e19994e3ee891101b1841f30a545cb49a9"
 
+[[package]]
+name = "hybrid-array"
+version = "0.4.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "707114b52a152fa7bdb290cd7cd5912d9467273b6d74e21b8d81aca1f8533f6b"
+dependencies = [
+ "typenum",
+]
+
 [[package]]
 name = "hyper"
 version = "1.9.0"
@@ -1069,9 +1284,9 @@ checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2"
 
 [[package]]
 name = "libc"
-version = "0.2.185"
+version = "0.2.189"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "52ff2c0fe9bc6cb6b14a0592c2ff4fa9ceb83eea9db979b0487cd054946a2b8f"
+checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"
 
 [[package]]
 name = "libfuzzer-sys"
@@ -1127,9 +1342,19 @@ dependencies = [
 
 [[package]]
 name = "matchit"
-version = "0.7.3"
+version = "0.8.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0e7465ac9959cc2b1404e8e2367b43684a6d13790fe23056cc8c6c5a6b7bcb94"
+checksum = "47e1ffaa40ddd1f3ed91f717a33c8c0ee23fff369e3aa8772b9605cc1d22f4c3"
+
+[[package]]
+name = "matrixmultiply"
+version = "0.3.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f607c237553f086e7043417a51df26b2eb899d3caff94e6a67592ff992fedc7"
+dependencies = [
+ "autocfg",
+ "rawpointer",
+]
 
 [[package]]
 name = "memchr"
@@ -1143,12 +1368,6 @@ version = "0.3.17"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6877bb514081ee2a7ff5ef9de3281f14a4dd4bceac4c09388074a6b5df8a139a"
 
-[[package]]
-name = "minimal-lexical"
-version = "0.2.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
-
 [[package]]
 name = "mio"
 version = "1.2.0"
@@ -1160,6 +1379,37 @@ dependencies = [
  "windows-sys 0.61.2",
 ]
 
+[[package]]
+name = "nalgebra"
+version = "0.35.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "adc43a60c217b0c6ff46e47f26911015ad8d2e5a8be1af668c67e370d99a4346"
+dependencies = [
+ "approx",
+ "glam 0.30.10",
+ "glam 0.31.1",
+ "glam 0.32.1",
+ "glam 0.33.6",
+ "matrixmultiply",
+ "nalgebra-macros",
+ "num-complex",
+ "num-rational",
+ "num-traits",
+ "simba",
+ "typenum",
+]
+
+[[package]]
+name = "nalgebra-macros"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "973e7178a678cfd059ccec50887658d482ce16b0aa9da3888ddeab5cd5eb4889"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
 [[package]]
 name = "nibble_vec"
 version = "0.1.0"
@@ -1171,9 +1421,9 @@ dependencies = [
 
 [[package]]
 name = "nix"
-version = "0.29.0"
+version = "0.31.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "71e2746dc3a24dd78b3cfcb7be93368c6de9963d30f43a6a73998a9cf4b17b46"
+checksum = "cf20d2fde8ff38632c426f1165ed7436270b44f199fc55284c38276f9db47c3d"
 dependencies = [
  "bitflags",
  "cfg-if",
@@ -1183,12 +1433,11 @@ dependencies = [
 
 [[package]]
 name = "nom"
-version = "7.1.3"
+version = "8.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a"
+checksum = "df9761775871bdef83bee530e60050f7e54b1105350d6884eb0fb4f46c2f9405"
 dependencies = [
  "memchr",
- "minimal-lexical",
 ]
 
 [[package]]
@@ -1200,6 +1449,55 @@ dependencies = [
  "windows-sys 0.61.2",
 ]
 
+[[package]]
+name = "num-bigint"
+version = "0.4.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c89e69e7e0f03bea5ef08013795c25018e101932225a656383bd384495ecc367"
+dependencies = [
+ "num-integer",
+ "num-traits",
+]
+
+[[package]]
+name = "num-bigint"
+version = "0.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "93e7820bc0a80a0238e650327316f929ba18d5be054b647490a3a6a339f3e7c0"
+dependencies = [
+ "num-integer",
+ "num-traits",
+]
+
+[[package]]
+name = "num-complex"
+version = "0.4.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "73f88a1307638156682bada9d7604135552957b7818057dcef22705b4d509495"
+dependencies = [
+ "num-traits",
+]
+
+[[package]]
+name = "num-integer"
+version = "0.1.47"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7ce2d95d4b3734dc35aa2f45e1aa22cd416814592a4f9d9205e11affd5b8e10b"
+dependencies = [
+ "num-traits",
+]
+
+[[package]]
+name = "num-rational"
+version = "0.4.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f83d14da390562dca69fc84082e73e548e1ad308d24accdedd2720017cb37824"
+dependencies = [
+ "num-bigint 0.4.8",
+ "num-integer",
+ "num-traits",
+]
+
 [[package]]
 name = "num-traits"
 version = "0.2.19"
@@ -1256,6 +1554,16 @@ version = "0.2.17"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd"
 
+[[package]]
+name = "pkcs8"
+version = "0.10.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f950b2377845cebe5cf8b5165cb3cc1a5e0fa5cfa3e1f7f55707d8fd82e0a7b7"
+dependencies = [
+ "der",
+ "spki",
+]
+
 [[package]]
 name = "portable-atomic"
 version = "1.13.1"
@@ -1290,6 +1598,15 @@ dependencies = [
  "syn",
 ]
 
+[[package]]
+name = "primal-check"
+version = "0.3.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dc0d895b311e3af9902528fbb8f928688abbd95872819320517cc24ca6b2bd08"
+dependencies = [
+ "num-integer",
+]
+
 [[package]]
 name = "proc-macro2"
 version = "1.0.106"
@@ -1321,9 +1638,9 @@ dependencies = [
 
 [[package]]
 name = "quinn-proto"
-version = "0.11.14"
+version = "0.11.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "434b42fec591c96ef50e21e886936e66d3cc3f737104fdb9b737c40ffb94c098"
+checksum = "4fcb935c5bec503c2f0e306bdd3e58bb9029dcb14fa8d9ac76e3a5256ac0763e"
 dependencies = [
  "bytes",
  "getrandom 0.3.4",
@@ -1377,43 +1694,33 @@ checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf"
 
 [[package]]
 name = "radix_trie"
-version = "0.2.1"
+version = "0.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c069c179fcdc6a2fe24d8d18305cf085fdbd4f922c041943e203685d6a1c58fd"
+checksum = "3b4431027dcd37fc2a73ef740b5f233aa805897935b8bce0195e41bbf9a3289a"
 dependencies = [
  "endian-type",
  "nibble_vec",
 ]
 
-[[package]]
-name = "rand"
-version = "0.8.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5ca0ecfa931c29007047d1bc58e623ab12e5590e8c7cc53200d5202b69266d8a"
-dependencies = [
- "libc",
- "rand_chacha 0.3.1",
- "rand_core 0.6.4",
-]
-
 [[package]]
 name = "rand"
 version = "0.9.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea"
 dependencies = [
- "rand_chacha 0.9.0",
+ "rand_chacha",
  "rand_core 0.9.5",
 ]
 
 [[package]]
-name = "rand_chacha"
-version = "0.3.1"
+name = "rand"
+version = "0.10.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
+checksum = "c7f5fa3a058cd35567ef9bfa5e75732bee0f9e4c55fa90477bef2dfcdbc4be80"
 dependencies = [
- "ppv-lite86",
- "rand_core 0.6.4",
+ "chacha20",
+ "getrandom 0.4.2",
+ "rand_core 0.10.1",
 ]
 
 [[package]]
@@ -1444,6 +1751,18 @@ dependencies = [
  "getrandom 0.3.4",
 ]
 
+[[package]]
+name = "rand_core"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "63b8176103e19a2643978565ca18b50549f6101881c443590420e4dc998a3c69"
+
+[[package]]
+name = "rawpointer"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "60a357793950651c4ed0f3f52338f53b2f809f32d83a07f72909fa13e4c6c1e3"
+
 [[package]]
 name = "redox_syscall"
 version = "0.5.18"
@@ -1499,7 +1818,7 @@ dependencies = [
  "tokio",
  "tokio-rustls",
  "tower",
- "tower-http",
+ "tower-http 0.6.8",
  "tower-service",
  "url",
  "wasm-bindgen",
@@ -1528,6 +1847,29 @@ version = "2.1.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "94300abf3f1ae2e2b8ffb7b58043de3d399c73fa6f4b73826402a5c457614dbe"
 
+[[package]]
+name = "rustc_version"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92"
+dependencies = [
+ "semver",
+]
+
+[[package]]
+name = "rustfft"
+version = "6.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "21db5f9893e91f41798c88680037dba611ca6674703c1a18601b01a72c8adb89"
+dependencies = [
+ "num-complex",
+ "num-integer",
+ "num-traits",
+ "primal-check",
+ "strength_reduce",
+ "transpose",
+]
+
 [[package]]
 name = "rustix"
 version = "1.1.4"
@@ -1584,14 +1926,13 @@ checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d"
 
 [[package]]
 name = "rustyline"
-version = "15.0.0"
+version = "18.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2ee1e066dc922e513bda599c6ccb5f3bb2b0ea5870a579448f2622993f0a9a2f"
+checksum = "53f6a737db68eb1a8ccff86b584b2fc13eca6a7bb6f78ebc7c529547e3ab9684"
 dependencies = [
  "bitflags",
  "cfg-if",
  "clipboard-win",
- "fd-lock",
  "home",
  "libc",
  "log",
@@ -1601,7 +1942,7 @@ dependencies = [
  "unicode-segmentation",
  "unicode-width",
  "utf8parse",
- "windows-sys 0.59.0",
+ "windows-sys 0.61.2",
 ]
 
 [[package]]
@@ -1610,6 +1951,15 @@ version = "1.0.23"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9774ba4a74de5f7b1c1451ed6cd5285a32eddb5cccb8cc655a4e50009e06477f"
 
+[[package]]
+name = "safe_arch"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "42c6efa15875e6ecb39ca61fb0b0c1a40b84fac5a5ffe71eef7d1000c8eb3f5f"
+dependencies = [
+ "bytemuck",
+]
+
 [[package]]
 name = "scopeguard"
 version = "1.2.0"
@@ -1678,11 +2028,11 @@ dependencies = [
 
 [[package]]
 name = "serde_spanned"
-version = "0.6.9"
+version = "1.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bf41e0cfaf7226dca15e8197172c295a782857fcb97fad1808a166870dee75a3"
+checksum = "6662b5879511e06e8999a8a235d848113e942c9124f211511b16466ee2995f26"
 dependencies = [
- "serde",
+ "serde_core",
 ]
 
 [[package]]
@@ -1697,6 +2047,28 @@ dependencies = [
  "serde",
 ]
 
+[[package]]
+name = "sha2"
+version = "0.10.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283"
+dependencies = [
+ "cfg-if",
+ "cpufeatures 0.2.17",
+ "digest 0.10.7",
+]
+
+[[package]]
+name = "sha2"
+version = "0.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "446ba717509524cb3f22f17ecc096f10f4822d76ab5c0b9822c5f9c284e825f4"
+dependencies = [
+ "cfg-if",
+ "cpufeatures 0.3.0",
+ "digest 0.11.3",
+]
+
 [[package]]
 name = "sharded-slab"
 version = "0.1.7"
@@ -1722,6 +2094,27 @@ dependencies = [
  "libc",
 ]
 
+[[package]]
+name = "signature"
+version = "2.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "77549399552de45a898a580c1b41d445bf730df867cc44e6c0233bbc4b8329de"
+dependencies = [
+ "rand_core 0.6.4",
+]
+
+[[package]]
+name = "simba"
+version = "0.10.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f1a7200d82ff1c7b4235efd12f11e2537a402c91cf83a5cb97ce80eef787fde7"
+dependencies = [
+ "approx",
+ "num-complex",
+ "num-traits",
+ "wide",
+]
+
 [[package]]
 name = "slab"
 version = "0.4.12"
@@ -1744,12 +2137,28 @@ dependencies = [
  "windows-sys 0.61.2",
 ]
 
+[[package]]
+name = "spki"
+version = "0.7.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d91ed6c858b01f942cd56b37a94b3e0a1798290327d1236e4d9cf4eaca44d29d"
+dependencies = [
+ "base64ct",
+ "der",
+]
+
 [[package]]
 name = "stable_deref_trait"
 version = "1.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596"
 
+[[package]]
+name = "strength_reduce"
+version = "0.2.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fe895eb47f22e2ddd4dabc02bce419d2e643c8e3b585c78158b349195bc24d82"
+
 [[package]]
 name = "strsim"
 version = "0.11.1"
@@ -1922,44 +2331,42 @@ dependencies = [
 
 [[package]]
 name = "toml"
-version = "0.8.23"
+version = "1.1.5+spec-1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dc1beb996b9d83529a9e75c17a1686767d148d70663143c7854d8b4a09ced362"
+checksum = "12c0ba9680044b4ce98d391a62094047eada0d64860b80166c39f4a6b5640785"
 dependencies = [
- "serde",
+ "indexmap",
+ "serde_core",
  "serde_spanned",
  "toml_datetime",
- "toml_edit",
+ "toml_parser",
+ "toml_writer",
+ "winnow",
 ]
 
 [[package]]
 name = "toml_datetime"
-version = "0.6.11"
+version = "1.1.1+spec-1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "22cddaf88f4fbc13c51aebbf5f8eceb5c7c5a9da2ac40a13519eb5b0a0e8f11c"
+checksum = "3165f65f62e28e0115a00b2ebdd37eb6f3b641855f9d636d3cd4103767159ad7"
 dependencies = [
- "serde",
+ "serde_core",
 ]
 
 [[package]]
-name = "toml_edit"
-version = "0.22.27"
+name = "toml_parser"
+version = "1.1.3+spec-1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41fe8c660ae4257887cf66394862d21dbca4a6ddd26f04a3560410406a2f819a"
+checksum = "1d38ac1cf9b95face32296c0a3ede1fdc270627c9d9c02a7274dd6d960dc4d56"
 dependencies = [
- "indexmap",
- "serde",
- "serde_spanned",
- "toml_datetime",
- "toml_write",
  "winnow",
 ]
 
 [[package]]
-name = "toml_write"
-version = "0.1.2"
+name = "toml_writer"
+version = "1.1.2+spec-1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5d99f8c9a7727884afe522e9bd5edbfc91a3312b36a77b5fb8926e4c31a41801"
+checksum = "7d56353a2a665ad0f41a421187180aab746c8c325620617ad883a99a1cbe66d2"
 
 [[package]]
 name = "tower"
@@ -1993,6 +2400,22 @@ dependencies = [
  "tower",
  "tower-layer",
  "tower-service",
+]
+
+[[package]]
+name = "tower-http"
+version = "0.7.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "08a05a66a4fdd61cbbe0a1d755ffe0ca6aba159dd4820936a0ff8a8278245b9c"
+dependencies = [
+ "bitflags",
+ "bytes",
+ "http",
+ "http-body",
+ "percent-encoding",
+ "pin-project-lite",
+ "tower-layer",
+ "tower-service",
  "tracing",
 ]
 
@@ -2070,6 +2493,16 @@ dependencies = [
  "tracing-log",
 ]
 
+[[package]]
+name = "transpose"
+version = "0.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ad61aed86bc3faea4300c7aee358b4c6d0c8d6ccc36524c96e4c92ccf26e77e"
+dependencies = [
+ "num-integer",
+ "strength_reduce",
+]
+
 [[package]]
 name = "try-lock"
 version = "0.2.5"
@@ -2083,6 +2516,12 @@ dependencies = [
  "anyhow",
 ]
 
+[[package]]
+name = "typenum"
+version = "1.20.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b6f5e870be6c3b371b77fe0ee0bafb859fa4964b4404c27de1d380043c4dda20"
+
 [[package]]
 name = "unicode-ident"
 version = "1.0.24"
@@ -2145,9 +2584,9 @@ checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
 
 [[package]]
 name = "uuid"
-version = "1.23.1"
+version = "1.26.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ddd74a9687298c6858e9b88ec8935ec45d22e8fd5e6394fa1bd4e99a87789c76"
+checksum = "b5772d71c9be8a8a6ac2117d949c5b224c1b72241bb611d9a3012edcf8af7812"
 dependencies = [
  "getrandom 0.4.2",
  "js-sys",
@@ -2161,6 +2600,12 @@ version = "0.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ba73ea9cf16a25df0c8caa16c51acb937d5712a8429db78a3ee29d5dcacd3a65"
 
+[[package]]
+name = "version_check"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
+
 [[package]]
 name = "want"
 version = "0.3.1"
@@ -2312,6 +2757,16 @@ dependencies = [
  "rustls-pki-types",
 ]
 
+[[package]]
+name = "wide"
+version = "1.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8cf05ca94c9fba0c51316899caa1d1e74a064fc310a5efa7375e614343d415be"
+dependencies = [
+ "bytemuck",
+ "safe_arch",
+]
+
 [[package]]
 name = "windows-core"
 version = "0.62.2"
@@ -2380,15 +2835,6 @@ dependencies = [
  "windows-targets 0.52.6",
 ]
 
-[[package]]
-name = "windows-sys"
-version = "0.59.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b"
-dependencies = [
- "windows-targets 0.52.6",
-]
-
 [[package]]
 name = "windows-sys"
 version = "0.60.2"
@@ -2538,12 +2984,9 @@ checksum = "d6bbff5f0aada427a1e5a6da5f1f98158182f26556f345ac9e04d36d0ebed650"
 
 [[package]]
 name = "winnow"
-version = "0.7.15"
+version = "1.0.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "df79d97927682d2fd8adb29682d1140b343be4ac0f08fd68b7765d9c059d3945"
-dependencies = [
- "memchr",
-]
+checksum = "23b97319f7b8343df12cc98938e5c3eb436064524c8d2b4e30a1d3a36eecdf81"
 
 [[package]]
 name = "wit-bindgen"
diff --git a/src/rust/provers/coq.rs b/src/rust/provers/coq.rs
index 940aecbe..685fc5eb 100644
--- a/src/rust/provers/coq.rs
+++ b/src/rust/provers/coq.rs
@@ -945,8 +945,10 @@ impl ProverBackend for CoqBackend {
             return Ok(output.status.success());
         }
         if let Some(source) = state.metadata.get("coq_source").and_then(|v| v.as_str()) {
-            let temp_file =
-                std::env::temp_dir().join(format!("echidna_coq_verify_{}.v", uuid::Uuid::new_v4().simple()));
+            let temp_file = std::env::temp_dir().join(format!(
+                "echidna_coq_verify_{}.v",
+                uuid::Uuid::new_v4().simple()
+            ));
             tokio::fs::write(&temp_file, source)
                 .await
                 .context("Failed to write temp file")?;
diff --git a/src/rust/provers/dafny.rs b/src/rust/provers/dafny.rs
index 395e313b..56075dcc 100644
--- a/src/rust/provers/dafny.rs
+++ b/src/rust/provers/dafny.rs
@@ -20,7 +20,8 @@ impl DafnyBackend {
 
     /// Generate a minimal valid Dafny program with assertions for the goal and axioms.
     fn to_input_format(&self, state: &ProofState) -> Result<String> {
-        let mut s = String::from("// SPDX-License-Identifier: AGPL-3.0-or-later\nmethod EchidnaGoal() {\n");
+        let mut s =
+            String::from("// SPDX-License-Identifier: AGPL-3.0-or-later\nmethod EchidnaGoal() {\n");
 
         // Add axioms as assume statements
         for (i, ax) in state.context.axioms.iter().enumerate() {
diff --git a/src/rust/server.rs b/src/rust/server.rs
index 2c41e1eb..8cff7384 100644
--- a/src/rust/server.rs
+++ b/src/rust/server.rs
@@ -534,11 +534,7 @@ async fn verify_handler(Json(req): Json<VerifyRequest>) -> Result<Json<VerifyRes
         // A completed SMT query is not necessarily a discharged obligation.
         // Only unsat closes a query interpreted as the negated obligation.
         let verified = raw.valid && matches!(smt_status.as_deref(), Some("unsat"));
-        let outcome_str = if verified {
-            "PROVED"
-        } else {
-            "NO_PROOF_FOUND"
-        };
+        let outcome_str = if verified { "PROVED" } else { "NO_PROOF_FOUND" };
         return Ok(Json(VerifyResponse {
             valid: verified,
             outcome: outcome_str.to_string(),

From 2ddd1a3fd90b4efdc541445461a919f975f8d931 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 7 Sep 2026 03:28:13 +0100
Subject: [PATCH 3/5] fix(ci): verify Isabelle downloads and repair governance
 source pointers

---
 .claude/CLAUDE.md                             |  4 +--
 .github/workflows/chapel-ci.yml               |  6 ++--
 .github/workflows/formal-verification.yml     |  4 +--
 .github/workflows/label-triage.yml            |  1 +
 .github/workflows/labels.yml                  |  1 +
 .github/workflows/live-provers.yml            | 10 +++----
 .github/workflows/mvp-smoke.yml               |  4 +--
 .github/workflows/proof-safety.yml            |  2 +-
 .github/workflows/rust-native-reusable.yml    |  5 ++--
 .github/workflows/s4-loop.yml                 |  4 +--
 .github/workflows/server-boot-gate.yml        |  4 +--
 .../workflows/verification-proofs-cron.yml    | 29 ++++---------------
 .github/workflows/workflow-linter.yml         | 16 ++++------
 0-AI-MANIFEST.a2ml                            |  2 +-
 EXPLAINME.adoc                                |  4 +--
 QUICKSTART-USER.adoc                          |  3 +-
 README.adoc                                   |  3 +-
 RSR_COMPLIANCE.adoc                           |  2 +-
 SECURITY.md                                   |  8 +++++
 docs/ARCHITECTURE.adoc                        |  4 +--
 docs/DEBT.adoc                                | 10 ++++---
 docs/ROADMAP.adoc                             |  4 +--
 docs/governance/JUST_AND_MUST_FRAMEWORK.adoc  | 12 ++++----
 docs/handover/llm-warmup-dev.adoc             |  4 ++-
 docs/releases/RELEASE_NOTES_v1.2.adoc         |  4 ++-
 docs/releases/RELEASE_NOTES_v1.3.adoc         | 10 ++++---
 docs/wiki/Architecture.md                     |  4 +--
 src/rust/agent/explanations.rs                |  6 +---
 src/rust/provers/mizar.rs                     |  2 +-
 29 files changed, 75 insertions(+), 97 deletions(-)
 create mode 100644 SECURITY.md

diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index ec44278b..61c39017 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -107,7 +107,7 @@ package definitions (not metadata files) and must NOT be deleted.
 | **Chapel** | Optional parallel proof dispatch | Wired via Cargo `chapel` feature |
 | **Guile Scheme** | Guix package definitions (`guix.scm`, `manifests/*.scm`) | `.scm` metadata files are deprecated — see below |
 | **Bash/POSIX Shell** | Build scripts, CI glue | Keep minimal |
-| **AffineScript** | UI components (TEA architecture, compiled to typed-wasm / wasm, served via Deno) | Replaces AffineScript per `docs/ROADMAP.md`; migration in progress at `src/affinescript/` |
+| **AffineScript** | UI components (TEA architecture, compiled to typed-wasm / wasm, served via Deno) | Replaces AffineScript per `docs/ROADMAP.md`; migration in progress at `src/ui/` |
 | **Bun** | Runtime for compiled AffineScript-TEA UI | Replaces Node/npm/Deno |
 | **JavaScript** | Build tooling only (Tailwind config, test harness) | Not for business logic |
 | **OCaml** | AffineScript compiler host | Decision locked — AffineScript selected for UI |
@@ -127,7 +127,7 @@ package definitions (not metadata files) and must NOT be deleted.
 
 ### Enforcement Rules
 
-1. **No new TypeScript or ReScript files** - Use AffineScript-TEA; migrate existing `src/affinescript/` to AffineScript per `docs/ROADMAP.md`
+1. **No new TypeScript or ReScript files** - Use AffineScript-TEA; migrate existing `src/ui/` to AffineScript per `docs/ROADMAP.md`
 2. **Use `package.json` + `bun.lock` for JS runtime deps** - Bun is npm-compatible; a manifest is REQUIRED
 3. **`bun install --production --frozen-lockfile` for production deps** - resolved from `package.json` and pinned via `bun.lock`; `--frozen-lockfile` makes a lockfile mismatch a build failure rather than a silent re-resolve
 4. **No Go code** - Use Rust instead
diff --git a/.github/workflows/chapel-ci.yml b/.github/workflows/chapel-ci.yml
index 1d8b017b..61cc65e7 100644
--- a/.github/workflows/chapel-ci.yml
+++ b/.github/workflows/chapel-ci.yml
@@ -1,7 +1,5 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
 name: Chapel Accelerator CI
 
 on:
@@ -155,7 +153,7 @@ jobs:
           toolchain: stable
 
       - name: Rust cache
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
 
       - name: Download FFI library
         uses: actions/download-artifact@v8.0.1
@@ -209,7 +207,7 @@ jobs:
           toolchain: stable
 
       - name: Rust cache
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
 
       - name: Download real Chapel library
         uses: actions/download-artifact@v8.0.1
diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml
index 5c2ed2b2..d38c0094 100644
--- a/.github/workflows/formal-verification.yml
+++ b/.github/workflows/formal-verification.yml
@@ -1,7 +1,5 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # formal-verification.yml — Creusot formal verification of the trust-pipeline kernel.
@@ -58,7 +56,7 @@ jobs:
           toolchain: stable
 
       - name: Cache Rust build artefacts
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
         with:
           workspaces: ". -> target"
 
diff --git a/.github/workflows/label-triage.yml b/.github/workflows/label-triage.yml
index fc799478..84379981 100644
--- a/.github/workflows/label-triage.yml
+++ b/.github/workflows/label-triage.yml
@@ -47,6 +47,7 @@ permissions:
 jobs:
   triage:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Classify and label
         env:
diff --git a/.github/workflows/labels.yml b/.github/workflows/labels.yml
index af34c6b2..2926f5e8 100644
--- a/.github/workflows/labels.yml
+++ b/.github/workflows/labels.yml
@@ -33,6 +33,7 @@ permissions:
 jobs:
   sync:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Apply canonical labels
         env:
diff --git a/.github/workflows/live-provers.yml b/.github/workflows/live-provers.yml
index 0441c9ec..07d02fc4 100644
--- a/.github/workflows/live-provers.yml
+++ b/.github/workflows/live-provers.yml
@@ -1,7 +1,5 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
 # ECHIDNA — Live-Prover CI
 #
 # Exercises real prover binaries against canonical micro-goals. Complements
@@ -85,7 +83,7 @@ jobs:
           toolchain: stable
 
       - name: Cache Cargo
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
 
       - name: Provision prover (${{ matrix.backend }})
         run: |
@@ -179,7 +177,7 @@ jobs:
         with:
           toolchain: stable
       - name: Cache Cargo
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
       - name: Provision ${{ matrix.backend }} (best-effort via apt / upstream release)
         continue-on-error: true
         run: |
@@ -329,7 +327,7 @@ jobs:
         with:
           toolchain: stable
       - name: Cache Cargo
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
       - name: Provision ${{ matrix.backend }} (best-effort)
         continue-on-error: true
         run: |
@@ -459,7 +457,7 @@ jobs:
         with:
           toolchain: stable
       - name: Cache Cargo
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
       - name: Provision ${{ matrix.backend }} (best-effort, CUDA/OpenCL required)
         continue-on-error: true
         run: |
diff --git a/.github/workflows/mvp-smoke.yml b/.github/workflows/mvp-smoke.yml
index 2df68dd1..1a813a27 100644
--- a/.github/workflows/mvp-smoke.yml
+++ b/.github/workflows/mvp-smoke.yml
@@ -1,7 +1,5 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
 name: MVP Smoke (Best Effort)
 
 on:
@@ -39,7 +37,7 @@ jobs:
           toolchain: stable
 
       - name: Cache Cargo
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
 
       - name: Install just
         uses: taiki-e/install-action@v2.86.4
diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index 5b91710e..840b4729 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -21,7 +21,7 @@ jobs:
       - uses: actions/checkout@v7.0.1
         with:
           persist-credentials: false
-      - uses: Swatinem/rust-cache@v2.9.2
+      - uses: swatinem/rust-cache@v2.9.2
       - name: Install required native provers
         run: |
           sudo apt-get update
diff --git a/.github/workflows/rust-native-reusable.yml b/.github/workflows/rust-native-reusable.yml
index 498c4183..a4b2eadb 100644
--- a/.github/workflows/rust-native-reusable.yml
+++ b/.github/workflows/rust-native-reusable.yml
@@ -2,7 +2,6 @@
 # This workflow is managed by gh actions-lock.
 # Derived from hyperpolymath/standards@571cc734cd69fb846032ec77a662aa8ee4fc32cd.
 # Native workspace variant installs schema compilers before check/test/coverage.
-# This workflow is managed by gh actions-lock.
 # rust-ci-reusable.yml — Reusable Rust CI bundle (RSR).
 #
 # Replaces the per-repo `rust-ci.yml` template that copy-drifted across
@@ -195,7 +194,7 @@ jobs:
           version: ${{ inputs.zig_version }}
 
       - name: Cache cargo registry and build
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
         with:
           workspaces: ${{ inputs.working_directory }}
 
@@ -248,7 +247,7 @@ jobs:
           version: ${{ inputs.zig_version }}
 
       - name: Cache cargo registry and build
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
         with:
           workspaces: ${{ inputs.working_directory }}
 
diff --git a/.github/workflows/s4-loop.yml b/.github/workflows/s4-loop.yml
index 195e2ca5..395bd793 100644
--- a/.github/workflows/s4-loop.yml
+++ b/.github/workflows/s4-loop.yml
@@ -1,7 +1,5 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
 # S4 loop-closure CI — brings up verisim-api as a service container and
 # runs the echidna s4_loop_closure integration test.  Filed once
 # ghcr.io/hyperpolymath/verisimdb-api:latest became available (PR #121).
@@ -41,7 +39,7 @@ jobs:
         with:
           toolchain: stable
       - name: Cache Cargo
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
       - name: Install just
         uses: taiki-e/install-action@v2.86.4
         with:
diff --git a/.github/workflows/server-boot-gate.yml b/.github/workflows/server-boot-gate.yml
index 9234df5f..ffd08035 100644
--- a/.github/workflows/server-boot-gate.yml
+++ b/.github/workflows/server-boot-gate.yml
@@ -1,7 +1,5 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
 # Server boot gate — builds the echidna binary, boots the server, and
 # verifies that /api/health, /api/provers, and a session {id} route all
 # respond.  Exists so "compiles" can never again mean "boots" — the
@@ -33,7 +31,7 @@ jobs:
         with:
           toolchain: stable
       - name: Cache Cargo
-        uses: Swatinem/rust-cache@v2.9.2
+        uses: swatinem/rust-cache@v2.9.2
       - name: Install system dependencies
         run: sudo apt-get install -y libssl-dev pkg-config
       - name: Build echidna binary
diff --git a/.github/workflows/verification-proofs-cron.yml b/.github/workflows/verification-proofs-cron.yml
index 06513f7c..f224aea9 100644
--- a/.github/workflows/verification-proofs-cron.yml
+++ b/.github/workflows/verification-proofs-cron.yml
@@ -1,7 +1,5 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
 # Weekly verification of the heavier self-proof corpora that are too slow and too
 # network-heavy to gate on every PR: currently Isabelle/HOL (proofs/isabelle). The
 # Isabelle toolchain is a large, non-apt download (~500MB tarball), so this runs on
@@ -46,29 +44,14 @@ jobs:
       - name: Install Isabelle
         run: |
           set -euo pipefail
-          # Resolve the current Isabelle linux x86_64 tarball from the website. A
-          # pinned /dist/IsabelleYYYY URL 404s once a newer release supersedes it
-          # (live-provers.yml's Isabelle2024 pin has rotted), so discover the link
-          # from the homepage, then fall back to the dist/ directory listing.
-          url=""
-          for src in "https://isabelle.in.tum.de/" "https://isabelle.in.tum.de/dist/"; do
-            page="$(curl -fsSL --max-time 120 --retry 3 "$src" || true)"
-            echo "--- candidates from $src ---"
-            printf '%s\n' "$page" | grep -oE '(dist/)?Isabelle[0-9][0-9-]*_linux\.tar\.gz' | sort -V | uniq | tail -5 || true
-            rel="$(printf '%s\n' "$page" | grep -oE '(dist/)?Isabelle[0-9][0-9-]*_linux\.tar\.gz' | sort -V | uniq | tail -1)"
-            if [ -n "$rel" ]; then
-              case "$rel" in dist/*) url="https://isabelle.in.tum.de/$rel" ;; *) url="https://isabelle.in.tum.de/dist/$rel" ;; esac
-              break
-            fi
-          done
-          [ -n "$url" ] || { echo "could not resolve Isabelle linux tarball URL" >&2; exit 1; }
-          echo "Resolved Isabelle URL: $url"
-          curl -fsSL --max-time 900 --retry 3 --retry-delay 15 -o /tmp/isabelle.tar.gz "$url"
+          # Official Cambridge distribution mirror; immutable version and digest.
+          curl -fL --max-time 900 --retry 3 --retry-delay 15 \
+            -o /tmp/isabelle.tar.gz \
+            https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2025-2_linux.tar.gz
+          echo "a20a507bc7c1270d8be96a9f3fbec06345387789d2dc2c4d3df6260d47bfb33c  /tmp/isabelle.tar.gz" | sha256sum --check
           sudo mkdir -p /opt/isabelle
           sudo tar xzf /tmp/isabelle.tar.gz -C /opt/isabelle
-          ISABELLE_BIN="$(find /opt/isabelle -type f -name isabelle | head -n 1)"
-          [ -n "$ISABELLE_BIN" ] || { echo "isabelle launcher not found after extract" >&2; exit 1; }
-          sudo ln -sf "$ISABELLE_BIN" /usr/local/bin/isabelle
+          sudo ln -sf /opt/isabelle/Isabelle2025-2/bin/isabelle /usr/local/bin/isabelle
           isabelle version
 
       - name: Install just
diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml
index 2e3180cb..43bd7580 100644
--- a/.github/workflows/workflow-linter.yml
+++ b/.github/workflows/workflow-linter.yml
@@ -1,7 +1,5 @@
 # SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
 # Prevention workflow - validates all workflows have proper security config
 name: Workflow Security Linter
 
@@ -46,13 +44,9 @@ jobs:
           done
           exit $errors
 
-      - name: Check pinned actions
+      - name: Verify immutable action lockfile with the authoritative tool
+        env:
+          GH_TOKEN: ${{ github.token }}
         run: |
-          errors=0
-          for f in .github/workflows/*.yml .github/workflows/*.yaml; do
-            [ -f "$f" ] || continue
-            # Look for uses: without SHA
-            if grep -E "uses:.*@v[0-9]" "$f" | grep -v "#"; then
-              echo "WARNING: $f has unpinned actions (missing SHA comment)"
-            fi
-          done
+          gh extension install github/gh-actions-lock --pin v0.1.6
+          gh actions-lock --rescan --no-fix
diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
index a42f0bc2..cb824dfe 100644
--- a/0-AI-MANIFEST.a2ml
+++ b/0-AI-MANIFEST.a2ml
@@ -66,7 +66,7 @@ exchange = "src/rust/exchange/"     # Cross-prover proof exchange (OpenTheory, D
 agent = "src/rust/agent/"           # Agentic proof search (actor model)
 interfaces = "src/interfaces/"      # GraphQL + gRPC + REST (workspace members)
 julia-ml = "src/julia/"             # Neural premise selection
-affinescript-ui = "src/affinescript/"       # UI components
+affinescript-ui = "src/ui/"       # UI components
 
 [trust-pipeline]
 # 11-step trust hardening (v1.5+)
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
index 4e30f2ce..7cc46484 100644
--- a/EXPLAINME.adoc
+++ b/EXPLAINME.adoc
@@ -144,7 +144,7 @@ summary line is the only post-build truth.
 | **Zig**           | `ffi/zig/`, `src/zig_ffi/` — C-ABI FFI layer, hex/base64 primitives
 | **Chapel**        | `src/chapel/` — optional parallel proof dispatch with per-prover cwd/filename hooks
 | **AffineScript /     +
-  AffineScript**     | `src/affinescript/`, `src/ui/` — UI components; migration to AffineScript-TEA tracked alongside `affinescript/stdlib` primitives
+  AffineScript**     | `src/ui/`, `src/ui/` — UI components; migration to AffineScript-TEA tracked alongside `affinescript/stdlib` primitives
 |===
 
 == Dogfooded across the estate
@@ -189,7 +189,7 @@ Rust trust-pipeline properties; see `proofs/agda/`.
 | `src/rust/repl.rs`         | Interactive REPL
 | `src/interfaces/`          | API interfaces (GraphQL, gRPC, REST with real prover invocation)
 | `src/julia/`               | ML layer (logistic-regression tactic prediction)
-| `src/affinescript/`, `src/ui/` | UI components — migration to AffineScript-TEA in progress
+| `src/ui/`, `src/ui/` | UI components — migration to AffineScript-TEA in progress
 | `src/abi/`                 | Idris2 formal specifications (ABI contracts + totality proofs)
 | `ffi/zig/`, `src/zig_ffi/` | Zig FFI implementation
 | `proofs/agda/`             | Agda meta-checker (independent verification of trust properties)
diff --git a/QUICKSTART-USER.adoc b/QUICKSTART-USER.adoc
index 2f49766c..9415fc04 100644
--- a/QUICKSTART-USER.adoc
+++ b/QUICKSTART-USER.adoc
@@ -46,8 +46,7 @@ Optional, by component (only needed if you exercise that surface):
 * Julia >= 1.10 — ML layer in `src/julia/`
 * Chapel — optional parallel proof dispatch in `src/chapel/`
   (built behind `--features chapel`)
-* Deno >= 2.0 — AffineScript / AffineScript UI in `src/affinescript/`,
-  `src/ui/`
+* Bun — estate JavaScript runtime; UI sources are in `src/ui/`.
 
 Run `just doctor` to see what is and isn't present; `just heal`
 offers to install missing pieces non-destructively.
diff --git a/README.adoc b/README.adoc
index 0b275c39..574362b2 100644
--- a/README.adoc
+++ b/README.adoc
@@ -217,8 +217,7 @@ Optional, by component:
 * *Zig* >= 0.13.0 — FFI bridge (`+ffi/zig/+`, `+src/zig_ffi/+`)
 * *Chapel* — optional parallel proof dispatch (`+src/chapel/+`,
 `+--features+` `+chapel+`)
-* *Deno* >= 2.0 — AffineScript / AffineScript UI (`+src/affinescript/+`,
-`+src/ui/+`)
+* *Bun* — estate JavaScript runtime; UI sources are in `+src/ui/+`.
 
 Run `+just+` `+doctor+` to verify what’s actually installed; `+just+`
 `+heal+` will offer to install missing pieces non-destructively.
diff --git a/RSR_COMPLIANCE.adoc b/RSR_COMPLIANCE.adoc
index 88a344b1..ff6b8cef 100644
--- a/RSR_COMPLIANCE.adoc
+++ b/RSR_COMPLIANCE.adoc
@@ -53,7 +53,7 @@ ECHIDNA diverges from the strict RSR template in three places:
    migration documented in `.claude/CLAUDE.md`.
 2. *Polyglot source layout*: `src/` contains per-language subdirectories
    (`src/rust/`, `src/julia/`, `src/abi/`, `src/chapel/`, `src/zig_ffi/`,
-   `src/ada/`, `src/affinescript/`, `src/ui/`, `src/interfaces/`) rather than
+   `src/ada/`, `src/ui/`, `src/ui/`, `src/interfaces/`) rather than
    a single language tree. The split is intentional — see CLAUDE.md.
 3. *Extracted Rust crates*: workspace-member crates live in `crates/`
    alongside `src/rust/`. The split between `src/rust/` (binary + main
diff --git a/SECURITY.md b/SECURITY.md
new file mode 100644
index 00000000..64363595
--- /dev/null
+++ b/SECURITY.md
@@ -0,0 +1,8 @@
+<!-- SPDX-License-Identifier: AGPL-3.0-or-later -->
+# Security policy
+
+Report vulnerabilities privately using [GitHub Security Advisories](https://github.com/hyperpolymath/echidna/security/advisories/new).
+If GitHub is unavailable, contact the maintainer at j.d.a.jewell@open.ac.uk.
+Do not disclose vulnerabilities in public issues.
+
+The full policy, supported versions, requested report details, and response timelines are maintained in [SECURITY.adoc](SECURITY.adoc).
diff --git a/docs/ARCHITECTURE.adoc b/docs/ARCHITECTURE.adoc
index 257a50a7..86a8b844 100644
--- a/docs/ARCHITECTURE.adoc
+++ b/docs/ARCHITECTURE.adoc
@@ -24,7 +24,7 @@ independently reproduced where formats allow (Alethe, DRAT/LRAT, TSTP).
 ....
 ┌─────────────────────────────────────────────────────────────────────────┐
 │                              UI Layer                                   │
-│   AffineScript-TEA (migrating from src/affinescript/), served by Deno      │
+│   AffineScript-TEA (migrating from src/ui/), served by Deno      │
 └──────────────────────────────┬──────────────────────────────────────────┘
                                │ HTTP / WebSocket (Cap'n Proto, planned L1)
 ┌──────────────────────────────▼──────────────────────────────────────────┐
@@ -157,7 +157,7 @@ eval)
 
 |`+src/ada/+` |Ada + SPARK |Formal companion library
 
-|`+src/affinescript/+` |AffineScript → AffineScript |UI (migration in
+|`+src/ui/+` |AffineScript → AffineScript |UI (migration in
 progress)
 
 |`+src/ui/+` |static assets |Public UI files
diff --git a/docs/DEBT.adoc b/docs/DEBT.adoc
index e5059476..034cd631 100644
--- a/docs/DEBT.adoc
+++ b/docs/DEBT.adoc
@@ -1,3 +1,5 @@
+NOTE: Historical document. `retired-affinescript` denotes the former UI source tree, which is absent from the current checkout. Commands and file-level examples using it are archival, not current build instructions. Current UI sources are in `src/ui/`; use the root Justfile for supported commands.
+
 == Debt register
 
 Known, measured debt in this repository: licensing, documentation, and
@@ -106,7 +108,7 @@ because each is a distinct class worth re-checking after any future
 licence change:
 
 [arabic]
-. *Stale `+MIT+` grants.* `+src/affinescript/.gitignore+`,
+. *Stale `+MIT+` grants.* `+retired-affinescript/.gitignore+`,
 `+styles/main.css+` and `+tailwind.config.js+` still declared
 `+MIT OR Palimpsest-0.6+` — pre-dating even the MPL migration. Removing
 only the Palimpsest half would have left them *MIT*. Now
@@ -118,9 +120,9 @@ line for a header sweep to match. Eight declared MPL-2.0:
 `+stapeln.toml+`, `+container/manifest.toml+`, three Ada `+alire.toml+`
 manifests under `+spark/+`,
 `+.machine_readable/descriptiles/META.a2ml+`, and
-`+0-AI-MANIFEST.a2ml+`. Plus a *nested `+src/affinescript/.reuse/dep5+`*
+`+0-AI-MANIFEST.a2ml+`. Plus a *nested `+retired-affinescript/.reuse/dep5+`*
 declaring `+MIT OR    Palimpsest-0.6+` for the UI sub-tree.
-. *A user-facing licence string.* `+src/affinescript/src/Main.res+`
+. *A user-facing licence string.* `+retired-affinescript/src/Main.res+`
 rendered `+"MIT OR Palimpsest-0.6 License"+` in the UI — a false licence
 statement shown to users, invisible to every header-based check.
 . *OCI image labels* — 16
@@ -282,7 +284,7 @@ repointed.
 
 ==== C1. AffineScript — removed 2026-08
 
-The 37 AffineScript files (24 in `+src/affinescript/+`, 13 orphaned
+The 37 AffineScript files (24 in `+retired-affinescript/+`, 13 orphaned
 `+.res+` prover clients in `+src/provers/+`) were deleted, along with
 the build and CI wiring that referenced them. AffineScript is a banned
 language under the estate policy.
diff --git a/docs/ROADMAP.adoc b/docs/ROADMAP.adoc
index c19972ed..2eac3d64 100644
--- a/docs/ROADMAP.adoc
+++ b/docs/ROADMAP.adoc
@@ -115,7 +115,7 @@ Stage 7  Sovereign tooling surround         the rest of the ecosystem
     7c  Selur scheduler
     7d  Svalinn trust boundary
     7e  Cerro‑Torre observability
-    7f  AffineScript‑TEA frontend           src/affinescript/, ≥33 modules
+    7f  AffineScript‑TEA frontend           src/ui/, ≥33 modules
     7g  LOL i18n                            locale/ + t!() macro
     7h  Zig ABI 16‑endpoint surface         src/zig/echidna_abi.zig
 
@@ -167,7 +167,7 @@ named as a versioned dependency in Cargo.toml or the container
 definition, wired into its role
 
 |"`AffineScript‑TEA frontend`" |Not present (10 `+.res+` files stub)
-|*`+src/affinescript/+`* holds ≥33 AffineScript‑TEA modules, persistent
+|*`+src/ui/+`* holds ≥33 AffineScript‑TEA modules, persistent
 Model → Msg → Update loop, talks to core over Cap’n Proto WebSocket
 
 |"`LOL i18n`" |Not present |*`+locale/+`* with LOL‑sourced translations;
diff --git a/docs/governance/JUST_AND_MUST_FRAMEWORK.adoc b/docs/governance/JUST_AND_MUST_FRAMEWORK.adoc
index b7d9c663..ff8872a1 100644
--- a/docs/governance/JUST_AND_MUST_FRAMEWORK.adoc
+++ b/docs/governance/JUST_AND_MUST_FRAMEWORK.adoc
@@ -1,3 +1,5 @@
+NOTE: Historical document. `retired-affinescript` denotes the former UI source tree, which is absent from the current checkout. Commands and file-level examples using it are archival, not current build instructions. Current UI sources are in `src/ui/`; use the root Justfile for supported commands.
+
 == ECHIDNA: Just and Must Framework
 
 *Status*: Design Standard *Date*: 2026-01-29 *Purpose*: Standardize
@@ -67,7 +69,7 @@ build-wasm:
 # Build UI components
 build-ui:
     @echo "Compiling AffineScript UI..."
-    cd src/affinescript && npm run build
+    cd retired-affinescript && npm run build
 
 # Build Julia ML components
 build-ml:
@@ -201,7 +203,7 @@ dev-julia:
 
 # Start UI development server
 dev-ui:
-    cd src/affinescript && npm run dev
+    cd retired-affinescript && npm run dev
 
 # Watch for changes and rebuild
 watch:
@@ -218,13 +220,13 @@ install-deps:
     @echo "Installing Julia dependencies..."
     cd src/julia && julia --project -e 'using Pkg; Pkg.instantiate()'
     @echo "Installing AffineScript dependencies..."
-    cd src/affinescript && npm install
+    cd retired-affinescript && npm install
 
 # Update dependencies
 update-deps:
     cargo update
     cd src/julia && julia --project -e 'using Pkg; Pkg.update()'
-    cd src/affinescript && npm update
+    cd retired-affinescript && npm update
 
 # Check for outdated dependencies
 check-deps:
@@ -323,7 +325,7 @@ release-tag VERSION:
 clean:
     cargo clean
     rm -rf target/
-    rm -rf src/affinescript/lib/
+    rm -rf retired-affinescript/lib/
     find . -name "*.bs.js" -delete
 
 # Deep clean (including dependencies)
diff --git a/docs/handover/llm-warmup-dev.adoc b/docs/handover/llm-warmup-dev.adoc
index d934237f..e67d7f57 100644
--- a/docs/handover/llm-warmup-dev.adoc
+++ b/docs/handover/llm-warmup-dev.adoc
@@ -1,3 +1,5 @@
+NOTE: Historical document. `retired-affinescript` denotes the former UI source tree, which is absent from the current checkout. Commands and file-level examples using it are archival, not current build instructions. Current UI sources are in `src/ui/`; use the root Justfile for supported commands.
+
 == ECHIDNA — Developer Context
 
 === Architecture
@@ -110,7 +112,7 @@ Flux.jl Transformer models.
 
 4 shared libraries. Bridges Idris2 ABI to C ABI.
 
-==== AffineScript UI (src/affinescript/)
+==== AffineScript UI (retired-affinescript/)
 
 33 .res files. Deno runtime. Zero TypeScript.
 
diff --git a/docs/releases/RELEASE_NOTES_v1.2.adoc b/docs/releases/RELEASE_NOTES_v1.2.adoc
index e855a7f5..2058d121 100644
--- a/docs/releases/RELEASE_NOTES_v1.2.adoc
+++ b/docs/releases/RELEASE_NOTES_v1.2.adoc
@@ -1,3 +1,5 @@
+NOTE: Historical document. `retired-affinescript` denotes the former UI source tree, which is absent from the current checkout. Commands and file-level examples using it are archival, not current build instructions. Current UI sources are in `src/ui/`; use the root Justfile for supported commands.
+
 == ECHIDNA v1.2 Release Notes
 
 *Release Date:* 2026-01-29 *Tag:* v1.2.0 *Status:* Production Ready
@@ -194,7 +196,7 @@ No breaking changes. Simply rebuild:
 [source,bash]
 ----
 cargo build --release
-cd src/affinescript && npm run build
+cd retired-affinescript && npm run build
 ----
 
 ==== New Dependencies
diff --git a/docs/releases/RELEASE_NOTES_v1.3.adoc b/docs/releases/RELEASE_NOTES_v1.3.adoc
index 2cdcffd5..af242fd0 100644
--- a/docs/releases/RELEASE_NOTES_v1.3.adoc
+++ b/docs/releases/RELEASE_NOTES_v1.3.adoc
@@ -1,3 +1,5 @@
+NOTE: Historical document. `retired-affinescript` denotes the former UI source tree, which is absent from the current checkout. Commands and file-level examples using it are archival, not current build instructions. Current UI sources are in `src/ui/`; use the root Justfile for supported commands.
+
 == ECHIDNA v1.3 Release Notes
 
 *Release Date:* 2026-01-29 *Tag:* v1.3.0 *Status:* Production Ready -
@@ -140,7 +142,7 @@ API usage - Troubleshooting guide - Development workflow
 ----
 julia src/julia/api_server.jl &
 ./target/release/echidna server --port 8081 --enable-cors &
-cd src/affinescript && python3 -m http.server 3000 &
+cd retired-affinescript && python3 -m http.server 3000 &
 ----
 
 *Access:* http://127.0.0.1:3000
@@ -258,7 +260,7 @@ only)
 ==== Production Checklist
 
 * [ ] Build Rust in release mode: `+cargo build --release+`
-* [ ] Compile AffineScript UI: `+cd src/affinescript && npm run build+`
+* [ ] Compile AffineScript UI: `+cd retired-affinescript && npm run build+`
 * [ ] Train models if needed: `+julia src/julia/train_models.jl+`
 * [ ] Start Julia ML API: `+julia src/julia/api_server.jl+`
 * [ ] Start Rust backend:
@@ -299,7 +301,7 @@ services:
 . Install Julia packages:
 `+julia -e 'using Pkg; Pkg.add(["HTTP", "JSON3"])'+`
 . Rebuild Rust: `+cargo build --release+`
-. Rebuild AffineScript: `+cd src/affinescript && npm run build+`
+. Rebuild AffineScript: `+cd retired-affinescript && npm run build+`
 . Start services (see Quick Start)
 . Run tests: `+./tests/integration_test.sh+`
 
@@ -313,7 +315,7 @@ repo root)
 `+http://127.0.0.1:9000+` (hardcoded in server.rs:48)
 
 *AffineScript UI:* - API base: `+http://localhost:8081/api+`
-(src/affinescript/src/api/Client.res:12)
+(retired-affinescript/src/api/Client.res:12)
 
 === Contributors
 
diff --git a/docs/wiki/Architecture.md b/docs/wiki/Architecture.md
index 612c5175..c97b8545 100644
--- a/docs/wiki/Architecture.md
+++ b/docs/wiki/Architecture.md
@@ -26,7 +26,7 @@ on-the-wire data dictionary is the formal E-R schema in
 [`crates/echidna-wire/schemas/verisim_er.capnp`](https://github.com/hyperpolymath/echidna/blob/main/crates/echidna-wire/schemas/verisim_er.capnp)).
 **Idris2** (`src/abi/`) carries the FFI ABI proofs (zero `believe_me`).
 **Agda** (`meta-checker/`) carries trust-pipeline meta-proofs. **AffineScript**
-(in migration from AffineScript at `src/affinescript/`) carries the UI, served by
+(in migration from AffineScript at `src/ui/`) carries the UI, served by
 Deno.
 
 ## Corpus Ingest
@@ -212,6 +212,6 @@ See [`src/rust/provers/mod.rs`](https://github.com/hyperpolymath/echidna/blob/ma
 | `meta-checker/` | Agda | Trust-pipeline meta-proofs |
 | `src/chapel/` + `src/zig_ffi/` | Chapel + Zig | Parallel proof search (L2.1 live) |
 | `src/ada/` + `spark/` | Ada/SPARK | Formal companion library |
-| `src/affinescript/` → AffineScript | AffineScript→AffineScript | UI (migration in progress) |
+| `src/ui/` → AffineScript | AffineScript→AffineScript | UI (migration in progress) |
 
 Pointers and history evolve; the in-repo [`docs/ARCHITECTURE.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/ARCHITECTURE.md) is authoritative.
diff --git a/src/rust/agent/explanations.rs b/src/rust/agent/explanations.rs
index ca5d1ce8..efd20e79 100644
--- a/src/rust/agent/explanations.rs
+++ b/src/rust/agent/explanations.rs
@@ -329,11 +329,7 @@ impl ExplanationGenerator {
                     self.format_term(body)
                 )
             },
-            Term::Match {
-                scrutinee,
-                branches: _,
-                ..
-            } => {
+            Term::Match { scrutinee, .. } => {
                 format!("match {} with ...", self.format_term(scrutinee))
             },
             Term::Fix { name, body, .. } => {
diff --git a/src/rust/provers/mizar.rs b/src/rust/provers/mizar.rs
index 213b0dd9..9b00281f 100644
--- a/src/rust/provers/mizar.rs
+++ b/src/rust/provers/mizar.rs
@@ -611,7 +611,7 @@ impl ProverBackend for MizarBackend {
             Term::Pi { .. } => {
                 suggestions.push(Tactic::Intro(None));
             },
-            Term::App { func: _, .. } => {
+            Term::App { .. } => {
                 for theorem in &state.context.theorems {
                     suggestions.push(Tactic::Apply(theorem.name.clone()));
                     if suggestions.len() >= limit {

From 858e796c804864b29487131716bcb7408fe94c44 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 7 Sep 2026 03:35:55 +0100
Subject: [PATCH 4/5] fix(ci): retain allowlisted action owner spelling

---
 .github/workflows/chapel-ci.yml            | 4 ++--
 .github/workflows/formal-verification.yml  | 2 +-
 .github/workflows/live-provers.yml         | 8 ++++----
 .github/workflows/mvp-smoke.yml            | 2 +-
 .github/workflows/proof-safety.yml         | 2 +-
 .github/workflows/rust-native-reusable.yml | 4 ++--
 .github/workflows/s4-loop.yml              | 2 +-
 .github/workflows/server-boot-gate.yml     | 2 +-
 8 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/.github/workflows/chapel-ci.yml b/.github/workflows/chapel-ci.yml
index 61cc65e7..d2dfaec6 100644
--- a/.github/workflows/chapel-ci.yml
+++ b/.github/workflows/chapel-ci.yml
@@ -153,7 +153,7 @@ jobs:
           toolchain: stable
 
       - name: Rust cache
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
 
       - name: Download FFI library
         uses: actions/download-artifact@v8.0.1
@@ -207,7 +207,7 @@ jobs:
           toolchain: stable
 
       - name: Rust cache
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
 
       - name: Download real Chapel library
         uses: actions/download-artifact@v8.0.1
diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml
index d38c0094..d1e4cc60 100644
--- a/.github/workflows/formal-verification.yml
+++ b/.github/workflows/formal-verification.yml
@@ -56,7 +56,7 @@ jobs:
           toolchain: stable
 
       - name: Cache Rust build artefacts
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
         with:
           workspaces: ". -> target"
 
diff --git a/.github/workflows/live-provers.yml b/.github/workflows/live-provers.yml
index 07d02fc4..dfb2e8f6 100644
--- a/.github/workflows/live-provers.yml
+++ b/.github/workflows/live-provers.yml
@@ -83,7 +83,7 @@ jobs:
           toolchain: stable
 
       - name: Cache Cargo
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
 
       - name: Provision prover (${{ matrix.backend }})
         run: |
@@ -177,7 +177,7 @@ jobs:
         with:
           toolchain: stable
       - name: Cache Cargo
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
       - name: Provision ${{ matrix.backend }} (best-effort via apt / upstream release)
         continue-on-error: true
         run: |
@@ -327,7 +327,7 @@ jobs:
         with:
           toolchain: stable
       - name: Cache Cargo
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
       - name: Provision ${{ matrix.backend }} (best-effort)
         continue-on-error: true
         run: |
@@ -457,7 +457,7 @@ jobs:
         with:
           toolchain: stable
       - name: Cache Cargo
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
       - name: Provision ${{ matrix.backend }} (best-effort, CUDA/OpenCL required)
         continue-on-error: true
         run: |
diff --git a/.github/workflows/mvp-smoke.yml b/.github/workflows/mvp-smoke.yml
index 1a813a27..c8b45511 100644
--- a/.github/workflows/mvp-smoke.yml
+++ b/.github/workflows/mvp-smoke.yml
@@ -37,7 +37,7 @@ jobs:
           toolchain: stable
 
       - name: Cache Cargo
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
 
       - name: Install just
         uses: taiki-e/install-action@v2.86.4
diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index 840b4729..5b91710e 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -21,7 +21,7 @@ jobs:
       - uses: actions/checkout@v7.0.1
         with:
           persist-credentials: false
-      - uses: swatinem/rust-cache@v2.9.2
+      - uses: Swatinem/rust-cache@v2.9.2
       - name: Install required native provers
         run: |
           sudo apt-get update
diff --git a/.github/workflows/rust-native-reusable.yml b/.github/workflows/rust-native-reusable.yml
index a4b2eadb..d0c26b5a 100644
--- a/.github/workflows/rust-native-reusable.yml
+++ b/.github/workflows/rust-native-reusable.yml
@@ -194,7 +194,7 @@ jobs:
           version: ${{ inputs.zig_version }}
 
       - name: Cache cargo registry and build
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
         with:
           workspaces: ${{ inputs.working_directory }}
 
@@ -247,7 +247,7 @@ jobs:
           version: ${{ inputs.zig_version }}
 
       - name: Cache cargo registry and build
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
         with:
           workspaces: ${{ inputs.working_directory }}
 
diff --git a/.github/workflows/s4-loop.yml b/.github/workflows/s4-loop.yml
index 395bd793..e975e77f 100644
--- a/.github/workflows/s4-loop.yml
+++ b/.github/workflows/s4-loop.yml
@@ -39,7 +39,7 @@ jobs:
         with:
           toolchain: stable
       - name: Cache Cargo
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
       - name: Install just
         uses: taiki-e/install-action@v2.86.4
         with:
diff --git a/.github/workflows/server-boot-gate.yml b/.github/workflows/server-boot-gate.yml
index ffd08035..89365a95 100644
--- a/.github/workflows/server-boot-gate.yml
+++ b/.github/workflows/server-boot-gate.yml
@@ -31,7 +31,7 @@ jobs:
         with:
           toolchain: stable
       - name: Cache Cargo
-        uses: swatinem/rust-cache@v2.9.2
+        uses: Swatinem/rust-cache@v2.9.2
       - name: Install system dependencies
         run: sudo apt-get install -y libssl-dev pkg-config
       - name: Build echidna binary

From f60248fa01c50fce07ed04a0d77c8d2bdc7c5edd Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 7 Sep 2026 04:17:58 +0100
Subject: [PATCH 5/5] Reject forged SMT status output and address verification
 review findings

---
 .claude/CLAUDE.md                          |   6 +-
 .github/workflows/proof-safety.yml         |   2 -
 .github/workflows/rust-native-reusable.yml |   5 +-
 .github/workflows/workflow-linter.yml      |   6 +-
 Cargo.lock                                 |   1 +
 Cargo.toml                                 |   1 +
 EXPLAINME.adoc                             |   5 +-
 README.adoc                                |   4 +-
 RSR_COMPLIANCE.adoc                        |   2 +-
 SECURITY.md                                |   2 +-
 docs/ARCHITECTURE.adoc                     |   7 +-
 docs/wiki/Architecture.md                  |   9 +-
 fuzz/Cargo.lock                            |  22 +++
 src/rust/provers/mod.rs                    |   2 +-
 src/rust/server.rs                         | 148 ++++++++++++++++++---
 tests/e2e_prover_test.rs                   |   4 +-
 tests/live_service_regressions.rs          |  42 +++---
 17 files changed, 206 insertions(+), 62 deletions(-)

diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 61c39017..0a2820f4 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -107,8 +107,8 @@ package definitions (not metadata files) and must NOT be deleted.
 | **Chapel** | Optional parallel proof dispatch | Wired via Cargo `chapel` feature |
 | **Guile Scheme** | Guix package definitions (`guix.scm`, `manifests/*.scm`) | `.scm` metadata files are deprecated — see below |
 | **Bash/POSIX Shell** | Build scripts, CI glue | Keep minimal |
-| **AffineScript** | UI components (TEA architecture, compiled to typed-wasm / wasm, served via Deno) | Replaces AffineScript per `docs/ROADMAP.md`; migration in progress at `src/ui/` |
-| **Bun** | Runtime for compiled AffineScript-TEA UI | Replaces Node/npm/Deno |
+| **AffineScript** | TEA sources in `src/ui/tea/`; static shell in `src/ui/public/` | The compile pipeline is unavailable; `build-ui` fails explicitly |
+| **Bun** | Estate JavaScript runtime | The legacy serve recipes still require migration; open `src/ui/public/prove.html` directly for the working static UI |
 | **JavaScript** | Build tooling only (Tailwind config, test harness) | Not for business logic |
 | **OCaml** | AffineScript compiler host | Decision locked — AffineScript selected for UI |
 | **Nickel** | Configuration language | Used across `configs/`, `echidna-playground/contractiles/k9/`, `.machine_readable/`, `echidnabot/config/` (11+ `.ncl` files) |
@@ -127,7 +127,7 @@ package definitions (not metadata files) and must NOT be deleted.
 
 ### Enforcement Rules
 
-1. **No new TypeScript or ReScript files** - Use AffineScript-TEA; migrate existing `src/ui/` to AffineScript per `docs/ROADMAP.md`
+1. **No new TypeScript or ReScript files** - Use AffineScript-TEA sources in `src/ui/tea/`; the compiled UI pipeline is not yet wired
 2. **Use `package.json` + `bun.lock` for JS runtime deps** - Bun is npm-compatible; a manifest is REQUIRED
 3. **`bun install --production --frozen-lockfile` for production deps** - resolved from `package.json` and pinned via `bun.lock`; `--frozen-lockfile` makes a lockfile mismatch a build failure rather than a silent re-resolve
 4. **No Go code** - Use Rust instead
diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index 5b91710e..80b8287d 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -15,8 +15,6 @@ jobs:
     name: Proof safety regressions
     runs-on: ubuntu-24.04
     timeout-minutes: 25
-    env:
-      VERISIMDB_URL: http://127.0.0.1:17799
     steps:
       - uses: actions/checkout@v7.0.1
         with:
diff --git a/.github/workflows/rust-native-reusable.yml b/.github/workflows/rust-native-reusable.yml
index d0c26b5a..d0cd78ac 100644
--- a/.github/workflows/rust-native-reusable.yml
+++ b/.github/workflows/rust-native-reusable.yml
@@ -345,7 +345,7 @@ jobs:
         # Self-contained: no external coverage service. Own the gate on our runner.
         run: |
           set -euo pipefail
-          cargo llvm-cov --workspace --locked --json --output-path cov.json
+          cargo llvm-cov --locked --json --output-path cov.json
           PCT=$(jq -r '.data[0].totals.lines.percent' cov.json)
           printf '### Line coverage: %.2f%% (floor %s%%)\n' "$PCT" "$FLOOR" >> "$GITHUB_STEP_SUMMARY"
           echo "pct=$PCT" >> "$GITHUB_OUTPUT"
@@ -354,6 +354,9 @@ jobs:
         run: |
           set -euo pipefail
           awk -v p="${{ steps.cov.outputs.pct }}" -v f="$FLOOR" 'BEGIN {
+            if (f !~ /^[0-9]+([.][0-9]+)?$/ || f + 0 > 100 || p !~ /^[0-9]+([.][0-9]+)?$/ || p + 0 > 100) {
+              print "FAIL: coverage and floor must be numeric percentages in [0, 100]"; exit 1
+            }
             if (p + 0 < f + 0) { printf "FAIL: line coverage %.2f%% is below floor %s%%\n", p, f; exit 1 }
             printf "OK: line coverage %.2f%% >= floor %s%%\n", p, f
           }'
diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml
index 43bd7580..546889ff 100644
--- a/.github/workflows/workflow-linter.yml
+++ b/.github/workflows/workflow-linter.yml
@@ -48,5 +48,7 @@ jobs:
         env:
           GH_TOKEN: ${{ github.token }}
         run: |
-          gh extension install github/gh-actions-lock --pin v0.1.6
-          gh actions-lock --rescan --no-fix
+          curl -fsSL --retry 3 -o "$RUNNER_TEMP/gh-actions-lock" https://github.com/github/gh-actions-lock/releases/download/v0.1.6/linux-amd64
+          echo "4181ec1da5408b34b9a542a7ee5c6ce3a4d6ac815c7d0206a00ceca8a817f4e3  $RUNNER_TEMP/gh-actions-lock" | sha256sum --check
+          chmod u+x "$RUNNER_TEMP/gh-actions-lock"
+          "$RUNNER_TEMP/gh-actions-lock" --rescan --no-fix
diff --git a/Cargo.lock b/Cargo.lock
index dcb0ed11..f23b92d4 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1109,6 +1109,7 @@ dependencies = [
  "serde",
  "serde_json",
  "sha2 0.11.0",
+ "strum",
  "tempfile",
  "thiserror",
  "tiny-keccak",
diff --git a/Cargo.toml b/Cargo.toml
index 3bfe87ef..cc7e3b40 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -65,6 +65,7 @@ uuid = { version = "1.25.0", features = ["v4", "serde"] }
 
 # Lazy statics
 lazy_static = "1"
+strum = { version = "0.27.2", features = ["derive"] }
 
 # VeriSimDB integration (optional — behind "verisim" feature)
 ciborium = { version = "0.2", optional = true }
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
index 7cc46484..af5acad5 100644
--- a/EXPLAINME.adoc
+++ b/EXPLAINME.adoc
@@ -143,8 +143,7 @@ summary line is the only post-build truth.
 | **Idris2**        | `src/abi/` — type-level ABI specifications + totality proofs (zero `believe_me`)
 | **Zig**           | `ffi/zig/`, `src/zig_ffi/` — C-ABI FFI layer, hex/base64 primitives
 | **Chapel**        | `src/chapel/` — optional parallel proof dispatch with per-prover cwd/filename hooks
-| **AffineScript /     +
-  AffineScript**     | `src/ui/`, `src/ui/` — UI components; migration to AffineScript-TEA tracked alongside `affinescript/stdlib` primitives
+| **AffineScript-TEA / HTML** | `src/ui/tea/` — TEA sources (compile pipeline unavailable); `src/ui/public/` — working static shell
 |===
 
 == Dogfooded across the estate
@@ -189,7 +188,7 @@ Rust trust-pipeline properties; see `proofs/agda/`.
 | `src/rust/repl.rs`         | Interactive REPL
 | `src/interfaces/`          | API interfaces (GraphQL, gRPC, REST with real prover invocation)
 | `src/julia/`               | ML layer (logistic-regression tactic prediction)
-| `src/ui/`, `src/ui/` | UI components — migration to AffineScript-TEA in progress
+| `src/ui/tea/`, `src/ui/public/` | TEA sources (compile pipeline unavailable) and working static shell
 | `src/abi/`                 | Idris2 formal specifications (ABI contracts + totality proofs)
 | `ffi/zig/`, `src/zig_ffi/` | Zig FFI implementation
 | `proofs/agda/`             | Agda meta-checker (independent verification of trust properties)
diff --git a/README.adoc b/README.adoc
index 574362b2..5e29fc6f 100644
--- a/README.adoc
+++ b/README.adoc
@@ -285,7 +285,7 @@ podman run -it echidna:latest
 * *Rust*: Core logic, prover backends, trust pipeline, CLI, REPL, API
 servers
 * *Julia*: ML inference (tactic prediction, premise selection)
-* *AffineScript + Deno*: UI components
+* *AffineScript-TEA*: UI sources in `src/ui/tea/` (compile pipeline unavailable); working static shell in `src/ui/public/`
 * *Chapel*: Optional parallel proof dispatch
 
 === Key Modules
@@ -544,7 +544,7 @@ total-order proofs, in-range round-trip lemmas), `+Provers+`,
 (`+tryProver+`) and L2.3 cancel-token preemption.
 * *Wave-3 container infrastructure*: 8-cell weekly cron building each
 Tier-3 prover image with stub-sentinel detection.
-* *Estate migrations in flight*: AffineScript→AffineScript UI; npm→Deno
+* *Estate migrations in flight*: AffineScript-TEA UI compilation; legacy JavaScript runtime→Bun
 for `+echidna-playground+`; CI workflow consolidation under the
 governance ruleset.
 
diff --git a/RSR_COMPLIANCE.adoc b/RSR_COMPLIANCE.adoc
index ff6b8cef..1abc945c 100644
--- a/RSR_COMPLIANCE.adoc
+++ b/RSR_COMPLIANCE.adoc
@@ -53,7 +53,7 @@ ECHIDNA diverges from the strict RSR template in three places:
    migration documented in `.claude/CLAUDE.md`.
 2. *Polyglot source layout*: `src/` contains per-language subdirectories
    (`src/rust/`, `src/julia/`, `src/abi/`, `src/chapel/`, `src/zig_ffi/`,
-   `src/ada/`, `src/ui/`, `src/ui/`, `src/interfaces/`) rather than
+   `src/ada/`, `src/ui/`, `src/interfaces/`) rather than
    a single language tree. The split is intentional — see CLAUDE.md.
 3. *Extracted Rust crates*: workspace-member crates live in `crates/`
    alongside `src/rust/`. The split between `src/rust/` (binary + main
diff --git a/SECURITY.md b/SECURITY.md
index 64363595..4bc2c5fa 100644
--- a/SECURITY.md
+++ b/SECURITY.md
@@ -1,4 +1,4 @@
-<!-- SPDX-License-Identifier: AGPL-3.0-or-later -->
+<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
 # Security policy
 
 Report vulnerabilities privately using [GitHub Security Advisories](https://github.com/hyperpolymath/echidna/security/advisories/new).
diff --git a/docs/ARCHITECTURE.adoc b/docs/ARCHITECTURE.adoc
index 86a8b844..82f9fb43 100644
--- a/docs/ARCHITECTURE.adoc
+++ b/docs/ARCHITECTURE.adoc
@@ -24,7 +24,7 @@ independently reproduced where formats allow (Alethe, DRAT/LRAT, TSTP).
 ....
 ┌─────────────────────────────────────────────────────────────────────────┐
 │                              UI Layer                                   │
-│   AffineScript-TEA (migrating from src/ui/), served by Deno      │
+│   TEA sources: src/ui/tea/; static shell: src/ui/public/      │
 └──────────────────────────────┬──────────────────────────────────────────┘
                                │ HTTP / WebSocket (Cap'n Proto, planned L1)
 ┌──────────────────────────────▼──────────────────────────────────────────┐
@@ -157,10 +157,9 @@ eval)
 
 |`+src/ada/+` |Ada + SPARK |Formal companion library
 
-|`+src/ui/+` |AffineScript → AffineScript |UI (migration in
-progress)
+|`+src/ui/tea/+` |AffineScript-TEA |UI sources (compile pipeline unavailable)
 
-|`+src/ui/+` |static assets |Public UI files
+|`+src/ui/public/+` |HTML/static assets |Browser shell; open prove.html directly
 
 |`+src/interfaces/+` |Rust |GraphQL, gRPC, REST workspace crates
 |===
diff --git a/docs/wiki/Architecture.md b/docs/wiki/Architecture.md
index c97b8545..49771e43 100644
--- a/docs/wiki/Architecture.md
+++ b/docs/wiki/Architecture.md
@@ -25,9 +25,9 @@ on-the-wire data dictionary is the formal E-R schema in
 (companion Cap'n Proto schema:
 [`crates/echidna-wire/schemas/verisim_er.capnp`](https://github.com/hyperpolymath/echidna/blob/main/crates/echidna-wire/schemas/verisim_er.capnp)).
 **Idris2** (`src/abi/`) carries the FFI ABI proofs (zero `believe_me`).
-**Agda** (`meta-checker/`) carries trust-pipeline meta-proofs. **AffineScript**
-(in migration from AffineScript at `src/ui/`) carries the UI, served by
-Deno.
+**Agda** (`meta-checker/`) carries trust-pipeline meta-proofs. **AffineScript-TEA** sources live in `src/ui/tea/`; their compile pipeline
+is not yet wired. The working static shell is `src/ui/public/prove.html`,
+which can be opened directly in a browser.
 
 ## Corpus Ingest
 
@@ -212,6 +212,7 @@ See [`src/rust/provers/mod.rs`](https://github.com/hyperpolymath/echidna/blob/ma
 | `meta-checker/` | Agda | Trust-pipeline meta-proofs |
 | `src/chapel/` + `src/zig_ffi/` | Chapel + Zig | Parallel proof search (L2.1 live) |
 | `src/ada/` + `spark/` | Ada/SPARK | Formal companion library |
-| `src/ui/` → AffineScript | AffineScript→AffineScript | UI (migration in progress) |
+| `src/ui/tea/` | AffineScript-TEA | UI sources; compile pipeline unavailable |
+| `src/ui/public/` | HTML/static assets | Working browser shell |
 
 Pointers and history evolve; the in-repo [`docs/ARCHITECTURE.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/ARCHITECTURE.md) is authoritative.
diff --git a/fuzz/Cargo.lock b/fuzz/Cargo.lock
index 0cf3a9c3..e395d39a 100644
--- a/fuzz/Cargo.lock
+++ b/fuzz/Cargo.lock
@@ -633,6 +633,7 @@ dependencies = [
  "serde",
  "serde_json",
  "sha2 0.11.0",
+ "strum",
  "tempfile",
  "thiserror",
  "tiny-keccak",
@@ -2165,6 +2166,27 @@ version = "0.11.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
 
+[[package]]
+name = "strum"
+version = "0.27.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "af23d6f6c1a224baef9d3f61e287d2761385a5b88fdab4eb4c6f11aeb54c4bcf"
+dependencies = [
+ "strum_macros",
+]
+
+[[package]]
+name = "strum_macros"
+version = "0.27.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7695ce3845ea4b33927c055a39dc438a45b059f7c1b3d91d38d10355fb8cbca7"
+dependencies = [
+ "heck",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
 [[package]]
 name = "subtle"
 version = "2.6.1"
diff --git a/src/rust/provers/mod.rs b/src/rust/provers/mod.rs
index 13592bd5..d62dfcf7 100644
--- a/src/rust/provers/mod.rs
+++ b/src/rust/provers/mod.rs
@@ -124,7 +124,7 @@ pub mod z3;
 pub mod zipperposition;
 
 /// Enumeration of all supported provers
-#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, strum::EnumIter)]
 pub enum ProverKind {
     // Tier 1: Original + SMT solvers
     Agda,
diff --git a/src/rust/server.rs b/src/rust/server.rs
index 8cff7384..0dee6520 100644
--- a/src/rust/server.rs
+++ b/src/rust/server.rs
@@ -523,17 +523,12 @@ async fn verify_handler(Json(req): Json<VerifyRequest>) -> Result<Json<VerifyRes
     // run passthrough evaluation instead of proof-obligation negation semantics.
     if should_passthrough_smt_eval(&req) {
         let Json(raw) = verify_raw_handler(Json(req.clone())).await?;
-        let smt_status =
-            extract_smt_status(&raw.stdout).or_else(|| extract_smt_status(&raw.stderr));
-        let goals_remaining = if matches!(smt_status.as_deref(), Some("unsat")) {
-            0
-        } else {
-            1
-        };
+        let smt_status = extract_smt_status(&raw.stdout);
 
         // A completed SMT query is not necessarily a discharged obligation.
         // Only unsat closes a query interpreted as the negated obligation.
-        let verified = raw.valid && matches!(smt_status.as_deref(), Some("unsat"));
+        let verified = raw.valid && discharged_smt_queries(&req.content, &raw.stdout);
+        let goals_remaining = if verified { 0 } else { 1 };
         let outcome_str = if verified { "PROVED" } else { "NO_PROOF_FOUND" };
         return Ok(Json(VerifyResponse {
             valid: verified,
@@ -816,16 +811,129 @@ fn should_passthrough_smt_eval(req: &VerifyRequest) -> bool {
 }
 
 fn extract_smt_status(text: &str) -> Option<String> {
-    let lower = text.to_ascii_lowercase();
-    if lower.contains("unsat") {
-        Some("unsat".to_string())
-    } else if lower.contains("sat") {
-        Some("sat".to_string())
-    } else if lower.contains("unknown") {
-        Some("unknown".to_string())
-    } else {
-        None
+    // Result tokens are case-sensitive, standalone SMT-LIB responses.
+    // A satisfiable or unknown query prevents an aggregate proof claim.
+    let statuses: Vec<_> = text
+        .lines()
+        .map(str::trim)
+        .filter(|line| matches!(*line, "sat" | "unsat" | "unknown"))
+        .collect();
+    ["sat", "unknown", "unsat"]
+        .into_iter()
+        .find(|status| statuses.contains(status))
+        .map(str::to_owned)
+}
+
+fn discharged_smt_queries(source: &str, stdout: &str) -> bool {
+    let Some(commands) = smt_commands(source) else {
+        return false;
+    };
+    // Z3 emits echo strings without quotes. Never authenticate an echoed
+    // "unsat" as a solver answer, including echo+exit before a query.
+    if commands
+        .iter()
+        .any(|command| matches!(*command, "echo" | "exit"))
+    {
+        return false;
+    }
+    let queries = commands
+        .iter()
+        .filter(|command| matches!(**command, "check-sat" | "check-sat-assuming"))
+        .count();
+    let statuses: Vec<_> = stdout
+        .lines()
+        .map(str::trim)
+        .filter(|line| matches!(*line, "sat" | "unsat" | "unknown"))
+        .collect();
+    queries > 0 && statuses.len() == queries && statuses.iter().all(|status| *status == "unsat")
+}
+
+/// Read command names only; the real solver still validates SMT-LIB terms.
+/// Strings, quoted symbols and line comments cannot introduce commands.
+fn smt_commands(source: &str) -> Option<Vec<&str>> {
+    let bytes = source.as_bytes();
+    let mut commands = Vec::new();
+    let (mut index, mut depth) = (0, 0usize);
+    while index < bytes.len() {
+        match bytes[index] {
+            b';' => {
+                while index < bytes.len() && bytes[index] != b'\n' {
+                    index += 1;
+                }
+            },
+            b'"' | b'|' => {
+                if depth == 0 {
+                    return None;
+                }
+                let delimiter = bytes[index];
+                index += 1;
+                loop {
+                    if index == bytes.len() {
+                        return None;
+                    }
+                    if bytes[index] == delimiter {
+                        index += 1;
+                        if delimiter == b'"' && bytes.get(index) == Some(&b'"') {
+                            index += 1;
+                        } else {
+                            break;
+                        }
+                    } else {
+                        index += 1;
+                    }
+                }
+            },
+            b'(' => {
+                if depth == 0 {
+                    index += 1;
+                    // Whitespace and comments are legal before the command.
+                    loop {
+                        while bytes.get(index).is_some_and(u8::is_ascii_whitespace) {
+                            index += 1;
+                        }
+                        if bytes.get(index) != Some(&b';') {
+                            break;
+                        }
+                        while index < bytes.len() && bytes[index] != b'\n' {
+                            index += 1;
+                        }
+                    }
+                    let start = index;
+                    while bytes
+                        .get(index)
+                        .is_some_and(|b| b.is_ascii_alphanumeric() || *b == b'-')
+                    {
+                        index += 1;
+                    }
+                    if index == start
+                        || !bytes
+                            .get(index)
+                            .is_some_and(|b| b.is_ascii_whitespace() || matches!(b, b')' | b';'))
+                    {
+                        return None;
+                    }
+                    commands.push(&source[start..index]);
+                } else {
+                    index += 1;
+                }
+                depth += 1;
+            },
+            b')' => {
+                depth = depth.checked_sub(1)?;
+                index += 1;
+            },
+            byte if byte.is_ascii_whitespace() => {
+                index += 1;
+            },
+            _ => {
+                if depth == 0 {
+                    return None;
+                }
+                index += 1;
+            },
+        }
     }
+    (depth == 0).then_some(commands)
 }
 
 /// Get tactic suggestions
@@ -1271,9 +1379,9 @@ async fn search_theorems_ui(
     // stable shape, and the real query goes through the search
     // workspace member.
     let results = vec![
-        format!("Theorem: associativity_add (a + b) + c = a + (b + c)"),
-        format!("Theorem: commutativity_mul a * b = b * a"),
-        format!("Lemma: distributivity a * (b + c) = a * b + a * c"),
+        "Theorem: associativity_add (a + b) + c = a + (b + c)".to_string(),
+        "Theorem: commutativity_mul a * b = b * a".to_string(),
+        "Lemma: distributivity a * (b + c) = a * b + a * c".to_string(),
     ];
 
     Ok(Json(SearchTheoremsUIResponse { results }))
diff --git a/tests/e2e_prover_test.rs b/tests/e2e_prover_test.rs
index 95a6b463..d954818e 100644
--- a/tests/e2e_prover_test.rs
+++ b/tests/e2e_prover_test.rs
@@ -368,12 +368,12 @@ async fn e2e_malformed_input_returns_error_not_panic() -> Result<()> {
         match result {
             Ok(r) => eprintln!(
                 "E2E malformed[{}..]: Ok(verified={})",
-                &input.chars().take(20).collect::<String>(),
+                input.chars().take(20).collect::<String>(),
                 r.verified
             ),
             Err(e) => eprintln!(
                 "E2E malformed[{}..]: Err({})",
-                &input.chars().take(20).collect::<String>(),
+                input.chars().take(20).collect::<String>(),
                 e
             ),
         }
diff --git a/tests/live_service_regressions.rs b/tests/live_service_regressions.rs
index be87a0b9..82df91f3 100644
--- a/tests/live_service_regressions.rs
+++ b/tests/live_service_regressions.rs
@@ -61,6 +61,28 @@ async fn http_verification_requires_a_discharged_obligation() {
             );
         }
     }
+    for prover in ["Z3", "CVC5"] {
+        for content in [
+            "(set-logic QF_LIA)\n(echo \"unsat\")\n(assert true)\n(check-sat)",
+            "(set-logic QF_LIA)\n(echo \"unsat\")\n(exit)\n; (check-sat)",
+            "(set-logic QF_LIA)\n(push 1)\n(assert false)\n(check-sat)\n(pop 1)\n(check-sat)",
+            "(set-logic QF_LIA)\n(; comment before command\n echo \"unsat\")\n(exit)\n(check-sat)",
+        ] {
+            let result: Value = client
+                .post(format!("{base}/api/verify"))
+                .json(&json!({"prover": prover, "content": content}))
+                .send()
+                .await
+                .unwrap()
+                .error_for_status()
+                .unwrap()
+                .json()
+                .await
+                .unwrap();
+            assert_eq!(result["valid"], false, "{prover}: {content}: {result}");
+            assert_ne!(result["outcome"], "PROVED", "{prover}: {content}: {result}");
+        }
+    }
     for (content, expected) in [
         (
             "Theorem identity : forall P : Prop, P -> P. Proof. intros P H. exact H. Qed.",
@@ -111,24 +133,12 @@ async fn coq_string_submission_accepts_proof_and_rejects_falsehood() {
 
 #[test]
 fn report_actual_backend_inventory() {
-    // Ask the compiled serde implementation for its accepted variants. This
-    // includes variants omitted by ProverKind::all(), unlike the CLI listing.
-    let error = serde_json::from_str::<ProverKind>("\"_inventory_probe_\"")
-        .unwrap_err()
-        .to_string();
-    let expected = error
-        .split("expected one of ")
-        .nth(1)
-        .expect("serde variant list");
-    let variants: Vec<_> = expected
-        .split('`')
-        .enumerate()
-        .filter_map(|(index, value)| (index % 2 == 1).then_some(value))
-        .collect();
+    use strum::IntoEnumIterator;
+    // Derived from the enum itself, including variants omitted by the CLI.
     let advertised = ProverKind::all();
     let mut records = Vec::new();
-    for name in variants {
-        let kind: ProverKind = serde_json::from_value(serde_json::json!(name)).unwrap();
+    for kind in ProverKind::iter() {
+        let name = serde_json::to_value(kind).unwrap();
         let executable = kind.default_executable();
         let path = which::which(executable).ok();
         records.push(serde_json::json!({