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.