diff --git a/.github/hooks/pre-commit b/.github/hooks/pre-commit
deleted file mode 100755
index d61f3b52..00000000
--- a/.github/hooks/pre-commit
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/usr/bin/env bash
-#
-# ECHIDNA Pre-commit Hook
-# Enforces npm ban and runs checks
-#
-# SPDX-License-Identifier: MPL-2.0
-
-set -euo pipefail
-
-echo "🦔 ECHIDNA Pre-commit Checks"
-echo "============================"
-
-# Run npm ban check
-if [ -x "scripts/ban-npm.sh" ]; then
-    bash scripts/ban-npm.sh
-fi
-
-# Run Deno checks if available
-if command -v deno &> /dev/null; then
-    echo ""
-    echo "Running Deno lint..."
-    deno lint src/provers/ || true
-
-    echo ""
-    echo "Running Deno check..."
-    deno check src/provers/mod.ts || true
-fi
-
-echo ""
-echo "✅ Pre-commit checks passed"
diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
index 611eccd0..091a936a 100644
--- a/.github/workflows/actions.lock
+++ b/.github/workflows/actions.lock
@@ -32,6 +32,7 @@ workflows:
         - 'actions/checkout@v7.0.1'
     '.github/workflows/dogfood-gate.yml':
         - 'actions/checkout@v7.0.1'
+        - 'oven-sh/setup-bun@v2.2.0'
     '.github/workflows/dogfood-proofs-ci.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/formal-verification.yml':
@@ -181,6 +182,11 @@ dependencies:
         commit: 'sha1-d1434d08867e3ee9daa34448df10607b98908d29'
         owner_id: 7289241
         repo_id: 812112570
+    'oven-sh/setup-bun@v2.2.0':
+        ref: 'v2.2.0'
+        commit: 'sha1-0c5077e51419868618aeaa5fe8019c62421857d6'
+        owner_id: 108928776
+        repo_id: 512644635
     'swatinem/rust-cache@v2.9.2':
         ref: 'v2.9.2'
         commit: 'sha1-6323deb102c322ba6fcbdcafc7e3dddab59af2b6'
diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml
index 442c4b39..37daf073 100644
--- a/.github/workflows/dogfood-gate.yml
+++ b/.github/workflows/dogfood-gate.yml
@@ -249,6 +249,11 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v7.0.1
 
+      - name: Set up bun
+        uses: oven-sh/setup-bun@v2.2.0
+        with:
+          bun-version: 1.3.14 # matches mise.lock
+
       - name: Check and validate eclexiaiser manifest
         id: eclex
         run: |
@@ -263,34 +268,9 @@ jobs:
 
           echo "has_manifest=true" >> "$GITHUB_OUTPUT"
 
-          # Validate TOML structure using Python 3.11+ tomllib.
-          # The Python heredoc body sits at the YAML block-scalar base
-          # indentation, so after GitHub strips the block's common indent
-          # the interpreter receives it column-aligned (no sed dedent —
-          # a sed-based dedent breaks because YAML removes the block's
-          # leading indent before the script ever reaches the shell).
-          if ! python3 - <<'PY'
-          import tomllib, sys
-          with open('eclexiaiser.toml', 'rb') as f:
-              data = tomllib.load(f)
-          project = data.get('project', {})
-          if not project.get('name', '').strip():
-              print('ERROR: project.name is required', file=sys.stderr)
-              sys.exit(1)
-          functions = data.get('functions', [])
-          if not functions:
-              print('ERROR: at least one [[functions]] entry is required', file=sys.stderr)
-              sys.exit(1)
-          for fn in functions:
-              if not fn.get('name', '').strip():
-                  print('ERROR: function name cannot be empty', file=sys.stderr)
-                  sys.exit(1)
-              if not fn.get('source', '').strip():
-                  print(f'ERROR: function {fn["name"]} has no source path', file=sys.stderr)
-                  sys.exit(1)
-          print(f'Valid: {project["name"]} ({len(functions)} function(s))')
-          PY
-          then
+          # Structural checks live in scripts/validate-eclexiaiser.js (tested by
+          # scripts/validate-eclexiaiser.test.js); bun parses the TOML.
+          if ! bun scripts/validate-eclexiaiser.js eclexiaiser.toml; then
             echo "::error file=eclexiaiser.toml::Invalid eclexiaiser.toml — see step output for details"
             exit 1
           fi
@@ -308,13 +288,36 @@ jobs:
           fi
 
   # ---------------------------------------------------------------------------
-  # Job 6: Dogfooding summary
+  # Job 6: Banned-runtime check (no npm or deno artefacts; bun is the runtime)
+  # ---------------------------------------------------------------------------
+  runtime-ban:
+    name: Banned-runtime check
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+
+      - name: Set up bun
+        uses: oven-sh/setup-bun@v2.2.0
+        with:
+          bun-version: 1.3.14 # matches mise.lock
+
+      - name: Test the repo bun scripts
+        run: bun test scripts/
+
+      - name: No npm or deno artefacts
+        run: bash scripts/ban-npm.sh
+
+  # ---------------------------------------------------------------------------
+  # Job 7: Dogfooding summary
   # ---------------------------------------------------------------------------
   dogfood-summary:
     name: Dogfooding compliance summary
     runs-on: ubuntu-latest
     timeout-minutes: 10
-    needs: [a2ml-validate, k9-validate, empty-lint, groove-check, eclexiaiser-validate]
+    needs: [a2ml-validate, k9-validate, empty-lint, groove-check, eclexiaiser-validate, runtime-ban]
     if: always()
 
     steps:
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
deleted file mode 100644
index 9088b338..00000000
--- a/.pre-commit-config.yaml
+++ /dev/null
@@ -1,51 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-# Pre-commit hooks for hyperpolymath RSR repos.
-# Install: pip install pre-commit && pre-commit install
-# Run manually: pre-commit run --all-files
-
-repos:
-  # --- Standard hooks ---
-  - repo: https://github.com/pre-commit/pre-commit-hooks
-    rev: v5.0.0
-    hooks:
-      - id: trailing-whitespace
-      - id: end-of-file-fixer
-      - id: check-yaml
-      - id: check-json
-      - id: check-toml
-      - id: check-merge-conflict
-      - id: detect-private-key
-      - id: check-added-large-files
-        args: ['--maxkb=1024']
-
-  # --- A2ML manifest validation ---
-  - repo: https://github.com/hyperpolymath/a2ml-pre-commit
-    rev: main
-    hooks:
-      - id: validate-a2ml
-        name: Validate A2ML manifests
-
-  # --- K9 contract validation ---
-  - repo: https://github.com/hyperpolymath/k9-pre-commit
-    rev: main
-    hooks:
-      - id: validate-k9
-        name: Validate K9 contracts
-
-  # --- Shell linting ---
-  - repo: https://github.com/shellcheck-py/shellcheck-py
-    rev: v0.10.0.1
-    hooks:
-      - id: shellcheck
-
-  # --- EditorConfig ---
-  - repo: https://github.com/editorconfig-checker/editorconfig-checker.python
-    rev: 3.2.1
-    hooks:
-      - id: editorconfig-checker
-        exclude: '(\.git|node_modules|target|_build|deps|\.deno|external_corpora|\.lake)/'
-
-  # --- Secret detection ---
-  # Secret scanning is enforced in CI via TruffleHog
-  # (.github/workflows/secret-scanner.yml). gitleaks removed 2026-06-14
-  # (estate standardisation on TruffleHog).
diff --git a/NOTICE b/NOTICE
index fdfe9b9f..52f9719b 100644
--- a/NOTICE
+++ b/NOTICE
@@ -81,7 +81,7 @@ own licences. See the respective component directories and files for details.
 
 Rust dependencies:    Cargo.toml + `cargo license`
 Julia packages:       Project.toml + Manifest.toml
-Deno / AffineScript:  deno.json (run `deno info`)
+Bun scripts:          scripts/*.js (bun built-ins only, no third-party packages)
 
 Theorem provers (integrated, not redistributed):
   Agda            BSD-3-Clause
diff --git a/hooks/pre-commit b/hooks/pre-commit
index db881a89..619386a4 100755
--- a/hooks/pre-commit
+++ b/hooks/pre-commit
@@ -7,6 +7,9 @@
 # Enable per clone:  git config core.hooksPath hooks
 set -euo pipefail
 
+# Banned runtimes (npm, deno) — fast, needs no toolchain, so it runs before the just check.
+bash scripts/ban-npm.sh
+
 if ! command -v just >/dev/null 2>&1; then
   echo "pre-commit: 'just' not on PATH (RSR-H14 build tool); skipping gate." >&2
   exit 0
diff --git a/scripts/ban-npm.sh b/scripts/ban-npm.sh
index 4bc8a679..4304ed98 100755
--- a/scripts/ban-npm.sh
+++ b/scripts/ban-npm.sh
@@ -30,19 +30,20 @@ if find . -type d -name "node_modules" 2>/dev/null | grep -q .; then
     VIOLATIONS=$((VIOLATIONS + 1))
 fi
 
+# Check for Deno manifests or lockfiles (deno is banned estate-wide; bun is the runtime)
+DENO_FILES=$(find . \( -name .git -o -name target -o -name node_modules \) -prune -o -type f \( -name deno.json -o -name deno.jsonc -o -name deno.lock \) -print 2>/dev/null)
+if [ -n "$DENO_FILES" ]; then
+    echo -e "${RED}❌ VIOLATION: Deno manifest or lockfile found${NC}"
+    echo "$DENO_FILES"
+    VIOLATIONS=$((VIOLATIONS + 1))
+fi
+
 # Check for npm/npx usage in scripts
 if grep -r "npm install\|npm i \|npx \|npm run" scripts/ 2>/dev/null | grep -v "ban-npm"; then
     echo -e "${RED}❌ VIOLATION: npm/npx commands found in scripts${NC}"
     VIOLATIONS=$((VIOLATIONS + 1))
 fi
 
-# Check for npm imports in TypeScript (should use https:// or npm: specifier)
-BAD_IMPORTS=$(grep -r "from ['\"][@a-z]" src/provers/ 2>/dev/null | grep -v "from ['\"]https://" | grep -v "from ['\"]npm:" | grep -v "from ['\"]\./" | grep -v "from ['\"]\.\./" || true)
-if [ -n "$BAD_IMPORTS" ]; then
-    echo -e "${YELLOW}⚠️  WARNING: Bare imports found (should use https:// or npm: specifier)${NC}"
-    echo "$BAD_IMPORTS"
-fi
-
 # Check Justfile for npm commands
 if [ -f "Justfile" ] && grep -q "npm\|npx" Justfile; then
     echo -e "${RED}❌ VIOLATION: npm/npx found in Justfile${NC}"
@@ -55,11 +56,10 @@ if [ $VIOLATIONS -eq 0 ]; then
     echo -e "${GREEN}✅ No npm violations found!${NC}"
     echo ""
     echo "Approved package managers:"
-    echo "  ✓ Deno (deno.json, deno task)"
-    echo "  ✓ Bun (only if Deno impossible)"
+    echo "  ✓ Bun (the estate JavaScript runtime)"
     echo ""
     echo "Banned:"
-    echo "  ✗ npm, npx, node_modules"
+    echo "  ✗ npm, npx, node_modules, deno"
     echo "  ✗ package-lock.json"
     exit 0
 else
@@ -68,7 +68,6 @@ else
     echo "To fix:"
     echo "  1. Remove package-lock.json: rm package-lock.json"
     echo "  2. Remove node_modules: rm -rf node_modules"
-    echo "  3. Use 'deno task' instead of 'npm run'"
-    echo "  4. Use https:// or npm: imports in Deno"
+    echo "  3. Use 'bun run' instead of 'npm run'"
     exit 1
 fi
diff --git a/scripts/ban-npm.test.js b/scripts/ban-npm.test.js
new file mode 100644
index 00000000..4b321bb9
--- /dev/null
+++ b/scripts/ban-npm.test.js
@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+//
+// Planted-fixture tests for scripts/ban-npm.sh: each banned artefact is placed
+// in a scratch tree and the script must exit 1; the clean tree must exit 0.
+// Run: bun test scripts/
+import { afterEach, expect, test } from "bun:test";
+import { cpSync, mkdirSync, mkdtempSync, rmSync, writeFileSync } from "node:fs";
+import { tmpdir } from "node:os";
+import { dirname, join } from "node:path";
+
+const SCRIPT = new URL("./ban-npm.sh", import.meta.url).pathname;
+const trees = [];
+
+/** Builds a scratch tree holding the script plus `files` (path → content) and returns its exit code. */
+function runIn(files) {
+  const root = mkdtempSync(join(tmpdir(), "ban-npm-"));
+  trees.push(root);
+  mkdirSync(join(root, "scripts"));
+  cpSync(SCRIPT, join(root, "scripts", "ban-npm.sh"));
+  for (const [path, content] of Object.entries(files)) {
+    mkdirSync(dirname(join(root, path)), { recursive: true });
+    writeFileSync(join(root, path), content);
+  }
+  return Bun.spawnSync(["bash", "scripts/ban-npm.sh"], { cwd: root, stdout: "pipe", stderr: "pipe" }).exitCode;
+}
+
+afterEach(() => { while (trees.length) rmSync(trees.pop(), { recursive: true, force: true }); });
+
+test("a clean tree passes", () => expect(runIn({ "README.adoc": "x\n" })).toBe(0));
+test("package-lock.json fails", () => expect(runIn({ "package-lock.json": "{}" })).toBe(1));
+test("a root deno.json fails", () => expect(runIn({ "deno.json": "{}" })).toBe(1));
+test("a nested deno.lock fails", () => expect(runIn({ "sub/app/deno.lock": "{}" })).toBe(1));
+test("a deno.jsonc fails", () => expect(runIn({ "tools/deno.jsonc": "{}" })).toBe(1));
diff --git a/scripts/build-production.sh b/scripts/build-production.sh
deleted file mode 100755
index c612881a..00000000
--- a/scripts/build-production.sh
+++ /dev/null
@@ -1,151 +0,0 @@
-#!/bin/bash
-# SPDX-License-Identifier: MPL-2.0
-# Production build script for ECHIDNA
-
-set -e
-
-echo "╔════════════════════════════════════════════════════════════╗"
-echo "║         ECHIDNA Production Build                           ║"
-echo "╚════════════════════════════════════════════════════════════╝"
-echo ""
-
-# Colors
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[1;33m'
-NC='\033[0m' # No Color
-
-# Step 1: Build Rust backend
-echo -e "${YELLOW}[1/4]${NC} Building Rust backend (release mode)..."
-cargo build --release
-echo -e "${GREEN}✓${NC} Rust backend built"
-echo ""
-
-# Step 2: Build ReScript frontend
-echo -e "${YELLOW}[2/4]${NC} Building ReScript frontend..."
-cd src/rescript
-./node_modules/.bin/rescript build
-echo -e "${GREEN}✓${NC} ReScript frontend compiled"
-echo ""
-
-# Step 3: Create distribution directory
-echo -e "${YELLOW}[3/4]${NC} Creating distribution package..."
-cd ../..
-mkdir -p dist/echidna
-mkdir -p dist/echidna/bin
-mkdir -p dist/echidna/ui
-mkdir -p dist/echidna/models
-mkdir -p dist/echidna/examples
-
-# Copy binaries
-cp target/release/echidna dist/echidna/bin/
-
-# Copy UI files
-cp src/rescript/index.html dist/echidna/ui/
-cp -r src/rescript/src/*.bs.js dist/echidna/ui/
-cp -r src/rescript/src/**/*.bs.js dist/echidna/ui/ 2>/dev/null || true
-
-# Copy ML models if they exist
-cp models/*.jlso dist/echidna/models/ 2>/dev/null || true
-
-# Copy examples
-cp -r examples/*.* dist/echidna/examples/ 2>/dev/null || true
-
-echo -e "${GREEN}✓${NC} Distribution package created"
-echo ""
-
-# Step 4: Create startup script
-echo -e "${YELLOW}[4/4]${NC} Creating startup script..."
-cat > dist/echidna/start.sh << 'STARTUP'
-#!/bin/bash
-# Start ECHIDNA platform
-
-# Start backend
-echo "Starting ECHIDNA backend..."
-./bin/echidna server --port 8081 --cors &
-BACKEND_PID=$!
-
-# Wait for backend to be ready
-sleep 2
-
-# Start frontend
-echo "Starting ECHIDNA frontend..."
-cd ui
-python3 -m http.server 3000 &
-FRONTEND_PID=$!
-
-echo ""
-echo "╔════════════════════════════════════════════════════════════╗"
-echo "║              ECHIDNA is now running!                       ║"
-echo "╠════════════════════════════════════════════════════════════╣"
-echo "║  UI:  http://127.0.0.1:3000                                ║"
-echo "║  API: http://127.0.0.1:8081/api                            ║"
-echo "╚════════════════════════════════════════════════════════════╝"
-echo ""
-echo "Press Ctrl+C to stop both servers"
-
-# Wait for Ctrl+C
-trap "kill $BACKEND_PID $FRONTEND_PID" EXIT
-wait
-STARTUP
-
-chmod +x dist/echidna/start.sh
-
-echo -e "${GREEN}✓${NC} Startup script created"
-echo ""
-
-# Create README
-cat > dist/echidna/README.md << 'README'
-# ECHIDNA Distribution
-
-**Neurosymbolic Theorem Proving Platform**
-
-## Quick Start
-
-```bash
-./start.sh
-```
-
-Then open http://127.0.0.1:3000 in your browser.
-
-## Contents
-
-- `bin/echidna` - Main executable
-- `ui/` - Web interface
-- `models/` - ML models
-- `examples/` - Example proofs
-- `start.sh` - Startup script
-
-## Requirements
-
-- Python 3 (for UI server)
-- Modern web browser
-- Linux/macOS
-
-## Manual Start
-
-Backend:
-```bash
-./bin/echidna server --port 8081 --cors
-```
-
-Frontend:
-```bash
-cd ui && python3 -m http.server 3000
-```
-
-## Documentation
-
-See QUICKSTART.md for full documentation.
-README
-
-echo "╔════════════════════════════════════════════════════════════╗"
-echo "║              Production Build Complete! ✓                  ║"
-echo "╚════════════════════════════════════════════════════════════╝"
-echo ""
-echo "Distribution created in: dist/echidna/"
-echo ""
-echo "To run:"
-echo "  cd dist/echidna"
-echo "  ./start.sh"
-echo ""
diff --git a/scripts/validate-eclexiaiser.js b/scripts/validate-eclexiaiser.js
new file mode 100755
index 00000000..63659967
--- /dev/null
+++ b/scripts/validate-eclexiaiser.js
@@ -0,0 +1,42 @@
+#!/usr/bin/env bun
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+//
+// Structural check of eclexiaiser.toml for the dogfood-gate workflow. It
+// replaces a python3 tomllib heredoc (python is banned estate-wide) and keeps
+// its four rejections and messages. Usage: bun scripts/validate-eclexiaiser.js [path]
+
+/** Returns true when `v` is a string with non-whitespace content. */
+const filled = (v) => typeof v === "string" && v.trim() !== "";
+
+/**
+ * Validates eclexiaiser manifest text.
+ * Returns { ok, message }: ok is false on a parse error, a blank or missing
+ * project.name, no [[functions]] entry, or a function lacking name or source.
+ */
+export function validateEclexiaiser(text) {
+  let data;
+  try {
+    data = Bun.TOML.parse(text);
+  } catch (e) {
+    return { ok: false, message: `ERROR: eclexiaiser.toml does not parse: ${e.message}` };
+  }
+  const project = data.project ?? {};
+  if (!filled(project.name)) return { ok: false, message: "ERROR: project.name is required" };
+  const functions = Array.isArray(data.functions) ? data.functions : [];
+  if (functions.length === 0) {
+    return { ok: false, message: "ERROR: at least one [[functions]] entry is required" };
+  }
+  for (const fn of functions) {
+    if (!filled(fn.name)) return { ok: false, message: "ERROR: function name cannot be empty" };
+    if (!filled(fn.source)) return { ok: false, message: `ERROR: function ${fn.name} has no source path` };
+  }
+  return { ok: true, message: `Valid: ${project.name} (${functions.length} function(s))` };
+}
+
+if (import.meta.main) {
+  const path = process.argv[2] ?? "eclexiaiser.toml";
+  const result = validateEclexiaiser(await Bun.file(path).text());
+  (result.ok ? console.log : console.error)(result.message);
+  process.exit(result.ok ? 0 : 1);
+}
diff --git a/scripts/validate-eclexiaiser.test.js b/scripts/validate-eclexiaiser.test.js
new file mode 100644
index 00000000..8c655129
--- /dev/null
+++ b/scripts/validate-eclexiaiser.test.js
@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+//
+// Tests for scripts/validate-eclexiaiser.js — the four rejections the
+// dogfood-gate eclexiaiser job enforced in its retired python3 heredoc, plus
+// the valid case and the repo's own manifest. Run: bun test scripts/
+import { describe, expect, test } from "bun:test";
+import { validateEclexiaiser } from "./validate-eclexiaiser.js";
+
+const VALID = `
+[project]
+name = "echidna"
+
+[[functions]]
+name = "scan"
+source = "src/main.rs"
+`;
+
+describe("validateEclexiaiser", () => {
+  test("accepts a manifest with a project name and a complete function", () => {
+    expect(validateEclexiaiser(VALID)).toEqual({ ok: true, message: "Valid: echidna (1 function(s))" });
+  });
+
+  test("rejects a missing or blank project.name", () => {
+    expect(validateEclexiaiser(`[project]\nname = "  "\n[[functions]]\nname="a"\nsource="b"\n`))
+      .toEqual({ ok: false, message: "ERROR: project.name is required" });
+    expect(validateEclexiaiser(`[[functions]]\nname="a"\nsource="b"\n`))
+      .toEqual({ ok: false, message: "ERROR: project.name is required" });
+  });
+
+  test("rejects a manifest with no [[functions]] entry", () => {
+    expect(validateEclexiaiser(`[project]\nname = "x"\n`))
+      .toEqual({ ok: false, message: "ERROR: at least one [[functions]] entry is required" });
+  });
+
+  test("rejects a function with a blank name", () => {
+    expect(validateEclexiaiser(`[project]\nname="x"\n[[functions]]\nname=""\nsource="b"\n`))
+      .toEqual({ ok: false, message: "ERROR: function name cannot be empty" });
+  });
+
+  test("rejects a function with no source path", () => {
+    expect(validateEclexiaiser(`[project]\nname="x"\n[[functions]]\nname="scan"\n`))
+      .toEqual({ ok: false, message: "ERROR: function scan has no source path" });
+  });
+
+  test("rejects TOML that does not parse, without throwing", () => {
+    const r = validateEclexiaiser(`[project\nname = `);
+    expect(r.ok).toBe(false);
+    expect(r.message).toStartWith("ERROR: eclexiaiser.toml does not parse:");
+  });
+
+  test("the repo's own eclexiaiser.toml is valid", async () => {
+    const text = await Bun.file(new URL("../eclexiaiser.toml", import.meta.url)).text();
+    expect(validateEclexiaiser(text).ok).toBe(true);
+  });
+});