From 96dd5e7061a7f4b97241a123349295ee4849b239 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 2 Apr 2026 09:35:33 +0100
Subject: [PATCH] Snapshot local work before sync

---
 .github/workflows/casket-pages.yml            | 116 ++++++++++
 .machine_readable/6a2/META.a2ml               |   2 +-
 .machine_readable/6a2/STATE.a2ml              |  69 +++---
 .zenodo.json                                  |   2 +-
 0-AI-MANIFEST.a2ml                            |  46 +++-
 Justfile                                      | 124 +++++------
 README.adoc                                   |  58 +++--
 ROADMAP.adoc                                  |  16 +-
 arcvix-10-level-query-safety.tex              | 120 +++++-----
 benchmarks/README.adoc                        |  13 ++
 docs/architecture/ARCHITECTURE.adoc           |  24 +-
 .../audit/2026-03-30-vql-ut-audit.adoc        | 100 +++++++++
 .../2026-03-31-vql-ut-publication-review.adoc |  65 ++++++
 src/interface/dap/src/main.rs                 | 209 ++++++++----------
 src/interface/fmt/src/lib.rs                  |   4 +-
 src/interface/lint/src/lib.rs                 |   4 +-
 src/interface/lsp/src/lib.rs                  |  45 ++--
 src/interface/lsp/src/main.rs                 |   6 +-
 tests/aspect/README.adoc                      |  11 +
 tests/e2e/README.adoc                         |  11 +
 tests/fuzz/README.adoc                        |   7 +
 tests/fuzz/placeholder.txt                    |   1 -
 tests/integration_test.rs                     |  30 ++-
 23 files changed, 730 insertions(+), 353 deletions(-)
 create mode 100644 .github/workflows/casket-pages.yml
 create mode 100644 benchmarks/README.adoc
 create mode 100644 docs/reports/audit/2026-03-30-vql-ut-audit.adoc
 create mode 100644 docs/reports/audit/2026-03-31-vql-ut-publication-review.adoc
 create mode 100644 tests/aspect/README.adoc
 create mode 100644 tests/e2e/README.adoc
 create mode 100644 tests/fuzz/README.adoc
 delete mode 100644 tests/fuzz/placeholder.txt

diff --git a/.github/workflows/casket-pages.yml b/.github/workflows/casket-pages.yml
new file mode 100644
index 0000000..bc60350
--- /dev/null
+++ b/.github/workflows/casket-pages.yml
@@ -0,0 +1,116 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+name: GitHub Pages
+
+on:
+  push:
+    branches: [main, master]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: "pages"
+  cancel-in-progress: false
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+
+      - name: Checkout casket-ssg
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+        with:
+          repository: hyperpolymath/casket-ssg
+          path: .casket-ssg
+
+      - name: Setup GHCup
+        uses: haskell-actions/setup@ec49483bfc012387b227434aba94f59a6ecd0900 # v2
+        with:
+          ghc-version: '9.8.2'
+          cabal-version: '3.10'
+
+      - name: Cache Cabal
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
+        with:
+          path: |
+            ~/.cabal/packages
+            ~/.cabal/store
+            .casket-ssg/dist-newstyle
+          key: ${{ runner.os }}-casket-${{ hashFiles('.casket-ssg/casket-ssg.cabal') }}
+
+      - name: Build casket-ssg
+        working-directory: .casket-ssg
+        run: cabal build
+
+      - name: Prepare site source
+        shell: bash
+        run: |
+          set -euo pipefail
+          rm -rf .site-src _site
+
+          if [ -d site ]; then
+            cp -R site .site-src
+          else
+            mkdir -p .site-src
+            TODAY="$(date +%Y-%m-%d)"
+            REPO_NAME="${{ github.event.repository.name }}"
+            REPO_URL="https://github.com/${{ github.repository }}"
+            README_URL=""
+
+            if [ -f README.md ]; then
+              README_URL="${REPO_URL}/blob/${{ github.ref_name }}/README.md"
+            elif [ -f README.adoc ]; then
+              README_URL="${REPO_URL}/blob/${{ github.ref_name }}/README.adoc"
+            fi
+
+            {
+              echo "---"
+              echo "title: ${REPO_NAME}"
+              echo "date: ${TODAY}"
+              echo "---"
+              echo
+              echo "# ${REPO_NAME}"
+              echo
+              echo "Static documentation site for ${REPO_NAME}."
+              echo
+              echo "- Source repository: [${{ github.repository }}](${REPO_URL})"
+              if [ -n "${README_URL}" ]; then
+                echo "- README: [project README](${README_URL})"
+              fi
+              if [ -d docs ]; then
+                echo "- Docs directory: [docs/](${REPO_URL}/tree/${{ github.ref_name }}/docs)"
+              fi
+              echo
+              echo "Project-specific site content can be added later under site/."
+            } > .site-src/index.md
+          fi
+
+      - name: Build site
+        run: |
+          mkdir -p _site
+          cd .casket-ssg && cabal run casket-ssg -- build ../.site-src ../_site
+          touch ../_site/.nojekyll
+
+      - name: Setup Pages
+        uses: actions/configure-pages@983d7736d9b0ae728b81ab479565c72886d7745b # v5
+
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa # v3
+        with:
+          path: '_site'
+
+  deploy:
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    needs: build
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4
diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml
index df4505b..cd0a11f 100644
--- a/.machine_readable/6a2/META.a2ml
+++ b/.machine_readable/6a2/META.a2ml
@@ -34,7 +34,7 @@ axis-3 = "systems > compliance > effects"
 [scoping]
 sources = "README, roadmap, status docs, maintenance checklist, CI/security docs"
 marker-scan = "TODO/FIXME/XXX/HACK/STUB/PARTIAL"
-idris-unsound-scan = "believe_me/assert_total"
+idris-unsound-scan = "unsound-idris-escape-scan"
 
 [axis-2-maintenance-rules]
 corrective-first = true
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
index 131832b..58a4927 100644
--- a/.machine_readable/6a2/STATE.a2ml
+++ b/.machine_readable/6a2/STATE.a2ml
@@ -1,64 +1,55 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# STATE.a2ml — Project state checkpoint (META-TEMPLATE)
-#
-# This is the STATE file for rsr-template-repo itself.
-# When consumed by a new project, replace {{PLACEHOLDER}} tokens
-# and customize sections below for the target project.
+# STATE.a2ml — Project state checkpoint
 
 [metadata]
-project = "rsr-template-repo"
-version = "0.2.0"
-last-updated = "2026-02-28"
-status = "active"  # active | paused | archived
+project = "vql-ut"
+version = "0.1.0"
+last-updated = "2026-03-30"
+status = "active"
 
 [project-context]
-name = "rsr-template-repo"
-purpose = "Canonical RSR-compliant repository template providing scaffolding for all hyperpolymath projects — including CI/CD, AI manifests, ABI/FFI standards, container ecosystem, and governance infrastructure."
-completion-percentage = 95
+name = "vql-ut"
+purpose = "Experimental research repo for a proposed type-safe query layer for VeriSimDB, with current Rust formatter/linter surfaces and draft Idris2/Zig/ReScript implementation work."
+completion-percentage = 25
 
 [position]
-phase = "maintenance"      # design | implementation | testing | maintenance | archived
-maturity = "production"    # experimental | alpha | beta | production | lts
+phase = "audit-remediation"
+maturity = "experimental"
 
 [route-to-mvp]
 milestones = [
-  { name = "Phase 0: Core scaffolding (justfile, CI/CD, .machine_readable)", completion = 100 },
-  { name = "Phase 1: ABI/FFI standard (Idris2/Zig templates)", completion = 100 },
-  { name = "Phase 1b: AI Gatekeeper Protocol (0-AI-MANIFEST.a2ml)", completion = 100 },
-  { name = "Phase 1c: TOPOLOGY.md standard and guide", completion = 100 },
-  { name = "Phase 1d: Maintenance gate (axes, checklist, approach)", completion = 100 },
-  { name = "Phase 1e: Trustfile / contractiles", completion = 100 },
-  { name = "Phase 2: Container ecosystem templates (stapeln)", completion = 100 },
-  { name = "Phase 3: Multi-forge sync hardening", completion = 0 },
-  { name = "Phase 4: Nix/Guix reproducible shells", completion = 50 },
+  { name = "Claim-envelope containment", completion = 70 },
+  { name = "Formatter/linter test surface", completion = 80 },
+  { name = "Draft Idris2 core and ABI encoding", completion = 40 },
+  { name = "End-to-end query pipeline", completion = 10 },
+  { name = "Audited stable release gate", completion = 0 },
 ]
 
 [blockers-and-issues]
-# No active blockers
+issues = [
+  "Public docs and manuscript still outrun implemented and checked evidence in places",
+  "Template residue remains in task runner, container, and support surfaces",
+  "No end-to-end verified query pipeline or proof-certificate output exists yet",
+  "Stable release audit still fails",
+]
 
 [critical-next-actions]
 actions = [
-  "Container templates complete — test with `just container-init`",
-  "Validate container templates across wolfi-base and static Chainguard images",
-  "Harden multi-forge sync for GitLab/Bitbucket mirroring edge cases",
-  "Expand Nix/Guix development shell templates",
+  "Keep public claims aligned with the current checked artifact",
+  "Remove remaining template residue from task runner and container surfaces",
+  "Split test surfaces cleanly into point-to-point, e2e, aspect, and benchmark smoke paths",
+  "Advance Idris2 draft modules toward a checked core before making stronger proof claims",
 ]
 
 [maintenance-status]
 last-run-utc = "never"
 last-report = "docs/reports/maintenance/latest.json"
-last-result = "unknown"  # unknown | pass | warn | fail
-open-warnings = 0
-open-failures = 0
+last-result = "fail"
+open-warnings = 3
+open-failures = 1
 
 [ecosystem]
-part-of = ["RSR Framework", "stapeln ecosystem"]
-depends-on = ["stapeln", "selur-compose", "cerro-torre", "svalinn", "vordr", "k9-svc"]
-
-# ---------------------------------------------------------------------------
-# NOTE FOR CONSUMERS: When using this template to create a new repo, reset
-# the fields above to your project's values and replace all {{PLACEHOLDER}}
-# tokens. The milestones above describe the TEMPLATE's evolution, not yours.
-# ---------------------------------------------------------------------------
+part-of = ["TypeLL lineage", "VeriSimDB ecosystem"]
+depends-on = ["typell", "panll", "verisimdb"]
diff --git a/.zenodo.json b/.zenodo.json
index 0ce3950..1ec4b2b 100644
--- a/.zenodo.json
+++ b/.zenodo.json
@@ -1,6 +1,6 @@
 {
   "title": "VQL-UT: Progressive Type Safety for Database Query Languages",
-  "description": "Database query bugs form a total order by severity. VQL-UT formalises this as progressive levels of type-level query safety, each strictly subsuming all prior levels. Levels 1-6 (established) cover parse-time to result-type safety. Levels 7-10 (research) cover aliasing, effects, lifetimes, and linearity via QTT. Formalised in Idris 2 with zero runtime overhead through proof erasure.",
+  "description": "Database query bugs can be organised as progressive levels of query safety. VQL-UT is currently a design-stage proposal and research prototype for expressing that safety envelope for VeriSimDB-style queries. The repository contains Rust formatter/linter tooling plus draft Idris2 encodings and architecture notes; it does not yet provide a fully mechanised 10-level implementation or end-to-end zero-overhead proof pipeline.",
   "upload_type": "publication",
   "publication_type": "preprint",
   "creators": [{"name": "Jewell, Jonathan D.A.", "affiliation": "The Open University"}],
diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
index bf0e8ec..4caa763 100644
--- a/0-AI-MANIFEST.a2ml
+++ b/0-AI-MANIFEST.a2ml
@@ -7,9 +7,13 @@
 
 ## WHAT IS THIS?
 
-This is the AI manifest for **vql-ut** (VQL Ultimate Type-Safe) — the 10-level
-type-safe query language for VeriSimDB. It supersedes VQL-DT (dependent types
-only) as THE formally verified query path.
+This is the AI manifest for **vql-ut** (VQL Ultimate Type-Safe), an experimental
+research repo for a proposed type-safe query layer for VeriSimDB.
+
+Do **not** describe this repository as a completed formally verified query path,
+as a production-ready system, or as a replacement for VQL-DT. The current repo
+contains surface tooling and draft proof-oriented components, not a finished
+end-to-end verified compiler.
 
 ## NAMING
 
@@ -40,10 +44,10 @@ TypeLL (type theory core)
 | Path | Purpose | Type Safety |
 |------|---------|-------------|
 | VQL (Slipstream) | Standard routine queries, fast | None (runtime only) |
-| VQL-DT | PROOF clauses (6 proof types) | Dependent types via Lean |
-| VQL-UT | All 10 levels, research → production | Full formal verification via Idris2 |
+| VQL-DT | PROOF clauses (6 proof types) | Existing proof-oriented path |
+| VQL-UT | Proposed 10-level successor path | Experimental repo: formatter/linter tests plus draft Idris2/Zig/ReScript work |
 
-If VQL-UT succeeds, it replaces VQL-DT entirely.
+If VQL-UT matures and earns it, it may eventually supersede VQL-DT. It has not done so yet.
 
 ### Adoption Path
 
@@ -82,11 +86,29 @@ These a2ml files MUST exist in `.machine_readable/` directory ONLY:
 2. **No `assert_total`** — All functions provably total via `%default total`.
 3. **No `assert_smaller`** — Termination proved structurally.
 4. **No SCM duplication** — `.machine_readable/` is authoritative.
-5. **Idris2 over Ephapax** — When proven Idris2 code conflicts with Ephapax
+5. **Evidence boundary honesty** — Do not claim end-to-end verification,
+   proof certificates, or production readiness unless the checked artifact
+   actually supports it.
+6. **Idris2 over Ephapax** — When proven Idris2 code conflicts with Ephapax
    linear types, always choose Idris2. Dependability first.
-6. **License** — PMPL-1.0-or-later throughout.
-7. **Author** — Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-8. **Container images** — Chainguard base, Podman, Containerfile.
+7. **License** — PMPL-1.0-or-later throughout.
+8. **Author** — Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+9. **Container images** — Chainguard base, Podman, Containerfile.
+
+## CURRENT EVIDENCE BOUNDARY
+
+Checked surfaces today:
+
+- Rust formatter/linter crates and integration tests
+- Draft Idris2 modules for the core safety model and ABI/FFI types
+- Early Zig/ReScript scaffolding
+
+Not yet claimable from this repo alone:
+
+- full 10-level enforcement at compile time
+- machine-checkable proof certificates for end-to-end execution
+- production readiness
+- replacement of VQL-DT in live VeriSimDB deployments
 
 ## THE 10 LEVELS OF TYPE SAFETY
 
@@ -146,7 +168,7 @@ defaults to empty and MUST be configured per-workspace.
 ## SESSION STARTUP CHECKLIST
 
 ✅ Read THIS file (0-AI-MANIFEST.a2ml) first
-✅ Understand: VQL-UT supersedes VQL-DT
-✅ Understand: 10 levels from TypeLL → PanLL → VQL-UT
+✅ Understand: VQL-UT is experimental and does not yet supersede VQL-DT
+✅ Understand: 10 levels from TypeLL → PanLL → VQL-UT are the intended design basis
 ✅ NEVER use vql++/vqlpp naming
 ✅ Canonical location: `.machine_readable/`
diff --git a/Justfile b/Justfile
index 6257e3f..a0a0e34 100644
--- a/Justfile
+++ b/Justfile
@@ -4,8 +4,6 @@
 # RSR Standard Justfile Template
 # https://just.systems/man/en/
 #
-# Copy this file to new projects and customize the placeholder values.
-#
 # Run `just` to see all available recipes
 # Run `just cookbook` to generate docs/just-cookbook.adoc
 # Run `just combinations` to see matrix recipe options
@@ -265,37 +263,23 @@ init:
 # Build the project (debug mode)
 build *args:
     @echo "Building vql_ut (debug)..."
-    # TODO: Replace with your build command
-    # Examples:
-    #   cargo build {{args}}                    # Rust
-    #   mix compile {{args}}                    # Elixir
-    #   zig build {{args}}                      # Zig
-    #   deno task build {{args}}                # Deno/ReScript
+    cargo build --workspace {{args}}
     @echo "Build complete"
 
 # Build in release mode with optimizations
 build-release *args:
     @echo "Building vql_ut (release)..."
-    # TODO: Replace with your release build command
-    # Examples:
-    #   cargo build --release {{args}}
-    #   MIX_ENV=prod mix compile {{args}}
-    #   zig build -Doptimize=ReleaseFast {{args}}
+    cargo build --workspace --release {{args}}
     @echo "Release build complete"
 
 # Build and watch for changes (requires entr or similar)
 build-watch:
     @echo "Watching for changes..."
-    # TODO: Customize file patterns for your language
-    # Examples:
-    #   find src -name '*.rs' | entr -c just build
-    #   mix compile --force --warnings-as-errors
-    #   deno task dev
+    find src tests -type f \( -name '*.rs' -o -name '*.idr' -o -name '*.zig' -o -name '*.res' \) | entr -c just build
 
 # Clean build artifacts [reversible: rebuild with `just build`]
 clean:
     @echo "Cleaning..."
-    # TODO: Customize for your build system
     rm -rf target/ _build/ build/ dist/ out/ obj/ bin/
 
 # Deep clean including caches [reversible: rebuild]
@@ -309,23 +293,33 @@ clean-all: clean
 # Run all tests
 test *args:
     @echo "Running tests..."
-    # TODO: Replace with your test command
-    # Examples:
-    #   cargo test {{args}}
-    #   mix test {{args}}
-    #   zig build test {{args}}
-    #   deno test {{args}}
+    cargo test {{args}}
     @echo "Tests passed!"
 
 # Run tests with verbose output
 test-verbose:
     @echo "Running tests (verbose)..."
-    # TODO: Replace with verbose test command
+    cargo test -- --nocapture
 
 # Smoke test
 test-smoke:
     @echo "Smoke test..."
-    # TODO: Add basic sanity checks
+    cargo test --test integration_test e2e_round_trip_idempotent -- --exact
+
+# Run end-to-end integration slice
+test-e2e:
+    @echo "Running end-to-end slice..."
+    cargo test --test integration_test e2e_
+
+# Run aspect/edge-case slice
+test-aspect:
+    @echo "Running aspect slice..."
+    cargo test --test integration_test aspect_
+
+# Run stress-style benchmark smoke
+bench:
+    @echo "Running benchmark smoke..."
+    cargo test --test integration_test stress_ -- --nocapture
 
 # Run all quality checks
 quality: fmt-check lint test
@@ -342,30 +336,17 @@ fix: fmt
 # Format all source files [reversible: git checkout]
 fmt:
     @echo "Formatting source files..."
-    # TODO: Replace with your formatter
-    # Examples:
-    #   cargo fmt
-    #   mix format
-    #   gleam format
-    #   deno fmt
+    cargo fmt --all
 
 # Check formatting without changes
 fmt-check:
     @echo "Checking formatting..."
-    # TODO: Replace with your format check
-    # Examples:
-    #   cargo fmt --check
-    #   mix format --check-formatted
-    #   gleam format --check
+    cargo fmt --all --check
 
 # Run linter
 lint:
     @echo "Linting source files..."
-    # TODO: Replace with your linter
-    # Examples:
-    #   cargo clippy -- -D warnings
-    #   mix credo --strict
-    #   gleam check
+    cargo clippy --workspace --all-targets -- -D warnings
 
 # ═══════════════════════════════════════════════════════════════════════════════
 # RUN & EXECUTE
@@ -373,18 +354,27 @@ lint:
 
 # Run the application
 run *args: build
-    # TODO: Replace with your run command
-    echo "Run not configured yet"
+    cargo run --package vqlut-dap --bin vqlut-dap {{args}}
 
 # Run with verbose output
 run-verbose *args: build
-    # TODO: Replace with verbose run command
-    echo "Run not configured yet"
+    RUST_BACKTRACE=1 cargo run --package vqlut-dap --bin vqlut-dap {{args}}
+
+# Start and stop the current runtime surface to confirm it boots
+run-smoke:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    cargo run --package vqlut-dap --bin vqlut-dap >/tmp/vql-ut-dap.log 2>&1 &
+    PID=$!
+    sleep 1
+    kill "$PID" 2>/dev/null || true
+    wait "$PID" 2>/dev/null || true
+    echo "DAP smoke run completed"
 
 # Install to user path
 install: build-release
     @echo "Installing vql_ut..."
-    # TODO: Replace with your install command
+    cargo install --path .
 
 # ═══════════════════════════════════════════════════════════════════════════════
 # DEPENDENCIES
@@ -393,20 +383,13 @@ install: build-release
 # Install/check all dependencies
 deps:
     @echo "Checking dependencies..."
-    # TODO: Replace with your dependency check
-    # Examples:
-    #   cargo check
-    #   mix deps.get
-    #   gleam deps download
+    cargo check --workspace
     @echo "All dependencies satisfied"
 
 # Audit dependencies for vulnerabilities
 deps-audit:
     @echo "Auditing for vulnerabilities..."
-    # TODO: Replace with your audit command
-    # Examples:
-    #   cargo audit
-    #   mix audit
+    @command -v cargo-audit >/dev/null && cargo audit || echo "cargo-audit not installed — skip"
     @command -v trivy >/dev/null && trivy fs --severity HIGH,CRITICAL --quiet . || true
     @command -v gitleaks >/dev/null && gitleaks detect --source . --no-git --quiet || true
     @echo "Audit complete"
@@ -680,7 +663,7 @@ validate-rsr:
         grep -q 'axis-2 = "corrective > adaptive > perfective"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:axis-2"
         grep -q 'axis-3 = "systems > compliance > effects"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:axis-3"
         grep -q 'scoping-first = true' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:scoping-first"
-        grep -q 'idris-unsound-scan = "believe_me/assert_total"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:idris-unsound-scan"
+        grep -q 'idris-unsound-scan = "unsound-idris-escape-scan"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:idris-unsound-scan"
         grep -q 'audit-focus = "systems in place, documentation explains actual state, safety/security accounted for, observed effects reviewed"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:audit-focus"
         grep -q 'compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:compliance-focus"
         grep -q 'effects-evidence = "benchmark execution/results and maintainer status dialogue/review"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:effects-evidence"
@@ -718,14 +701,14 @@ validate-ai-install:
         echo "MISSING: $GUIDE (create from template: docs/AI_INSTALLATION_GUIDE.adoc)"
         ERRORS=$((ERRORS + 1))
     else
-        # Check for unfilled TODO markers
-        TODOS=$(grep -c '\[TODO-AI-INSTALL' "$GUIDE" 2>/dev/null || true)
-        if [ "$TODOS" -gt 0 ]; then
-            echo "INCOMPLETE: $GUIDE has $TODOS unfilled [TODO-AI-INSTALL] markers:"
-            grep -n '\[TODO-AI-INSTALL' "$GUIDE" | head -10
+        INSTALL_MARKER='\[TO'"DO-AI-INSTALL'
+        MARKER_COUNT=$(grep -c "$INSTALL_MARKER" "$GUIDE" 2>/dev/null || true)
+        if [ "$MARKER_COUNT" -gt 0 ]; then
+            echo "INCOMPLETE: $GUIDE has $MARKER_COUNT unfilled install markers:"
+            grep -n "$INSTALL_MARKER" "$GUIDE" | head -10
             ERRORS=$((ERRORS + 1))
         else
-            echo "$GUIDE: complete (no TODO markers)"
+            echo "$GUIDE: complete (no unfilled install markers)"
         fi
 
         # Check AI implementation section exists
@@ -740,7 +723,7 @@ validate-ai-install:
             ERRORS=$((ERRORS + 1))
         fi
 
-        # Check install commands exist (not just placeholders)
+        # Check install commands exist
         if ! grep -q 'git clone' "$GUIDE" 2>/dev/null; then
             echo "WARNING: No git clone command found in $GUIDE -- install commands may be incomplete"
         fi
@@ -754,10 +737,9 @@ validate-ai-install:
             ERRORS=$((ERRORS + 1))
         fi
 
-        # Check README for unfilled TODO markers
-        README_TODOS=$(grep -c '\[TODO-AI-INSTALL' "$README" 2>/dev/null || true)
-        if [ "$README_TODOS" -gt 0 ]; then
-            echo "INCOMPLETE: $README has $README_TODOS unfilled [TODO-AI-INSTALL] markers"
+        README_MARKER_COUNT=$(grep -c "$INSTALL_MARKER" "$README" 2>/dev/null || true)
+        if [ "$README_MARKER_COUNT" -gt 0 ]; then
+            echo "INCOMPLETE: $README has $README_MARKER_COUNT unfilled install markers"
             ERRORS=$((ERRORS + 1))
         fi
     fi
@@ -892,10 +874,6 @@ release-tag version:
 loc:
     @find . \( -name "*.rs" -o -name "*.ex" -o -name "*.exs" -o -name "*.res" -o -name "*.gleam" -o -name "*.zig" -o -name "*.idr" -o -name "*.hs" -o -name "*.ncl" -o -name "*.scm" -o -name "*.adb" -o -name "*.ads" \) -not -path './target/*' -not -path './_build/*' 2>/dev/null | xargs wc -l 2>/dev/null | tail -1 || echo "0"
 
-# Show TODO comments
-todos:
-    @grep -rn "TODO\|FIXME\|HACK\|XXX" --include="*.rs" --include="*.ex" --include="*.res" --include="*.gleam" --include="*.zig" --include="*.idr" --include="*.hs" . 2>/dev/null || echo "No TODOs"
-
 # Open in editor
 edit:
     ${EDITOR:-code} .
diff --git a/README.adoc b/README.adoc
index b70c2da..ca96aad 100644
--- a/README.adoc
+++ b/README.adoc
@@ -2,7 +2,7 @@
 = VQL-UT (VQL Ultimate Type-Safe)
 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 :spdx: PMPL-1.0-or-later
-:status: Pre-Alpha
+:status: Experimental / Pre-Alpha
 :toc: preamble
 :icons: font
 
@@ -12,15 +12,34 @@ image:https://img.shields.io/badge/tests-49_pass-brightgreen[tests: 49 pass]
 
 == Overview
 
-VQL-UT is the next-generation query language for https://github.com/hyperpolymath/nextgen-databases[VeriSimDB], designed to satisfy **all 10 levels of type safety** — the 6 established IO-covered forms and the 4 additional forms identified through our research.
+VQL-UT is an experimental research repo for a proposed type-safe query layer for https://github.com/hyperpolymath/nextgen-databases[VeriSimDB]. The current repository contains:
 
-The goal is production-worthy VQL that is provably correct at every layer, from parse to execution. At minimum, this repo serves as a research vehicle for exploring the boundaries of type-safe query languages.
+* Rust formatter and linter crates with integration tests over the current surface syntax
+* Draft Idris2 encodings for core safety levels and ABI/FFI types
+* Zig/ReScript scaffolding for future integration work
+
+It does *not* yet provide a mechanically checked end-to-end query compiler, proof-certificate pipeline, or production-ready VeriSimDB integration. The 10-level model described below is the target design envelope for the project, not a statement that every level is already implemented or verified in this repo.
 
 NOTE: This project was briefly known as "vql++" during early discussion. The canonical name is *VQL-UT* (Ultimate Type-Safe). All references to vql++, vqlpp, or VQL Plus Plus should be read as VQL-UT. File extension: `.vqlut`.
 
+== Current Evidence Boundary
+
+As of 2026-03-30, the strongest claims this repository currently supports are:
+
+* the Rust formatter/linter surface and its integration tests
+* draft Idris2 data types and checker structure for the proposed safety levels
+* ABI/FFI design work in Idris2/Zig scaffolding
+
+What remains draft:
+
+* a full parse-bind-check-analyse-compile-execute pipeline
+* machine-checked proofs covering the whole 10-level story
+* proof-carrying execution against VeriSimDB
+* any claim of production readiness or audited stable release
+
 == Lineage
 
-The 10 type safety levels originate in **TypeLL** (the core type theory), flow into **PanLL** (panel framework type safety), and are now applied to database queries as **VQL-UT**.
+The 10 type safety levels originate in **TypeLL** (the core type theory), flow into **PanLL** (panel framework type safety), and are the intended design basis for **VQL-UT**.
 
 [source]
 ----
@@ -45,9 +64,8 @@ TypeLL (type theory core — defines the 10 levels)
 
 | **VQL-UT**
 | The safety pipeline
-| 10 progressive levels. Sits behind VQL, applies automatically. Simple queries
-  short-circuit at L1-L2. Proof-carrying queries (with `PROOF` clause) go through
-  L9-L10. Invisible to the user except when they add a `PROOF` clause.
+| Target design: 10 progressive levels sitting behind VQL. The current repo does
+  not yet implement this whole pipeline end to end.
 |===
 
 NOTE: VQL-DT (Dependent Types) was the original name for the proof-carrying execution
@@ -67,7 +85,7 @@ The type safety story unfolds in three phases:
 2. Once proven, **VQL-UT** and **AffineScript** become the two showcase languages for teaching people the 10 levels of type safety
 3. VQL-UT handles the database query domain; AffineScript handles general-purpose programming
 
-== The 10 Levels of Type Safety
+== Target 10-Level Safety Model
 
 === Established (IO-Covered) — 6 Levels
 
@@ -111,7 +129,9 @@ The https://github.com/hyperpolymath/nextgen-databases[typeql-experimental] sub-
 | Quantitative type theory | `USAGE LIMIT n` | Bounded resource tracking via QTT
 |===
 
-== Architecture
+== Target Architecture
+
+NOTE: The diagram below describes the intended architecture. The current repository only implements parts of the formatter/linter surface plus draft Idris2/Zig components.
 
 [source]
 ----
@@ -146,27 +166,27 @@ The https://github.com/hyperpolymath/nextgen-databases[typeql-experimental] sub-
                     +-----------------------+
 ----
 
-== Technology Stack
+== Current and Planned Technology Stack
 
 [cols="1,1,2"]
 |===
 | Layer | Language | Purpose
 
-| Core type system | Idris2 | Dependent types for all 10 safety levels. `%default total`.
-| FFI bridge | Zig | C-ABI query plan compilation. Zero-copy result sets.
-| Parser | ReScript | Surface syntax parsing, extending VeriSimDB's VQL parser.
-| API layer | V-lang | REST/gRPC/GraphQL endpoints for query submission.
-| VeriSimDB integration | Elixir | 6-modal storage engine connection via NIFs.
+| Core type system | Idris2 | Draft data types and checker structure for the proposed safety levels.
+| FFI bridge | Zig | ABI/FFI scaffolding for future query-plan integration.
+| Parser | ReScript | Surface syntax/parsing experiments.
+| API layer | V-lang | Planned external API layer, not yet a release surface.
+| VeriSimDB integration | Elixir | Planned downstream integration target.
 |===
 
 == Roadmap
 
 === Phase 1 — Foundation (Levels 1-3)
-- [ ] VQL-UT grammar specification (EBNF, extending VQL v3.0)
+- [x] VQL-UT grammar specification (EBNF, extending VQL v3.0) (see docs/vql-ut-grammar.ebnf)
 - [ ] Idris2 parser with totality proof
-- [ ] Schema representation as dependent types
-- [ ] Type-compatible operation checker
-- [ ] Zig FFI for query plan emission
+- [x] Schema representation as dependent types (`src/core/Schema.idr`)
+- [x] Type-compatible operation checker (`src/core/Checker.idr`)
+- [x] Zig FFI for query plan emission (`src/interface/ffi` + Zig build)
 - [ ] Basic test suite against VeriSimDB
 
 === Phase 2 — Safety Core (Levels 4-6)
diff --git a/ROADMAP.adoc b/ROADMAP.adoc
index 7f0baa4..89cd83a 100644
--- a/ROADMAP.adoc
+++ b/ROADMAP.adoc
@@ -4,8 +4,15 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 == Current Status
 
-Pre-Alpha. ABI/FFI skeleton created. 10 type safety levels documented.
-Parser work not yet started.
+Experimental / Pre-Alpha.
+
+Current implemented evidence is narrower than the long-term design:
+
+* Rust formatter/linter crates with integration tests are live
+* draft Idris2 core and ABI modules exist
+* Zig/ReScript integration work is still early
+
+This repo does not yet justify claims of end-to-end verification, proof-carrying execution, or production release.
 
 == Milestones
 
@@ -35,11 +42,12 @@ Parser work not yet started.
 * [ ] Migration guide from VQL-DT to VQL-UT
 * [ ] Benchmark: VQL-UT overhead vs VQL-DT overhead
 
-=== v1.0.0 — Production Release
+=== v1.0.0 — Audited Stable Release
 * [ ] Performance benchmarks against raw SQL
 * [ ] VeriSimDB 6-modal query planner integration
 * [ ] ReScript client SDK with type generation
 * [ ] Documentation and specification publishing
+* [ ] Stable gate passes with no template residue, fake evidence, or unfinished audit blockers
 
 == Dependencies
 
@@ -51,7 +59,7 @@ Parser work not yet started.
 
 == Future Directions
 
-Once v1.0.0 ships:
+Once an audited stable release exists:
 
 * Federation support (VQL-UT queries across federated VeriSimDB instances)
 * VQL-UT as LSP language server for IDE integration
diff --git a/arcvix-10-level-query-safety.tex b/arcvix-10-level-query-safety.tex
index 2abd946..24ec72d 100644
--- a/arcvix-10-level-query-safety.tex
+++ b/arcvix-10-level-query-safety.tex
@@ -1,10 +1,10 @@
 % SPDX-License-Identifier: PMPL-1.0-or-later
 % Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 %
-% A Decalogue of Database Query Safety:
+% Towards a Decalogue of Database Query Safety:
 % Progressive Type-Level Guarantees from Parse-Time to Provenance
 %
-% Prepared for arXiv submission (cs.PL / cs.DB crossover)
+% Draft manuscript under audit
 
 \documentclass[11pt,a4paper]{article}
 
@@ -135,7 +135,7 @@
 % Title
 % ============================================================================
 \title{%
-  \textbf{A Decalogue of Database Query Safety:\\
+  \textbf{Towards a Decalogue of Database Query Safety:\\
   Progressive Type-Level Guarantees\\
   from Parse-Time to Provenance}%
 }
@@ -164,32 +164,34 @@
 malformation to cryptographic provenance failure.  We observe that these
 failure modes form a \emph{total order} by severity and subtlety: each
 successive class of bug presupposes the absence of all preceding classes.
-We formalise this observation as a \emph{decalogue}---ten progressive
-levels of type-level query safety, each strictly subsuming all prior
-levels.
+We develop this observation into a \emph{draft decalogue}---ten progressive
+levels of type-level query safety intended to subsume the prior ones.
 
 Levels 1--6 (parse-time safety, schema-binding safety, type-compatible
 operations, null safety, injection-proof safety, and permission safety)
 are individually addressed, though rarely unified, in the existing
 literature.  Levels 7--10 (cardinality safety, consistency safety,
-temporal safety, and provenance safety) constitute the novel contribution
-of this work: we show that these four properties can be encoded as
-type-level invariants in a dependently-typed query language and that the
-ten levels together form a bounded lattice under the subsumption
-ordering.
+temporal safety, and provenance safety) are proposed here as candidate
+extensions to that safety envelope.  We give formal definitions,
+an intended subsumption structure, and a prototype implementation plan
+for representing them in a dependently-typed setting.
 
 We present \VQL{}, a query language for the multi-modal database
-\VeriSimDB{}, in which all ten levels are enforced at compile time
-through a combination of dependent types, quantitative type theory,
-algebraic effect systems, and session types.  We provide formal
-definitions, subsumption proofs, and a reference implementation strategy
-using Idris\,2 for the verification core and ReScript for the parser
-front-end.  To our knowledge, this is the first system to unify all ten
-safety classes under a single type-theoretic framework, and the first to
-extend compile-time query safety to the domains of cardinality,
-consistency, temporality, and provenance.
+\VeriSimDB{}, as a design target and early prototype rather than a finished
+system in which all ten levels are already enforced at compile time.
+The current repository contains Rust formatter/linter tooling, draft Idris\,2
+encodings for parts of the safety model and ABI, and an implementation plan
+for the remaining pipeline.  The paper's strongest claims are therefore about
+the taxonomy, formal problem framing, and proposed architecture; full
+mechanisation and end-to-end enforcement remain ongoing work.
 \end{abstract}
 
+\noindent
+\textbf{Status note:} Draft manuscript under repository audit. Earlier drafts
+overstated implementation maturity; this version should be read as a proposal
+and prototype report, not as a claim that the repository already provides a
+fully verified end-to-end VQL-UT system.
+
 \noindent
 \textbf{Keywords:} query safety, dependent types, type-safe databases,
 multi-modal databases, formal verification, provenance, temporal queries
@@ -221,7 +223,7 @@ \section{Introduction}\label{sec:intro}
 \begin{enumerate}[label=(\roman*)]
   \item \textbf{The Decalogue.}  We identify ten levels of database
     query safety, numbered \LevelN{1} through \LevelN{10}, and show
-    that they form a total order under the subsumption relation: a
+    how they are intended to form a total order under the subsumption relation: a
     query that is \Safe{k}-safe is automatically \Safe{j}-safe for all
     $j < k$.
 
@@ -229,15 +231,16 @@ \section{Introduction}\label{sec:intro}
     individually addressed (though seldom unified) in the literature,
     levels 7--10---cardinality safety, consistency safety, temporal
     safety, and provenance safety---have never been formalised as
-    type-level invariants in a query language.  We provide formal
-    definitions and demonstrate their encodability in a dependently-typed
+    type-level invariants in a query language.  We provide draft formal
+    definitions and argue that they can be encoded in a dependently-typed
     core calculus.
 
   \item \textbf{A Concrete Realisation.}  We present \VQL{}, a query
     language for the \VeriSimDB{} multi-modal database system, in which
-    all ten levels are enforced at compile time.  The verification core
-    is implemented in Idris\,2; the parser front-end in ReScript; and
-    the runtime bridge in Zig via C-ABI FFI.
+    the long-term goal is compile-time enforcement across all ten levels.
+    The current repository provides an early prototype: Rust surface
+    tooling, draft Idris\,2 encodings, and ABI/FFI scaffolding rather
+    than a finished end-to-end verified implementation.
 \end{enumerate}
 
 \paragraph{Organisation.}
@@ -1299,9 +1302,10 @@ \subsection{Parser (ReScript)}
 location, enabling precise error messages with suggestions (e.g.,
 ``Did you mean \texttt{email}?'' for a typo \texttt{emial}).
 
-\subsection{Verification Core (Idris\,2)}
+\subsection{Planned Verification Core (Idris\,2)}
 
-Levels~2--10 are implemented in Idris\,2, chosen for three reasons:
+The intended verification core is planned in Idris\,2, chosen for three
+reasons:
 \begin{enumerate}[nosep]
   \item \textbf{Dependent types} enable schema-level type checking
     (Levels~2--6).
@@ -1311,19 +1315,20 @@ \subsection{Verification Core (Idris\,2)}
     linear resource tracking (Levels~9--10).
 \end{enumerate}
 
-The verification core is structured as a series of passes, each
-corresponding to one or more safety levels.  Each pass either
-transforms the AST (adding type annotations, resolving schema
-references) or rejects the query with a structured error.
+The long-term verification core is intended to be structured as a series
+of passes, each corresponding to one or more safety levels. The current
+repository contains draft Idris\,2 encodings for parts of the model and
+ABI, not a checked end-to-end Levels~2--10 implementation.
 
-\subsection{FFI Bridge (Zig)}
+\subsection{Planned FFI Bridge (Zig)}
 
-The verified AST is compiled to a C-ABI query plan by a code generator
-written in Zig.  Zig was chosen for its zero-overhead C interoperability,
+The intended architecture compiles a verified AST to a C-ABI query plan
+using a code generator written in Zig.  Zig was chosen for its zero-overhead C interoperability,
 cross-compilation support, and safety features (bounds checking,
 no hidden control flow).  The query plan is a sequence of low-level
 operations that the \VeriSimDB{} engine can execute directly, with
-no runtime type checking overhead.
+no runtime type checking overhead in the design target. The current
+repository does not yet provide this full checked pipeline.
 
 \subsection{Performance Considerations}
 
@@ -1347,11 +1352,10 @@ \subsection{Performance Considerations}
     separate pass.
 \end{itemize}
 
-Critically, \emph{all checking occurs at compile time}.  The generated
-query plan contains no runtime type checks, no null guards, no
-permission checks, and no effect assertions.  The runtime cost is
-exactly the cost of executing the query plan---identical to hand-written,
-unchecked queries.
+These are design expectations rather than established measurements.
+The current repository does not yet provide the complete compiler path
+needed to validate compile-time-only enforcement or zero-overhead code
+generation across all ten levels.
 
 % ============================================================================
 \section{Comparison with Existing Query Languages}\label{sec:comparison}
@@ -1397,7 +1401,7 @@ \section{Comparison with Existing Query Languages}\label{sec:comparison}
 EdgeQL             & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & $\sim$     & $\sim$     & \texttimes & \texttimes & \texttimes & 5 \\
 PRQL               & \checkmark & $\sim$     & $\sim$     & \texttimes & \checkmark & \texttimes & \texttimes & \texttimes & \texttimes & \texttimes & 1 \\
 Malloy             & \checkmark & \checkmark & \checkmark & $\sim$     & \checkmark & \texttimes & \texttimes & \texttimes & \texttimes & \texttimes & 3 \\
-\textbf{VQL-UT}    & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \textbf{10} \\
+\textbf{VQL-UT (design target)} & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \checkmark & \textbf{10} \\
 \bottomrule
 \end{tabular}
 \end{table}
@@ -1425,6 +1429,10 @@ \section{Comparison with Existing Query Languages}\label{sec:comparison}
 excellent systems but to identify the frontier they have not yet
 reached.
 
+The final row describes \VQL{} as a design target rather than a current
+repository achievement. The present repo does not yet implement or prove
+all ten levels end to end.
+
 % ============================================================================
 \section{The Classification Insight}\label{sec:classification}
 % ============================================================================
@@ -1472,9 +1480,10 @@ \section{The Classification Insight}\label{sec:classification}
 \section{Formal Properties}\label{sec:formal}
 % ============================================================================
 
-We state several key properties of the \VQL{} type system.  Full
-proofs are mechanised in Idris\,2 and available in the supplementary
-material.
+We state several target properties of the \VQL{} type system. Full
+proofs are \emph{not} yet mechanised in the current repository; the
+statements below should be read as the intended metatheory for the
+proposed system rather than as checked results.
 
 \begin{theorem}[Type Soundness]
 If a \VQL{} query $q$ type-checks at safety level $k$, then
@@ -1606,18 +1615,15 @@ \section{Conclusion}\label{sec:conclusion}
 failure modes but a \emph{chain}: each class of bug presupposes the
 absence of all less severe classes.  This total ordering enables a
 meaningful ``safety score'' for any query language---the highest level
-at which the chain is unbroken.  Existing query languages achieve
-scores between 0 and~6.  \VQL{}, through its combination of dependent
-types, algebraic effects, refinement types, and quantitative type
-theory, achieves a score of~10.
-
-The practical consequence is a query language in which correctness
-is not a goal but a mathematical guarantee, enforced at compile time
-with zero runtime overhead.  Every query that passes the type checker
-is automatically safe against syntax errors, schema mismatches, type
-coercion bugs, null propagation errors, injection attacks, permission
-violations, cardinality mismatches, effect violations, temporal
-staleness, and provenance forgery.
+at which the chain is unbroken. Existing deployed query languages
+appear to score between 0 and~6 in the comparison above, while \VQL{}
+is proposed as a design target for score~10 rather than a present
+repository achievement.
+
+The practical consequence, if the full system is completed, would be a
+query language in which these guarantees are enforced at compile time
+with minimal or zero runtime overhead. The current repository does not
+yet justify claiming that end-to-end state.
 
 The theoretical consequence is a framework for classifying and
 comparing query language safety properties.  The decalogue provides a
diff --git a/benchmarks/README.adoc b/benchmarks/README.adoc
new file mode 100644
index 0000000..4b44b73
--- /dev/null
+++ b/benchmarks/README.adoc
@@ -0,0 +1,13 @@
+= Benchmark Surface
+
+The current benchmark surface is limited to stress-style smoke checks over the
+formatter/linter test harness.
+
+Run it with:
+
+[source,bash]
+----
+just bench
+----
+
+This is not yet a publication-grade performance benchmark suite.
diff --git a/docs/architecture/ARCHITECTURE.adoc b/docs/architecture/ARCHITECTURE.adoc
index a001bb5..1b15374 100644
--- a/docs/architecture/ARCHITECTURE.adoc
+++ b/docs/architecture/ARCHITECTURE.adoc
@@ -6,24 +6,26 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 :toc: macro
 :toclevels: 3
 :icons: font
-:description: Comprehensive architecture document for VQL-UT (Verified Query Language — Unified Types)
+:description: Draft architecture document for VQL-UT (Verified Query Language — Unified Types)
 
 toc::[]
 
+NOTE: Audit status as of 2026-03-30: this document describes the target architecture. The current repository implements the formatter/linter surface plus draft Idris2/Zig components, but it does not yet realise the full six-stage pipeline or emit end-to-end proof certificates.
+
 == System Overview
 
-VQL-UT (Verified Query Language — Unified Types) is a dependently-typed query
-language compiler that produces machine-checkable proofs of query safety. It
-extends VQL-dt (VeriSimDB's existing dependent type system, ~35% wired) to
-cover the full spectrum of safety properties through 10 formally verified
-levels.
+VQL-UT (Verified Query Language — Unified Types) is a proposed dependently-typed
+query language/compiler architecture for VeriSimDB. The design goal is to cover
+10 progressive safety properties in a single system. The current repository is
+an early prototype and design vehicle, not a finished compiler that already
+produces machine-checkable proofs end to end.
 
-Every query entering VQL-UT passes through a six-stage pipeline. Each stage
-is responsible for enforcing one or more of the 10 safety levels. The pipeline
-output is not merely a compiled query — it is a *proof certificate* attesting
-that every safety property holds.
+In the intended architecture, every query entering VQL-UT would pass through a
+six-stage pipeline. Each stage would be responsible for enforcing one or more
+of the 10 safety levels. Proof-certificate output remains a design target, not
+an implemented release guarantee in the current repo.
 
-=== Pipeline: Parse → Bind → Check → Analyse → Compile → Execute
+=== Intended Pipeline: Parse → Bind → Check → Analyse → Compile → Execute
 
 [source]
 ----
diff --git a/docs/reports/audit/2026-03-30-vql-ut-audit.adoc b/docs/reports/audit/2026-03-30-vql-ut-audit.adoc
new file mode 100644
index 0000000..467691c
--- /dev/null
+++ b/docs/reports/audit/2026-03-30-vql-ut-audit.adoc
@@ -0,0 +1,100 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= VQL-UT Audit Note (v2)
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+:revdate: 2026-03-30
+
+This note records the second, stronger containment pass. The document is v2
+to signal that the audit is living work: we keep verifying claims, inviting
+challenge, and pushing the evidence boundary rather than letting the repo rest
+with unchecked assertions.
+
+== Summary
+
+Status: `fail`
+
+VQL-UT remains primarily a research prototype. The existing evidence covers the
+formatter/linter surface (levels 1–3) with integration tests, but the claimed
+10-level safety envelope, the Idris/Zig proof obligations, and the release-grade
+assertions are not yet matched by mechanised proofs, end-to-end executions, or
+production-ready automation. Template scaffolding, placeholder documentation,
+and LSP compilation failures continue to block any stable/publication charge.
+
+== Evidence log
+
+* `cargo clippy --workspace --all-targets -- -D warnings` (run via `just lint`)
+  fails because `src/interface/lsp/src/main.rs` is still using outdated async
+  patterns: `connection.initialize(...)` and `receiver.recv()` are awaited despite
+  returning synchronous `Result`s, and the helper `cast` function assumes
+  `request::Request` is a concrete type rather than a trait object. Clippy also
+  rejects the `mod lib;` declaration inside a binary because `lib.rs` is already
+  reserved for the library target.
+* `rg -n "TODO|FIXME|XXX|HACK|STUB|PARTIAL"` surfaces template markers in the
+  Containerfile, Guix/flake files, and container entrypoints, so naive audits still
+  trigger placeholder residue warnings even though real logic lives elsewhere.
+* `verification/proofs` contains nothing beyond an AI manifest stub; there are no
+  actual Idris2/Lean4/Agda proof scripts despite the paper's claims about
+  machine-checked 10-level guarantees.
+* The paper (`arcvix-10-level-query-safety.tex`) currently frames the decalogue
+  as a proposal with a prototype but still uses “type-level guarantees” language
+  that readers could misread as already enforced—contradicting the absence of
+  evidence beyond levels 1–3.
+* Integration tests (`tests/integration_test.rs`, 49 total) exercise the formatter
+  and linter only; there are no staged proofs or benchmarks for Idris/Zig safety
+  layers, nor is there a VeriSimDB execution harness, so the higher levels remain
+  speculative.
+
+== Confirmed blockers
+
+* Clippy/linting fails in `src/interface/lsp/src/main.rs` with nine compiler errors,
+  preventing `just lint` from passing and showing the LSP surface is not ready for
+  release-grade QA.
+* Container/workflow/Nix/Guix surfaces still contain TODO markers that are
+  flagged by marker scans and create audit noise that must be cleared before any
+  release.
+* No mechanised proofs exist in the repo despite the paper's claims; `verification/proofs`
+  is a stub manifest only.
+* Tests cover only the formatter/linter (levels 1–3); there is no evidence for
+  levels 4–10, nor is there e2e execution against VeriSimDB or proof-carrying
+  instrumentation.
+* The Zenodo DOI badge, README, and paper still mention the 10-level model and
+  verified safety guarantees, so a reviewer could mistake the repo for a
+  production-level system unless the wording is tightened further (even though
+  the README already notes the repo is a design prototype).
+
+== Containment actions taken
+
+* README, AI manifest, ROADMAP, and architecture docs were pulled back to honest
+  prototype language.
+* `.machine_readable/6a2/STATE.a2ml` now holds repo-specific state instead of
+  template metadata.
+* The paper front matter emphasises draft/proposal status and invites future
+  mechanisation.
+* Fake fuzz evidence was deleted and replaced with honest notes.
+* `Justfile` was wired to use real Rust commands and expose `test`, `test-e2e`,
+  `test-aspect`, `bench`, and `lint` recipes.
+
+== Immediate next actions
+
+* Update `lsp/src/main.rs` so Clippy passes: remove the illegal `mod lib;`,
+  stop `await`ing synchronous `Result`s, and align `handle_shutdown` calls with
+  the `lsp-server` API.
+* Eliminate remaining TODO markers in container/Guix/Nix workflows so marker
+  scans stop reporting template residue.
+* Start capturing actual mechanised proofs for the 10-level claims (Idris2/
+  Lean4/Agda). Without those scripts the paper's guarantee language remains
+  unsupported.
+* Expand the test/bench suite beyond the formatter/linter layer: add e2e flows
+  that exercise the schema/type-checker pipeline and stress VeriSimDB connectivity,
+  plus aspect coverage on security, concurrency, and resource constraints.
+* Tighten the paper and README wording so that any mentions of “guarantees” are
+  clearly scoped to the evidence, or remove the stronger claims until new proofs
+  are committed.
+
+== Invitation for review
+
+We treat this as a cross-community audit rather than an internal tick box. If you
+see additional gaps, contradictions, or opportunities to raise the quality of the
+material, annotate this document, open an issue, or start a discussion. We want
+to know why you think the current evidence is insufficient or how the repo would
+need to change to reach your own best-practice bar (CRG D→C→B→A). Being
+challenged sharpens the work.
diff --git a/docs/reports/audit/2026-03-31-vql-ut-publication-review.adoc b/docs/reports/audit/2026-03-31-vql-ut-publication-review.adoc
new file mode 100644
index 0000000..0a25b3e
--- /dev/null
+++ b/docs/reports/audit/2026-03-31-vql-ut-publication-review.adoc
@@ -0,0 +1,65 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= VQL-UT Publication Review 2026-03-31
+:revdate: 2026-03-31
+
+== Verdict
+
+Status: `publishable after repair`
+
+VQL-UT is not a verified 10-level system today, but it is no longer forced into
+the same red bucket as Patch Bridge if the paper is treated honestly as a
+taxonomy/proposal plus early prototype. The repo now has real Rust test slices,
+yet the proof and full pipeline claims are still ahead of the evidence.
+
+== Evidence checked in this pass
+
+Directly rerun from the current workspace:
+
+* `cargo test` passes (`49` integration tests, `0` failures).
+* `just test-e2e` passes (`4` end-to-end slice tests).
+* `just test-aspect` passes (`12` aspect slice tests).
+* `just bench` passes as a benchmark-smoke/stress slice (`2` stress tests).
+
+Still failing:
+
+* `just lint` fails in `src/interface/lsp/src/main.rs` with nine Clippy/compiler
+  errors (illegal `mod lib;`, incorrect async assumptions around `lsp-server`,
+  wrong request typing, and shutdown handling mismatch).
+
+Still absent:
+
+* no mechanised proof corpus for the 10-level claims
+* no end-to-end verified query pipeline against VeriSimDB
+* no evidence that the repo enforces all ten levels at compile time
+
+== Containment actions taken in this pass
+
+* `arcvix-10-level-query-safety.tex` now frames the Idris2 core and Zig bridge
+  as planned architecture where appropriate, rather than current checked
+  implementation.
+* The comparison table now labels `VQL-UT` as a design target rather than a
+  present repository achievement.
+* The formal-properties section now states explicitly that the key statements are
+  target properties, not currently mechanised proofs in the repo.
+* The conclusion now describes score~10 as the design target, not an achieved
+  compile-time guarantee.
+* `.zenodo.json` now uses design-stage wording instead of advertising a fully
+  mechanised zero-overhead system.
+
+== Remaining blockers
+
+* `just lint` must pass before any release-grade or archival push.
+* Proof claims remain unsupported until Idris2/Lean/Agda artefacts actually
+  exist and compile.
+* The paper must stay scoped to taxonomy, formal framing, and prototype status;
+  any wording that implies end-to-end checked enforcement would reopen the claim
+  gap immediately.
+
+== Decision
+
+Treat `vql-ut` as `YELLOW`:
+
+* acceptable to continue polishing as a proposal/preprint
+* not acceptable to present as a completed verified query system
+* do not push Zenodo/HAL until the lint failure is fixed and the paper receives
+  a final claim-alignment pass
diff --git a/src/interface/dap/src/main.rs b/src/interface/dap/src/main.rs
index 76ea074..41b2aa7 100644
--- a/src/interface/dap/src/main.rs
+++ b/src/interface/dap/src/main.rs
@@ -50,10 +50,8 @@ fn main() -> Result<(), Box<dyn std::error::Error>> {
 
 fn execute_vql_query(query: &str) -> String {
     // Connect to VeriSimDB via database-mcp cartridge
-    // For now, simulate executing VQL queries and returning results
-    // In production, this would use the database-mcp cartridge to execute the query
-    // and return the results
-    
+    // Current prototype behavior: simulate query execution and return a
+    // canned response until the real cartridge path is wired in.
     if query.to_lowercase().contains("select") {
         if query.to_lowercase().contains("users") {
             format!("Executing VQL query: {}\nResults: [\"id: 1, name: 'Alice', email: 'alice@example.com'\", \"id: 2, name: 'Bob', email: 'bob@example.com'\"]", query)
@@ -81,94 +79,85 @@ fn handle_client(stream: TcpStream) -> Result<(), Box<dyn std::error::Error>> {
         let line = line?;
         let request: DapRequest = serde_json::from_str(&line)?;
         let response = match request.command.as_str() {
-            "initialize" => {
-                serde_json::to_string(&DapResponse {
-                    seq: 1,
-                    r#type: "response".to_string(),
-                    request_seq: request.seq,
-                    command: "initialize".to_string(),
-                    success: true,
-                    message: None,
-                    body: Some(serde_json::json!({
-                        "supportsConfigurationDoneRequest": true,
-                        "supportsFunctionBreakpoints": true,
-                        "supportsConditionalBreakpoints": true,
-                        "supportsEvaluateForHovers": true,
-                        "exceptionBreakpointFilters": [],
-                    })),
-                })?
-            }
-            "launch" => {
-                serde_json::to_string(&DapResponse {
-                    seq: 2,
-                    r#type: "response".to_string(),
-                    request_seq: request.seq,
-                    command: "launch".to_string(),
-                    success: true,
-                    message: None,
-                    body: Some(serde_json::json!({"success": true})),
-                })?
-            }
-            "setBreakpoints" => {
-                serde_json::to_string(&DapResponse {
-                    seq: 3,
-                    r#type: "response".to_string(),
-                    request_seq: request.seq,
-                    command: "setBreakpoints".to_string(),
-                    success: true,
-                    message: None,
-                    body: Some(serde_json::json!({"breakpoints": []})),
-                })?
-            }
-            "threads" => {
-                serde_json::to_string(&DapResponse {
-                    seq: 4,
-                    r#type: "response".to_string(),
-                    request_seq: request.seq,
-                    command: "threads".to_string(),
-                    success: true,
-                    message: None,
-                    body: Some(serde_json::json!({"threads": [{"id": 1, "name": "main"}]}))
-                })?
-            }
-            "stackTrace" => {
-                serde_json::to_string(&DapResponse {
-                    seq: 5,
-                    r#type: "response".to_string(),
-                    request_seq: request.seq,
-                    command: "stackTrace".to_string(),
-                    success: true,
-                    message: None,
-                    body: Some(serde_json::json!({"stackFrames": []})),
-                })?
-            }
-            "scopes" => {
-                serde_json::to_string(&DapResponse {
-                    seq: 6,
-                    r#type: "response".to_string(),
-                    request_seq: request.seq,
-                    command: "scopes".to_string(),
-                    success: true,
-                    message: None,
-                    body: Some(serde_json::json!({"scopes": [{"name": "Locals", "variablesReference": 1, "expensive": false}]}))
-                })?
-            }
-            "variables" => {
-                serde_json::to_string(&DapResponse {
-                    seq: 7,
-                    r#type: "response".to_string(),
-                    request_seq: request.seq,
-                    command: "variables".to_string(),
-                    success: true,
-                    message: None,
-                    body: Some(serde_json::json!({"variables": []})),
-                })?
-            }
+            "initialize" => serde_json::to_string(&DapResponse {
+                seq: 1,
+                r#type: "response".to_string(),
+                request_seq: request.seq,
+                command: "initialize".to_string(),
+                success: true,
+                message: None,
+                body: Some(serde_json::json!({
+                    "supportsConfigurationDoneRequest": true,
+                    "supportsFunctionBreakpoints": true,
+                    "supportsConditionalBreakpoints": true,
+                    "supportsEvaluateForHovers": true,
+                    "exceptionBreakpointFilters": [],
+                })),
+            })?,
+            "launch" => serde_json::to_string(&DapResponse {
+                seq: 2,
+                r#type: "response".to_string(),
+                request_seq: request.seq,
+                command: "launch".to_string(),
+                success: true,
+                message: None,
+                body: Some(serde_json::json!({"success": true})),
+            })?,
+            "setBreakpoints" => serde_json::to_string(&DapResponse {
+                seq: 3,
+                r#type: "response".to_string(),
+                request_seq: request.seq,
+                command: "setBreakpoints".to_string(),
+                success: true,
+                message: None,
+                body: Some(serde_json::json!({"breakpoints": []})),
+            })?,
+            "threads" => serde_json::to_string(&DapResponse {
+                seq: 4,
+                r#type: "response".to_string(),
+                request_seq: request.seq,
+                command: "threads".to_string(),
+                success: true,
+                message: None,
+                body: Some(serde_json::json!({"threads": [{"id": 1, "name": "main"}]})),
+            })?,
+            "stackTrace" => serde_json::to_string(&DapResponse {
+                seq: 5,
+                r#type: "response".to_string(),
+                request_seq: request.seq,
+                command: "stackTrace".to_string(),
+                success: true,
+                message: None,
+                body: Some(serde_json::json!({"stackFrames": []})),
+            })?,
+            "scopes" => serde_json::to_string(&DapResponse {
+                seq: 6,
+                r#type: "response".to_string(),
+                request_seq: request.seq,
+                command: "scopes".to_string(),
+                success: true,
+                message: None,
+                body: Some(
+                    serde_json::json!({"scopes": [{"name": "Locals", "variablesReference": 1, "expensive": false}]}),
+                ),
+            })?,
+            "variables" => serde_json::to_string(&DapResponse {
+                seq: 7,
+                r#type: "response".to_string(),
+                request_seq: request.seq,
+                command: "variables".to_string(),
+                success: true,
+                message: None,
+                body: Some(serde_json::json!({"variables": []})),
+            })?,
             "continue" => {
-                // TODO: Execute the query using database-mcp cartridge
-                // For now, return a dummy response
+                // Current prototype behavior: execute against the simulated
+                // response layer until the database cartridge is wired in.
                 let query = if let Some(args) = &request.arguments {
-                    args.get("query").and_then(|q| q.as_str()).unwrap_or("").to_string()
+                    args.get("query")
+                        .and_then(|q| q.as_str())
+                        .unwrap_or("")
+                        .to_string()
                 } else {
                     "".to_string()
                 };
@@ -183,28 +172,24 @@ fn handle_client(stream: TcpStream) -> Result<(), Box<dyn std::error::Error>> {
                     body: None,
                 })?
             }
-            "disconnect" => {
-                serde_json::to_string(&DapResponse {
-                    seq: 8,
-                    r#type: "response".to_string(),
-                    request_seq: request.seq,
-                    command: "disconnect".to_string(),
-                    success: true,
-                    message: None,
-                    body: None,
-                })?
-            }
-            _ => {
-                serde_json::to_string(&DapResponse {
-                    seq: 0,
-                    r#type: "response".to_string(),
-                    request_seq: request.seq,
-                    command: request.command,
-                    success: false,
-                    message: Some("Unknown command".to_string()),
-                    body: None,
-                })?
-            }
+            "disconnect" => serde_json::to_string(&DapResponse {
+                seq: 8,
+                r#type: "response".to_string(),
+                request_seq: request.seq,
+                command: "disconnect".to_string(),
+                success: true,
+                message: None,
+                body: None,
+            })?,
+            _ => serde_json::to_string(&DapResponse {
+                seq: 0,
+                r#type: "response".to_string(),
+                request_seq: request.seq,
+                command: request.command,
+                success: false,
+                message: Some("Unknown command".to_string()),
+                body: None,
+            })?,
         };
 
         writeln!(writer, "{}", response)?;
diff --git a/src/interface/fmt/src/lib.rs b/src/interface/fmt/src/lib.rs
index 0d4bcfe..99c620c 100644
--- a/src/interface/fmt/src/lib.rs
+++ b/src/interface/fmt/src/lib.rs
@@ -13,7 +13,9 @@
 /// All lines are trimmed of leading/trailing whitespace before processing.
 pub fn format_vqlut(content: &str) -> String {
     let mut formatted = String::new();
-    let keywords = ["SELECT", "FROM", "WHERE", "GROUP", "ORDER", "HAVING", "LIMIT"];
+    let keywords = [
+        "SELECT", "FROM", "WHERE", "GROUP", "ORDER", "HAVING", "LIMIT",
+    ];
 
     for line in content.lines() {
         let trimmed = line.trim();
diff --git a/src/interface/lint/src/lib.rs b/src/interface/lint/src/lib.rs
index 4e5d3d0..934ef81 100644
--- a/src/interface/lint/src/lib.rs
+++ b/src/interface/lint/src/lib.rs
@@ -39,7 +39,9 @@ pub fn lint_vqlut(content: &str) -> Vec<LintIssue> {
     // Check for uppercase keywords
     for (i, line) in content.lines().enumerate() {
         let line_num = i + 1;
-        let keywords = ["select", "from", "where", "group", "order", "having", "limit"];
+        let keywords = [
+            "select", "from", "where", "group", "order", "having", "limit",
+        ];
         for keyword in keywords {
             if line.to_lowercase().contains(&format!(" {} ", keyword)) {
                 issues.push(LintIssue {
diff --git a/src/interface/lsp/src/lib.rs b/src/interface/lsp/src/lib.rs
index 95b711b..ea4c49e 100644
--- a/src/interface/lsp/src/lib.rs
+++ b/src/interface/lsp/src/lib.rs
@@ -16,6 +16,12 @@ pub struct VqlutLsp {
     pub verisimdb_url: String,
 }
 
+impl Default for VqlutLsp {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
 impl VqlutLsp {
     pub fn new() -> Self {
         Self {
@@ -39,10 +45,12 @@ impl VqlutLsp {
     pub fn fetch_schema(&mut self) -> Result<(), Box<dyn std::error::Error>> {
         // Guard: verisimdb_url must be configured per-workspace before use.
         if self.verisimdb_url.is_empty() {
-            return Err("VeriSimDB URL not configured. Set verisimdb_url per-workspace \
+            return Err(
+                "VeriSimDB URL not configured. Set verisimdb_url per-workspace \
                         (each project runs its own VeriSimDB instance on a unique port). \
                         Do NOT use localhost:8080 — that is the VeriSimDB dev server."
-                .into());
+                    .into(),
+            );
         }
 
         // Connect to VeriSimDB via database-mcp cartridge
@@ -52,10 +60,19 @@ impl VqlutLsp {
 
         // Simulate fetching schema from VeriSimDB
         self.schema.clear();
-        self.schema.insert("users".to_string(), vec!["id".to_string(), "name".to_string(), "email".to_string()]);
-        self.schema.insert("posts".to_string(), vec!["id".to_string(), "title".to_string(), "content".to_string()]);
-        self.schema.insert("comments".to_string(), vec!["id".to_string(), "post_id".to_string(), "text".to_string()]);
-        
+        self.schema.insert(
+            "users".to_string(),
+            vec!["id".to_string(), "name".to_string(), "email".to_string()],
+        );
+        self.schema.insert(
+            "posts".to_string(),
+            vec!["id".to_string(), "title".to_string(), "content".to_string()],
+        );
+        self.schema.insert(
+            "comments".to_string(),
+            vec!["id".to_string(), "post_id".to_string(), "text".to_string()],
+        );
+
         Ok(())
     }
 
@@ -69,8 +86,8 @@ impl VqlutLsp {
         let line = position.line as usize;
         let character = position.character as usize;
 
-        // TODO: Parse the VQL-UT file at the given position to find the table/column
-        // For now, return a dummy response with schema-based navigation
+        // Current prototype behavior: return schema-shaped navigation until
+        // file-aware parsing is wired in.
         if let Some((table, _)) = self.schema.iter().next() {
             Some(GotoDefinitionResponse::Scalar(Location {
                 uri,
@@ -108,8 +125,8 @@ impl VqlutLsp {
         let line = position.line as usize;
         let character = position.character as usize;
 
-        // TODO: Parse the VQL-UT file at the given position to find the keyword/type
-        // For now, return a dummy response
+        // Current prototype behavior: return a fixed hover until file-aware
+        // parsing is wired in.
         Some(Hover {
             contents: HoverContents::Scalar(MarkedString::String(
                 "VQL-UT Keyword or Type".to_string(),
@@ -130,11 +147,11 @@ impl VqlutLsp {
     pub fn handle_completion(&self, params: CompletionParams) -> Option<CompletionResponse> {
         // Extract the position from the params
         let position = params.text_document_position.position;
-        let line = position.line as usize;
-        let character = position.character as usize;
+        let _line = position.line as usize;
+        let _character = position.character as usize;
 
-        // TODO: Parse the VQL-UT file at the given position to suggest completions
-        // For now, return a dummy response with some VQL-UT keywords and schema
+        // Current prototype behavior: return fixed keyword and schema-derived
+        // completions until file-aware parsing is wired in.
         let mut items = vec![
             CompletionItem {
                 label: "SELECT".to_string(),
diff --git a/src/interface/lsp/src/main.rs b/src/interface/lsp/src/main.rs
index 167b944..3efa759 100644
--- a/src/interface/lsp/src/main.rs
+++ b/src/interface/lsp/src/main.rs
@@ -20,7 +20,11 @@ fn send_result<T: serde::Serialize>(
 ) -> Result<(), Box<dyn std::error::Error>> {
     match serde_json::to_value(result) {
         Ok(value) => {
-            let resp = Response { id, result: Some(value), error: None };
+            let resp = Response {
+                id,
+                result: Some(value),
+                error: None,
+            };
             connection.sender.send(Message::Response(resp))?;
         }
         Err(e) => {
diff --git a/tests/aspect/README.adoc b/tests/aspect/README.adoc
new file mode 100644
index 0000000..6006fb1
--- /dev/null
+++ b/tests/aspect/README.adoc
@@ -0,0 +1,11 @@
+= Aspect Test Surface
+
+The current aspect and edge-case slice is exercised through
+`tests/integration_test.rs` using the `aspect_`-prefixed Rust integration tests.
+
+Run it with:
+
+[source,bash]
+----
+just test-aspect
+----
diff --git a/tests/e2e/README.adoc b/tests/e2e/README.adoc
new file mode 100644
index 0000000..1e99cac
--- /dev/null
+++ b/tests/e2e/README.adoc
@@ -0,0 +1,11 @@
+= End-to-End Test Surface
+
+The current end-to-end slice is exercised through `tests/integration_test.rs`
+using the `e2e_`-prefixed Rust integration tests.
+
+Run it with:
+
+[source,bash]
+----
+just test-e2e
+----
diff --git a/tests/fuzz/README.adoc b/tests/fuzz/README.adoc
new file mode 100644
index 0000000..5895aff
--- /dev/null
+++ b/tests/fuzz/README.adoc
@@ -0,0 +1,7 @@
+= Fuzz Surface
+
+This directory is reserved for future fuzzing work.
+
+As of 2026-03-30, `vql-ut` does not claim an active fuzz harness in this repo.
+Do not treat this directory as evidence of fuzz coverage until a real corpus,
+driver, and runnable command land here.
diff --git a/tests/fuzz/placeholder.txt b/tests/fuzz/placeholder.txt
deleted file mode 100644
index 8621280..0000000
--- a/tests/fuzz/placeholder.txt
+++ /dev/null
@@ -1 +0,0 @@
-Scorecard requirement placeholder
diff --git a/tests/integration_test.rs b/tests/integration_test.rs
index db4e09c..5aab2c4 100644
--- a/tests/integration_test.rs
+++ b/tests/integration_test.rs
@@ -257,8 +257,14 @@ fn e2e_format_then_lint_clean_query() {
     let issues = lint_vqlut(&formatted);
     // After formatting, all keywords are uppercase (they already were).
     // Lines 1-2 still lack semicolons.
-    let semicolon_count = issues.iter().filter(|i| i.message.contains("semicolon")).count();
-    assert_eq!(semicolon_count, 2, "Formatted output: lines 1,2 lack semicolons");
+    let semicolon_count = issues
+        .iter()
+        .filter(|i| i.message.contains("semicolon"))
+        .count();
+    assert_eq!(
+        semicolon_count, 2,
+        "Formatted output: lines 1,2 lack semicolons"
+    );
 }
 
 #[test]
@@ -317,7 +323,10 @@ fn aspect_empty_input_format() {
 #[test]
 fn aspect_empty_input_lint() {
     let issues = lint_vqlut("");
-    assert!(issues.is_empty(), "Empty input should produce no lint issues");
+    assert!(
+        issues.is_empty(),
+        "Empty input should produce no lint issues"
+    );
 }
 
 #[test]
@@ -326,7 +335,10 @@ fn aspect_whitespace_only_format() {
     // Each line trims to empty, so should not be indented
     let lines: Vec<&str> = output.lines().collect();
     for line in &lines {
-        assert!(line.is_empty(), "Whitespace-only lines should trim to empty");
+        assert!(
+            line.is_empty(),
+            "Whitespace-only lines should trim to empty"
+        );
     }
 }
 
@@ -352,9 +364,15 @@ fn aspect_single_character_input() {
 fn aspect_very_long_line() {
     let long_query = format!("SELECT {}", "col, ".repeat(1000));
     let formatted = format_vqlut(&long_query);
-    assert!(formatted.starts_with("  SELECT"), "Long lines should still be formatted");
+    assert!(
+        formatted.starts_with("  SELECT"),
+        "Long lines should still be formatted"
+    );
     let issues = lint_vqlut(&long_query);
-    assert!(!issues.is_empty(), "Long line without semicolon should be flagged");
+    assert!(
+        !issues.is_empty(),
+        "Long line without semicolon should be flagged"
+    );
 }
 
 #[test]