From 47a1c1914e3c09fd295a5036cadc87bd03f29ede Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 24 Aug 2026 08:51:15 +0100
Subject: [PATCH] refactor: migrate repository documentation from Markdown to
 AsciiDoc

---
 ARCHITECTURE.adoc                    |  48 ++++++++
 ARCHITECTURE.md                      |  47 --------
 CHANGELOG.adoc                       | 169 +++++++++++++++++++++++++++
 CHANGELOG.md                         | 161 -------------------------
 CODE_OF_CONDUCT.adoc                 |  24 ++++
 CODE_OF_CONDUCT.md                   |  27 -----
 CONTRIBUTING.adoc                    |  71 +++++++++++
 CONTRIBUTING.md                      |  66 -----------
 GOVERNANCE.adoc                      |  60 ++++++++++
 GOVERNANCE.md                        |  60 ----------
 README.adoc.invariants.adoc          |  28 +++++
 README.adoc.invariants.md            |  26 -----
 SECURITY.adoc                        |  16 +++
 SECURITY.md                          |  20 ----
 docs/onboarding/llm-warmup-dev.adoc  |  19 +++
 docs/onboarding/llm-warmup-dev.md    |  16 ---
 docs/onboarding/llm-warmup-user.adoc |  19 +++
 docs/onboarding/llm-warmup-user.md   |  16 ---
 docs/proof-debt.adoc                 |  58 +++++++++
 docs/proof-debt.md                   |  57 ---------
 docs/status/PROOF-NEEDS.adoc         | 145 +++++++++++++++++++++++
 docs/status/PROOF-NEEDS.md           |  83 -------------
 docs/status/TEST-NEEDS.adoc          |  86 ++++++++++++++
 docs/status/TEST-NEEDS.md            |  61 ----------
 docs/tech-debt-2026-05-26.adoc       |  80 +++++++++++++
 docs/tech-debt-2026-05-26.md         |  71 -----------
 26 files changed, 823 insertions(+), 711 deletions(-)
 create mode 100644 ARCHITECTURE.adoc
 delete mode 100644 ARCHITECTURE.md
 create mode 100644 CHANGELOG.adoc
 delete mode 100644 CHANGELOG.md
 create mode 100644 CODE_OF_CONDUCT.adoc
 delete mode 100644 CODE_OF_CONDUCT.md
 create mode 100644 CONTRIBUTING.adoc
 delete mode 100644 CONTRIBUTING.md
 create mode 100644 GOVERNANCE.adoc
 delete mode 100644 GOVERNANCE.md
 create mode 100644 README.adoc.invariants.adoc
 delete mode 100644 README.adoc.invariants.md
 create mode 100644 SECURITY.adoc
 delete mode 100644 SECURITY.md
 create mode 100644 docs/onboarding/llm-warmup-dev.adoc
 delete mode 100644 docs/onboarding/llm-warmup-dev.md
 create mode 100644 docs/onboarding/llm-warmup-user.adoc
 delete mode 100644 docs/onboarding/llm-warmup-user.md
 create mode 100644 docs/proof-debt.adoc
 delete mode 100644 docs/proof-debt.md
 create mode 100644 docs/status/PROOF-NEEDS.adoc
 delete mode 100644 docs/status/PROOF-NEEDS.md
 create mode 100644 docs/status/TEST-NEEDS.adoc
 delete mode 100644 docs/status/TEST-NEEDS.md
 create mode 100644 docs/tech-debt-2026-05-26.adoc
 delete mode 100644 docs/tech-debt-2026-05-26.md

diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc
new file mode 100644
index 0000000..1c0a7a6
--- /dev/null
+++ b/ARCHITECTURE.adoc
@@ -0,0 +1,48 @@
+== Architecture
+
+=== Overview
+
+This repository follows a modular, maintainable architecture designed
+for clarity, scalability, and long-term sustainability.
+
+=== Directory Structure
+
+....
+.
+├── src/           # Source code
+├── tests/        # Test suites
+├── docs/         # Documentation
+├── scripts/      # Utility scripts
+├── config/       # Configuration files
+├── LICENSE       # License file
+├── LICENSES/     # Full license texts
+└── README.adoc   # Project documentation
+....
+
+=== Design Principles
+
+* *Separation of Concerns*: Each module has a single responsibility
+* *Testability*: Code is written to be easily testable
+* *Documentation*: All public APIs are documented
+* *Configuration*: Environment-specific settings are externalized
+
+=== Dependencies
+
+* External dependencies are minimized and clearly declared
+* Version pinning is used for reproducibility
+
+=== Security Considerations
+
+* Sensitive data is never committed to the repository
+* Secrets are managed through environment variables or secure vaults
+* Regular dependency audits are performed
+
+=== Maintainability
+
+* Code follows consistent style guidelines
+* Pull requests require review and CI checks
+* Issues and discussions are tracked transparently
+
+'''''
+
+_Last updated: 2026-07-18_
diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md
deleted file mode 100644
index 607e3d8..0000000
--- a/ARCHITECTURE.md
+++ /dev/null
@@ -1,47 +0,0 @@
-# Architecture
-
-## Overview
-
-This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability.
-
-## Directory Structure
-
-```
-.
-├── src/           # Source code
-├── tests/        # Test suites
-├── docs/         # Documentation
-├── scripts/      # Utility scripts
-├── config/       # Configuration files
-├── LICENSE       # License file
-├── LICENSES/     # Full license texts
-└── README.adoc   # Project documentation
-```
-
-## Design Principles
-
-- **Separation of Concerns**: Each module has a single responsibility
-- **Testability**: Code is written to be easily testable
-- **Documentation**: All public APIs are documented
-- **Configuration**: Environment-specific settings are externalized
-
-## Dependencies
-
-- External dependencies are minimized and clearly declared
-- Version pinning is used for reproducibility
-
-## Security Considerations
-
-- Sensitive data is never committed to the repository
-- Secrets are managed through environment variables or secure vaults
-- Regular dependency audits are performed
-
-## Maintainability
-
-- Code follows consistent style guidelines
-- Pull requests require review and CI checks
-- Issues and discussions are tracked transparently
-
----
-
-*Last updated: 2026-07-18*
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
new file mode 100644
index 0000000..3801949
--- /dev/null
+++ b/CHANGELOG.adoc
@@ -0,0 +1,169 @@
+== Changelog
+
+All notable changes to this project will be documented in this file.
+
+The format is based on https://keepachangelog.com/en/1.1.0/[Keep a
+Changelog], and this project adheres to
+https://semver.org/spec/v2.0.0.html[Semantic Versioning].
+
+=== [Unreleased]
+
+=== [0.2.0] — 2026-06-13
+
+==== Added
+
+*vclt-gate — VeriSimDB admissibility gate producer* (B1–B3).
+`+vclt-gate+` is a standalone binary
+(`+src/interface/parse/src/bin/vclt-gate.rs+`) that wraps the existing
+trusted parser to act as an out-of-process admissibility gate for
+VeriSimDB’s VCL executor:
+
+* *Binary protocol*: reads a single-line JSON payload
+`+{"schema_version":1,"statement":"...","schema":{}}+` from stdin; exits
+0 (admit, `+admissible:true+`, `+certified_level+` ≥ 0), 1 (reject,
+`+admissible:false+`, `+reasons:[...]+`), or 2 (gate_failed, unexpected
+error).
+* *`+certified_level+` surface*
+(`+src/interface/parse/src/decider.rs+`): the `+Decider+` now exposes
+`+certified_level_for+` — the integer level the corpus would certify for
+a parsed statement — directly to the gate output, so consumers see the
+same grade the proof corpus assigns.
+* *Gate test suite* (`+src/interface/parse/tests/gate.rs+`): 6 tests
+covering admit / reject / injection / level-plumbing; added to
+`+src/interface/parse/Cargo.toml+` as an integration test target.
+* *Workspace cleanup* (`+Cargo.toml+`): removed `+src/interface/lsp+`,
+`+src/interface/dap+`, `+src/interface/echidna-client+`, and
+`+src/interface+` (all have external path-deps that break standalone
+CI); updated comment explaining the `+src/interface/parse+`
+separate-workspace-root design.
+
+==== Verified
+
+*VclTotal proof corpus — Phase 0→4 remediation + Phase 5 boundary
+reinforcement* (2026-05-18/19, hyperpolymath/standards#124,
+hyperpolymath/vcl-ut#25). The `+src/core/**+` Idris2 corpus, which at
+Phase 0 did not compile and had never been machine-checked, is now
+CI-gated and green:
+
+* `+verification/proofs/vclut-core.ipkg+` builds clean under idris2
+0.8.0 (`+idris2 --build+`, exit 0, `+%default total+`) as *12 modules*,
+with *zero proof-escape symbols* (no
+`+believe_me+`/`+postulate+`/`+assert_*+`/ `+idris_crash+`/`+sorry+`),
+enforced by `+.github/workflows/proof-corpus.yml+`.
+* Phase 1 (#21): corpus resurrection — `+ABI.Types+`/`+Grammar+`
+repaired, `+.ipkg+`/CI added, L4 verified in situ.
+* Phase 2 (#22): L2/L3/L5 de-vacuized over the shared `+Core.Decide+`
+deciders + `+checkLevel2/3/5Sound+` + genuine `+composeJoin+` closure.
+* Phase 3 (#23): L1 + L6–L10 soundness; `+Checker.certifyAt+`/
+`+certifyRequested+` assemble a genuine dependent `+SafetyCertificate+`;
+`+ABI.Layout+` made sound; Phase 3d removed the fabricating Zig FFI (now
+fail-closed) and added the proof-gated `+Checker.certifiedLevel+`.
+* Phase 4 (PR #24): `+ABI.LayoutProofs+` (genuine alignment/no-padding/
+bounds) + L6–L10 `+composeJoin+` closure (`+l6..l9Compose+`,
+`+epiStructJoin+`); L10 acyclicity carried by the explicit
+`+JoinSideCondition+` (provably non-closed, not faked).
+* Phase 5 / vcl-ut#25 (boundary reinforcement): trusted Rust/SPARK-grade
+parser (P5a, #26) + deterministic versioned wire codec (P5b step 1,
+#28); *P5b step 2 (this change)* — `+VclTotal.Interface.WireDecode+`, a
+total (`+%default total+`, zero proof-escape) decoder of the v1 wire
+format into the certified `+Statement+`, recursion bounded by an
+input-length fuel `+Nat+`; `+VclTotal.Interface.WireConformance+` proves
+it byte-for-byte conformant with the Rust `+to_wire+` encoder by
+`+Refl+` on golden fixtures (regeneration oracle:
+`+src/interface/parse/tests/conformance_emit.rs+`). The C-ABI
+`+Statement+` marshalling _decode_ side is certified. Disclosed: the NaN
+_payload_ is not preserved across the Idris `+Double+` boundary (finite
++ infinite values bit-exact; Rust proptest remains the exhaustive float
+witness).
+* Phase 5 / vcl-ut#25 — *Tier-1 recompute-PCC RESOLVED*: P5c-1 (#30)
+certified `+OctadSchema+` codec (closes schema-marshalling OWED);
+P5c-2/3/4 (#31) `+vcltotal_parse::decider+` — a faithful Rust port of
+the corpus decision core (`+Schema+`/`+Decide+`/`+Checker+`
+`+checkLevel0..10+`/`+certifiedLevel+`), machine-pinned to the corpus’s
+public deciders via `+WireConformance+` on shared golden bytes
+(find-dependent verdicts pinned Rust-side + input-value conformance,
+disclosed); P5c-5 (#32) the recompute *`+wasm32+`* artefact
+`+src/interface/recompute-wasm+` (`+vcl_recompute+`, fail-closed, one
+audited host/guest `+unsafe+` block; all logic in the forbid-unsafe
+crate); P5c-6 (this change) the `+OWED→RESOLVED+` stance flip + ADR
+`+docs/decisions/0002-ffi-attestation-trust-boundary.adoc+`. The
+consumer *re-runs* the certified decision and compares — PCC by
+recomputation, not proof transport. Plain `+wasm32+` suffices (type
+system not load-bearing under recompute); `+affinescriptiser+` N/A
+(resource-required + wasm-backend-pending; disclosed in
+`+AFFINESCRIPTISER-NA.adoc+`, not faked).
+* Phase 5 / vcl-ut#25 — *Tier-2 (P5d) RESOLVED*:
+`+src/interface/attest+` (`+vcltotal-attest+`) mints/verifies an Ed25519
+attestation over
+`+DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level+` (level =
+the conformance-pinned `+certified_level+`, signed iff `+0..=10+`,
+fail-closed); the previously-OWED `+vclut_rs_verify+` backend is this
+crate, linked into `+ffi/zig/src/lib.zig+` (`+vclut_verify_wire+`) by
+`+build.zig+` (`+zig build test+` 4/4, end-to-end). Unforgeable + bound
+(roundtrip + 5 tamper variants + fail-closed + C-ABI tests).
+`+ed25519-dalek+`/`+sha2+` contained to the Tier-2 crate; zero-dep
+forbid-unsafe core untouched; one audited host/guest `+unsafe+` block.
+Spec `+src/interface/attest/ATTESTATION-FORMAT.adoc+`; ADR-0002 → both
+tiers RESOLVED. *The vcl-ut#25 boundary-reinforcement workstream is
+complete* (only the precisely-scoped disclosed limits remain — not
+gaps). A re-checkable proof is impossible _only_ over the C-ABI fallback
+tier; Tier-2 is honestly its weaker trusted-certifier ceiling (canonical
+two-tier model: `+verification/proofs/VERIFICATION-STANCE.adoc+`).
+
+`+verification/proofs/VERIFICATION-STANCE.adoc+` is the authoritative,
+precisely-scoped catalogue (residual OWED items disclosed, not masked).
+
+==== Renamed
+
+*V\{Q→C}L-\{UT→total}* (2026-04-05). Full repo-wide migration of the
+project identity, carried out as part of the ecosystem-wide
+query-language → consonance-language reframing:
+
+* *Q → C*: _VeriSim Query Language_ → _VeriSim Consonance Language_.
+Verisim operations are *propositions to a consonance engine*, not
+queries against a passive store. Operations split into propositional
+(`+DECLARE+`, `+ASSERT+`, `+RETRACT+`) and epistemic (`+INSPECT+`,
+`+VERIFY+`).
+* *UT → total*: the "`Ultimate Type-safe`" suffix becomes "`Total
+Type-safe`", denoting totality in the dependent-type sense (no partial
+functions, no undefined behaviour at type level).
+* *VeriSimDB → Verisim*: the underlying engine’s name shortens in
+discussion (the GitHub repository stays `+verisimdb+` to avoid rename
+damage).
+
+==== Scope of this rename pass
+
+Changed in this commit:
+
+* Crate names in Cargo.toml manifests (core, interface, fmt, lint, lsp,
+dap)
+* Rust module and file names (src/**, benches/, tests/)
+* ReScript bridge modules (src/bridges/, src/definitions/, src/errors/)
+* Idris2 sources and module declarations
+* File extension `+.vqlut+` → `+.vcltotal+`
+* Documentation prose in `+docs/+`, `+QUICKSTART-*.adoc+`,
+`+EXPLAINME.adoc+`, `+ROADMAP.adoc+`, `+CONTRIBUTING.adoc+`,
+`+SECURITY.md+`
+* CI workflow job names and README badges
+* Contractile K9 guard file
+* Container and dev-container configuration
+* Machine-readable manifests (`+.machine_readable/+`,
+`+0-AI-MANIFEST.a2ml+`)
+* Zenodo metadata file (.zenodo.json)
+* LaTeX paper (arcvix-10-level-query-safety.tex)
+
+==== NOT changed (deliberately)
+
+* *GitHub repository name*: still `+hyperpolymath/vql-ut+`. A repository
+rename would ripple to clone URLs, mirror paths, CI tokens, and issue/PR
+continuity via GitHub redirects — tracked as a separate decision.
+* *GitLab mirror path* at `+gitlab.com/hyperpolymath/vql-ut+`.
+* *Zenodo DOI* 10.5281/zenodo.19329501 — registered under the original
+name. A new DOI under the updated name can be minted at the next
+release.
+* *External citations* — published references still resolve through the
+historical record (git history, Zenodo, preprints).
+
+The ecosystem-level migration landed 2026-04-05 in `+verisimdb+`,
+`+hypatia+`, `+gitbot-fleet+`, and `+echidna+` repositories. This repo
+now joins that naming scheme.
diff --git a/CHANGELOG.md b/CHANGELOG.md
deleted file mode 100644
index 92ef95b..0000000
--- a/CHANGELOG.md
+++ /dev/null
@@ -1,161 +0,0 @@
-# Changelog
-
-All notable changes to this project will be documented in this file.
-
-The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
-and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
-
-<!-- Generated by git-cliff: https://git-cliff.org -->
-<!-- Run: just changelog -->
-
-## [Unreleased]
-
-## [0.2.0] — 2026-06-13
-
-### Added
-
-**vclt-gate — VeriSimDB admissibility gate producer** (B1–B3).
-`vclt-gate` is a standalone binary (`src/interface/parse/src/bin/vclt-gate.rs`)
-that wraps the existing trusted parser to act as an out-of-process
-admissibility gate for VeriSimDB's VCL executor:
-
-- **Binary protocol**: reads a single-line JSON payload
-  `{"schema_version":1,"statement":"...","schema":{}}` from stdin;
-  exits 0 (admit, `admissible:true`, `certified_level` ≥ 0),
-  1 (reject, `admissible:false`, `reasons:[...]`),
-  or 2 (gate_failed, unexpected error).
-- **`certified_level` surface** (`src/interface/parse/src/decider.rs`):
-  the `Decider` now exposes `certified_level_for` — the integer level
-  the corpus would certify for a parsed statement — directly to the gate
-  output, so consumers see the same grade the proof corpus assigns.
-- **Gate test suite** (`src/interface/parse/tests/gate.rs`): 6 tests
-  covering admit / reject / injection / level-plumbing; added to
-  `src/interface/parse/Cargo.toml` as an integration test target.
-- **Workspace cleanup** (`Cargo.toml`): removed `src/interface/lsp`,
-  `src/interface/dap`, `src/interface/echidna-client`, and `src/interface`
-  (all have external path-deps that break standalone CI); updated comment
-  explaining the `src/interface/parse` separate-workspace-root design.
-
-### Verified
-
-**VclTotal proof corpus — Phase 0→4 remediation + Phase 5 boundary
-reinforcement** (2026-05-18/19, hyperpolymath/standards#124,
-hyperpolymath/vcl-ut#25). The `src/core/**` Idris2 corpus, which at
-Phase 0 did not compile and had never been machine-checked, is now
-CI-gated and green:
-
-- `verification/proofs/vclut-core.ipkg` builds clean under idris2 0.8.0
-  (`idris2 --build`, exit 0, `%default total`) as **12 modules**, with
-  **zero proof-escape symbols** (no `believe_me`/`postulate`/`assert_*`/
-  `idris_crash`/`sorry`), enforced by `.github/workflows/proof-corpus.yml`.
-- Phase 1 (#21): corpus resurrection — `ABI.Types`/`Grammar` repaired,
-  `.ipkg`/CI added, L4 verified in situ.
-- Phase 2 (#22): L2/L3/L5 de-vacuized over the shared `Core.Decide`
-  deciders + `checkLevel2/3/5Sound` + genuine `composeJoin` closure.
-- Phase 3 (#23): L1 + L6–L10 soundness; `Checker.certifyAt`/
-  `certifyRequested` assemble a genuine dependent `SafetyCertificate`;
-  `ABI.Layout` made sound; Phase 3d removed the fabricating Zig FFI
-  (now fail-closed) and added the proof-gated `Checker.certifiedLevel`.
-- Phase 4 (PR #24): `ABI.LayoutProofs` (genuine alignment/no-padding/
-  bounds) + L6–L10 `composeJoin` closure (`l6..l9Compose`,
-  `epiStructJoin`); L10 acyclicity carried by the explicit
-  `JoinSideCondition` (provably non-closed, not faked).
-- Phase 5 / vcl-ut#25 (boundary reinforcement): trusted Rust/SPARK-grade
-  parser (P5a, #26) + deterministic versioned wire codec (P5b step 1,
-  #28); **P5b step 2 (this change)** — `VclTotal.Interface.WireDecode`,
-  a total (`%default total`, zero proof-escape) decoder of the v1 wire
-  format into the certified `Statement`, recursion bounded by an
-  input-length fuel `Nat`; `VclTotal.Interface.WireConformance` proves
-  it byte-for-byte conformant with the Rust `to_wire` encoder by `Refl`
-  on golden fixtures (regeneration oracle:
-  `src/interface/parse/tests/conformance_emit.rs`). The C-ABI
-  `Statement` marshalling *decode* side is certified. Disclosed:
-  the NaN *payload* is not preserved across the Idris `Double` boundary
-  (finite + infinite values bit-exact; Rust proptest remains the
-  exhaustive float witness).
-- Phase 5 / vcl-ut#25 — **Tier-1 recompute-PCC RESOLVED**: P5c-1 (#30)
-  certified `OctadSchema` codec (closes schema-marshalling OWED);
-  P5c-2/3/4 (#31) `vcltotal_parse::decider` — a faithful Rust port of
-  the corpus decision core (`Schema`/`Decide`/`Checker`
-  `checkLevel0..10`/`certifiedLevel`), machine-pinned to the corpus's
-  public deciders via `WireConformance` on shared golden bytes
-  (find-dependent verdicts pinned Rust-side + input-value conformance,
-  disclosed); P5c-5 (#32) the recompute **`wasm32`** artefact
-  `src/interface/recompute-wasm` (`vcl_recompute`, fail-closed, one
-  audited host/guest `unsafe` block; all logic in the forbid-unsafe
-  crate); P5c-6 (this change) the `OWED→RESOLVED` stance flip + ADR
-  `docs/decisions/0002-ffi-attestation-trust-boundary.adoc`. The
-  consumer **re-runs** the certified decision and compares — PCC by
-  recomputation, not proof transport. Plain `wasm32` suffices (type
-  system not load-bearing under recompute); `affinescriptiser` N/A
-  (resource-required + wasm-backend-pending; disclosed in
-  `AFFINESCRIPTISER-NA.adoc`, not faked).
-- Phase 5 / vcl-ut#25 — **Tier-2 (P5d) RESOLVED**: `src/interface/attest`
-  (`vcltotal-attest`) mints/verifies an Ed25519 attestation over
-  `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level` (level =
-  the conformance-pinned `certified_level`, signed iff `0..=10`,
-  fail-closed); the previously-OWED `vclut_rs_verify` backend is this
-  crate, linked into `ffi/zig/src/lib.zig` (`vclut_verify_wire`) by
-  `build.zig` (`zig build test` 4/4, end-to-end). Unforgeable + bound
-  (roundtrip + 5 tamper variants + fail-closed + C-ABI tests).
-  `ed25519-dalek`/`sha2` contained to the Tier-2 crate; zero-dep
-  forbid-unsafe core untouched; one audited host/guest `unsafe` block.
-  Spec `src/interface/attest/ATTESTATION-FORMAT.adoc`; ADR-0002 →
-  both tiers RESOLVED. **The vcl-ut#25 boundary-reinforcement
-  workstream is complete** (only the precisely-scoped disclosed limits
-  remain — not gaps). A re-checkable proof is impossible *only* over
-  the C-ABI fallback tier; Tier-2 is honestly its weaker
-  trusted-certifier ceiling (canonical two-tier model:
-  `verification/proofs/VERIFICATION-STANCE.adoc`).
-
-`verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative,
-precisely-scoped catalogue (residual OWED items disclosed, not masked).
-
-### Renamed
-
-**V{Q→C}L-{UT→total}** (2026-04-05). Full repo-wide migration of the project
-identity, carried out as part of the ecosystem-wide query-language → consonance-language
-reframing:
-
-- **Q → C**: *VeriSim Query Language* → *VeriSim Consonance Language*.
-  Verisim operations are **propositions to a consonance engine**, not queries
-  against a passive store. Operations split into propositional (`DECLARE`,
-  `ASSERT`, `RETRACT`) and epistemic (`INSPECT`, `VERIFY`).
-- **UT → total**: the "Ultimate Type-safe" suffix becomes "Total Type-safe",
-  denoting totality in the dependent-type sense (no partial functions, no
-  undefined behaviour at type level).
-- **VeriSimDB → Verisim**: the underlying engine's name shortens in discussion
-  (the GitHub repository stays `verisimdb` to avoid rename damage).
-
-### Scope of this rename pass
-
-Changed in this commit:
-
-- Crate names in Cargo.toml manifests (core, interface, fmt, lint, lsp, dap)
-- Rust module and file names (src/**, benches/, tests/)
-- ReScript bridge modules (src/bridges/, src/definitions/, src/errors/)
-- Idris2 sources and module declarations
-- File extension `.vqlut` → `.vcltotal`
-- Documentation prose in `docs/`, `QUICKSTART-*.adoc`, `EXPLAINME.adoc`,
-  `ROADMAP.adoc`, `CONTRIBUTING.adoc`, `SECURITY.md`
-- CI workflow job names and README badges
-- Contractile K9 guard file
-- Container and dev-container configuration
-- Machine-readable manifests (`.machine_readable/`, `0-AI-MANIFEST.a2ml`)
-- Zenodo metadata file (.zenodo.json)
-- LaTeX paper (arcvix-10-level-query-safety.tex)
-
-### NOT changed (deliberately)
-
-- **GitHub repository name**: still `hyperpolymath/vql-ut`. A repository
-  rename would ripple to clone URLs, mirror paths, CI tokens, and issue/PR
-  continuity via GitHub redirects — tracked as a separate decision.
-- **GitLab mirror path** at `gitlab.com/hyperpolymath/vql-ut`.
-- **Zenodo DOI** 10.5281/zenodo.19329501 — registered under the original
-  name. A new DOI under the updated name can be minted at the next release.
-- **External citations** — published references still resolve through the
-  historical record (git history, Zenodo, preprints).
-
-The ecosystem-level migration landed 2026-04-05 in `verisimdb`, `hypatia`,
-`gitbot-fleet`, and `echidna` repositories. This repo now joins that naming
-scheme.
diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc
new file mode 100644
index 0000000..bd2a83c
--- /dev/null
+++ b/CODE_OF_CONDUCT.adoc
@@ -0,0 +1,24 @@
+== Contributor Covenant Code of Conduct
+
+=== Our Pledge
+
+We pledge to make participation a harassment-free experience for
+everyone.
+
+=== Our Standards
+
+*Positive behavior:* * Using welcoming language * Being respectful of
+differing viewpoints * Accepting constructive criticism * Focusing on
+what is best for the community
+
+*Unacceptable behavior:* * Harassment, trolling, or personal attacks *
+Publishing private information without permission
+
+=== Enforcement
+
+Report issues to the maintainers. All complaints will be reviewed.
+
+=== Attribution
+
+Adapted from https://www.contributor-covenant.org/[Contributor Covenant]
+v2.1.
diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
deleted file mode 100644
index caeda1c..0000000
--- a/CODE_OF_CONDUCT.md
+++ /dev/null
@@ -1,27 +0,0 @@
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-# Contributor Covenant Code of Conduct
-
-## Our Pledge
-
-We pledge to make participation a harassment-free experience for everyone.
-
-## Our Standards
-
-**Positive behavior:**
-* Using welcoming language
-* Being respectful of differing viewpoints
-* Accepting constructive criticism
-* Focusing on what is best for the community
-
-**Unacceptable behavior:**
-* Harassment, trolling, or personal attacks
-* Publishing private information without permission
-
-## Enforcement
-
-Report issues to the maintainers. All complaints will be reviewed.
-
-## Attribution
-
-Adapted from [Contributor Covenant](https://www.contributor-covenant.org/) v2.1.
-
diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc
new file mode 100644
index 0000000..858f44f
--- /dev/null
+++ b/CONTRIBUTING.adoc
@@ -0,0 +1,71 @@
+== Contributing
+
+Thank you for your interest in contributing! We follow a "`Dual-Track`"
+architecture where human-readable documentation lives in the root and
+machine-readable policies live in `+.machine_readable/+`.
+
+=== How to Contribute
+
+We welcome contributions in many forms:
+
+* *Code:* Improving the core stack or extensions
+* *Documentation:* Enhancing docs or AI manifests
+* *Testing:* Adding property-based tests or formal proofs
+* *Bug reports:* Filing clear, reproducible issues
+
+=== Getting Started
+
+[arabic]
+. *Read the AI Manifest:* Start with `+0-AI-MANIFEST.a2ml+` (if present)
+to understand the repository structure.
+. *Environment:* Use `+nix develop+` or `+direnv allow+` to set up your
+tools.
+. *Task Runner:* Use `+just+` to see available commands
+(`+just --list+`).
+
+=== Development Workflow
+
+==== Branch Naming
+
+....
+docs/short-description       # Documentation
+test/what-added              # Test additions
+feat/short-description       # New features
+fix/issue-number-description # Bug fixes
+refactor/what-changed        # Code improvements
+security/what-fixed          # Security fixes
+....
+
+==== Commit Messages
+
+We follow https://www.conventionalcommits.org/[Conventional Commits]:
+
+....
+<type>(<scope>): <description>
+
+[optional body]
+
+[optional footer]
+....
+
+Types: `+feat+`, `+fix+`, `+docs+`, `+test+`, `+refactor+`, `+ci+`,
+`+chore+`, `+security+`
+
+=== Reporting Bugs
+
+Before reporting: 1. Search existing issues 2. Check if it’s already
+fixed in `+main+`
+
+When reporting, include: - Clear, descriptive title - Environment
+details (OS, versions, toolchain) - Steps to reproduce - Expected vs
+actual behaviour
+
+=== Code of Conduct
+
+All contributors are expected to adhere to our
+link:CODE_OF_CONDUCT.md[Code of Conduct].
+
+=== License
+
+By contributing, you agree that your contributions will be licensed
+under the same license as the project (see LICENSE).
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
deleted file mode 100644
index 80ecdac..0000000
--- a/CONTRIBUTING.md
+++ /dev/null
@@ -1,66 +0,0 @@
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-# Contributing
-
-Thank you for your interest in contributing! We follow a "Dual-Track" architecture where human-readable documentation lives in the root and machine-readable policies live in `.machine_readable/`.
-
-## How to Contribute
-
-We welcome contributions in many forms:
-
-- **Code:** Improving the core stack or extensions
-- **Documentation:** Enhancing docs or AI manifests
-- **Testing:** Adding property-based tests or formal proofs
-- **Bug reports:** Filing clear, reproducible issues
-
-## Getting Started
-
-1. **Read the AI Manifest:** Start with `0-AI-MANIFEST.a2ml` (if present) to understand the repository structure.
-2. **Environment:** Use `nix develop` or `direnv allow` to set up your tools.
-3. **Task Runner:** Use `just` to see available commands (`just --list`).
-
-## Development Workflow
-
-### Branch Naming
-
-```
-docs/short-description       # Documentation
-test/what-added              # Test additions
-feat/short-description       # New features
-fix/issue-number-description # Bug fixes
-refactor/what-changed        # Code improvements
-security/what-fixed          # Security fixes
-```
-
-### Commit Messages
-
-We follow [Conventional Commits](https://www.conventionalcommits.org/):
-
-```
-<type>(<scope>): <description>
-
-[optional body]
-
-[optional footer]
-```
-
-Types: `feat`, `fix`, `docs`, `test`, `refactor`, `ci`, `chore`, `security`
-
-## Reporting Bugs
-
-Before reporting:
-1. Search existing issues
-2. Check if it's already fixed in `main`
-
-When reporting, include:
-- Clear, descriptive title
-- Environment details (OS, versions, toolchain)
-- Steps to reproduce
-- Expected vs actual behaviour
-
-## Code of Conduct
-
-All contributors are expected to adhere to our [Code of Conduct](CODE_OF_CONDUCT.md).
-
-## License
-
-By contributing, you agree that your contributions will be licensed under the same license as the project (see [LICENSE](LICENSE)).
diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc
new file mode 100644
index 0000000..9b836fb
--- /dev/null
+++ b/GOVERNANCE.adoc
@@ -0,0 +1,60 @@
+== Governance
+
+=== Overview
+
+This project is governed by the following principles and structures to
+ensure transparent, inclusive, and effective decision-making.
+
+=== Roles and Responsibilities
+
+==== Maintainers
+
+Maintainers are responsible for: - Reviewing and merging pull requests -
+Managing releases and versioning - Ensuring code quality and standards -
+Triaging issues and bug reports - Community engagement and support
+
+==== Contributors
+
+Contributors are expected to: - Follow the code of conduct - Submit
+well-documented pull requests - Write tests for new functionality -
+Maintain existing tests - Update documentation as needed
+
+=== Decision Making
+
+==== Minor Changes
+
+* Can be made by any maintainer
+* Include bug fixes, documentation updates, dependency updates
+
+==== Major Changes
+
+* Require discussion in issues or pull requests
+* Include new features, architectural changes, API changes
+* Need approval from at least 2 maintainers
+
+==== Breaking Changes
+
+* Require RFC (Request for Comments) process
+* Need approval from majority of maintainers
+* Must include migration guide
+
+=== Code of Conduct
+
+All participants are expected to follow our Code of Conduct. Violations
+can be reported to the maintainers.
+
+=== Communication
+
+* *Issues*: For bug reports and feature requests
+* *Discussions*: For questions and general discussion
+* *Pull Requests*: For code contributions
+
+=== Licensing
+
+All contributions are made under the terms of the repository’s LICENSE
+file. By submitting a pull request, you agree to license your
+contributions accordingly.
+
+'''''
+
+_Last updated: 2026-07-18_
diff --git a/GOVERNANCE.md b/GOVERNANCE.md
deleted file mode 100644
index e27364c..0000000
--- a/GOVERNANCE.md
+++ /dev/null
@@ -1,60 +0,0 @@
-# Governance
-
-## Overview
-
-This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making.
-
-## Roles and Responsibilities
-
-### Maintainers
-
-Maintainers are responsible for:
-- Reviewing and merging pull requests
-- Managing releases and versioning
-- Ensuring code quality and standards
-- Triaging issues and bug reports
-- Community engagement and support
-
-### Contributors
-
-Contributors are expected to:
-- Follow the code of conduct
-- Submit well-documented pull requests
-- Write tests for new functionality
-- Maintain existing tests
-- Update documentation as needed
-
-## Decision Making
-
-### Minor Changes
-- Can be made by any maintainer
-- Include bug fixes, documentation updates, dependency updates
-
-### Major Changes
-- Require discussion in issues or pull requests
-- Include new features, architectural changes, API changes
-- Need approval from at least 2 maintainers
-
-### Breaking Changes
-- Require RFC (Request for Comments) process
-- Need approval from majority of maintainers
-- Must include migration guide
-
-## Code of Conduct
-
-All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers.
-
-## Communication
-
-- **Issues**: For bug reports and feature requests
-- **Discussions**: For questions and general discussion
-- **Pull Requests**: For code contributions
-
-## Licensing
-
-All contributions are made under the terms of the repository's LICENSE file.
-By submitting a pull request, you agree to license your contributions accordingly.
-
----
-
-*Last updated: 2026-07-18*
diff --git a/README.adoc.invariants.adoc b/README.adoc.invariants.adoc
new file mode 100644
index 0000000..39d5f6d
--- /dev/null
+++ b/README.adoc.invariants.adoc
@@ -0,0 +1,28 @@
+== Invariant Path Scan: README.adoc
+
+=== Invariant: ip-1629e2d2d1e45be1
+
+*Source Text:* "`Query language`" is
+
+*Target Text:* a misnomer; "`consonance language`" names
+
+*Invariant Type:* causal_relationship
+
+*Notes:* auto-generated heuristic suggestion; editable
+
+[width="5%",cols="100%",]
+|===
+|## Invariant: ip-d97cbe9bc8db0047
+
+|⚠️ *ISSUE DETECTED / 🔍 REVIEW REQUIRED*
+
+|*Source Text:* *ReScript evangeliser*
+
+|*Target Text:* the concept first — demonstrate the value of these type
+safety levels in ReScript itself, where the developer community can
+experience them firsthand
+
+|*Invariant Type:* risk_probability
+
+|*Notes:* auto-generated heuristic suggestion; editable
+|===
diff --git a/README.adoc.invariants.md b/README.adoc.invariants.md
deleted file mode 100644
index 81bf059..0000000
--- a/README.adoc.invariants.md
+++ /dev/null
@@ -1,26 +0,0 @@
-# Invariant Path Scan: README.adoc
-
-## Invariant: ip-1629e2d2d1e45be1
-
-**Source Text:** "Query language" is
-
-**Target Text:** a misnomer; "consonance language" names
-
-**Invariant Type:** causal_relationship
-
-**Notes:** auto-generated heuristic suggestion; editable
-
----
-## Invariant: ip-d97cbe9bc8db0047
-
-⚠️ **ISSUE DETECTED / 🔍 REVIEW REQUIRED**
-
-**Source Text:** **ReScript evangeliser**
-
-**Target Text:** the concept first — demonstrate the value of these type safety levels in ReScript itself, where the developer community can experience them firsthand
-
-**Invariant Type:** risk_probability
-
-**Notes:** auto-generated heuristic suggestion; editable
-
----
diff --git a/SECURITY.adoc b/SECURITY.adoc
new file mode 100644
index 0000000..e47fdd9
--- /dev/null
+++ b/SECURITY.adoc
@@ -0,0 +1,16 @@
+== Security Policy
+
+=== Reporting a Vulnerability
+
+If you discover a security vulnerability, please report it responsibly.
+
+*Email:* j.d.a.jewell@open.ac.uk
+
+*Please include:* - Description of the vulnerability - Steps to
+reproduce - Potential impact
+
+*Response timeline:* - Acknowledgement within 48 hours - Initial
+assessment within 7 days - Fix or mitigation within 90 days
+
+*Safe harbour:* We will not pursue legal action against security
+researchers who follow responsible disclosure.
diff --git a/SECURITY.md b/SECURITY.md
deleted file mode 100644
index 5c4d5e9..0000000
--- a/SECURITY.md
+++ /dev/null
@@ -1,20 +0,0 @@
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-# Security Policy
-
-## Reporting a Vulnerability
-
-If you discover a security vulnerability, please report it responsibly.
-
-**Email:** j.d.a.jewell@open.ac.uk
-
-**Please include:**
-- Description of the vulnerability
-- Steps to reproduce
-- Potential impact
-
-**Response timeline:**
-- Acknowledgement within 48 hours
-- Initial assessment within 7 days
-- Fix or mitigation within 90 days
-
-**Safe harbour:** We will not pursue legal action against security researchers who follow responsible disclosure.
diff --git a/docs/onboarding/llm-warmup-dev.adoc b/docs/onboarding/llm-warmup-dev.adoc
new file mode 100644
index 0000000..b4ed7f3
--- /dev/null
+++ b/docs/onboarding/llm-warmup-dev.adoc
@@ -0,0 +1,19 @@
+== LLM Warmup — vcl-total (Developer)
+
+=== What is vcl-total?
+
+See README.adoc for overview.
+
+=== Key Commands
+
+* `+just setup+` — set up development environment
+* `+just build+` — build the project
+* `+just test+` — run tests
+* `+just doctor+` — diagnose issues
+* `+just heal+` — attempt auto-repair
+
+=== Quick Context
+
+* License: MPL-2.0
+* Part of hyperpolymath ecosystem
+* See EXPLAINME.adoc for architecture
diff --git a/docs/onboarding/llm-warmup-dev.md b/docs/onboarding/llm-warmup-dev.md
deleted file mode 100644
index 6418097..0000000
--- a/docs/onboarding/llm-warmup-dev.md
+++ /dev/null
@@ -1,16 +0,0 @@
-# LLM Warmup — vcl-total (Developer)
-
-## What is vcl-total?
-See README.adoc for overview.
-
-## Key Commands
-- `just setup` — set up development environment
-- `just build` — build the project
-- `just test` — run tests
-- `just doctor` — diagnose issues
-- `just heal` — attempt auto-repair
-
-## Quick Context
-- License: MPL-2.0
-- Part of hyperpolymath ecosystem
-- See EXPLAINME.adoc for architecture
diff --git a/docs/onboarding/llm-warmup-user.adoc b/docs/onboarding/llm-warmup-user.adoc
new file mode 100644
index 0000000..b0b316f
--- /dev/null
+++ b/docs/onboarding/llm-warmup-user.adoc
@@ -0,0 +1,19 @@
+== LLM Warmup — vcl-total (User)
+
+=== What is vcl-total?
+
+See README.adoc for overview.
+
+=== Key Commands
+
+* `+just setup+` — set up development environment
+* `+just build+` — build the project
+* `+just test+` — run tests
+* `+just doctor+` — diagnose issues
+* `+just heal+` — attempt auto-repair
+
+=== Quick Context
+
+* License: MPL-2.0
+* Part of hyperpolymath ecosystem
+* See EXPLAINME.adoc for architecture
diff --git a/docs/onboarding/llm-warmup-user.md b/docs/onboarding/llm-warmup-user.md
deleted file mode 100644
index c68e351..0000000
--- a/docs/onboarding/llm-warmup-user.md
+++ /dev/null
@@ -1,16 +0,0 @@
-# LLM Warmup — vcl-total (User)
-
-## What is vcl-total?
-See README.adoc for overview.
-
-## Key Commands
-- `just setup` — set up development environment
-- `just build` — build the project
-- `just test` — run tests
-- `just doctor` — diagnose issues
-- `just heal` — attempt auto-repair
-
-## Quick Context
-- License: MPL-2.0
-- Part of hyperpolymath ecosystem
-- See EXPLAINME.adoc for architecture
diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc
new file mode 100644
index 0000000..0e92b4d
--- /dev/null
+++ b/docs/proof-debt.adoc
@@ -0,0 +1,58 @@
+== Proof Debt — vcl-ut
+
+*Schema*:
+https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc[hyperpolymath/standards
+`+TRUSTED-BASE-REDUCTION-POLICY.adoc+`] (standards#203).
+
+=== Current state
+
+*Zero soundness-relevant escape hatches* in this repo as of 2026-05-26.
+
+Verified by `+scripts/check-trusted-base.sh+` from
+https://github.com/hyperpolymath/standards[hyperpolymath/standards] —
+all matches found by syntactic scan were inside docstrings explicitly
+stating the file does NOT use `+believe_me+` / `+assert_total+` /
+`+postulate+` / `+sorry+` / `+Admitted+` (the "`no escape hatches`"
+discipline pattern).
+
+=== (a) DISCHARGED in this repo
+
+_(None — never any to discharge.)_
+
+=== (b) BUDGETED — tested with a refutation budget
+
+_(None.)_
+
+=== (c) NECESSARY AXIOM
+
+_(None.)_
+
+=== (d) DEBT — actively to be closed
+
+_(None.)_
+
+=== Preservation contract
+
+This file exists to assert the *zero-debt invariant* for the
+`+scripts/check-trusted-base.sh+` CI gate (standards#211). Any future PR
+that introduces a soundness-relevant escape hatch MUST either:
+
+[arabic]
+. annotate the call site with a leading `+TRUSTED:+` / `+AXIOM:+`
+comment, OR
+. add an entry to this file under §(b) / §(c) / §(d).
+
+PRs that introduce un-annotated escape hatches will fail CI.
+
+=== Companion documents
+
+* https://github.com/hyperpolymath/standards/pull/195[standards#195] —
+estate proof-debt audit.
+* https://github.com/hyperpolymath/standards/pull/203[standards#203] —
+trusted-base reduction policy (the schema this file follows).
+* https://github.com/hyperpolymath/standards/pull/211[standards#211] —
+`+check-trusted-base.sh+` CI enforcement.
+
+'''''
+
+🤖 Initial seed by Claude Code, 2026-05-26.
diff --git a/docs/proof-debt.md b/docs/proof-debt.md
deleted file mode 100644
index 24947d5..0000000
--- a/docs/proof-debt.md
+++ /dev/null
@@ -1,57 +0,0 @@
-<!--
-SPDX-License-Identifier: CC-BY-SA-4.0
-SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
--->
-
-# Proof Debt — vcl-ut
-
-**Schema**: [hyperpolymath/standards `TRUSTED-BASE-REDUCTION-POLICY.adoc`](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc) (standards#203).
-
-## Current state
-
-**Zero soundness-relevant escape hatches** in this repo as of 2026-05-26.
-
-Verified by `scripts/check-trusted-base.sh` from
-[hyperpolymath/standards](https://github.com/hyperpolymath/standards) —
-all matches found by syntactic scan were inside docstrings explicitly
-stating the file does NOT use `believe_me` / `assert_total` /
-`postulate` / `sorry` / `Admitted` (the "no escape hatches"
-discipline pattern).
-
-## (a) DISCHARGED in this repo
-
-*(None — never any to discharge.)*
-
-## (b) BUDGETED — tested with a refutation budget
-
-*(None.)*
-
-## (c) NECESSARY AXIOM
-
-*(None.)*
-
-## (d) DEBT — actively to be closed
-
-*(None.)*
-
-## Preservation contract
-
-This file exists to assert the **zero-debt invariant** for the
-`scripts/check-trusted-base.sh` CI gate (standards#211). Any future PR
-that introduces a soundness-relevant escape hatch MUST either:
-
-1. annotate the call site with a leading `TRUSTED:` / `AXIOM:`
-   comment, OR
-2. add an entry to this file under §(b) / §(c) / §(d).
-
-PRs that introduce un-annotated escape hatches will fail CI.
-
-## Companion documents
-
-- [standards#195](https://github.com/hyperpolymath/standards/pull/195) — estate proof-debt audit.
-- [standards#203](https://github.com/hyperpolymath/standards/pull/203) — trusted-base reduction policy (the schema this file follows).
-- [standards#211](https://github.com/hyperpolymath/standards/pull/211) — `check-trusted-base.sh` CI enforcement.
-
----
-
-🤖 Initial seed by Claude Code, 2026-05-26.
diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc
new file mode 100644
index 0000000..2635c79
--- /dev/null
+++ b/docs/status/PROOF-NEEDS.adoc
@@ -0,0 +1,145 @@
+== PROOF-NEEDS.md
+
+=== Current State
+
+* *LOC*: ~8,000
+* *Languages*: Rust, ReScript, Idris2, Zig
+* *Existing ABI proofs*: `+src/interface/abi/*.idr+` + domain-specific
+Idris2: `+src/core/Checker.idr+`, `+Grammar.idr+`, `+Levels.idr+`,
+`+Schema.idr+`, `+Composition.idr+`
+* *Machine-verified*: the full `+VclTotal+` proof corpus —
+`+verification/proofs/vclut-core.ipkg+` builds clean under idris2 0.8.0
+(`+idris2 --build+`, exit 0, `+%default total+`, *zero proof-escape
+symbols*, CI-gated by `+.github/workflows/proof-corpus.yml+`) as *12
+modules* (`+ABI.{Types,Layout,LayoutProofs}+` +
+`+Core.{Grammar,Schema,Decide,Levels,Checker,Composition,Epistemic}+` +
+`+Interface.{WireDecode,WireConformance}+`), plus the self-contained
+`+verification/proofs/SafetyL4Model.idr+` (`+--check+`, exit 0). Phases
+1–4 are on `+origin/main+` (PRs #21/#22/#23/#24); Phase 5 / vcl-ut#25
+(trusted Rust parser P5a #26, wire codec P5b-step-1 #28, *certified
+Idris wire decoder + cross-language `+Refl+` conformance* P5b-step-2)
+reinforces the FFI boundary.
+* *Status (Phase 0 → 4 RESOLVED, honestly; Phase 5 boundary
+reinforcement in progress)*: the Phase-0 blockers are fixed, not faked —
+the corpus compiles and is machine-checked; `+ABI.Types+`/`+Grammar+`
+errors repaired; *L2/L3/L5 de-vacuized* (Phase 2, evidence-carrying
+predicates over `+Core.Decide+`); all ten levels carry
+`+checkLevelNSound+` and `+Checker.certifyAt+`/`+certifyRequested+`
+assemble a genuine dependent `+SafetyCertificate+` (Phase 3); the Zig
+FFI is no longer a fabricating stub — it is *fail-closed* with a
+proof-gated `+Checker.certifiedLevel+` mint (Phase 3d). *Phase 5
+(vcl-ut#25)*: a trusted Rust/SPARK-grade parser + a deterministic
+versioned wire codec exist, and the _decode_ side of the C-ABI
+`+Statement+` marshalling is now *certified* —
+`+VclTotal.Interface.WireDecode+` is a total (zero-escape) decoder
+proven byte-for-byte conformant with the Rust encoder by `+Refl+`
+(`+WireConformance+`). *P5c (vcl-ut#25) — Tier-1 recompute-PCC RESOLVED*
+(#26/#28/#29/#30/#31/#32): trusted Rust parser, certified
+`+Statement+`+`+OctadSchema+` decoder (`+Refl+`-pinned), faithful Rust
+decision port machine-pinned to the corpus, and a fail-closed recompute
+`+wasm32+` artefact the consumer re-runs. Remaining honest gaps
+precisely scoped: *P5d* = C-ABI signed-attestation _fallback_ contract
+for non-wasm consumers (Tier-2, OWED); plus the disclosed limits
+(NaN-payload reconstruction; cross-module `+Refl+` non-reduction of
+`+find+`/`+elemBy+` ⇒ schema-resolution-dependent verdicts pinned
+Rust-side + input-value conformance; L3 subquery/heuristic scoping;
+L9/L10 predicate depth; additive↔ceil `+alignUp+` sliver). A
+re-checkable proof is impossible _only_ over the C-ABI fallback tier;
+Tier-1 sidesteps it by recomputation, not proof transport.
+`+verification/proofs/VERIFICATION-STANCE.adoc+` is the authoritative,
+proof-backed catalogue and takes precedence over this file.
+
+=== What Needs Proving
+
+==== Query Type Checker (src/core/Checker.idr)
+
+* Already in Idris2 — verify it type-checks and that the checking
+algorithm is total
+* Prove: well-typed VCL-total queries produce well-typed results against
+a schema
+
+==== Grammar Specification (src/core/Grammar.idr)
+
+* VCL-total grammar defined in Idris2 — prove the grammar is unambiguous
+* Prove: parser (ReScript side) accepts exactly the Idris2-specified
+grammar
+
+==== Level System (src/core/Levels.idr)
+
+* ✅ L4 `+NoRawUserInput+` de-vacuized + `+checkLevel4Sound+` +
+`+noRawUserInputCompose+` (verified in
+`+verification/proofs/SafetyL4Model.idr+` and in situ in the corpus)
+* ✅ L2/L3/L5 de-vacuized (Phase 2) — evidence-carrying predicates over
+`+Core.Decide+`, with `+checkLevel2/3/5Sound+` and genuine
+`+composeJoin+` closure
+* ✅ L1 + L6–L10 sound (Phase 3) + genuine L6–L10 `+composeJoin+`
+closure (Phase 4: `+l6..l9Compose+`, `+epiStructJoin+`); L10 acyclicity
+carried by the explicit `+JoinSideCondition+` (provably non-closed, not
+faked)
+* 10-level type safety hierarchy — prove level ordering is a lattice
+* Prove: level promotion/demotion preserves query safety
+
+==== Schema Validation (src/core/Schema.idr)
+
+* Prove: schema-validated queries cannot produce runtime type errors
+* Prove: schema evolution preserves backward compatibility for existing
+queries
+
+==== Rust DAP/Formatter (src/interface/dap/, src/interface/fmt/)
+
+* Debug adapter and formatter — lower priority but should preserve query
+semantics
+
+==== ReScript Bridge (src/bridges/)
+
+* `+VclTotalParser.res+`, `+VclTotalBridge.res+` — a *standalone
+ReScript frontend* (a working recursive-descent parser producing a
+_ReScript_ AST). It is *not* on the verified path: it does not connect
+to, or marshal into, the Idris2 `+Statement+` the proof corpus
+certifies, nor the Rust core. (`+VERIFICATION-STANCE.adoc+` "`no
+string→`+Statement+` parser exists`" is precise — it means no parser
+whose output is the _certified_ Idris2 `+Statement+`.)
+* The _trusted_ boundary parser is the Rust/SPARK-grade
+`+src/interface/parse+` crate (`+vcltotal-parse+`, P5a of vcl-ut#25),
+which mirrors `+Grammar.idr+` and feeds the certifier across the C-ABI.
+Its `+wire.rs+` codec (P5b step 1) serialises the parsed `+Statement+`
+to a deterministic versioned binary format
+(`+src/interface/parse/WIRE-FORMAT.adoc+`).
+* The _certified_ receiver of that format is
+`+VclTotal.Interface.WireDecode+` (P5b step 2): a total, zero-escape
+Idris decoder into the certified `+Statement+`, proven byte-for-byte
+conformant with the Rust encoder by `+Refl+` in
+`+VclTotal.Interface.WireConformance+`. The marshalling seam’s _decode_
+side is machine-verified. *P5c — RESOLVED (Tier-1 recompute-PCC):* the
+consumer re-runs the certified decision itself from the fail-closed
+`+wasm32+` module `+src/interface/recompute-wasm+` (`+vcl_recompute+`);
+the decision core is a faithful Rust port of the corpus
+(`+Schema+`/`+Decide+`/`+Checker+`) machine-pinned via
+`+WireConformance+`. TCB = conformance-pinned decider image + wasm
+runtime + the once-proved corpus (offline-re-checkable) — _not_ a
+trusted tag, _not_ a transported proof object. Plain `+wasm32+` suffices
+(type system not load-bearing under recompute); `+affinescriptiser+` N/A
+(disclosed). *P5d — RESOLVED (Tier-2 fallback):*
+`+src/interface/attest+` mints/verifies an Ed25519 attestation bound to
+`+(sha256(stmt_wire), sha256(schema_wire),   level)+` (fail-closed); the
+`+vclut_rs_verify+` backend is linked into `+ffi/zig+`
+(`+vclut_verify_wire+`, `+zig build test+` green end-to-end).
+Trusted-certifier (weaker than Tier-1), crypto contained. *The vcl-ut#25
+workstream is complete* — only precisely-scoped disclosed limits remain
+(not gaps). See the canonical two-tier boundary model in
+`+verification/proofs/VERIFICATION-STANCE.adoc+` (authoritative).
+* Optional future work: prove the ReScript frontend faithfully tracks
+the Idris2 grammar (low priority; it is a convenience frontend, not a
+trust anchor).
+
+=== Recommended Prover
+
+* *Idris2* (already in use for core — complete the proofs in
+Checker.idr, Grammar.idr, Levels.idr, Schema.idr)
+
+=== Priority
+
+*HIGH* — VCL-total is the query language for VeriSimDB. Incorrect type
+checking could allow queries that corrupt data or return wrong results.
+The Idris2 core is already in place — completing the proofs is high
+value for low effort.
diff --git a/docs/status/PROOF-NEEDS.md b/docs/status/PROOF-NEEDS.md
deleted file mode 100644
index 9976472..0000000
--- a/docs/status/PROOF-NEEDS.md
+++ /dev/null
@@ -1,83 +0,0 @@
-# PROOF-NEEDS.md
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-
-## Current State
-
-- **LOC**: ~8,000
-- **Languages**: Rust, ReScript, Idris2, Zig
-- **Existing ABI proofs**: `src/interface/abi/*.idr` + domain-specific Idris2: `src/core/Checker.idr`, `Grammar.idr`, `Levels.idr`, `Schema.idr`, `Composition.idr`
-- **Machine-verified**: the full `VclTotal` proof corpus — `verification/proofs/vclut-core.ipkg` builds clean under idris2 0.8.0 (`idris2 --build`, exit 0, `%default total`, **zero proof-escape symbols**, CI-gated by `.github/workflows/proof-corpus.yml`) as **12 modules** (`ABI.{Types,Layout,LayoutProofs}` + `Core.{Grammar,Schema,Decide,Levels,Checker,Composition,Epistemic}` + `Interface.{WireDecode,WireConformance}`), plus the self-contained `verification/proofs/SafetyL4Model.idr` (`--check`, exit 0). Phases 1–4 are on `origin/main` (PRs #21/#22/#23/#24); Phase 5 / vcl-ut#25 (trusted Rust parser P5a #26, wire codec P5b-step-1 #28, **certified Idris wire decoder + cross-language `Refl` conformance** P5b-step-2) reinforces the FFI boundary.
-- **Status (Phase 0 → 4 RESOLVED, honestly; Phase 5 boundary reinforcement in progress)**: the Phase-0 blockers are fixed, not faked — the corpus compiles and is machine-checked; `ABI.Types`/`Grammar` errors repaired; **L2/L3/L5 de-vacuized** (Phase 2, evidence-carrying predicates over `Core.Decide`); all ten levels carry `checkLevelNSound` and `Checker.certifyAt`/`certifyRequested` assemble a genuine dependent `SafetyCertificate` (Phase 3); the Zig FFI is no longer a fabricating stub — it is **fail-closed** with a proof-gated `Checker.certifiedLevel` mint (Phase 3d). **Phase 5 (vcl-ut#25)**: a trusted Rust/SPARK-grade parser + a deterministic versioned wire codec exist, and the *decode* side of the C-ABI `Statement` marshalling is now **certified** — `VclTotal.Interface.WireDecode` is a total (zero-escape) decoder proven byte-for-byte conformant with the Rust encoder by `Refl` (`WireConformance`). **P5c (vcl-ut#25) — Tier-1 recompute-PCC RESOLVED** (#26/#28/#29/#30/#31/#32): trusted Rust parser, certified `Statement`+`OctadSchema` decoder (`Refl`-pinned), faithful Rust decision port machine-pinned to the corpus, and a fail-closed recompute `wasm32` artefact the consumer re-runs. Remaining honest gaps precisely scoped: **P5d** = C-ABI signed-attestation *fallback* contract for non-wasm consumers (Tier-2, OWED); plus the disclosed limits (NaN-payload reconstruction; cross-module `Refl` non-reduction of `find`/`elemBy` ⇒ schema-resolution-dependent verdicts pinned Rust-side + input-value conformance; L3 subquery/heuristic scoping; L9/L10 predicate depth; additive↔ceil `alignUp` sliver). A re-checkable proof is impossible *only* over the C-ABI fallback tier; Tier-1 sidesteps it by recomputation, not proof transport. `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative, proof-backed catalogue and takes precedence over this file.
-
-## What Needs Proving
-
-### Query Type Checker (src/core/Checker.idr)
-- Already in Idris2 — verify it type-checks and that the checking algorithm is total
-- Prove: well-typed VCL-total queries produce well-typed results against a schema
-
-### Grammar Specification (src/core/Grammar.idr)
-- VCL-total grammar defined in Idris2 — prove the grammar is unambiguous
-- Prove: parser (ReScript side) accepts exactly the Idris2-specified grammar
-
-### Level System (src/core/Levels.idr)
-- ✅ L4 `NoRawUserInput` de-vacuized + `checkLevel4Sound` + `noRawUserInputCompose` (verified in `verification/proofs/SafetyL4Model.idr` and in situ in the corpus)
-- ✅ L2/L3/L5 de-vacuized (Phase 2) — evidence-carrying predicates over `Core.Decide`, with `checkLevel2/3/5Sound` and genuine `composeJoin` closure
-- ✅ L1 + L6–L10 sound (Phase 3) + genuine L6–L10 `composeJoin` closure (Phase 4: `l6..l9Compose`, `epiStructJoin`); L10 acyclicity carried by the explicit `JoinSideCondition` (provably non-closed, not faked)
-- 10-level type safety hierarchy — prove level ordering is a lattice
-- Prove: level promotion/demotion preserves query safety
-
-### Schema Validation (src/core/Schema.idr)
-- Prove: schema-validated queries cannot produce runtime type errors
-- Prove: schema evolution preserves backward compatibility for existing queries
-
-### Rust DAP/Formatter (src/interface/dap/, src/interface/fmt/)
-- Debug adapter and formatter — lower priority but should preserve query semantics
-
-### ReScript Bridge (src/bridges/)
-- `VclTotalParser.res`, `VclTotalBridge.res` — a **standalone ReScript
-  frontend** (a working recursive-descent parser producing a *ReScript*
-  AST). It is **not** on the verified path: it does not connect to, or
-  marshal into, the Idris2 `Statement` the proof corpus certifies, nor
-  the Rust core. (`VERIFICATION-STANCE.adoc` "no string→`Statement`
-  parser exists" is precise — it means no parser whose output is the
-  *certified* Idris2 `Statement`.)
-- The *trusted* boundary parser is the Rust/SPARK-grade
-  `src/interface/parse` crate (`vcltotal-parse`, P5a of vcl-ut#25),
-  which mirrors `Grammar.idr` and feeds the certifier across the C-ABI.
-  Its `wire.rs` codec (P5b step 1) serialises the parsed `Statement`
-  to a deterministic versioned binary format
-  (`src/interface/parse/WIRE-FORMAT.adoc`).
-- The *certified* receiver of that format is
-  `VclTotal.Interface.WireDecode` (P5b step 2): a total, zero-escape
-  Idris decoder into the certified `Statement`, proven byte-for-byte
-  conformant with the Rust encoder by `Refl` in
-  `VclTotal.Interface.WireConformance`. The marshalling seam's *decode*
-  side is machine-verified. **P5c — RESOLVED (Tier-1 recompute-PCC):**
-  the consumer re-runs the certified decision itself from the
-  fail-closed `wasm32` module `src/interface/recompute-wasm`
-  (`vcl_recompute`); the decision core is a faithful Rust port of the
-  corpus (`Schema`/`Decide`/`Checker`) machine-pinned via
-  `WireConformance`. TCB = conformance-pinned decider image + wasm
-  runtime + the once-proved corpus (offline-re-checkable) — *not* a
-  trusted tag, *not* a transported proof object. Plain `wasm32`
-  suffices (type system not load-bearing under recompute);
-  `affinescriptiser` N/A (disclosed). **P5d — RESOLVED (Tier-2
-  fallback):** `src/interface/attest` mints/verifies an Ed25519
-  attestation bound to `(sha256(stmt_wire), sha256(schema_wire),
-  level)` (fail-closed); the `vclut_rs_verify` backend is linked into
-  `ffi/zig` (`vclut_verify_wire`, `zig build test` green end-to-end).
-  Trusted-certifier (weaker than Tier-1), crypto contained. **The
-  vcl-ut#25 workstream is complete** — only precisely-scoped disclosed
-  limits remain (not gaps). See the canonical two-tier boundary model
-  in `verification/proofs/VERIFICATION-STANCE.adoc` (authoritative).
-- Optional future work: prove the ReScript frontend faithfully tracks
-  the Idris2 grammar (low priority; it is a convenience frontend, not a
-  trust anchor).
-
-## Recommended Prover
-
-- **Idris2** (already in use for core — complete the proofs in Checker.idr, Grammar.idr, Levels.idr, Schema.idr)
-
-## Priority
-
-**HIGH** — VCL-total is the query language for VeriSimDB. Incorrect type checking could allow queries that corrupt data or return wrong results. The Idris2 core is already in place — completing the proofs is high value for low effort.
diff --git a/docs/status/TEST-NEEDS.adoc b/docs/status/TEST-NEEDS.adoc
new file mode 100644
index 0000000..383f8e0
--- /dev/null
+++ b/docs/status/TEST-NEEDS.adoc
@@ -0,0 +1,86 @@
+== TEST-NEEDS: vcl-total
+
+=== CRG Grade: C — ACHIEVED 2026-04-04
+
+=== Current State
+
+[width="100%",cols="40%,26%,34%",options="header",]
+|===
+|Category |Count |Details
+|*Source modules* |27 |Idris2 core (4: Checker, Grammar, Levels,
+Schema), ReScript bridges (3: Ast, Bridge, Parser), ReScript
+definitions/errors (2), Rust interfaces (LSP 2, DAP 2, fmt 2, lint 2,
+lib), 3 Idris2 interface ABI, Zig FFI
+
+|*Unit tests* |1 file |integration_test.rs (49 #[test])
+
+|*Integration tests* |0 |Despite the filename, these are unit tests
+
+|*E2E tests* |0 |None
+
+|*Benchmarks* |0 |None
+
+|*Fuzz tests* |0 |None
+|===
+
+=== What’s Missing
+
+==== P2P Tests (CRITICAL)
+
+* [ ] No tests for ReScript parser -> Idris2 checker pipeline
+* [ ] No tests for LSP server handling real editor requests
+* [ ] No tests for DAP server with real debugger
+* [ ] No tests for fmt/lint tools on actual VCL-total code
+
+==== E2E Tests (CRITICAL)
+
+* [ ] No test that parses VCL-total, type-checks it through all 10
+levels, and executes it
+* [ ] No test for LSP completion/hover/diagnostics
+* [ ] No test for DAP breakpoints/stepping
+
+==== Aspect Tests
+
+* [ ] *Security*: Query language with no injection tests
+* [ ] *Performance*: No benchmarks for type checking, parsing throughput
+* [ ] *Concurrency*: No concurrent query compilation tests
+* [ ] *Error handling*: No tests for malformed VCL-total, type errors at
+each level
+
+==== Build & Execution
+
+* [ ] 4 Idris2 core modules with 0 Idris2-level tests – are proofs
+checked?
+* [ ] 4 Rust tool interfaces (LSP, DAP, fmt, lint) with 0 tests each
+* [ ] Zig FFI integration_test.zig likely template placeholder
+
+==== Benchmarks Needed
+
+* [ ] VCL-total parsing throughput
+* [ ] Type checking per level (L1-L10)
+* [ ] LSP response latency
+* [ ] Query compilation time
+
+==== Self-Tests
+
+* [ ] No VCL-total self-consistency check
+
+=== FLAGGED ISSUES
+
+* *49 tests for 27 source modules* = thin coverage
+* *4 developer tools (LSP, DAP, fmt, lint) with 0 tests* – tools that
+developers will use are untested
+* *10-level type system with 0 level-specific tests* – can’t verify any
+level works
+* *Idris2 formal core is unverified* – the proofs exist but nobody tests
+that they check
+
+=== Priority: P0 (CRITICAL)
+
+=== FAKE-FUZZ ALERT
+
+* `+tests/fuzz/placeholder.txt+` is a scorecard placeholder inherited
+from rsr-template-repo — it does NOT provide real fuzz testing
+* Replace with an actual fuzz harness (see
+rsr-template-repo/tests/fuzz/README.adoc) or remove the file
+* Priority: P2 — creates false impression of fuzz coverage
diff --git a/docs/status/TEST-NEEDS.md b/docs/status/TEST-NEEDS.md
deleted file mode 100644
index e3b7633..0000000
--- a/docs/status/TEST-NEEDS.md
+++ /dev/null
@@ -1,61 +0,0 @@
-# TEST-NEEDS: vcl-total
-
-## CRG Grade: C — ACHIEVED 2026-04-04
-
-## Current State
-
-| Category | Count | Details |
-|----------|-------|---------|
-| **Source modules** | 27 | Idris2 core (4: Checker, Grammar, Levels, Schema), ReScript bridges (3: Ast, Bridge, Parser), ReScript definitions/errors (2), Rust interfaces (LSP 2, DAP 2, fmt 2, lint 2, lib), 3 Idris2 interface ABI, Zig FFI |
-| **Unit tests** | 1 file | integration_test.rs (49 #[test]) |
-| **Integration tests** | 0 | Despite the filename, these are unit tests |
-| **E2E tests** | 0 | None |
-| **Benchmarks** | 0 | None |
-| **Fuzz tests** | 0 | None |
-
-## What's Missing
-
-### P2P Tests (CRITICAL)
-- [ ] No tests for ReScript parser -> Idris2 checker pipeline
-- [ ] No tests for LSP server handling real editor requests
-- [ ] No tests for DAP server with real debugger
-- [ ] No tests for fmt/lint tools on actual VCL-total code
-
-### E2E Tests (CRITICAL)
-- [ ] No test that parses VCL-total, type-checks it through all 10 levels, and executes it
-- [ ] No test for LSP completion/hover/diagnostics
-- [ ] No test for DAP breakpoints/stepping
-
-### Aspect Tests
-- [ ] **Security**: Query language with no injection tests
-- [ ] **Performance**: No benchmarks for type checking, parsing throughput
-- [ ] **Concurrency**: No concurrent query compilation tests
-- [ ] **Error handling**: No tests for malformed VCL-total, type errors at each level
-
-### Build & Execution
-- [ ] 4 Idris2 core modules with 0 Idris2-level tests -- are proofs checked?
-- [ ] 4 Rust tool interfaces (LSP, DAP, fmt, lint) with 0 tests each
-- [ ] Zig FFI integration_test.zig likely template placeholder
-
-### Benchmarks Needed
-- [ ] VCL-total parsing throughput
-- [ ] Type checking per level (L1-L10)
-- [ ] LSP response latency
-- [ ] Query compilation time
-
-### Self-Tests
-- [ ] No VCL-total self-consistency check
-
-## FLAGGED ISSUES
-- **49 tests for 27 source modules** = thin coverage
-- **4 developer tools (LSP, DAP, fmt, lint) with 0 tests** -- tools that developers will use are untested
-- **10-level type system with 0 level-specific tests** -- can't verify any level works
-- **Idris2 formal core is unverified** -- the proofs exist but nobody tests that they check
-
-## Priority: P0 (CRITICAL)
-
-## FAKE-FUZZ ALERT
-
-- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
-- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
-- Priority: P2 — creates false impression of fuzz coverage
diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc
new file mode 100644
index 0000000..b6fbdba
--- /dev/null
+++ b/docs/tech-debt-2026-05-26.adoc
@@ -0,0 +1,80 @@
+== Tech-Debt Audit — vcl-ut — 2026-05-26
+
+*Source:* estate-wide automated scan 2026-05-26. *Companion:*
+https://github.com/hyperpolymath/standards/tree/main/docs/audits[`+hyperpolymath/standards+`
+2026-05-26-estate-*-debt audits]. *Combined severity:* `+MEDIUM+`.
+
+This file records the _raw findings_ — it does not by itself fix the
+debt. Each section ends with a '`Recommended next move`' line; closing
+the debt is follow-up work.
+
+=== 1. Proof debt
+
+Scanner counted the following markers in proof-bearing files of this
+repo:
+
+....
+files=   16 | Coq-Axm/Adm=   0 | Lean-srry/ax=   0 | Agda-pst=   0 | Idr-blv=   8 | Idr-prtl=   0 | Fstr-asm=  0 | TODO= 14 | Unsafe=  0
+....
+
+*Total markers:* 22. *Severity:* `+>022+`.
+
+*Marker types* (any non-zero counts above): - Coq `+Axiom+`/`+Admitted+`
+— unconditional proof escapes. - Lean `+sorry+`/`+axiom+` — Lean’s
+equivalent. - Agda `+postulate+` — accepted axiomatically. - Idris2
+`+believe_me+`/`+assert_total+` — runtime-safe coercion / totality
+assumption. - Idris2 top-level `+partial+` — totality-check waived. - F*
+`+assume val+`/`+admit_p+` — F* admit. - `+TODO PROOF+` / `+OWED:+` —
+self-documented debt markers. - `+unsafePerformIO+`/`+unsafeCoerce+` —
+soundness-relevant escape hatches in Haskell/Rust source.
+
+*Recommended next move:* triage each finding into one of: (a) discharge
+by proof, (b) cover with property-tests + a documented refutation
+budget, or (c) annotate as a known/necessary axiom (e.g. `+funExt+`) in
+`+docs/proof-debt.md+`.
+
+=== 2. Licence debt
+
+[cols=",",options="header",]
+|===
+|Field |Value
+|LICENSE file |`+LICENSE+`
+|SPDX header |`+MPL-2.0+`
+|Manifest licence |`+MPL-2.0+`
+|Body classifier |`+Palimp-MPL-2.0+`
+|Severity |`+ok+`
+|===
+
+*Recommended next move:* none for licence.
+
+=== 3. Documentation debt
+
+[cols=",",options="header",]
+|===
+|Field |Value
+|README lines |213
+|`+docs/+` files |65
+|`+docs/+` LoC |6613
+|CHANGELOG.md |Y
+|CONTRIBUTING.md |Y
+|CODE_OF_CONDUCT.md |Y
+|SECURITY.md |Y
+|Severity |`+OK+`
+|===
+
+*Recommended next move:* none for docs.
+
+=== Cross-references
+
+* Estate proof-debt audit:
+`+hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md+`
+* Estate licence-debt audit:
+`+hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md+`
+* Estate documentation-debt audit:
+`+hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md+`
+
+'''''
+
+🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26).
+This file is informational — closing the debt is follow-up work owned by
+the maintainer.
diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md
deleted file mode 100644
index b12a962..0000000
--- a/docs/tech-debt-2026-05-26.md
+++ /dev/null
@@ -1,71 +0,0 @@
-<!--
-SPDX-License-Identifier: CC-BY-SA-4.0
-SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
--->
-
-# Tech-Debt Audit — vcl-ut — 2026-05-26
-
-**Source:** estate-wide automated scan 2026-05-26.
-**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits).
-**Combined severity:** `MEDIUM`.
-
-This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work.
-
-## 1. Proof debt
-
-Scanner counted the following markers in proof-bearing files of this repo:
-
-```
-files=   16 | Coq-Axm/Adm=   0 | Lean-srry/ax=   0 | Agda-pst=   0 | Idr-blv=   8 | Idr-prtl=   0 | Fstr-asm=  0 | TODO= 14 | Unsafe=  0
-```
-
-**Total markers:** 22. **Severity:** `>022`.
-
-**Marker types** (any non-zero counts above):
-- Coq `Axiom`/`Admitted` — unconditional proof escapes.
-- Lean `sorry`/`axiom` — Lean's equivalent.
-- Agda `postulate` — accepted axiomatically.
-- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption.
-- Idris2 top-level `partial` — totality-check waived.
-- F\* `assume val`/`admit_p` — F\* admit.
-- `TODO PROOF` / `OWED:` — self-documented debt markers.
-- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source.
-
-**Recommended next move:** triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`.
-
-## 2. Licence debt
-
-| Field | Value |
-|---|---|
-| LICENSE file | `LICENSE` |
-| SPDX header | `MPL-2.0` |
-| Manifest licence | `MPL-2.0` |
-| Body classifier | `Palimp-MPL-2.0` |
-| Severity | `ok` |
-
-**Recommended next move:** none for licence.
-
-## 3. Documentation debt
-
-| Field | Value |
-|---|---|
-| README lines | 213 |
-| `docs/` files | 65 |
-| `docs/` LoC | 6613 |
-| CHANGELOG.md | Y |
-| CONTRIBUTING.md | Y |
-| CODE_OF_CONDUCT.md | Y |
-| SECURITY.md | Y |
-| Severity | `OK` |
-
-**Recommended next move:** none for docs.
-
-## Cross-references
-
-- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md`
-- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md`
-- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md`
-
----
-
-🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer.