From c1c21081200e7affd7795ef446cc92e6cbfecbe8 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sat, 13 Jun 2026 13:27:43 +0000
Subject: [PATCH] =?UTF-8?q?docs(#84):=20VCL=20rename=20stage=20A=20?=
 =?UTF-8?q?=E2=80=94=20reframe=20language=20prose,=20rename=209=20vql-*=20?=
 =?UTF-8?q?doc=20files,=20add=20doc-drift=20gate?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Build-safe (docs only). 'VeriSim Query Language' -> 'VeriSim Consonance Language' across all docs (now 0); the 9 renamed spec/grammar files fully VCL-ified. git mv vql-*.adoc/.ebnf -> vcl-*; fixed every link incl. doc-path refs in comments/scripts (formal/VCL.v, src/vql/VQLTypes.res, vql_e2e_test.exs describe-strings, sync-wiki.sh) — NO code symbols renamed. Added tests/doc-consonance-gate.sh + .github/workflows/doc-consonance.yml (fail-closed misnomer guard; SHA-pinned checkout + permissions + timeout).

Deferred to later staged chunks: bare 'VQL' token sweep (CHANGELOG/ANCHOR/grammar history, openapi/seed/playground) and code-symbol renames (vql_*, /api/v1/vql/execute, .vql fixtures) via re-export shims with cargo/mix verification.

https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME
---
 .claude/CLAUDE.md                             |   2 +-
 .github/workflows/doc-consonance.yml          |  19 +++
 .machine_readable/6a2/NEUROSYM.a2ml           |   2 +-
 .machine_readable/anchors/ANCHOR.a2ml         |   2 +-
 .../cross-thread-quarantine.a2ml              |   4 +-
 .../contractiles/must/Mustfile.a2ml           |   4 +-
 .verisimdb/octads/commit-0ca572654610.json    |   2 +-
 .verisimdb/octads/commit-3da4daef75f9.json    |   2 +-
 .verisimdb/octads/commit-529b85ff223e.json    |   2 +-
 .verisimdb/octads/commit-74f45a7491e2.json    |   2 +-
 .verisimdb/octads/commit-7b8c073708d5.json    |   2 +-
 .verisimdb/octads/commit-8cd1f416878e.json    |   2 +-
 .verisimdb/octads/commit-9746771f7457.json    |   2 +-
 .verisimdb/octads/commit-9d353c5546f5.json    |   2 +-
 .verisimdb/octads/commit-aa63510d99bd.json    |   2 +-
 .verisimdb/octads/commit-d7a13170c87c.json    |   2 +-
 .verisimdb/octads/commit-d8593016e679.json    |   2 +-
 .verisimdb/octads/commit-de2fd383992a.json    |   2 +-
 .verisimdb/octads/commit-e6dbf191a423.json    |   2 +-
 .verisimdb/octads/commit-e84118929733.json    |   2 +-
 .verisimdb/octads/issue-005.json              |   2 +-
 .verisimdb/octads/issue-021.json              |   2 +-
 CONTRIBUTING.md                               |   2 +-
 EXPLAINME.adoc                                |   6 +-
 KNOWN-ISSUES.adoc                             |  10 +-
 README.adoc                                   |  18 +--
 ROADMAP.md                                    |   2 +-
 debugger/.claude/CLAUDE.md                    |   6 +-
 docs/INDEX.md                                 |  18 +--
 docs/{VQL-SPEC.adoc => VCL-SPEC.adoc}         | 134 +++++++++---------
 docs/adoption-strategy.adoc                   |  18 +--
 docs/architecture/topology.md                 |   2 +-
 docs/business/business-case.adoc              |  14 +-
 docs/business/marketing/one-pager.adoc        |   4 +-
 .../marketing/pitch-deck-outline.adoc         |   8 +-
 docs/business/pr/faq.adoc                     |  20 +--
 docs/business/pr/key-messages.adoc            |  10 +-
 docs/business/pr/press-release.adoc           |   2 +-
 docs/business/strategy/adoption-roadmap.adoc  |   6 +-
 .../business/strategy/economics-analysis.adoc |   4 +-
 docs/business/strategy/functional-units.adoc  |   4 +-
 docs/business/strategy/go-to-market.adoc      |   6 +-
 docs/cache-sharing-strategy.adoc              |   2 +-
 docs/caching-strategy.adoc                    |   2 +-
 docs/consultation-dependent-types-zkp.adoc    |   2 +-
 ...IGN-2026-02-27-strategic-improvements.adoc |  30 ++--
 ... DESIGN-2026-02-27-vcl-dt-assessment.adoc} |  56 ++++----
 ...SIGN-2026-02-28-panll-interop-telemetry.md |   4 +-
 docs/error-handling-strategy.adoc             |   2 +-
 docs/federation-readiness.adoc                |   8 +-
 docs/getting-started.adoc                     |  12 +-
 docs/panll-module-audit.adoc                  |   2 +-
 docs/papers/arcvix-octad-data-model.tex       |   4 +-
 .../verisimdb-federated-consistency.adoc      |  36 ++---
 docs/query-optimization-overview.adoc         |   4 +-
 docs/reversibility-design.adoc                |   2 +-
 docs/safety-and-fault-tolerance.adoc          |   2 +-
 ...rchitecture.adoc => vcl-architecture.adoc} |  30 ++--
 docs/{vql-examples.adoc => vcl-examples.adoc} |  16 +--
 ...mantics.adoc => vcl-formal-semantics.adoc} |  14 +-
 docs/{vql-grammar.ebnf => vcl-grammar.ebnf}   |   4 +-
 ...-type-system.adoc => vcl-type-system.adoc} |  18 +--
 docs/{vql-vs-sql.adoc => vcl-vs-sql.adoc}     |  46 +++---
 ...{vql-vs-vql-dt.adoc => vcl-vs-vcl-dt.adoc} |  52 +++----
 .../test/verisim/query/vql_e2e_test.exs       |   8 +-
 formal/VCL.v                                  |   2 +-
 spec/grammar.ebnf                             |   2 +-
 src/vql/VQLTypes.res                          |   2 +-
 sync-wiki.sh                                  |  10 +-
 tests/doc-consonance-gate.sh                  |  35 +++++
 70 files changed, 410 insertions(+), 356 deletions(-)
 create mode 100644 .github/workflows/doc-consonance.yml
 rename docs/{VQL-SPEC.adoc => VCL-SPEC.adoc} (95%)
 rename docs/design/{DESIGN-2026-02-27-vql-dt-assessment.adoc => DESIGN-2026-02-27-vcl-dt-assessment.adoc} (93%)
 rename docs/{vql-architecture.adoc => vcl-architecture.adoc} (95%)
 rename docs/{vql-examples.adoc => vcl-examples.adoc} (98%)
 rename docs/{vql-formal-semantics.adoc => vcl-formal-semantics.adoc} (97%)
 rename docs/{vql-grammar.ebnf => vcl-grammar.ebnf} (99%)
 rename docs/{vql-type-system.adoc => vcl-type-system.adoc} (97%)
 rename docs/{vql-vs-sql.adoc => vcl-vs-sql.adoc} (85%)
 rename docs/{vql-vs-vql-dt.adoc => vcl-vs-vcl-dt.adoc} (86%)
 create mode 100755 tests/doc-consonance-gate.sh

diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 5048785..3ccab9f 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -336,7 +336,7 @@ User prompt → Haiku classifier → Route to:
 See `KNOWN-ISSUES.adoc` at repo root for all honest gaps. All 25 issues resolved.
 
 Resolved in recent sessions:
-- VQL-DT type checker wired end-to-end (Elixir-native + ReScript + Rust ZKP bridge)
+- VCL-DT type checker wired end-to-end (Elixir-native + ReScript + Rust ZKP bridge)
 - 11 proof types: EXISTENCE, INTEGRITY, CONSISTENCY, PROVENANCE, FRESHNESS, ACCESS, CITATION, CUSTOM, ZKP, PROVEN, SANCTIFY
 - Multi-proof parsing: PROOF A(x) AND B(y) splits correctly
 - Modality compatibility validation (INTEGRITY needs semantic, PROVENANCE needs provenance, etc.)
diff --git a/.github/workflows/doc-consonance.yml b/.github/workflows/doc-consonance.yml
new file mode 100644
index 0000000..14b70d1
--- /dev/null
+++ b/.github/workflows/doc-consonance.yml
@@ -0,0 +1,19 @@
+# SPDX-License-Identifier: MPL-2.0
+name: Doc Consonance Gate
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+permissions:
+  contents: read
+
+jobs:
+  doc-consonance:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      - name: Doc-consonance gate (no query-language misnomer in docs)
+        run: bash tests/doc-consonance-gate.sh
diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/6a2/NEUROSYM.a2ml
index eeb1f34..8a9f030 100644
--- a/.machine_readable/6a2/NEUROSYM.a2ml
+++ b/.machine_readable/6a2/NEUROSYM.a2ml
@@ -19,7 +19,7 @@
          (("formal/VCL.v"            . "N2 normalize_idempotent + V2 vql_preservation"))
          (("formal/WAL.v"            . "C7 wal_replay_idempotent on observable state")))
        (idris2-bridge
-         ((path . "VQL-DT type checker via Elixir-native + ReScript + Rust ZKP bridge")
+         ((path . "VCL-DT type checker via Elixir-native + ReScript + Rust ZKP bridge")
           (proof-types . ("EXISTENCE" "INTEGRITY" "CONSISTENCY" "PROVENANCE" "FRESHNESS"
                            "ACCESS" "CITATION" "CUSTOM" "ZKP" "PROVEN" "SANCTIFY"))))))
 
diff --git a/.machine_readable/anchors/ANCHOR.a2ml b/.machine_readable/anchors/ANCHOR.a2ml
index 09ba95c..d674189 100644
--- a/.machine_readable/anchors/ANCHOR.a2ml
+++ b/.machine_readable/anchors/ANCHOR.a2ml
@@ -42,7 +42,7 @@ semantic-authority:
   owns:
     - "Octad entity model and cross-modal consistency semantics"
     - "Drift-detection thresholds and self-normalisation behaviour"
-    - "VQL (VeriSim Query Language) syntax, type system, and proof obligations"
+    - "VQL (VeriSim Consonance Language) syntax, type system, and proof obligations"
     - "Contractile invariant definitions (.machine_readable/contractiles/)"
   authoritative-files:
     formal-proofs: "formal/ (Coq: Drift.v, Normalizer.v, Provenance.v, Transaction.v, WAL.v, Planner.v, VCL.v)"
diff --git a/.machine_readable/bot_directives/cross-thread-quarantine.a2ml b/.machine_readable/bot_directives/cross-thread-quarantine.a2ml
index 981eee3..bfba1b3 100644
--- a/.machine_readable/bot_directives/cross-thread-quarantine.a2ml
+++ b/.machine_readable/bot_directives/cross-thread-quarantine.a2ml
@@ -13,7 +13,7 @@ bot = "cross-thread-quarantine"
 scope = "inbound artifacts from sibling agent threads: CLAUDE.md edits, migration directives, ADRs, roadmap items, plans, comparative-corpus columns"
 rule = "QUARANTINE every inbound cross-thread artifact as proposed-unverified until checked against this repo's own spec."
 
-verify-against = ["README.adoc", "EXPLAINME.adoc", "docs/VQL-SPEC.adoc"]
+verify-against = ["README.adoc", "EXPLAINME.adoc", "docs/VCL-SPEC.adoc"]
 provenance-tags = ["user-directed", "derived", "proposed-unverified"]
 
 must = [
@@ -28,4 +28,4 @@ deny = [
   "Write source-of-truth docs from an unverified cross-thread model, or present invented architecture as decided.",
 ]
 
-notes = "Doc-drift gate (a CI grep banning 'query language'/'queryable store'/CRUD framing in VCL-subject docs) is the FINISH LINE of the consonance reframing — add it once ANCHOR, the spec/grammar, VQL-SPEC.adoc and ADRs are reworded, else it red-CIs on legacy residue."
+notes = "Doc-drift gate (a CI grep banning 'query language'/'queryable store'/CRUD framing in VCL-subject docs) is the FINISH LINE of the consonance reframing — add it once ANCHOR, the spec/grammar, VCL-SPEC.adoc and ADRs are reworded, else it red-CIs on legacy residue."
diff --git a/.machine_readable/contractiles/must/Mustfile.a2ml b/.machine_readable/contractiles/must/Mustfile.a2ml
index 35123fe..2cdcf85 100644
--- a/.machine_readable/contractiles/must/Mustfile.a2ml
+++ b/.machine_readable/contractiles/must/Mustfile.a2ml
@@ -77,7 +77,7 @@ These are hard requirements: CI and pre-commit hooks fail if any check fails.
 - run: test -f .editorconfig
 - severity: warning
 
-## VQL (VeriSim Query Language)
+## VQL (VeriSim Consonance Language)
 
 ### vql-rescript-parser
 - description: ReScript VQL parser source must exist
@@ -89,7 +89,7 @@ These are hard requirements: CI and pre-commit hooks fail if any check fails.
 - run: test -f elixir-orchestration/lib/verisim/query/vql_bridge.ex
 - severity: high
 
-### vql-examples-present
+### vcl-examples-present
 - description: At least one .vql example/fixture must exist
 - run: test -n "$(find . -name '*.vql' -not -path '*/.git/*' 2>/dev/null)"
 - severity: warning
diff --git a/.verisimdb/octads/commit-0ca572654610.json b/.verisimdb/octads/commit-0ca572654610.json
index 5403120..013c4f4 100644
--- a/.verisimdb/octads/commit-0ca572654610.json
+++ b/.verisimdb/octads/commit-0ca572654610.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"}]
+    "relationships": [{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"}]
   },
   "vector": {
     "embedding": [-1.000000,0.898437,0.078125,-0.656250,0.742187,-0.562500,0.210937,0.320312,-0.031250,0.429687,-0.757812,0.234375,-0.375000,-0.859375,-0.757812,-0.281250,-0.421875,-0.031250,0.179687,-0.640625,-0.101562,-0.054687,0.289062,-0.992187,-0.031250,0.125000,-0.742187,0.328125,-0.093750,0.539062,0.375000,0.187500,-1.000000,0.898437,0.078125,-0.656250,0.742187,-0.562500,0.210937,0.320312,-0.031250,0.429687,-0.757812,0.234375,-0.375000,-0.859375,-0.757812,-0.281250,-0.421875,-0.031250,0.179687,-0.640625,-0.101562,-0.054687,0.289062,-0.992187,-0.031250,0.125000,-0.742187,0.328125,-0.093750,0.539062,0.375000,0.187500],
diff --git a/.verisimdb/octads/commit-3da4daef75f9.json b/.verisimdb/octads/commit-3da4daef75f9.json
index 5fe5712..c08b0d6 100644
--- a/.verisimdb/octads/commit-3da4daef75f9.json
+++ b/.verisimdb/octads/commit-3da4daef75f9.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"}]
+    "relationships": [{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"}]
   },
   "vector": {
     "embedding": [-0.242187,-0.656250,-0.242187,0.976562,-0.578125,0.734375,0.843750,-0.843750,-0.281250,-0.234375,-0.718750,0.757812,-0.242187,0.828125,0.500000,-0.882812,-0.070312,0.078125,-0.726562,-0.187500,-0.304687,-0.515625,-0.820312,-0.132812,-0.101562,0.367187,0.703125,0.484375,0.914062,0.789062,-0.718750,-0.953125,-0.242187,-0.656250,-0.242187,0.976562,-0.578125,0.734375,0.843750,-0.843750,-0.281250,-0.234375,-0.718750,0.757812,-0.242187,0.828125,0.500000,-0.882812,-0.070312,0.078125,-0.726562,-0.187500,-0.304687,-0.515625,-0.820312,-0.132812,-0.101562,0.367187,0.703125,0.484375,0.914062,0.789062,-0.718750,-0.953125],
diff --git a/.verisimdb/octads/commit-529b85ff223e.json b/.verisimdb/octads/commit-529b85ff223e.json
index 5b3802e..c11a843 100644
--- a/.verisimdb/octads/commit-529b85ff223e.json
+++ b/.verisimdb/octads/commit-529b85ff223e.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:.claude/CLAUDE.md"},{"predicate":"modifies","target":"file:.machine_readable/STATE.scm"},{"predicate":"modifies","target":"file:KNOWN-ISSUES.adoc"},{"predicate":"modifies","target":"file:debugger/Cargo.toml"},{"predicate":"modifies","target":"file:docs/federation-readiness.adoc"},{"predicate":"modifies","target":"file:docs/vql-vs-sql.adoc"},{"predicate":"modifies","target":"file:docs/vql-vs-vql-dt.adoc"}]
+    "relationships": [{"predicate":"modifies","target":"file:.claude/CLAUDE.md"},{"predicate":"modifies","target":"file:.machine_readable/STATE.scm"},{"predicate":"modifies","target":"file:KNOWN-ISSUES.adoc"},{"predicate":"modifies","target":"file:debugger/Cargo.toml"},{"predicate":"modifies","target":"file:docs/federation-readiness.adoc"},{"predicate":"modifies","target":"file:docs/vcl-vs-sql.adoc"},{"predicate":"modifies","target":"file:docs/vcl-vs-vcl-dt.adoc"}]
   },
   "vector": {
     "embedding": [-0.710937,0.031250,-0.835937,-0.117187,0.476562,-0.562500,0.054687,0.851562,-0.835937,-0.539062,0.781250,0.304687,-0.250000,-0.898437,0.468750,0.562500,-0.398437,-0.664062,0.343750,-0.593750,-0.132812,-0.078125,0,-0.718750,0.867187,-0.390625,-0.773437,0.531250,0.804687,-1.000000,-0.507812,-0.171875,-0.710937,0.031250,-0.835937,-0.117187,0.476562,-0.562500,0.054687,0.851562,-0.835937,-0.539062,0.781250,0.304687,-0.250000,-0.898437,0.468750,0.562500,-0.398437,-0.664062,0.343750,-0.593750,-0.132812,-0.078125,0,-0.718750,0.867187,-0.390625,-0.773437,0.531250,0.804687,-1.000000,-0.507812,-0.171875],
diff --git a/.verisimdb/octads/commit-74f45a7491e2.json b/.verisimdb/octads/commit-74f45a7491e2.json
index 2e8f837..369babd 100644
--- a/.verisimdb/octads/commit-74f45a7491e2.json
+++ b/.verisimdb/octads/commit-74f45a7491e2.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"}]
+    "relationships": [{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"}]
   },
   "vector": {
     "embedding": [0.437500,-0.914062,-0.062500,-0.132812,-0.312500,0.921875,-0.476562,-0.335937,-0.054687,0.171875,-0.273437,0.882812,-0.648437,-0.406250,0.390625,-0.046875,0.085937,0.593750,-0.914062,0.906250,-0.578125,-0.437500,-0.312500,-0.437500,0.664062,0.539062,0.671875,-0.085937,0.960937,0.992187,-0.375000,0.359375,0.437500,-0.914062,-0.062500,-0.132812,-0.312500,0.921875,-0.476562,-0.335937,-0.054687,0.171875,-0.273437,0.882812,-0.648437,-0.406250,0.390625,-0.046875,0.085937,0.593750,-0.914062,0.906250,-0.578125,-0.437500,-0.312500,-0.437500,0.664062,0.539062,0.671875,-0.085937,0.960937,0.992187,-0.375000,0.359375],
diff --git a/.verisimdb/octads/commit-7b8c073708d5.json b/.verisimdb/octads/commit-7b8c073708d5.json
index 37480e0..62bc89c 100644
--- a/.verisimdb/octads/commit-7b8c073708d5.json
+++ b/.verisimdb/octads/commit-7b8c073708d5.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:README.adoc"},{"predicate":"modifies","target":"file:docs/error-handling-strategy.adoc"},{"predicate":"modifies","target":"file:docs/vql-formal-semantics.adoc"},{"predicate":"modifies","target":"file:docs/vql-type-system.adoc"}]
+    "relationships": [{"predicate":"modifies","target":"file:README.adoc"},{"predicate":"modifies","target":"file:docs/error-handling-strategy.adoc"},{"predicate":"modifies","target":"file:docs/vcl-formal-semantics.adoc"},{"predicate":"modifies","target":"file:docs/vcl-type-system.adoc"}]
   },
   "vector": {
     "embedding": [0.281250,-0.484375,0.898437,0.820312,-0.945312,-0.960937,0.976562,0.031250,0.984375,0.664062,-0.734375,0.226562,-0.882812,0.851562,-0.703125,0.601562,0.406250,0.140625,0.812500,0.703125,-0.101562,-0.671875,-0.070312,0.187500,-0.531250,0.023437,-0.234375,0.039062,-0.882812,0.773437,-0.546875,0.585937,0.281250,-0.484375,0.898437,0.820312,-0.945312,-0.960937,0.976562,0.031250,0.984375,0.664062,-0.734375,0.226562,-0.882812,0.851562,-0.703125,0.601562,0.406250,0.140625,0.812500,0.703125,-0.101562,-0.671875,-0.070312,0.187500,-0.531250,0.023437,-0.234375,0.039062,-0.882812,0.773437,-0.546875,0.585937],
diff --git a/.verisimdb/octads/commit-8cd1f416878e.json b/.verisimdb/octads/commit-8cd1f416878e.json
index 525582a..5eb148c 100644
--- a/.verisimdb/octads/commit-8cd1f416878e.json
+++ b/.verisimdb/octads/commit-8cd1f416878e.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:README.adoc"},{"predicate":"modifies","target":"file:docs/vql-architecture.adoc"},{"predicate":"modifies","target":"file:docs/vql-examples.adoc"},{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"},{"predicate":"modifies","target":"file:src/vql/VQLParser.res"},{"predicate":"modifies","target":"file:src/vql/VQLParser_test.res"}]
+    "relationships": [{"predicate":"modifies","target":"file:README.adoc"},{"predicate":"modifies","target":"file:docs/vcl-architecture.adoc"},{"predicate":"modifies","target":"file:docs/vcl-examples.adoc"},{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"},{"predicate":"modifies","target":"file:src/vql/VQLParser.res"},{"predicate":"modifies","target":"file:src/vql/VQLParser_test.res"}]
   },
   "vector": {
     "embedding": [0.046875,0.351562,-0.851562,-0.640625,0.164062,0.132812,0.023437,0.039062,0.601562,-0.210937,-0.210937,0.718750,-0.195312,0.156250,0.546875,0.601562,0,0.328125,-0.046875,-0.367187,-0.117187,-0.781250,0.992187,-0.414062,-0.750000,0.476562,-0.187500,0.820312,0.890625,-0.593750,0.078125,-0.703125,0.046875,0.351562,-0.851562,-0.640625,0.164062,0.132812,0.023437,0.039062,0.601562,-0.210937,-0.210937,0.718750,-0.195312,0.156250,0.546875,0.601562,0,0.328125,-0.046875,-0.367187,-0.117187,-0.781250,0.992187,-0.414062,-0.750000,0.476562,-0.187500,0.820312,0.890625,-0.593750,0.078125,-0.703125],
diff --git a/.verisimdb/octads/commit-9746771f7457.json b/.verisimdb/octads/commit-9746771f7457.json
index 7b3e3a8..486a432 100644
--- a/.verisimdb/octads/commit-9746771f7457.json
+++ b/.verisimdb/octads/commit-9746771f7457.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"}]
+    "relationships": [{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"}]
   },
   "vector": {
     "embedding": [0.484375,-0.632812,0.320312,0.679687,-0.578125,-0.906250,0.429687,-0.093750,0.156250,0.179687,0.585937,-0.578125,-0.195312,0.937500,0.859375,-0.656250,-0.968750,0.968750,-0.078125,0.125000,0.835937,0.750000,-0.835937,-0.515625,-0.164062,0.421875,0.492187,0.070312,0.984375,0.546875,0.609375,0.351562,0.484375,-0.632812,0.320312,0.679687,-0.578125,-0.906250,0.429687,-0.093750,0.156250,0.179687,0.585937,-0.578125,-0.195312,0.937500,0.859375,-0.656250,-0.968750,0.968750,-0.078125,0.125000,0.835937,0.750000,-0.835937,-0.515625,-0.164062,0.421875,0.492187,0.070312,0.984375,0.546875,0.609375,0.351562],
diff --git a/.verisimdb/octads/commit-9d353c5546f5.json b/.verisimdb/octads/commit-9d353c5546f5.json
index 8a5843a..1033d0a 100644
--- a/.verisimdb/octads/commit-9d353c5546f5.json
+++ b/.verisimdb/octads/commit-9d353c5546f5.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:README.adoc"},{"predicate":"modifies","target":"file:docs/vql-examples.adoc"}]
+    "relationships": [{"predicate":"modifies","target":"file:README.adoc"},{"predicate":"modifies","target":"file:docs/vcl-examples.adoc"}]
   },
   "vector": {
     "embedding": [-0.781250,0.835937,0.734375,0.820312,0.851562,0.531250,0.414062,-0.710937,-0.742187,-0.359375,-0.710937,0.859375,0.992187,-0.210937,0.593750,-0.054687,0.679687,0.164062,-0.898437,-0.796875,-0.546875,-0.140625,0.890625,0.703125,-0.765625,-0.632812,0.953125,0.929687,-0.250000,0.828125,-0.250000,-0.218750,-0.781250,0.835937,0.734375,0.820312,0.851562,0.531250,0.414062,-0.710937,-0.742187,-0.359375,-0.710937,0.859375,0.992187,-0.210937,0.593750,-0.054687,0.679687,0.164062,-0.898437,-0.796875,-0.546875,-0.140625,0.890625,0.703125,-0.765625,-0.632812,0.953125,0.929687,-0.250000,0.828125,-0.250000,-0.218750],
diff --git a/.verisimdb/octads/commit-aa63510d99bd.json b/.verisimdb/octads/commit-aa63510d99bd.json
index 254b99a..c5ca69a 100644
--- a/.verisimdb/octads/commit-aa63510d99bd.json
+++ b/.verisimdb/octads/commit-aa63510d99bd.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"}]
+    "relationships": [{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"}]
   },
   "vector": {
     "embedding": [0.007812,-0.132812,0.257812,0.789062,-0.007812,-0.132812,-0.890625,0.164062,0.312500,-0.046875,0.296875,0.328125,0.726562,-0.609375,0.312500,0.054687,-0.218750,0.679687,0.687500,-0.453125,0.523437,-0.859375,-0.875000,-0.500000,-0.382812,0.281250,0.335937,0.468750,0.351562,-0.914062,-0.796875,0.375000,0.007812,-0.132812,0.257812,0.789062,-0.007812,-0.132812,-0.890625,0.164062,0.312500,-0.046875,0.296875,0.328125,0.726562,-0.609375,0.312500,0.054687,-0.218750,0.679687,0.687500,-0.453125,0.523437,-0.859375,-0.875000,-0.500000,-0.382812,0.281250,0.335937,0.468750,0.351562,-0.914062,-0.796875,0.375000],
diff --git a/.verisimdb/octads/commit-d7a13170c87c.json b/.verisimdb/octads/commit-d7a13170c87c.json
index 839d209..50cb9c4 100644
--- a/.verisimdb/octads/commit-d7a13170c87c.json
+++ b/.verisimdb/octads/commit-d7a13170c87c.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:README.adoc"},{"predicate":"modifies","target":"file:docs/backwards-compatibility.adoc"},{"predicate":"modifies","target":"file:docs/drift-handling.adoc"},{"predicate":"modifies","target":"file:docs/safety-theory-applied.adoc"},{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"},{"predicate":"modifies","target":"file:lib/verisim/adaptive_learner.ex"}]
+    "relationships": [{"predicate":"modifies","target":"file:README.adoc"},{"predicate":"modifies","target":"file:docs/backwards-compatibility.adoc"},{"predicate":"modifies","target":"file:docs/drift-handling.adoc"},{"predicate":"modifies","target":"file:docs/safety-theory-applied.adoc"},{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"},{"predicate":"modifies","target":"file:lib/verisim/adaptive_learner.ex"}]
   },
   "vector": {
     "embedding": [-0.578125,0.734375,0.359375,0.554687,0.632812,-0.968750,0.625000,-0.828125,0.859375,0.851562,0.726562,0.734375,-0.507812,-0.218750,-0.398437,-0.460937,-0.593750,-0.070312,-0.921875,0.953125,0.148437,-0.929687,0.281250,-0.632812,0.914062,-0.328125,0.804687,0.390625,0.625000,-0.054687,0.500000,0.609375,-0.578125,0.734375,0.359375,0.554687,0.632812,-0.968750,0.625000,-0.828125,0.859375,0.851562,0.726562,0.734375,-0.507812,-0.218750,-0.398437,-0.460937,-0.593750,-0.070312,-0.921875,0.953125,0.148437,-0.929687,0.281250,-0.632812,0.914062,-0.328125,0.804687,0.390625,0.625000,-0.054687,0.500000,0.609375],
diff --git a/.verisimdb/octads/commit-d8593016e679.json b/.verisimdb/octads/commit-d8593016e679.json
index 354224f..08f64a9 100644
--- a/.verisimdb/octads/commit-d8593016e679.json
+++ b/.verisimdb/octads/commit-d8593016e679.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"}]
+    "relationships": [{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"}]
   },
   "vector": {
     "embedding": [0.031250,0.429687,0.984375,0.632812,0.593750,-0.445312,0.007812,0.453125,-0.968750,0.109375,0.726562,0.820312,0.484375,0.742187,-0.539062,-0.359375,-0.265625,-0.554687,-0.039062,0.656250,0.937500,0.187500,-0.601562,-0.187500,-0.812500,0.554687,-0.953125,0.421875,-0.085937,-0.031250,-0.304687,0.125000,0.031250,0.429687,0.984375,0.632812,0.593750,-0.445312,0.007812,0.453125,-0.968750,0.109375,0.726562,0.820312,0.484375,0.742187,-0.539062,-0.359375,-0.265625,-0.554687,-0.039062,0.656250,0.937500,0.187500,-0.601562,-0.187500,-0.812500,0.554687,-0.953125,0.421875,-0.085937,-0.031250,-0.304687,0.125000],
diff --git a/.verisimdb/octads/commit-de2fd383992a.json b/.verisimdb/octads/commit-de2fd383992a.json
index 27d9b3c..7e7721f 100644
--- a/.verisimdb/octads/commit-de2fd383992a.json
+++ b/.verisimdb/octads/commit-de2fd383992a.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"}]
+    "relationships": [{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"}]
   },
   "vector": {
     "embedding": [-0.429687,0.445312,0.171875,0.179687,0.367187,0.859375,-0.531250,-0.890625,-0.828125,0.531250,0.179687,0.296875,0.859375,-0.328125,0.906250,0.718750,-0.289062,-0.328125,0.710937,0.320312,0.085937,0.414062,0.734375,-0.953125,0.679687,0.320312,0.953125,0.960937,0.828125,-0.968750,-0.945312,-0.968750,-0.429687,0.445312,0.171875,0.179687,0.367187,0.859375,-0.531250,-0.890625,-0.828125,0.531250,0.179687,0.296875,0.859375,-0.328125,0.906250,0.718750,-0.289062,-0.328125,0.710937,0.320312,0.085937,0.414062,0.734375,-0.953125,0.679687,0.320312,0.953125,0.960937,0.828125,-0.968750,-0.945312,-0.968750],
diff --git a/.verisimdb/octads/commit-e6dbf191a423.json b/.verisimdb/octads/commit-e6dbf191a423.json
index 9e7cdf2..8621bb6 100644
--- a/.verisimdb/octads/commit-e6dbf191a423.json
+++ b/.verisimdb/octads/commit-e6dbf191a423.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"}]
+    "relationships": [{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"}]
   },
   "vector": {
     "embedding": [-0.195312,-0.765625,-0.445312,-0.937500,0.929687,-0.906250,0.210937,-0.117187,0.046875,-0.828125,0.062500,-0.640625,0.640625,-0.453125,0.312500,-0.453125,-0.429687,-0.835937,0.234375,0.609375,-0.804687,0.421875,0.867187,-0.070312,-0.328125,-0.382812,-0.226562,-0.664062,0.804687,-0.148437,0.414062,-0.906250,-0.195312,-0.765625,-0.445312,-0.937500,0.929687,-0.906250,0.210937,-0.117187,0.046875,-0.828125,0.062500,-0.640625,0.640625,-0.453125,0.312500,-0.453125,-0.429687,-0.835937,0.234375,0.609375,-0.804687,0.421875,0.867187,-0.070312,-0.328125,-0.382812,-0.226562,-0.664062,0.804687,-0.148437,0.414062,-0.906250],
diff --git a/.verisimdb/octads/commit-e84118929733.json b/.verisimdb/octads/commit-e84118929733.json
index cf22bc7..bccbc45 100644
--- a/.verisimdb/octads/commit-e84118929733.json
+++ b/.verisimdb/octads/commit-e84118929733.json
@@ -14,7 +14,7 @@
     }
   },
   "graph": {
-    "relationships": [{"predicate":"modifies","target":"file:docs/vql-grammar.ebnf"}]
+    "relationships": [{"predicate":"modifies","target":"file:docs/vcl-grammar.ebnf"}]
   },
   "vector": {
     "embedding": [0.937500,0.406250,0.671875,-0.429687,-0.226562,-0.507812,-0.398437,-0.742187,0.500000,0.226562,-0.015625,0.750000,-0.992187,0.085937,-0.015625,-0.523437,-0.023437,-0.523437,-0.789062,0.507812,0.164062,-0.085937,0.640625,0.437500,-0.421875,-0.843750,-0.921875,0.375000,0.523437,0.640625,0.953125,0.132812,0.937500,0.406250,0.671875,-0.429687,-0.226562,-0.507812,-0.398437,-0.742187,0.500000,0.226562,-0.015625,0.750000,-0.992187,0.085937,-0.015625,-0.523437,-0.023437,-0.523437,-0.789062,0.507812,0.164062,-0.085937,0.640625,0.437500,-0.421875,-0.843750,-0.921875,0.375000,0.523437,0.640625,0.953125,0.132812],
diff --git a/.verisimdb/octads/issue-005.json b/.verisimdb/octads/issue-005.json
index 6f1f63b..20cc233 100644
--- a/.verisimdb/octads/issue-005.json
+++ b/.verisimdb/octads/issue-005.json
@@ -4,7 +4,7 @@
   "created_at": "2026-02-13T16:19:58Z",
   "document": {
     "title": "VQL-DT Not Connected to VQL PROOF Runtime",
-    "body": "\\n**Location:** `vql-dt/` (Lean type definitions), VQL query router\\n\\n**Current state:** Lean type definitions exist in the `vql-dt/` directory specifying dependent type contracts for all six PROOF types (EXISTENCE, INTEGRITY, CONSISTENCY, PROVENANCE, FRESHNESS, AUTHORIZATION). The VQL parser correctly parses `PROOF` clauses and the query router routes to the dependent-type execution path. However, the Lean type checker is not invoked at runtime. VQL-DT queries execute but do not generate real proof certificates.\\n\\n**Impact:** The `PROOF` clause is syntactically supported but semantically inert. Queries with `PROOF` clauses return data but the accompanying proof certificates are placeholders, not verifiable. This is the gap between the designed architecture and the current implementation.\\n\\n**Resolution:** Wire the Lean type checker into the VQL-DT execution path. This requires: (a) compiling Lean definitions to an executable checker, (b) generating proof obligations from the VQL AST, (c) invoking the checker and collecting proof witnesses from modality stores, (d) assembling and returning verifiable proof certificates. See link:docs/vql-vs-vql-dt.adoc[VQL Slipstream vs VQL-DT] for the phased roadmap.\\n\\n",
+    "body": "\\n**Location:** `vql-dt/` (Lean type definitions), VQL query router\\n\\n**Current state:** Lean type definitions exist in the `vql-dt/` directory specifying dependent type contracts for all six PROOF types (EXISTENCE, INTEGRITY, CONSISTENCY, PROVENANCE, FRESHNESS, AUTHORIZATION). The VQL parser correctly parses `PROOF` clauses and the query router routes to the dependent-type execution path. However, the Lean type checker is not invoked at runtime. VQL-DT queries execute but do not generate real proof certificates.\\n\\n**Impact:** The `PROOF` clause is syntactically supported but semantically inert. Queries with `PROOF` clauses return data but the accompanying proof certificates are placeholders, not verifiable. This is the gap between the designed architecture and the current implementation.\\n\\n**Resolution:** Wire the Lean type checker into the VQL-DT execution path. This requires: (a) compiling Lean definitions to an executable checker, (b) generating proof obligations from the VQL AST, (c) invoking the checker and collecting proof witnesses from modality stores, (d) assembling and returning verifiable proof certificates. See link:docs/vcl-vs-vcl-dt.adoc[VQL Slipstream vs VQL-DT] for the phased roadmap.\\n\\n",
     "fields": {
       "type": "known_issue",
       "status": "unknown",
diff --git a/.verisimdb/octads/issue-021.json b/.verisimdb/octads/issue-021.json
index 828646a..2421e77 100644
--- a/.verisimdb/octads/issue-021.json
+++ b/.verisimdb/octads/issue-021.json
@@ -4,7 +4,7 @@
   "created_at": "2026-02-13T16:20:02Z",
   "document": {
     "title": "VQL-DT Not Connected to VQL PROOF Runtime",
-    "body": "\\n**Location:** `vql-dt/` (Lean type definitions), VQL query router\\n\\n**Current state:** Lean type definitions exist specifying dependent type contracts for all six PROOF types. The VQL parser parses `PROOF` clauses and the executor routes proofs through `verify_single_proof/1` which validates contract existence. However, the Lean type checker itself is not invoked at runtime. VQL-DT queries execute but proof certificates are not formally verified by the Lean checker.\\n\\n**Impact:** PROOF clauses are semantically checked (contract existence, parameter validation) but not formally verified via the Lean dependent type checker. Custom ZKP circuits work (R1CS verification), but the VQL-DT formal path is not wired.\\n\\n**Resolution:** Wire the Lean type checker into the VQL-DT execution path. See link:docs/vql-vs-vql-dt.adoc[VQL Slipstream vs VQL-DT].\\n\\n",
+    "body": "\\n**Location:** `vql-dt/` (Lean type definitions), VQL query router\\n\\n**Current state:** Lean type definitions exist specifying dependent type contracts for all six PROOF types. The VQL parser parses `PROOF` clauses and the executor routes proofs through `verify_single_proof/1` which validates contract existence. However, the Lean type checker itself is not invoked at runtime. VQL-DT queries execute but proof certificates are not formally verified by the Lean checker.\\n\\n**Impact:** PROOF clauses are semantically checked (contract existence, parameter validation) but not formally verified via the Lean dependent type checker. Custom ZKP circuits work (R1CS verification), but the VQL-DT formal path is not wired.\\n\\n**Resolution:** Wire the Lean type checker into the VQL-DT execution path. See link:docs/vcl-vs-vcl-dt.adoc[VQL Slipstream vs VQL-DT].\\n\\n",
     "fields": {
       "type": "known_issue",
       "status": "open",
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 91da235..a0faa51 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -159,7 +159,7 @@ cargo fmt --check
 | **Rust** | Core database engine, modality stores, CLI tools |
 | **Elixir** | OTP orchestration, distributed coordination |
 | **ReScript** | VQL parser, playground PWA |
-| **VQL** | VeriSim Query Language (query interface) |
+| **VQL** | VeriSim Consonance Language (query interface) |
 
 ### Not Accepted
 
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
index e2a94e3..0f1a286 100644
--- a/EXPLAINME.adoc
+++ b/EXPLAINME.adoc
@@ -8,8 +8,8 @@
 
 This is the human-readable orientation. For the feature/benefit framing see
 link:README.adoc[README.adoc]; for the normative VCL grammar see
-link:docs/VQL-SPEC.adoc[the VCL specification] (file still historically named
-`VQL-SPEC.adoc`).
+link:docs/VCL-SPEC.adoc[the VCL specification] (file still historically named
+`VCL-SPEC.adoc`).
 
 toc::[]
 
@@ -125,6 +125,6 @@ traceable, authorised, and consonant enough to affect live state.
 == Where to go next
 
 * link:README.adoc[README.adoc] — capabilities, comparisons, quick start.
-* link:docs/VQL-SPEC.adoc[VCL specification] — normative grammar (historically `VQL-SPEC.adoc`).
+* link:docs/VCL-SPEC.adoc[VCL specification] — normative grammar (historically `VCL-SPEC.adoc`).
 * https://github.com/hyperpolymath/vcl-ut[vcl-ut] — VCL-total, the proof-bearing substrate.
 * link:KNOWN-ISSUES.adoc[KNOWN-ISSUES.adoc] — honest-gaps audit.
diff --git a/KNOWN-ISSUES.adoc b/KNOWN-ISSUES.adoc
index e938a9c..8dbc03c 100644
--- a/KNOWN-ISSUES.adoc
+++ b/KNOWN-ISSUES.adoc
@@ -50,11 +50,11 @@ VeriSimDB is a working system with real implementations in its core modality sto
 
 **Original issue:** Drift detection had to be triggered manually. No scheduled or event-driven trigger existed.
 
-=== 5. VQL-DT Not Connected to VQL PROOF Runtime — ✅ RESOLVED
+=== 5. VCL-DT Not Connected to VQL PROOF Runtime — ✅ RESOLVED
 
 **Location:** `elixir-orchestration/lib/verisim/query/vql_type_checker.ex`, `vql_executor.ex`, `vql_bridge.ex`
 
-**Resolved:** 2026-02-28. VQL-DT proof pipeline is now fully wired end-to-end with a three-tier type checking strategy:
+**Resolved:** 2026-02-28. VCL-DT proof pipeline is now fully wired end-to-end with a three-tier type checking strategy:
 
 1. **ReScript bidirectional type checker** (VQLBidir.res, 852 lines) — full formal system with subtyping, invoked via VQLBridge.typecheck/2 when Deno subprocess available
 2. **Elixir-native type checker** (VQLTypeChecker, 320 lines) — validates proof types, modality compatibility, composition rules; generates structured obligations with witness fields and circuit names. Used when ReScript subprocess unavailable.
@@ -82,7 +82,7 @@ Additionally:
 - VQL type checker (`vql_type_checker.ex`) registers `ZKP` and `SANCTIFY` as first-class proof types with modality compatibility (`semantic`), required witness fields, and circuit names (`zkp-base`, `sanctify-v1`).
 - VQL executor (`vql_executor.ex`) routes `PROOF ZKP(...)` queries to `RustClient.post("/proofs/generate", ...)` and `PROOF SANCTIFY(...)` to contract-existence validation against the semantic store.
 
-**Original issue:** ZKP/sanctify integration was documented as a consultation paper only; no circuits, proofs, or runtime verification existed. Resolution was blocked on VQL-DT (issue 5), which has also been resolved.
+**Original issue:** ZKP/sanctify integration was documented as a consultation paper only; no circuits, proofs, or runtime verification existed. Resolution was blocked on VCL-DT (issue 5), which has also been resolved.
 
 === 7. ReScript Registry 60% Complete — ✅ RESOLVED
 
@@ -219,11 +219,11 @@ Added `rescript.json` for build configuration.
 
 **Original issue:** The `CUSTOM` proof type used a hardcoded circuit configuration with no DSL, compiler, or registry.
 
-=== 21. VQL-DT Not Connected to VQL PROOF Runtime — ✅ RESOLVED
+=== 21. VCL-DT Not Connected to VQL PROOF Runtime — ✅ RESOLVED
 
 **Location:** `elixir-orchestration/lib/verisim/query/vql_type_checker.ex`
 
-**Resolved:** 2026-02-28. Superseded by issue #5 resolution. The VQL-DT pipeline is now wired with an Elixir-native type checker that validates proof types, modality compatibility, and composition rules without requiring the ReScript subprocess or a Lean checker. The Lean formal verification path remains aspirational (no Lean files were ever created); the practical implementation uses the ReScript bidirectional type checker (852 lines) backed by an Elixir fallback (320 lines).
+**Resolved:** 2026-02-28. Superseded by issue #5 resolution. The VCL-DT pipeline is now wired with an Elixir-native type checker that validates proof types, modality compatibility, and composition rules without requiring the ReScript subprocess or a Lean checker. The Lean formal verification path remains aspirational (no Lean files were ever created); the practical implementation uses the ReScript bidirectional type checker (852 lines) backed by an Elixir fallback (320 lines).
 
 **Note:** Formal verification via Lean/Idris2 would be a future enhancement for mathematical proof certificates. The current system provides structural type checking and real cryptographic proofs (SHA-256 commitments, Merkle proofs, R1CS circuit verification) via the Rust ZKP bridge.
 
diff --git a/README.adoc b/README.adoc
index 2101187..671063f 100644
--- a/README.adoc
+++ b/README.adoc
@@ -589,9 +589,9 @@ verisimdb/
 ├── demos/
 │   └── drift-detection/       # Drift detection demo script
 ├── docs/                      # Specifications and design documents
-│   ├── vql-grammar.ebnf       # VCL formal grammar
-│   ├── vql-formal-semantics.adoc
-│   └── vql-type-system.adoc
+│   ├── vcl-grammar.ebnf       # VCL formal grammar
+│   ├── vcl-formal-semantics.adoc
+│   └── vcl-type-system.adoc
 ├── registry/                  # ReScript federation registry
 └── .machine_readable/         # STATE.scm, META.scm, ECOSYSTEM.scm
 ----
@@ -623,14 +623,14 @@ Quick links:
 * link:SECURITY.md[Security Policy] — threat model and disclosure process
 * link:AUDIT.adoc[Audit Index] — RSR audit-trail index
 
-VCL language (file paths retain the historical `vql-` / `VQL-` names; the in-repo file rename is a separate, tracked cleanup):
+VCL language (file paths retain the historical `vcl-` / `VCL-` names; the in-repo file rename is a separate, tracked cleanup):
 
 * link:docs/getting-started.adoc[Getting Started] — step-by-step setup guide
-* link:docs/VQL-SPEC.adoc[VCL Specification] — normative language spec
-* link:docs/vql-grammar.ebnf[VCL Grammar] — formal EBNF
-* link:docs/vql-formal-semantics.adoc[VCL Formal Semantics] — operational semantics
-* link:docs/vql-type-system.adoc[VCL Type System] — dependent types + bidirectional checking
-* link:docs/vql-examples.adoc[VCL Examples] — worked examples
+* link:docs/VCL-SPEC.adoc[VCL Specification] — normative language spec
+* link:docs/vcl-grammar.ebnf[VCL Grammar] — formal EBNF
+* link:docs/vcl-formal-semantics.adoc[VCL Formal Semantics] — operational semantics
+* link:docs/vcl-type-system.adoc[VCL Type System] — dependent types + bidirectional checking
+* link:docs/vcl-examples.adoc[VCL Examples] — worked examples
 
 Deployment & operations:
 
diff --git a/ROADMAP.md b/ROADMAP.md
index 69a967d..7b70a63 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -137,7 +137,7 @@ Configurable by admin, overridable by user, defaults to global.
 ### 3.4 ZKP Integration (PLONK)
 **Criticality: HIGH** | Effort: Large
 
-Real zero-knowledge proof verification for VQL-DT PROOF clause.
+Real zero-knowledge proof verification for VCL-DT PROOF clause.
 Scheme: PLONK (see contractiles/trust/Trustfile for rationale).
 
 - `ark-plonk` integration in verisim-semantic
diff --git a/debugger/.claude/CLAUDE.md b/debugger/.claude/CLAUDE.md
index 54a239d..97d6b47 100644
--- a/debugger/.claude/CLAUDE.md
+++ b/debugger/.claude/CLAUDE.md
@@ -16,7 +16,7 @@ This debugger MUST be designed so that **PanLL can embed and drive it programmat
 | Modality Inspector | Pane-W (results) | View all 8 octad modalities for a given entity |
 | Drift Heatmap | Pane-W (results) | Colour-coded grid of drift scores across entities |
 | VQL Trace | Pane-N (reasoning) | Step-by-step VQL query execution trace |
-| Proof Verifier | Pane-L (constraints) | VQL-DT proof obligation checking and certificate display |
+| Proof Verifier | Pane-L (constraints) | VCL-DT proof obligation checking and certificate display |
 | Federation Map | Pane-W (results) | Live peer status, replication lag, adapter types |
 | Performance Flamegraph | Pane-W (results) | Query latency breakdown by modality |
 | Normalisation Timeline | Pane-N (reasoning) | History of self-normalisation events, before/after states |
@@ -39,7 +39,7 @@ PanLL should use this debugger as its **canonical example** for the database des
 PanLL should use **Eclexia** (from `nextgen-languages/eclexia/`) as the canonical example for its language design/development/evaluation module. The VeriSimDB debugger connects to Eclexia via:
 
 - VQL is defined in Eclexia's grammar format → debugger can show VQL parse trees
-- VQL-DT proof obligations are typed in Eclexia's type system → debugger can show type derivation trees
+- VCL-DT proof obligations are typed in Eclexia's type system → debugger can show type derivation trees
 - Eclexia's REPL can be embedded as a debugger panel for interactive VQL exploration
 
 ## Implementation Spec
@@ -94,7 +94,7 @@ Expose a JSON-over-stdio protocol so PanLL can drive the debugger headlessly:
 
 Add a panel that can:
 - Parse VQL using Eclexia's grammar and show the parse tree
-- Show VQL-DT type derivation trees using Eclexia's type system
+- Show VCL-DT type derivation trees using Eclexia's type system
 - Provide an interactive VQL REPL powered by Eclexia's evaluator
 
 ## Build Commands
diff --git a/docs/INDEX.md b/docs/INDEX.md
index 890c4d5..e44bacd 100644
--- a/docs/INDEX.md
+++ b/docs/INDEX.md
@@ -79,20 +79,20 @@ The repo root holds only documents that need maximum visibility for new readers,
 
 - [docs/design/DESIGN-2026-02-27-level-data-model.md](design/DESIGN-2026-02-27-level-data-model.md)
 - [docs/design/DESIGN-2026-02-27-strategic-improvements.adoc](design/DESIGN-2026-02-27-strategic-improvements.adoc)
-- [docs/design/DESIGN-2026-02-27-vql-dt-assessment.adoc](design/DESIGN-2026-02-27-vql-dt-assessment.adoc)
+- [docs/design/DESIGN-2026-02-27-vcl-dt-assessment.adoc](design/DESIGN-2026-02-27-vcl-dt-assessment.adoc)
 - [docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md](design/DESIGN-2026-02-28-panll-interop-telemetry.md)
 
 ### VQL language
 
 - [docs/getting-started.adoc](getting-started.adoc) — VQL getting started
-- [docs/VQL-SPEC.adoc](VQL-SPEC.adoc) — Full VQL specification
-- [docs/vql-grammar.ebnf](vql-grammar.ebnf) — ISO/IEC 14977 EBNF grammar
-- [docs/vql-architecture.adoc](vql-architecture.adoc) — Parser / executor architecture
-- [docs/vql-type-system.adoc](vql-type-system.adoc) — VQL-DT dependent type system
-- [docs/vql-formal-semantics.adoc](vql-formal-semantics.adoc) — Formal semantics
-- [docs/vql-examples.adoc](vql-examples.adoc) — Worked examples
-- [docs/vql-vs-vql-dt.adoc](vql-vs-vql-dt.adoc) — VQL vs VQL-DT comparison
-- [docs/vql-vs-sql.adoc](vql-vs-sql.adoc) — VQL vs SQL comparison
+- [docs/VCL-SPEC.adoc](VCL-SPEC.adoc) — Full VQL specification
+- [docs/vcl-grammar.ebnf](vcl-grammar.ebnf) — ISO/IEC 14977 EBNF grammar
+- [docs/vcl-architecture.adoc](vcl-architecture.adoc) — Parser / executor architecture
+- [docs/vcl-type-system.adoc](vcl-type-system.adoc) — VCL-DT dependent type system
+- [docs/vcl-formal-semantics.adoc](vcl-formal-semantics.adoc) — Formal semantics
+- [docs/vcl-examples.adoc](vcl-examples.adoc) — Worked examples
+- [docs/vcl-vs-vcl-dt.adoc](vcl-vs-vcl-dt.adoc) — VQL vs VCL-DT comparison
+- [docs/vcl-vs-sql.adoc](vcl-vs-sql.adoc) — VQL vs SQL comparison
 - [docs/rescript-registry-types.adoc](rescript-registry-types.adoc) — ReScript registry types
 
 ### Operational concerns
diff --git a/docs/VQL-SPEC.adoc b/docs/VCL-SPEC.adoc
similarity index 95%
rename from docs/VQL-SPEC.adoc
rename to docs/VCL-SPEC.adoc
index c2030c2..4da4caf 100644
--- a/docs/VQL-SPEC.adoc
+++ b/docs/VCL-SPEC.adoc
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
-= VeriSim Query Language (VQL) Specification
+= VeriSim Consonance Language (VCL) Specification
 :author: Jonathan D.A. Jewell
 :email: j.d.a.jewell@open.ac.uk
 :revnumber: 2.0
@@ -21,25 +21,25 @@
 
 === Purpose and Scope
 
-The VeriSim Query Language (VQL) is the native query interface for VeriSimDB, a cross-system entity consistency engine with drift detection, self-normalisation, and formally verified queries. This document is the **normative language specification** for VQL version 2.0.
+The VeriSim Consonance Language (VCL) is the native query interface for VeriSimDB, a cross-system entity consistency engine with drift detection, self-normalisation, and formally verified queries. This document is the **normative language specification** for VCL version 2.0.
 
-VQL is not SQL. It is a domain-specific language for querying and mutating **octad entities** — data objects that exist simultaneously across up to eight modalities (Graph, Vector, Tensor, Semantic, Document, Temporal, Provenance, Spatial). VQL provides:
+VCL is not SQL. It is a domain-specific language for querying and mutating **octad entities** — data objects that exist simultaneously across up to eight modalities (Graph, Vector, Tensor, Semantic, Document, Temporal, Provenance, Spatial). VCL provides:
 
 * **Multi-modal querying** — SELECT across any combination of eight modalities in a single statement.
-* **Dual-path execution** — Slipstream (fast, unverified) and VQL-DT (formally verified with ZKP proofs).
+* **Dual-path execution** — Slipstream (fast, unverified) and VCL-DT (formally verified with ZKP proofs).
 * **Federation** — Query across distributed VeriSimDB instances with configurable drift policies.
 * **Cross-modal conditions** — Filter on relationships _between_ modalities (drift, consistency, existence).
 * **Write path** — INSERT, UPDATE, DELETE with optional proof verification.
 
 This specification unifies and supersedes the information in:
 
-* `vql-grammar.ebnf` — Normative EBNF grammar (included in full as <<appendix-a>>)
-* `vql-type-system.adoc` — Formal type system
-* `vql-formal-semantics.adoc` — Operational and denotational semantics
-* `vql-examples.adoc` — 63 comprehensive examples
-* `vql-architecture.adoc` — Dual-path routing architecture
-* `vql-vs-vql-dt.adoc` — Slipstream vs dependent-type comparison
-* `vql-vs-sql.adoc` — SQL differences
+* `vcl-grammar.ebnf` — Normative EBNF grammar (included in full as <<appendix-a>>)
+* `vcl-type-system.adoc` — Formal type system
+* `vcl-formal-semantics.adoc` — Operational and denotational semantics
+* `vcl-examples.adoc` — 63 comprehensive examples
+* `vcl-architecture.adoc` — Dual-path routing architecture
+* `vcl-vs-vcl-dt.adoc` — Slipstream vs dependent-type comparison
+* `vcl-vs-sql.adoc` — SQL differences
 
 Those documents remain valid for deep dives; this specification is the authoritative reference for language behaviour.
 
@@ -50,7 +50,7 @@ Those documents remain valid for deep dives; this specification is the authorita
 | Convention | Meaning
 
 | `KEYWORD`
-| VQL keyword (case-insensitive in source, uppercase in this document)
+| VCL keyword (case-insensitive in source, uppercase in this document)
 
 | `identifier`
 | User-defined name
@@ -74,15 +74,15 @@ Those documents remain valid for deep dives; this specification is the authorita
 | Feature is specified but not yet implemented
 |===
 
-Keywords are **case-insensitive** throughout VQL. `SELECT`, `select`, and `Select` are equivalent.
+Keywords are **case-insensitive** throughout VCL. `SELECT`, `select`, and `Select` are equivalent.
 
 === Dual-Path Architecture
 
-VQL operates in two execution modes, determined by the presence or absence of a `PROOF` clause:
+VCL operates in two execution modes, determined by the presence or absence of a `PROOF` clause:
 
 [cols="1,1,1"]
 |===
-| Property | Slipstream (no PROOF) | VQL-DT (with PROOF)
+| Property | Slipstream (no PROOF) | VCL-DT (with PROOF)
 
 | Parse
 | Same parser, same AST
@@ -114,7 +114,7 @@ Both modes use the same parser and produce the same AST. They diverge at the **q
 .Dual-path architecture
 ----
                      ┌──────────────────────────────────────────────────┐
-                     │              VQL Statement                       │
+                     │              VCL Statement                       │
                      └───────────────────┬──────────────────────────────┘
                                          │
                                    ┌─────▼──────┐
@@ -130,7 +130,7 @@ Both modes use the same parser and produce the same AST. They diverge at the **q
                          ┌────▼────┐          ┌─────▼─────┐
                          │   NO    │          │    YES    │
                     ┌────▼────┐         ┌─────▼─────┐
-                    │Slipstream│         │  VQL-DT    │
+                    │Slipstream│         │  VCL-DT    │
                     │  Path    │         │  Path      │
                     └────┬────┘         └─────┬─────┘
                          │                     │
@@ -157,10 +157,10 @@ Both modes use the same parser and produce the same AST. They diverge at the **q
 
 === Conformance Levels
 
-A VQL implementation MAY support one or both execution paths:
+A VCL implementation MAY support one or both execution paths:
 
 * **Level 1 — Slipstream**: Parse, validate, execute queries without proof obligations. All SELECT, FROM, WHERE, GROUP BY, HAVING, ORDER BY, LIMIT, OFFSET, and mutation statements MUST be supported.
-* **Level 2 — Full (Slipstream + VQL-DT)**: All Level 1 features plus PROOF clause parsing, dependent type checking, proof generation, and proof certificate bundling.
+* **Level 2 — Full (Slipstream + VCL-DT)**: All Level 1 features plus PROOF clause parsing, dependent type checking, proof generation, and proof certificate bundling.
 
 VeriSimDB's current implementation is Level 1 complete with Level 2 partially implemented (parser and type checker complete; runtime proof generation planned).
 
@@ -173,7 +173,7 @@ VeriSimDB's current implementation is Level 1 complete with Level 2 partially im
 
 === Character Set
 
-VQL source text is encoded in **UTF-8**. Identifiers are restricted to ASCII letters, digits, and underscores. String literals may contain any valid UTF-8 sequence.
+VCL source text is encoded in **UTF-8**. Identifiers are restricted to ASCII letters, digits, and underscores. String literals may contain any valid UTF-8 sequence.
 
 === Keywords
 
@@ -327,7 +327,7 @@ Forward-slash delimited regular expressions. Example: `/\b(AI|ML|DL)\b.*ethics/`
 
 === Comments
 
-VQL supports two comment styles:
+VCL supports two comment styles:
 
 ----
 -- This is a line comment (extends to end of line)
@@ -418,7 +418,7 @@ Not every octad populates every modality. An octad might have only Document and
 
 === Primitive Types
 
-VQL's type system operates over these primitive types:
+VCL's type system operates over these primitive types:
 
 [cols="1,2,2"]
 |===
@@ -481,11 +481,11 @@ When drift exceeds configurable thresholds, the **self-normalizer** identifies t
 
 == Type System
 
-VQL has a rich type system that operates in two modes depending on the execution path. The slipstream path uses simple types for basic validation. The VQL-DT path adds dependent types, refinement types, and proof types for formal verification.
+VCL has a rich type system that operates in two modes depending on the execution path. The slipstream path uses simple types for basic validation. The VCL-DT path adds dependent types, refinement types, and proof types for formal verification.
 
 === Type Language
 
-The full VQL type language stem:[\tau] is defined by:
+The full VCL type language stem:[\tau] is defined by:
 
 [stem]
 ++++
@@ -533,7 +533,7 @@ type rec vqlType =
 
 `[.implemented]` All simple type checking in `VQLBidir.res`.
 
-=== Dependent Types (VQL-DT Path)
+=== Dependent Types (VCL-DT Path)
 
 When a `PROOF` clause is present, the type checker activates dependent type checking:
 
@@ -611,7 +611,7 @@ The subtyping relation stem:[\tau_1 <: \tau_2] governs when a value of type stem
 
 === Type Inference (Bidirectional)
 
-VQL uses **bidirectional type checking** with two modes:
+VCL uses **bidirectional type checking** with two modes:
 
 * **Synthesis** (stem:[\Gamma \vdash e \Rightarrow \tau]) — Infer the type of an expression from its structure.
 * **Checking** (stem:[\Gamma \vdash e \Leftarrow \tau]) — Verify that an expression has an expected type.
@@ -643,7 +643,7 @@ The `synthesizeQuery` function in `VQLBidir.res` walks the query AST through nin
 
 === Refinement Types
 
-Refinement types stem:[\{x : \tau \mid \phi(x)\}] constrain values beyond their base type. In VQL, refinement types appear implicitly in WHERE conditions:
+Refinement types stem:[\{x : \tau \mid \phi(x)\}] constrain values beyond their base type. In VCL, refinement types appear implicitly in WHERE conditions:
 
 ----
 WHERE FIELD severity > 3
@@ -655,7 +655,7 @@ This produces a refined query result type: stem:[\{h : \text{Octad} \mid h.\text
 
 === Type Safety Properties
 
-The VQL type system satisfies three key properties (proven in `vql-type-system.adoc`):
+The VCL type system satisfies three key properties (proven in `vcl-type-system.adoc`):
 
 * **Progress** — A well-typed query can always take a step (it is never stuck).
 * **Preservation** — If a query steps, the result is still well-typed.
@@ -1197,7 +1197,7 @@ LIMIT 50
 
 === PROOF Clause
 
-The PROOF clause activates the VQL-DT execution path and specifies proof obligations.
+The PROOF clause activates the VCL-DT execution path and specifies proof obligations.
 
 .Grammar
 ----
@@ -1317,7 +1317,7 @@ OFFSET 500
 
 == Mutation Statements
 
-VQL 2.0 adds a write path with INSERT, UPDATE, and DELETE operations. All mutations optionally accept a PROOF clause for verified writes.
+VCL 2.0 adds a write path with INSERT, UPDATE, and DELETE operations. All mutations optionally accept a PROOF clause for verified writes.
 
 .Grammar
 ----
@@ -1520,7 +1520,7 @@ STRICT < LATEST < REPAIR < TOLERATE
 
 == Proof System
 
-The proof system is the core differentiator between VQL and traditional query languages. It enables cryptographic verification of query results.
+The proof system is the core differentiator between VCL and traditional query languages. It enables cryptographic verification of query results.
 
 === Six Proof Types
 
@@ -1590,7 +1590,7 @@ CUSTOM     → user_circuit         (custom circuit from contract definition)
 
 === Proof Certificates
 
-When a VQL-DT query succeeds, the result includes a **proof certificate**:
+When a VCL-DT query succeeds, the result includes a **proof certificate**:
 
 [source,json]
 ----
@@ -1628,7 +1628,7 @@ The execution pipeline flows through three layers:
 
 .Execution pipeline
 ----
-VQL String
+VCL String
   → Parser (ReScript VQLParser.res / Elixir vql_bridge.ex fallback)
   → AST
   → Type Checker (VQLBidir.res)
@@ -1655,7 +1655,7 @@ The executor separates conditions into two categories:
 
 === Cross-Modal Joins
 
-VQL does not have explicit JOIN syntax. Instead, cross-modal querying is implicit — every octad is already the join of all its modalities. When you write:
+VCL does not have explicit JOIN syntax. Instead, cross-modal querying is implicit — every octad is already the join of all its modalities. When you write:
 
 [source,vql]
 ----
@@ -1689,7 +1689,7 @@ LIMIT 50
 
 .Example EXPLAIN output
 ----
-VQL Execution Plan
+VCL Execution Plan
 ==================
 Strategy: Parallel
 Steps:
@@ -1740,7 +1740,7 @@ Optimization hints:
 
 === Error Handling and Diagnostics
 
-VQL provides structured error responses with error codes, messages, and recovery hints.
+VCL provides structured error responses with error codes, messages, and recovery hints.
 
 ==== Error Categories
 
@@ -1859,11 +1859,11 @@ This section provides an honest assessment of what is implemented, partially imp
 |===
 | Feature | Version | Notes
 
-| VQL Parser (ReScript)
+| VCL Parser (ReScript)
 | 2.0
 | 1154 lines, monadic parser combinators. Handles all grammar productions.
 
-| VQL Parser (Elixir fallback)
+| VCL Parser (Elixir fallback)
 | 2.0
 | Built into `vql_bridge.ex` (672 lines). No external Deno/Node dependency needed.
 
@@ -1943,7 +1943,7 @@ This section provides an honest assessment of what is implemented, partially imp
 | Cross-modal write atomicity
 | INSERT/UPDATE/DELETE execute but atomic cross-modal writes (all modalities or none) are not guaranteed.
 
-| VQL Bridge (Elixir ↔ ReScript)
+| VCL Bridge (Elixir ↔ ReScript)
 | Port-based communication works. Falls back to built-in Elixir parser when Deno/Node unavailable.
 |===
 
@@ -1953,7 +1953,7 @@ This section provides an honest assessment of what is implemented, partially imp
 |===
 | Feature | Timeline
 
-| VQL-DT runtime (Lean type checker wired to execution)
+| VCL-DT runtime (Lean type checker wired to execution)
 | Next milestone
 
 | ZKP proof generation (proven-library / sanctify)
@@ -1987,11 +1987,11 @@ This section provides an honest assessment of what is implemented, partially imp
 [appendix]
 == Complete EBNF Grammar
 
-This is the normative grammar for VQL 2.0, reproduced from `vql-grammar.ebnf` (ISO/IEC 14977 EBNF notation).
+This is the normative grammar for VCL 2.0, reproduced from `vcl-grammar.ebnf` (ISO/IEC 14977 EBNF notation).
 
 [source,ebnf]
 ----
-(* VeriSim Query Language (VQL) Grammar *)
+(* VeriSim Consonance Language (VCL) Grammar *)
 (* Version: 2.0 — Dependent types, cross-modal correlation, write path *)
 
 (* 1. TOP-LEVEL STRUCTURE *)
@@ -2244,7 +2244,7 @@ keywords = 'SELECT' | 'FROM' | 'WHERE' | 'PROOF' | 'LIMIT' | 'OFFSET'
 [appendix]
 == Reserved Keywords
 
-Complete alphabetical list of all 70 reserved keywords. Keywords are case-insensitive in VQL source.
+Complete alphabetical list of all 70 reserved keywords. Keywords are case-insensitive in VCL source.
 
 [cols="4*"]
 |===
@@ -2717,32 +2717,32 @@ Complete alphabetical list of all 70 reserved keywords. Keywords are case-insens
 [appendix]
 == Related Specifications
 
-This specification is the authoritative reference for VQL language behaviour. The following documents provide deeper coverage of specific topics:
+This specification is the authoritative reference for VCL language behaviour. The following documents provide deeper coverage of specific topics:
 
 [cols="2,3"]
 |===
 | Document | Scope
 
-| link:vql-grammar.ebnf[`vql-grammar.ebnf`]
+| link:vcl-grammar.ebnf[`vcl-grammar.ebnf`]
 | Standalone EBNF grammar file (ISO/IEC 14977). Normative source reproduced in <<appendix-a>>.
 
-| link:vql-type-system.adoc[`vql-type-system.adoc`]
+| link:vcl-type-system.adoc[`vcl-type-system.adoc`]
 | Formal type system with LaTeX notation: type syntax, typing rules, type checking algorithm, subtyping, type equivalence, type safety proofs. 923 lines.
 
-| link:vql-formal-semantics.adoc[`vql-formal-semantics.adoc`]
+| link:vcl-formal-semantics.adoc[`vcl-formal-semantics.adoc`]
 | Operational semantics (big-step and small-step), denotational semantics, proof obligations, soundness theorems, drift semantics. 655 lines.
 
-| link:vql-examples.adoc[`vql-examples.adoc`]
-| 63 comprehensive examples covering all VQL constructs, both execution paths, error cases, and advanced use cases. 1078 lines.
+| link:vcl-examples.adoc[`vcl-examples.adoc`]
+| 63 comprehensive examples covering all VCL constructs, both execution paths, error cases, and advanced use cases. 1078 lines.
 
-| link:vql-architecture.adoc[`vql-architecture.adoc`]
+| link:vcl-architecture.adoc[`vcl-architecture.adoc`]
 | Dual-path routing architecture, ReScript/Elixir/Rust stack, metadata storage, audit trail, drift detection, API endpoint, performance comparison. 708 lines.
 
-| link:vql-vs-vql-dt.adoc[`vql-vs-vql-dt.adoc`]
-| Detailed comparison of Slipstream vs VQL-DT execution paths, six proof types, performance implications, honest implementation status. 282 lines.
+| link:vcl-vs-vcl-dt.adoc[`vcl-vs-vcl-dt.adoc`]
+| Detailed comparison of Slipstream vs VCL-DT execution paths, six proof types, performance implications, honest implementation status. 282 lines.
 
-| link:vql-vs-sql.adoc[`vql-vs-sql.adoc`]
-| Comparative guide between VQL and SQL for developers familiar with relational databases. 241 lines. Note: pre-dates v2.0 GROUP BY/ORDER BY/mutation additions.
+| link:vcl-vs-sql.adoc[`vcl-vs-sql.adoc`]
+| Comparative guide between VCL and SQL for developers familiar with relational databases. 241 lines. Note: pre-dates v2.0 GROUP BY/ORDER BY/mutation additions.
 |===
 
 === Implementation Files
@@ -2755,7 +2755,7 @@ This specification is the authoritative reference for VQL language behaviour. Th
 | ReScript parser (1154 lines). Monadic combinator library + grammar.
 
 | `src/vql/VQLTypes.res`
-| Core type definitions (296 lines). Modality, primitive, VQL, and proof types.
+| Core type definitions (296 lines). Modality, primitive, VCL, and proof types.
 
 | `src/vql/VQLBidir.res`
 | Bidirectional type inference engine (841 lines). 9-phase synthesis pipeline.
@@ -2773,39 +2773,39 @@ This specification is the authoritative reference for VQL language behaviour. Th
 | Elixir ↔ ReScript bridge (672 lines). Built-in fallback parser.
 
 | `elixir-orchestration/lib/verisim/query/vql_executor.ex`
-| Full VQL executor (1162 lines). Parse → type check → plan → route → aggregate.
+| Full VCL executor (1162 lines). Parse → type check → plan → route → aggregate.
 |===
 
 === Known Inconsistencies in Existing Documents
 
 For transparency, these inconsistencies exist between the pre-v2.0 documents:
 
-1. **`vql-vs-sql.adoc`** states VQL lacks GROUP BY, ORDER BY, aggregates, and mutations. This was true for v1.0 but is incorrect for v2.0. The grammar, parser, and executor all support these features.
+1. **`vcl-vs-sql.adoc`** states VCL lacks GROUP BY, ORDER BY, aggregates, and mutations. This was true for v1.0 but is incorrect for v2.0. The grammar, parser, and executor all support these features.
 
-2. **`vql-vs-vql-dt.adoc`** lists six proof types (EXISTENCE, INTEGRITY, CONSISTENCY, PROVENANCE, FRESHNESS, AUTHORIZATION) which differ from the grammar's six (EXISTENCE, CITATION, ACCESS, INTEGRITY, PROVENANCE, CUSTOM). This specification follows the grammar and implementation.
+2. **`vcl-vs-vcl-dt.adoc`** lists six proof types (EXISTENCE, INTEGRITY, CONSISTENCY, PROVENANCE, FRESHNESS, AUTHORIZATION) which differ from the grammar's six (EXISTENCE, CITATION, ACCESS, INTEGRITY, PROVENANCE, CUSTOM). This specification follows the grammar and implementation.
 
-3. **`vql-vs-sql.adoc`** describes VQL as "read-only" which is no longer accurate after v2.0 mutations.
+3. **`vcl-vs-sql.adoc`** describes VCL as "read-only" which is no longer accurate after v2.0 mutations.
 
 This specification resolves all three inconsistencies in favour of the implemented grammar and source code.
 
 // ============================================================================
-// APPENDIX E: VQL-dt++ EXTENSIONS (TYPELL INTEGRATION)
+// APPENDIX E: VCL-dt++ EXTENSIONS (TYPELL INTEGRATION)
 // ============================================================================
 
 [appendix]
-== VQL-dt++ Extensions (Typell Integration)
+== VCL-dt++ Extensions (Typell Integration)
 
-VQL-dt++ extends VQL v3.0 with six optional clauses that provide maximal type-theoretic strictness. These extensions are consumed by the **Typell verification kernel** (the formal verification substrate for PanLL) and are specified normatively in the grammar delta file:
+VCL-dt++ extends VCL v3.0 with six optional clauses that provide maximal type-theoretic strictness. These extensions are consumed by the **Typell verification kernel** (the formal verification substrate for PanLL) and are specified normatively in the grammar delta file:
 
 * link:../../typeql-experimental/docs/vql-dtpp-grammar.ebnf[`vql-dtpp-grammar.ebnf`] — EBNF grammar delta (199 lines)
 
-All six clauses are optional and composable in any combination. They append after the standard query structure with no keyword conflicts against VQL v3.0's 60+ reserved keywords.
+All six clauses are optional and composable in any combination. They append after the standard query structure with no keyword conflicts against VCL v3.0's 60+ reserved keywords.
 
-=== VQL-dt vs VQL-dt++ Feature Comparison
+=== VCL-dt vs VCL-dt++ Feature Comparison
 
 [cols="2,1,1,2"]
 |===
-| Feature | VQL-dt | VQL-dt++ | Typell Kernel Mapping
+| Feature | VCL-dt | VCL-dt++ | Typell Kernel Mapping
 
 | Dependent types (Pi, Sigma)
 | ✅
@@ -2999,7 +2999,7 @@ SELECT GRAPH.*, DOCUMENT.* FROM HEXAD 'entity-001'
 
 === Typell Integration
 
-VQL-dt++ queries are verified by the Typell kernel via JSON-RPC:
+VCL-dt++ queries are verified by the Typell kernel via JSON-RPC:
 
 [source]
 ----
@@ -3010,4 +3010,4 @@ The kernel returns: types, proof obligations, linear tracking, session protocol
 
 === Status
 
-`[.planned]` All six VQL-dt++ clauses. Grammar formally specified. Implementation pending Typell kernel (Phase 3+).
+`[.planned]` All six VCL-dt++ clauses. Grammar formally specified. Implementation pending Typell kernel (Phase 3+).
diff --git a/docs/adoption-strategy.adoc b/docs/adoption-strategy.adoc
index f46e89d..0ea65f9 100644
--- a/docs/adoption-strategy.adoc
+++ b/docs/adoption-strategy.adoc
@@ -28,7 +28,7 @@ by alignment strength, and provides a concrete outreach plan for each.
 * *Drift detection + auto-repair* across 8 modality representations
 * *Heterogeneous federation* -- unified queries across PostgreSQL, ArangoDB,
   Elasticsearch, and VeriSimDB instances
-* *Formally verifiable queries* (VQL-DT) with proof certificates
+* *Formally verifiable queries* (VCL-DT) with proof certificates
 
 === What VeriSimDB Is Not
 
@@ -133,7 +133,7 @@ A gene entity uses 6 of 8 modalities: graph (pathway relationships), vector
 (sequence embeddings), semantic (Gene Ontology terms), document (literature),
 tensor (expression matrices), provenance (lab, sequencing run, pipeline
 version). Drift detection flags when a gene's pathway position contradicts
-its expression profile. VQL-DT provides reproducibility guarantees. Provenance
+its expression profile. VCL-DT provides reproducibility guarantees. Provenance
 tracking satisfies FDA/EMA regulatory compliance.
 
 ==== Features Used
@@ -141,7 +141,7 @@ tracking satisfies FDA/EMA regulatory compliance.
 * All 8 modalities
 * Drift detection (cross-omics consistency)
 * Provenance tracking (regulatory compliance)
-* VQL-DT (reproducible queries)
+* VCL-DT (reproducible queries)
 
 ==== Outreach Targets
 
@@ -170,7 +170,7 @@ A patient entity spans document (clinical notes), tensor (medical images),
 graph (care team relationships), temporal (longitudinal records), spatial
 (facility locations), and provenance (clinician, device, lab attribution).
 Drift detection catches when a medication list in the pharmacy system diverges
-from the EHR -- a life-safety issue. VQL-DT proof certificates satisfy audit
+from the EHR -- a life-safety issue. VCL-DT proof certificates satisfy audit
 requirements.
 
 ==== Features Used
@@ -178,7 +178,7 @@ requirements.
 * Drift detection (medication/allergy discrepancies)
 * Multi-modal storage (6+ modalities)
 * Heterogeneous federation (EHR + pharmacy + lab databases)
-* VQL-DT (audit-grade queries)
+* VCL-DT (audit-grade queries)
 
 ==== Outreach Targets
 
@@ -280,13 +280,13 @@ A Wikidata entity exists as graph relationships, document text (300+
 languages), vector embeddings, semantic annotations, and provenance (editor,
 bot, source attribution). Drift detection catches when an entity's graph
 classification contradicts its textual description -- precisely the documented
-"conceptual disarray". VQL-DT formally verifies ontological constraints.
+"conceptual disarray". VCL-DT formally verifies ontological constraints.
 
 ==== Features Used
 
 * Drift detection (graph structure vs. semantic classification)
 * Multi-modal storage (graph + document + vector + semantic + provenance)
-* VQL-DT (ontological constraint verification)
+* VCL-DT (ontological constraint verification)
 * Self-normalisation (automated deduplication and constraint repair)
 
 ==== Outreach Targets
@@ -338,7 +338,7 @@ calibration divergence. Heterogeneous federation enables cross-archive queries
 
 [cols="1,1,1,1,1,1"]
 |===
-| Domain | Drift Detection | Federation | VQL-DT | Readiness | Priority
+| Domain | Drift Detection | Federation | VCL-DT | Readiness | Priority
 
 | GraphRAG | Critical | High | Medium | *Ship today* | *1*
 | Biomedical | Critical | High | Critical | Q2 2026 | 2
@@ -384,7 +384,7 @@ Any external adopter should know:
 |===
 | Gap | Impact
 
-| VQL-DT proofs incomplete | PROOF clauses parse but don't generate verifiable
+| VCL-DT proofs incomplete | PROOF clauses parse but don't generate verifiable
   certificates yet. Lean type checker integration planned Q2 2026.
 
 | No SQL dialect | VQL is intentionally not SQL. Users wanting familiar syntax
diff --git a/docs/architecture/topology.md b/docs/architecture/topology.md
index b12a6fc..5fad656 100644
--- a/docs/architecture/topology.md
+++ b/docs/architecture/topology.md
@@ -72,7 +72,7 @@
 | verisim-api            | `████████░░` 80%             | Active       |
 | Elixir OTP layer       | `███████░░░` 70%             | Active       |
 | VQL parser             | `█████████░` 95%             | Active       |
-| VQL-DT (Lean checker)  | `░░░░░░░░░░` 0%              | Not started  |
+| VCL-DT (Lean checker)  | `░░░░░░░░░░` 0%              | Not started  |
 | Idris2 ABI             | `████░░░░░░` 40%             | In progress  |
 | Zig FFI                | `████░░░░░░` 40%             | In progress  |
 | Containerfile          | `██████████` 100%            | Complete     |
diff --git a/docs/business/business-case.adoc b/docs/business/business-case.adoc
index fefd2d5..9739117 100644
--- a/docs/business/business-case.adoc
+++ b/docs/business/business-case.adoc
@@ -133,10 +133,10 @@ When drift exceeds configurable thresholds, VeriSimDB can:
 3. *Self-normalise* -- automatically reconcile representations using
    configurable resolution strategies
 
-=== Formal Verification: VQL-DT
+=== Formal Verification: VCL-DT
 
 VeriSimDB's query language, VQL (Verisimilitude Query Language), includes an
-optional dependent-type layer (VQL-DT) that provides *compile-time proofs* of
+optional dependent-type layer (VCL-DT) that provides *compile-time proofs* of
 query correctness. This means:
 
 * Type errors in queries are caught before execution
@@ -286,7 +286,7 @@ infrastructure without requiring data migration.
 | No
 | No
 
-| *Formal proofs (VQL-DT)*
+| *Formal proofs (VCL-DT)*
 | *Yes*
 | No
 | No
@@ -374,7 +374,7 @@ The community edition is intentionally full-featured. Revenue comes from the
    organisation size and SLA level
 2. *Deployment consulting* -- architecture review, migration planning,
    performance tuning, integration with existing infrastructure
-3. *Training and certification* -- VQL/VQL-DT training for development teams
+3. *Training and certification* -- VQL/VCL-DT training for development teams
 4. *OEM licensing* -- for vendors embedding VeriSimDB in their products
 
 == Financial Projections
@@ -518,9 +518,9 @@ profitability faster and at higher margins.
   fault-tolerant concurrency; extensive benchmark suite (510 Rust tests + 152
   Elixir tests, 0 failures)
 
-| VQL-DT complexity deters adoption
+| VCL-DT complexity deters adoption
 | Developers find dependent-type proofs intimidating
-| VQL (without DT) is the default; VQL-DT is opt-in for teams that want formal
+| VQL (without DT) is the default; VCL-DT is opt-in for teams that want formal
   guarantees. Progressive disclosure: start simple, add proofs when ready.
 
 | Federation reliability across heterogeneous backends
@@ -537,7 +537,7 @@ profitability faster and at higher margins.
 
 | Neo4j or ArangoDB adds drift detection
 | Reduces differentiation
-| VeriSimDB's octad model and VQL-DT provide deep moat; 8-modality consistency
+| VeriSimDB's octad model and VCL-DT provide deep moat; 8-modality consistency
   is architecturally difficult to retrofit onto existing databases
 
 | Market education required (new category)
diff --git a/docs/business/marketing/one-pager.adoc b/docs/business/marketing/one-pager.adoc
index d9626fa..2a78a96 100644
--- a/docs/business/marketing/one-pager.adoc
+++ b/docs/business/marketing/one-pager.adoc
@@ -37,7 +37,7 @@ cross-modal consistency monitoring.
 * *Self-normalisation* -- Automatic reconciliation of drifted data using
   configurable resolution strategies (alert, quarantine, or repair)
 * *VQL query language* -- Purpose-built query language for cross-modal operations
-  with optional dependent-type proofs (VQL-DT) for compile-time query verification
+  with optional dependent-type proofs (VCL-DT) for compile-time query verification
 * *Federation* -- Bring drift detection to existing infrastructure by federating
   across PostgreSQL, ArangoDB, Elasticsearch, Neo4j, and more
 * *Open source* -- Full-featured community edition under the Mozilla Public License 2.0 (MPL-2.0)
@@ -47,7 +47,7 @@ cross-modal consistency monitoring.
 
 * *Only database with cross-modal drift detection* -- No competitor (Neo4j,
   Pinecone, Weaviate, ArangoDB, SurrealDB) tracks cross-modal consistency
-* *Formally verified queries* -- VQL-DT provides dependent-type proofs of query
+* *Formally verified queries* -- VCL-DT provides dependent-type proofs of query
   correctness, catching type errors and semantic mismatches before execution
 * *Production-grade engineering* -- Rust core + Elixir/OTP orchestration; 662 tests
   (510 Rust + 152 Elixir), 0 failures; built for performance and fault tolerance
diff --git a/docs/business/marketing/pitch-deck-outline.adoc b/docs/business/marketing/pitch-deck-outline.adoc
index c3c26d9..85cba59 100644
--- a/docs/business/marketing/pitch-deck-outline.adoc
+++ b/docs/business/marketing/pitch-deck-outline.adoc
@@ -111,7 +111,7 @@ representations that together provide a complete picture of each entity.
 ----
                     ┌─────────────────────────┐
                     │       VQL Engine         │
-                    │   (Query + VQL-DT)       │
+                    │   (Query + VCL-DT)       │
                     └────────────┬────────────┘
                                  │
                     ┌────────────▼────────────┐
@@ -219,7 +219,7 @@ does not need to write reconciliation logic.
 | *VQL* -- Purpose-built for cross-modal operations
 
 | Formal verification
-| *VQL-DT* -- Dependent-type proofs of query correctness
+| *VCL-DT* -- Dependent-type proofs of query correctness
 
 | ABI definitions
 | *Idris2* -- Dependent types for interface verification
@@ -234,7 +234,7 @@ does not need to write reconciliation logic.
 
 Emphasise the engineering quality. Rust + Elixir is an increasingly popular
 combination for data infrastructure (used by Discord, Fly.io, and others). The
-test suite is comprehensive and runs in CI on every commit. VQL-DT's dependent
+test suite is comprehensive and runs in CI on every commit. VCL-DT's dependent
 types are optional -- teams can start with plain VQL and adopt formal verification
 incrementally.
 
@@ -365,7 +365,7 @@ coherence from the ground up.
 * *662 tests* (510 Rust + 152 Elixir), *0 failures*
 * *8 modalities* fully architected and implemented
 * *VQL grammar* specified in EBNF with formal semantics
-* *VQL-DT* dependent-type layer with Idris2 proofs
+* *VCL-DT* dependent-type layer with Idris2 proofs
 * *Federation connectors* for PostgreSQL, ArangoDB, Elasticsearch
 * *Comprehensive documentation:* Architecture, deployment, query language,
   drift handling, error handling, safety theory
diff --git a/docs/business/pr/faq.adoc b/docs/business/pr/faq.adoc
index 813d8f0..f4c5f51 100644
--- a/docs/business/pr/faq.adoc
+++ b/docs/business/pr/faq.adoc
@@ -124,7 +124,7 @@ has no drift detection, no temporal versioning, no provenance tracking, no forma
 query verification, and no federation.
 
 VeriSimDB supports 8 modalities with cross-modal drift detection and formal query
-proofs (VQL-DT). The fundamental difference is architectural: Weaviate treats
+proofs (VCL-DT). The fundamental difference is architectural: Weaviate treats
 vectors and objects as complementary storage; VeriSimDB treats all modalities as
 representations of a single entity that must remain consistent.
 
@@ -181,10 +181,10 @@ VQL is designed to be familiar to SQL users while supporting modality-specific
 operations (graph traversals, vector similarity, tensor operations, temporal
 time-travel, spatial containment, etc.) in a unified syntax.
 
-=== What are dependent-type proofs (VQL-DT)?
+=== What are dependent-type proofs (VCL-DT)?
 
-VQL-DT is an optional extension to VQL that adds dependent-type verification.
-When enabled, VQL-DT uses the Idris2 type system to prove properties of queries
+VCL-DT is an optional extension to VQL that adds dependent-type verification.
+When enabled, VCL-DT uses the Idris2 type system to prove properties of queries
 at compile time:
 
 * *Type correctness:* Ensure that query expressions are well-typed across
@@ -194,8 +194,8 @@ at compile time:
   meaningful
 * *Threshold validity:* Prove that coherence thresholds are within valid ranges
 
-VQL-DT is entirely optional. Teams can use plain VQL for standard operations and
-adopt VQL-DT incrementally when they want formal guarantees.
+VCL-DT is entirely optional. Teams can use plain VQL for standard operations and
+adopt VCL-DT incrementally when they want formal guarantees.
 
 === How does federation work?
 
@@ -257,7 +257,7 @@ j.d.a.jewell@open.ac.uk for a quote.
 1. Clone the repository: `git clone https://github.com/hyperpolymath/verisimdb`
 2. Follow the getting-started guide: `docs/getting-started.adoc`
 3. Run the test suite: `cargo test` (Rust) and `mix test` (Elixir)
-4. Explore the VQL examples: `docs/vql-examples.adoc`
+4. Explore the VQL examples: `docs/vcl-examples.adoc`
 
 === Is VeriSimDB production-ready?
 
@@ -289,7 +289,7 @@ The roadmap includes:
 
 * *Short-term (0-6 months):* Community building, documentation improvements,
   federation connector hardening, performance benchmarking
-* *Medium-term (6-18 months):* Container images, managed service pilot, VQL-DT
+* *Medium-term (6-18 months):* Container images, managed service pilot, VCL-DT
   tooling, additional federation connectors
 * *Long-term (18-36 months):* Enterprise features (RBAC, audit logging),
   OEM licensing framework, academic paper publications
@@ -312,6 +312,6 @@ See `CONTRIBUTING.md` in the repository for contribution guidelines.
 
 * *Repository:* https://github.com/hyperpolymath/verisimdb
 * *Documentation:* `docs/` directory in the repository
-* *VQL specification:* `docs/VQL-SPEC.adoc`
-* *Architecture:* `docs/vql-architecture.adoc`
+* *VQL specification:* `docs/VCL-SPEC.adoc`
+* *Architecture:* `docs/vcl-architecture.adoc`
 * *Contact:* j.d.a.jewell@open.ac.uk
diff --git a/docs/business/pr/key-messages.adoc b/docs/business/pr/key-messages.adoc
index 88b5100..d86a69f 100644
--- a/docs/business/pr/key-messages.adoc
+++ b/docs/business/pr/key-messages.adoc
@@ -42,7 +42,7 @@ before downstream systems consume contradictory data.
    temporal, provenance, and spatial in one entity
 3. *Self-normalisation* -- Automatic repair of drifted representations with
    configurable resolution strategies
-4. *Proof-carrying queries (VQL-DT)* -- Optional dependent-type verification
+4. *Proof-carrying queries (VCL-DT)* -- Optional dependent-type verification
    of query correctness using Idris2
 5. *Heterogeneous federation* -- Unified querying across PostgreSQL, ArangoDB,
    Elasticsearch, and Neo4j without data migration
@@ -71,7 +71,7 @@ alertable condition -- not an invisible failure mode.
   operations (graph traversals, vector similarity, tensor ops, temporal
   time-travel, spatial containment) in a unified syntax.
 
-* *VQL-DT*: Optional dependent-type layer using Idris2. Proves query type
+* *VCL-DT*: Optional dependent-type layer using Idris2. Proves query type
   correctness, semantic compatibility of cross-modal joins, and threshold
   validity at compile time. Entirely opt-in -- plain VQL works without it.
 
@@ -188,7 +188,7 @@ continuously and repairs it automatically.
 VeriSimDB formalises the concept of cross-modal drift in multimodal data systems
 and provides an operational system for detecting, quantifying, and repairing
 representational divergence across 8 data modalities. The query language includes
-an optional dependent-type verification layer (VQL-DT) that provides compile-time
+an optional dependent-type verification layer (VCL-DT) that provides compile-time
 proofs of query correctness.
 
 === Supporting Points
@@ -199,7 +199,7 @@ proofs of query correctness.
   consistency.
 
 * *Formal semantics*: VQL has published formal semantics (denotational and
-  operational). VQL-DT extends these with dependent-type judgements formalised in
+  operational). VCL-DT extends these with dependent-type judgements formalised in
   Idris2, providing machine-checkable proofs of query properties.
 
 * *Reproducibility*: The entire system is open source. Experiments can be
@@ -296,7 +296,7 @@ community edition. There is no "enterprise edition" that gates features.
 * Rust community (r/rust, Rust Users Forum) -- core engine, storage
 * BEAM community (Erlang/Elixir conferences, Code BEAM) -- fault tolerance
 * Database community (r/database, HN, Lobsters) -- novel architecture
-* Formal methods community (Idris2 Discourse, TYPES mailing list) -- VQL-DT
+* Formal methods community (Idris2 Discourse, TYPES mailing list) -- VCL-DT
 
 === Use These Phrases
 
diff --git a/docs/business/pr/press-release.adoc b/docs/business/pr/press-release.adoc
index c488705..540a4b0 100644
--- a/docs/business/pr/press-release.adoc
+++ b/docs/business/pr/press-release.adoc
@@ -39,7 +39,7 @@ designed from the ground up to detect and repair this kind of inconsistency."
 VeriSimDB is built on a *Rust core* for performance and memory safety, with
 *Elixir/OTP orchestration* for fault-tolerant concurrency. The database includes
 VQL (Verisimilitude Query Language), a purpose-built query language for
-cross-modal operations, and an optional dependent-type layer (VQL-DT) that
+cross-modal operations, and an optional dependent-type layer (VCL-DT) that
 provides compile-time proofs of query correctness using Idris2.
 
 The project's engineering maturity is demonstrated by a test suite of *662 tests*
diff --git a/docs/business/strategy/adoption-roadmap.adoc b/docs/business/strategy/adoption-roadmap.adoc
index 6159977..50897a0 100644
--- a/docs/business/strategy/adoption-roadmap.adoc
+++ b/docs/business/strategy/adoption-roadmap.adoc
@@ -163,7 +163,7 @@ credibility leverage.
 2. *Regulatory motivation*: FDA 21 CFR Part 11, EMA GxP requirements, and grant
    agency data management plans create institutional demand for data consistency
    tools with audit trails (provenance modality) and formal verification
-   (VQL-DT proof certificates).
+   (VCL-DT proof certificates).
 
 3. *Publication opportunity*: Successful pilot deployments generate academic
    papers, which generate citations, which generate credibility. A VLDB or
@@ -473,7 +473,7 @@ priorities, not marketing milestones.
 | Getting-started guide and VQL examples | Required | Required | Required
 | Federation (PostgreSQL connector) | Demo quality | Production quality | Production quality
 | Federation (ArangoDB, Elasticsearch, Neo4j) | Not required | Demo quality | Production quality
-| VQL-DT proof certificates | Documented design | Prototype | Production quality
+| VCL-DT proof certificates | Documented design | Prototype | Production quality
 | Container images (Podman/Docker) | Basic | Hardened | Production-grade
 | Monitoring and alerting (Prometheus) | Basic | Comprehensive | SLA-grade
 | RBAC and access control | Not required | Basic | Comprehensive
@@ -497,7 +497,7 @@ compelling demo. Engage consistently.
 | 1
 | Competitor adds drift detection
 | Low
-| Architectural depth (octad + VQL-DT) is difficult to retrofit. First-mover
+| Architectural depth (octad + VCL-DT) is difficult to retrofit. First-mover
 advantage in category definition.
 
 | 2
diff --git a/docs/business/strategy/economics-analysis.adoc b/docs/business/strategy/economics-analysis.adoc
index ca793bd..ac7cb20 100644
--- a/docs/business/strategy/economics-analysis.adoc
+++ b/docs/business/strategy/economics-analysis.adoc
@@ -227,7 +227,7 @@ not additional features.
 ==== Principle: No Feature Gating
 
 VeriSimDB's commercial licence does *not* add features beyond the community
-edition. All 8 modalities, drift detection, self-normalisation, VQL, VQL-DT,
+edition. All 8 modalities, drift detection, self-normalisation, VQL, VCL-DT,
 and federation ship in the open-source release.
 
 This is a deliberate strategic choice:
@@ -400,7 +400,7 @@ consulting revenue, with licence revenue becoming the primary driver by Year 3.
 
 | Competitor response (Neo4j adds drift detection)
 | Reduces differentiation but VeriSimDB has
-architectural depth advantage (octad + VQL-DT)
+architectural depth advantage (octad + VCL-DT)
 | Medium
 
 | Pricing acceptance ($40K ACV)
diff --git a/docs/business/strategy/functional-units.adoc b/docs/business/strategy/functional-units.adoc
index e543fe6..cbae04e 100644
--- a/docs/business/strategy/functional-units.adoc
+++ b/docs/business/strategy/functional-units.adoc
@@ -151,14 +151,14 @@ The Stage 1 engineering team expands with:
 
 ==== Query Engine Engineer (1 person)
 
-*Justification:* VQL and VQL-DT require dedicated attention as query complexity
+*Justification:* VQL and VCL-DT require dedicated attention as query complexity
 grows. The query planner (currently basic) needs optimisation for cross-modal
 queries spanning all 8 modalities.
 
 *Responsibilities:*
 
 * VQL parser and query planner development
-* VQL-DT type checker integration (Idris2 bridge)
+* VCL-DT type checker integration (Idris2 bridge)
 * Query performance optimisation (cost-based planning, modality pushdown)
 * Query language evolution (new syntax, new operators)
 
diff --git a/docs/business/strategy/go-to-market.adoc b/docs/business/strategy/go-to-market.adoc
index 61de1fe..6c8f0a5 100644
--- a/docs/business/strategy/go-to-market.adoc
+++ b/docs/business/strategy/go-to-market.adoc
@@ -84,7 +84,7 @@ cross-modal drift
 | Medium
 
 | *Formal methods enthusiasts*
-| VQL-DT dependent-type proofs are novel in a database context
+| VCL-DT dependent-type proofs are novel in a database context
 | Idris2 Discourse post, TYPES mailing list
 | Medium
 |===
@@ -238,7 +238,7 @@ Target: 3-5 consulting engagements, $50,000-$150,000 total revenue.
 
 | *ICFP/POPL*
 | Experience report (12 pages)
-| VQL-DT: dependent types in database query languages
+| VCL-DT: dependent types in database query languages
 |===
 
 === Success Metrics (Month 24)
@@ -374,7 +374,7 @@ engage consistently (48h issue response)
 | Competitor adds drift detection
 | Reduces differentiation
 | 8-modality octad model is architecturally difficult to retrofit; deep moat in
-VQL-DT formal verification; first-mover advantage in category definition
+VCL-DT formal verification; first-mover advantage in category definition
 |===
 
 === Phase 2 Risks
diff --git a/docs/cache-sharing-strategy.adoc b/docs/cache-sharing-strategy.adoc
index 7387701..45dbf00 100644
--- a/docs/cache-sharing-strategy.adoc
+++ b/docs/cache-sharing-strategy.adoc
@@ -740,6 +740,6 @@ end
 == References
 
 - link:caching-strategy.adoc[Caching Strategy Overview]
-- link:vql-architecture.adoc[VQL Architecture]
+- link:vcl-architecture.adoc[VQL Architecture]
 - link:challenges-federated.adoc[Federated Deployment Challenges]
 - link:../lib/verisim/query_cache.ex[Query Cache Implementation]
diff --git a/docs/caching-strategy.adoc b/docs/caching-strategy.adoc
index 79a4e80..8719c1a 100644
--- a/docs/caching-strategy.adoc
+++ b/docs/caching-strategy.adoc
@@ -589,6 +589,6 @@ QueryCache.invalidate_by_tag("project:thesis-2025")
 
 - link:query-optimization-overview.adoc[Query Optimization Overview]
 - link:reversibility-design.adoc[Reversibility Design]
-- link:vql-architecture.adoc[VQL Architecture]
+- link:vcl-architecture.adoc[VQL Architecture]
 - link:../lib/verisim/query_cache.ex[Query Cache Implementation]
 - link:../lib/verisim/query_router_cached.ex[Cached Query Router]
diff --git a/docs/consultation-dependent-types-zkp.adoc b/docs/consultation-dependent-types-zkp.adoc
index 98bd1d7..1043a84 100644
--- a/docs/consultation-dependent-types-zkp.adoc
+++ b/docs/consultation-dependent-types-zkp.adoc
@@ -1114,7 +1114,7 @@ e ::= x | n | true | false | ()
 
 === A.2 Typing Rules (Complete)
 
-See docs/vql-type-system.adoc for full 30+ typing rules.
+See docs/vcl-type-system.adoc for full 30+ typing rules.
 
 ---
 
diff --git a/docs/design/DESIGN-2026-02-27-strategic-improvements.adoc b/docs/design/DESIGN-2026-02-27-strategic-improvements.adoc
index 02b2df8..59cab15 100644
--- a/docs/design/DESIGN-2026-02-27-strategic-improvements.adoc
+++ b/docs/design/DESIGN-2026-02-27-strategic-improvements.adoc
@@ -87,7 +87,7 @@ automatically.  This is genuinely novel.
   and lacks documentation.  Without a usable query language, VerisimDB is an HTTP
   CRUD API with caching.  _This is the single biggest gap._
 
-| **VQL-DT not wired**
+| **VCL-DT not wired**
 | MEDIUM
 | Lean type definitions exist but the checker is not invoked at runtime.  PROOF
   clauses are syntactically supported but proof certificates are not formally
@@ -274,7 +274,7 @@ heterogeneous databases — ArangoDB, Postgres, Elasticsearch, Neo4j — with
 VerisimDB as the coordination layer.  The IDApTIK database bridge (ArangoDB +
 VerisimDB) is the first working example of this pattern.
 
-=== Layer 3: VQL-DT — Formally Verified Queries (Technical Moat)
+=== Layer 3: VCL-DT — Formally Verified Queries (Technical Moat)
 
 The deepest technical capability.  Small audience (formal methods, regulated
 industries, safety-critical systems) but impossible to replicate quickly.
@@ -283,11 +283,11 @@ _"VerisimDB returns your query results with a machine-verifiable proof
 certificate.  The Lean type checker proves the result satisfies your
 constraints."_
 
-No database in existence does this.  VQL-DT is the reason a competitor
+No database in existence does this.  VCL-DT is the reason a competitor
 cannot clone VerisimDB in a weekend after seeing the drift detection demo.
 It takes years of type theory knowledge to even attempt it.
 
-**Who cares about VQL-DT:**
+**Who cares about VCL-DT:**
 
 - Regulated industries (finance, medical devices, aerospace) where you must
   _prove_ a query result is correct, not just assert it
@@ -296,8 +296,8 @@ It takes years of type theory knowledge to even attempt it.
 - Safety-critical systems (Ada/SPARK territory)
 - Academic formal methods community
 
-**VQL-DT is not the lead pitch.** It is the moat.  Drift detection gets
-people in the door.  Federation keeps them.  VQL-DT ensures nobody can
+**VCL-DT is not the lead pitch.** It is the moat.  Drift detection gets
+people in the door.  Federation keeps them.  VCL-DT ensures nobody can
 compete.
 
 == Competitor Analysis: Data Quality / Observability Space
@@ -533,7 +533,7 @@ future session.
 **Why:** A database without a usable query language is a key-value store with
 extra steps.  This is the single highest-impact improvement.
 
-**Scope:** Not VQL-DT.  Just VQL.  The query language that end users type.
+**Scope:** Not VCL-DT.  Just VQL.  The query language that end users type.
 
 **What "finished" means:**
 
@@ -562,7 +562,7 @@ extra steps.  This is the single highest-impact improvement.
 
 **Deliverables:**
 
-- `docs/VQL-SPEC.adoc` -- language specification
+- `docs/VCL-SPEC.adoc` -- language specification
 - Updated parser/executor to cover all specified forms
 - 20+ integration tests proving the spec is implemented
 
@@ -672,18 +672,18 @@ peers via HTTP adapters.
 
 The `GraphStore` trait abstraction already exists, so this is a backend swap.
 
-=== Priority 7: Wire VQL-DT (HIGH — but after VQL)
+=== Priority 7: Wire VCL-DT (HIGH — but after VQL)
 
-**Why:** VQL-DT is the technical moat — the reason nobody can clone VerisimDB
+**Why:** VCL-DT is the technical moat — the reason nobody can clone VerisimDB
 quickly.  Formally verified query results via Lean type checking is genuinely
 unique in the database world.  But VQL must work reliably first (Priority 1).
 No point verifying proofs in a query language that cannot execute reliably.
 
 **Why it matters more than it might seem:**
 
-VQL-DT is not a nice-to-have.  It is the capability that separates VerisimDB
+VCL-DT is not a nice-to-have.  It is the capability that separates VerisimDB
 from every other database and every data quality tool.  Great Expectations can
-assert "this column has no nulls."  VerisimDB with VQL-DT can return a
+assert "this column has no nulls."  VerisimDB with VCL-DT can return a
 _machine-verifiable proof certificate_ that the query result satisfies
 dependent type constraints.  This is the kind of guarantee required in:
 
@@ -699,7 +699,7 @@ designed.  The gap is wiring the Lean checker into the execution path.
 **Defer until:** VQL spec is complete and integration-tested (Priority 1).
 Then this becomes the highest priority.
 
-**See:** KNOWN-ISSUES #21, `docs/vql-vs-vql-dt.adoc` for the phased roadmap.
+**See:** KNOWN-ISSUES #21, `docs/vcl-vs-vcl-dt.adoc` for the phased roadmap.
 
 == What NOT to Do
 
@@ -740,11 +740,11 @@ The path forward (priority order):
 4. **One external user** so the assumptions are _tested_
 5. **Heterogeneous federation** so enterprise adoption is _practical_
 6. **Reposition** around drift detection so the value proposition is _clear_
-7. **Wire VQL-DT** so the technical moat is _operational_ (after VQL is solid)
+7. **Wire VCL-DT** so the technical moat is _operational_ (after VQL is solid)
 
 The layered pitch:
 
 - **Drift detection** gets people in the door (broad audience, easy to explain)
 - **Federation** keeps them (watches existing databases, no migration)
 - **Provenance** makes them depend on it (audit trail, GDPR, compliance)
-- **VQL-DT** ensures nobody can compete (years of type theory to replicate)
+- **VCL-DT** ensures nobody can compete (years of type theory to replicate)
diff --git a/docs/design/DESIGN-2026-02-27-vql-dt-assessment.adoc b/docs/design/DESIGN-2026-02-27-vcl-dt-assessment.adoc
similarity index 93%
rename from docs/design/DESIGN-2026-02-27-vql-dt-assessment.adoc
rename to docs/design/DESIGN-2026-02-27-vcl-dt-assessment.adoc
index c5863b0..e13cb9b 100644
--- a/docs/design/DESIGN-2026-02-27-vql-dt-assessment.adoc
+++ b/docs/design/DESIGN-2026-02-27-vcl-dt-assessment.adoc
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-= VQL-DT (Dependent Type Path) Wiring Assessment
+= VCL-DT (Dependent Type Path) Wiring Assessment
 :author: Jonathan D.A. Jewell (hyperpolymath)
 :date: 2026-02-27
 :repo: verisimdb
@@ -9,7 +9,7 @@
 
 == Executive Summary
 
-VQL-DT has *substantially more real implementation than initially expected*.
+VCL-DT has *substantially more real implementation than initially expected*.
 The ReScript type checker and Rust proof/semantic layer are genuinely functional
 with real algorithms, tests, and meaningful code. However, the three layers
 (ReScript, Rust, Elixir) are **not wired together end-to-end**. Each layer
@@ -19,7 +19,7 @@ works in isolation but the integration seams are broken or stubbed.
 |===
 | Layer | Implementation | Integration | Assessment
 
-| ReScript VQL
+| ReScript VCL
 | ~85% real code
 | 0% connected to Elixir executor
 | *Impressive standalone work, needs integration*
@@ -40,12 +40,12 @@ works in isolation but the integration seams are broken or stubbed.
 | *No formal type checker present*
 |===
 
-**Honest overall VQL-DT completion: ~35%** (individual components exist;
+**Honest overall VCL-DT completion: ~35%** (individual components exist;
 end-to-end pipeline does not).
 
 == Layer-by-Layer Assessment
 
-=== 1. ReScript VQL Layer (`src/vql/`)
+=== 1. ReScript VCL Layer (`src/vql/`)
 
 ==== What Is Actually Implemented (Real Working Code)
 
@@ -125,10 +125,10 @@ end-to-end pipeline does not).
 ==== What Is Missing
 
 1. **No integration with Elixir executor.** The ReScript type checker runs
-   entirely client-side (in the browser or via Deno/Node). The Elixir VQL
+   entirely client-side (in the browser or via Deno/Node). The Elixir VCL
    executor comment says "Type-check if PROOF clause present (VQLTypeChecker
    -> VQLBidir)" but this invocation never happens. The Elixir executor
-   parses VQL independently using its own built-in parser.
+   parses VCL independently using its own built-in parser.
 
 2. **No proof generation triggered from type checker.** The type checker
    produces a `ProvedResultType` and `composedProofPlan`, but these are not
@@ -192,7 +192,7 @@ end-to-end pipeline does not).
 | `sanctify_bridge.rs` (414 lines)
 | *FULLY IMPLEMENTED.* Parses sanctify-php security reports, security issue
   types, severity levels, contract validation, proof blob conversion.
-  Tangential to VQL-DT but functional.
+  Tangential to VCL-DT but functional.
 |===
 
 ==== What Is Stubbed/Incomplete
@@ -225,9 +225,9 @@ two for `:zkp` and `:proven` proof types.
 
 ==== What Is NOT Exposed
 
-The Rust VQL endpoint (`vql.rs`) is a **Slipstream-only parser**. It handles
+The Rust VCL endpoint (`vql.rs`) is a **Slipstream-only parser**. It handles
 SELECT, SEARCH, INSERT, DELETE, SHOW, COUNT, EXPLAIN but has *zero PROOF
-clause handling*. Any VQL query with a PROOF clause sent to the Rust VQL
+clause handling*. Any VCL query with a PROOF clause sent to the Rust VCL
 endpoint would fail or be silently ignored.
 
 === 3. Elixir Orchestration Layer (`elixir-orchestration/lib/verisim/query/`)
@@ -240,7 +240,7 @@ endpoint would fail or be silently ignored.
 
 | `vql_bridge.ex` (672 lines)
 | *IMPLEMENTED with degraded fallback.* GenServer managing a Deno/Node
-  subprocess that runs compiled ReScript VQL parser. Falls back to built-in
+  subprocess that runs compiled ReScript VCL parser. Falls back to built-in
   Elixir parser when subprocess unavailable. `parse_dependent/2` exists but
   the fallback parser only collects PROOF tokens as raw strings, not
   structured proof specs.
@@ -253,7 +253,7 @@ endpoint would fail or be silently ignored.
 
 | `query_router.ex` (187 lines)
 | *IMPLEMENTED.* Routes queries by type (:text, :vector, :graph, :semantic,
-  :temporal, :multi) to RustClient. No VQL-DT-specific logic.
+  :temporal, :multi) to RustClient. No VCL-DT-specific logic.
 |===
 
 ==== The Critical Proof Verification Gap
@@ -296,7 +296,7 @@ core is down, ALL proof verification silently passes.
 ==== What The Elixir Executor Does NOT Do
 
 1. Does **not invoke the ReScript bidirectional type checker**
-2. Does **not type-check VQL-DT queries** (only the ReScript layer does this,
+2. Does **not type-check VCL-DT queries** (only the ReScript layer does this,
    client-side)
 3. Does **not generate actual proof obligations** from PROOF clauses (only the
    ReScript `VQLProofObligation.res` does this, client-side)
@@ -310,10 +310,10 @@ core is down, ALL proof verification silently passes.
 
 **Does not exist.** The Idris2 files found in `src/abi/` (Types.idr,
 Layout.idr, Foreign.idr) are standard ABI definitions for VeriSimDB's FFI
-layer, not VQL type checkers. No `.lean` files exist anywhere in the
+layer, not VCL type checkers. No `.lean` files exist anywhere in the
 repository.
 
-The CLAUDE.md Known Issues section acknowledges: "VQL-DT not connected to VQL
+The CLAUDE.md Known Issues section acknowledges: "VCL-DT not connected to VCL
 PROOF runtime (Lean type checker not invoked)." This is accurate — no Lean
 type checker has been written.
 
@@ -342,8 +342,8 @@ type checker has been written.
 | *BROKEN.* Executor never calls `/proofs/generate-with-circuit`.
 
 | Elixir executor
-| Rust VQL endpoint
-| *PARTIAL.* The Rust VQL endpoint has no PROOF handling.
+| Rust VCL endpoint
+| *PARTIAL.* The Rust VCL endpoint has no PROOF handling.
 
 | proven library (external)
 | Rust proven_bridge
@@ -356,10 +356,10 @@ type checker has been written.
 
 === Data Flow: What Should Happen vs What Actually Happens
 
-**Intended VQL-DT data flow:**
+**Intended VCL-DT data flow:**
 [source]
 ----
-Client sends VQL with PROOF clause
+Client sends VCL with PROOF clause
   -> Elixir executor receives query
   -> ReScript type checker validates types + generates proof obligations
   -> Proof obligations sent to Rust ZKP bridge
@@ -371,7 +371,7 @@ Client sends VQL with PROOF clause
 **What actually happens today:**
 [source]
 ----
-Client sends VQL with PROOF clause
+Client sends VCL with PROOF clause
   -> Elixir executor receives query (via fallback parser)
   -> PROOF tokens collected as raw strings
   -> verify_single_proof() called per spec
@@ -463,7 +463,7 @@ To get real ZK-SNARKs:
 The CLAUDE.md mentions a Lean type checker but none exists. Building one would
 mean:
 
-1. Define VQL-DT's type system in Lean 4 or Idris2.
+1. Define VCL-DT's type system in Lean 4 or Idris2.
 2. Implement bidirectional type checking with dependent types.
 3. Generate proof obligations as Lean/Idris2 terms.
 4. Verify proof obligations against the type system.
@@ -478,7 +478,7 @@ checker is sufficient for practical use.
 |===
 | Component | Code Written | Code Working | End-to-End Wired
 
-| ReScript VQL Parser
+| ReScript VCL Parser
 | 95%
 | 95%
 | 0%
@@ -518,12 +518,12 @@ checker is sufficient for practical use.
 | 90%
 | 0%
 
-| Elixir VQL Bridge
+| Elixir VCL Bridge
 | 70%
 | 70%
 | 40%
 
-| Elixir VQL Executor (proof path)
+| Elixir VCL Executor (proof path)
 | 30%
 | 30%
 | 15%
@@ -538,7 +538,7 @@ checker is sufficient for practical use.
 | 0%
 | 0%
 
-| *Overall VQL-DT Pipeline*
+| *Overall VCL-DT Pipeline*
 | *~60%*
 | *~55%*
 | *~10%*
@@ -546,7 +546,7 @@ checker is sufficient for practical use.
 
 NOTE: "Code Written" and "Code Working" are high because real algorithms are
 implemented and tests pass. "End-to-End Wired" is abysmal because the layers
-do not talk to each other for the VQL-DT path.
+do not talk to each other for the VCL-DT path.
 
 == Key Takeaways
 
@@ -558,7 +558,7 @@ do not talk to each other for the VQL-DT path.
    as isolated islands. The Elixir executor's proof verification is the weakest
    link — it's largely hardcoded `:ok` returns.
 
-3. **The shortest path to a working VQL-DT pipeline** is wiring the ReScript
+3. **The shortest path to a working VCL-DT pipeline** is wiring the ReScript
    type checker to the Elixir executor (Priority 1) and connecting proof
    obligations to the Rust ZKP bridge (Priority 2). This would give ~60%
    end-to-end functionality in roughly 1-2 weeks of focused work.
@@ -568,5 +568,5 @@ do not talk to each other for the VQL-DT path.
    provides no actual zero-knowledge properties. This is the honest truth.
 
 5. **The Lean type checker is aspirational.** The ReScript type checker is
-   capable enough for practical VQL-DT use. A Lean version would provide
+   capable enough for practical VCL-DT use. A Lean version would provide
    formal verification guarantees but is not blocking functionality.
diff --git a/docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md b/docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md
index 057a1fc..36c02cc 100644
--- a/docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md
+++ b/docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md
@@ -98,7 +98,7 @@ Each database module implements a standard protocol for PanLL integration:
 | `verisim.drift.modality_breakdown` | Which modalities drift most | Focus normalisation work |
 | `verisim.normalise.success_rate` | How often normalisation succeeds | Quality metric |
 | `verisim.federation.peer_health` | Federated peer availability | Operational monitoring |
-| `verisim.proof.type_usage` | Which proof types are used | VQL-DT adoption metric |
+| `verisim.proof.type_usage` | Which proof types are used | VCL-DT adoption metric |
 | `verisim.entity.modality_coverage` | Average modalities per entity | Data completeness metric |
 | `verisim.system.uptime` | Server uptime | Reliability metric |
 
@@ -111,7 +111,7 @@ The reporter aggregates raw telemetry into actionable insights:
 3. **Performance Trends** — is p95 latency improving or degrading over time?
 4. **Drift Frequency** — are entities staying consistent or constantly re-normalising?
 5. **Federation Health** — are peer backends reliable or flaky?
-6. **VQL-DT Adoption** — are users using dependent type proofs?
+6. **VCL-DT Adoption** — are users using dependent type proofs?
 
 ### PanLL Integration Points
 
diff --git a/docs/error-handling-strategy.adoc b/docs/error-handling-strategy.adoc
index de65c1c..d2e2778 100644
--- a/docs/error-handling-strategy.adoc
+++ b/docs/error-handling-strategy.adoc
@@ -1252,7 +1252,7 @@ Parse Error at 1:8: Expected 'GRAPH', 'VECTOR', ..., found 'GRPH'
 
 == References
 
-- link:vql-architecture.adoc[VQL Architecture]
+- link:vcl-architecture.adoc[VQL Architecture]
 - link:caching-strategy.adoc[Caching Strategy]
 - link:reversibility-design.adoc[Reversibility Design]
 - link:../src/vql/VQLError.res[VQL Error Types]
diff --git a/docs/federation-readiness.adoc b/docs/federation-readiness.adoc
index e3f8da7..e72e74a 100644
--- a/docs/federation-readiness.adoc
+++ b/docs/federation-readiness.adoc
@@ -52,7 +52,7 @@ If VQL were removed or not used, VeriSimDB would lose the following federation-c
 
 * **No drift policy enforcement on federated queries.** Drift policies (`DRIFT POLICY strict_consistency`, `DRIFT POLICY eventual`, etc.) are expressed in VQL and enforced by the query router. Without VQL, there is no standard mechanism to declare or enforce consistency requirements across federated peers.
 
-* **No cross-modal consistency checks across instances.** VQL's `PROOF CONSISTENCY` clause can request verification that graph, vector, and semantic modalities agree across federation peers. Without VQL-DT, there is no way to express or verify cross-instance consistency at query time.
+* **No cross-modal consistency checks across instances.** VQL's `PROOF CONSISTENCY` clause can request verification that graph, vector, and semantic modalities agree across federation peers. Without VCL-DT, there is no way to express or verify cross-instance consistency at query time.
 
 * **No unified result format.** VQL queries return results in a consistent format regardless of whether the data came from one instance or twenty. Without VQL, each peer's API response format would need to be handled individually.
 
@@ -127,7 +127,7 @@ Drift detection works: the `verisim-drift` crate computes drift scores across mo
 |Missing
 |No mechanism to verify or enforce consistency across federation peers.
 
-|**VQL-DT PROOF over Federation**
+|**VCL-DT PROOF over Federation**
 |Missing
 |PROOF clauses parse but do not generate real proofs, even for local queries. Federation adds no additional proof capability.
 |===
@@ -157,9 +157,9 @@ Drift detection works: the `verisim-drift` crate computes drift scores across mo
 
 === Phase 3: Verified Federation
 
-**Goal:** VQL-DT proofs work across federation boundaries.
+**Goal:** VCL-DT proofs work across federation boundaries.
 
-* Wire Lean type checker into the VQL-DT execution path (prerequisite: VQL-DT Phase 3 from link:vql-vs-vql-dt.adoc[VQL Slipstream vs VQL-DT]).
+* Wire Lean type checker into the VCL-DT execution path (prerequisite: VCL-DT Phase 3 from link:vcl-vs-vcl-dt.adoc[VQL Slipstream vs VCL-DT]).
 * Implement proof witness collection across peers: each peer contributes its portion of the proof.
 * Implement Raft consensus for coordinated writes (cross-instance referential integrity).
 * Implement `PROOF CONSISTENCY` verification across federation peers (cross-instance modal agreement).
diff --git a/docs/getting-started.adoc b/docs/getting-started.adoc
index c2e317e..b1a054e 100644
--- a/docs/getting-started.adoc
+++ b/docs/getting-started.adoc
@@ -291,7 +291,7 @@ show all scores back near zero.
 
 == Querying with VQL
 
-VeriSimDB uses its own query language, *VQL* (VeriSim Query Language),
+VeriSimDB uses its own query language, *VQL* (VeriSim Consonance Language),
 designed for cross-modal queries. VQL is not SQL -- it natively
 understands modalities and drift.
 
@@ -333,9 +333,9 @@ SELECT * FROM FEDERATION /*
 WHERE DOCUMENT.severity > GRAPH.importance
 ----
 
-=== VQL-DT (Formally Verified Queries)
+=== VCL-DT (Formally Verified Queries)
 
-VQL-DT extends VQL with proof certificates. Every result includes a
+VCL-DT extends VQL with proof certificates. Every result includes a
 cryptographic proof that the data satisfies stated constraints:
 
 [source,sql]
@@ -345,7 +345,7 @@ FROM HEXAD 'entity-id'
 PROOF EXISTENCE(entity-id), PROVENANCE(entity-id)
 ----
 
-NOTE: VQL-DT proof generation is under active development. The syntax
+NOTE: VCL-DT proof generation is under active development. The syntax
 parses correctly and proof obligations are extracted, but end-to-end
 verifiable certificates require the Lean type checker integration
 (planned for Q2 2026).
@@ -576,8 +576,8 @@ queries. The fallback warning can be safely ignored.
 
 == Next Steps
 
-* Read the link:VQL-SPEC.adoc[VQL Specification] for the full query language
-* See link:vql-examples.adoc[VQL Examples] for more query patterns
+* Read the link:VCL-SPEC.adoc[VQL Specification] for the full query language
+* See link:vcl-examples.adoc[VQL Examples] for more query patterns
 * Review link:federation-readiness.adoc[Federation Readiness] for deployment planning
 * Explore link:drift-handling.adoc[Drift Handling] for advanced configuration
 * Check link:deployment-modes.adoc[Deployment Modes] for production setup
diff --git a/docs/panll-module-audit.adoc b/docs/panll-module-audit.adoc
index 8fedbb4..6dd0cf2 100644
--- a/docs/panll-module-audit.adoc
+++ b/docs/panll-module-audit.adoc
@@ -54,7 +54,7 @@ These repos are already identified as PanLL modules:
 
 | **VeriSimDB**
 | `nextgen-databases/verisimdb`
-| L: VQL-DT proofs, drift thresholds. N: Query planning, drift analysis. W: Entity data, drift heatmap.
+| L: VCL-DT proofs, drift thresholds. N: Query planning, drift analysis. W: Entity data, drift heatmap.
 
 | **QuandleDB**
 | `nextgen-databases/quandledb`
diff --git a/docs/papers/arcvix-octad-data-model.tex b/docs/papers/arcvix-octad-data-model.tex
index 47cd348..13d22dc 100644
--- a/docs/papers/arcvix-octad-data-model.tex
+++ b/docs/papers/arcvix-octad-data-model.tex
@@ -746,7 +746,7 @@ \subsection{Query Model}
 
 A key advantage of the octad model is that queries can \emph{span modality
 boundaries} while maintaining type safety.  We define a cross-modal query
-language, VQL (VeriSim Query Language), that supports modality-specific
+language, VQL (VeriSim Consonance Language), that supports modality-specific
 operations composed through a common identity layer.
 
 \begin{definition}[Cross-Modal Query]\label{def:query}
@@ -1549,7 +1549,7 @@ \subsection{Spatial Space $\Sigma_\mathsf{X}$}
 $\mathit{lat} \in [-90, 90]$, $\mathit{lon} \in [-180, 180]$, and optional
 altitude in metres.
 
-\section{VQL Grammar (EBNF Excerpt)}\label{app:vql-grammar}
+\section{VQL Grammar (EBNF Excerpt)}\label{app:vcl-grammar}
 
 \begin{lstlisting}[language={},caption={VQL grammar excerpt (EBNF)},
   basicstyle=\ttfamily\scriptsize]
diff --git a/docs/papers/verisimdb-federated-consistency.adoc b/docs/papers/verisimdb-federated-consistency.adoc
index f1961a1..2cadf00 100644
--- a/docs/papers/verisimdb-federated-consistency.adoc
+++ b/docs/papers/verisimdb-federated-consistency.adoc
@@ -25,7 +25,7 @@ Modern data systems increasingly store entities across multiple representation t
 This polyglot persistence pattern creates consistency challenges that existing solutions cannot detect: when one representation of an entity is updated, others may silently diverge, producing _cross-modal drift_ invisible to any single store.
 We present VeriSimDB, a multimodal database engine that maintains entities simultaneously across eight modalities (the "octad": Graph, Vector, Tensor, Semantic, Document, Temporal, Provenance, Spatial) and employs cross-modal drift detection to identify and repair representational divergence.
 Our approach introduces a drift scoring algorithm based on cosine distance between modality embeddings, with adaptive thresholds that account for natural representational variance.
-We describe VQL-DT, a query language extension that supports proof-carrying queries with 11 formally verified proof types, enabling clients to request cryptographic certificates attesting to the consistency, provenance, and integrity of query results.
+We describe VCL-DT, a query language extension that supports proof-carrying queries with 11 formally verified proof types, enabling clients to request cryptographic certificates attesting to the consistency, provenance, and integrity of query results.
 We evaluate VeriSimDB on a suite of 510 Rust and 152 Elixir tests encompassing synthetic drift injection, federation coordination, and proof verification scenarios.
 Results show that VeriSimDB detects semantic-vector drift with precision exceeding 0.95 and recall of 0.91, and repairs 94% of detected divergences automatically through its self-normalisation engine.
 Federation overhead for cross-instance queries remains below 12ms per additional peer for modality-specific queries.
@@ -63,7 +63,7 @@ This paper makes four contributions:
 
 3. **Self-Normalisation** -- an authority-ranked repair engine that identifies the most authoritative modality for a drifted entity and regenerates divergent representations, with five configurable strategies ranging from fully automatic to human-in-the-loop.
 
-4. **VQL-DT** -- a dependent-type extension to the VeriSim Query Language (VQL) that supports 11 proof types, enabling clients to request and verify formal certificates of data consistency, integrity, and provenance.
+4. **VCL-DT** -- a dependent-type extension to the VeriSim Consonance Language (VCL) that supports 11 proof types, enabling clients to request and verify formal certificates of data consistency, integrity, and provenance.
 
 
 // ============================================================================
@@ -97,7 +97,7 @@ A system can be perfectly consistent in the ACID sense (all replicas agree on th
 Proof-carrying data has been explored in the context of authenticated data structures <<tamassia2003>>, where Merkle trees and hash chains provide integrity certificates.
 CertikOS and seL4 demonstrate that formal verification can be applied to systems software, but database systems have largely resisted formal methods due to the complexity of query optimisation and storage management.
 
-VQL-DT draws inspiration from proof-carrying code <<necula1997>> and dependent type systems in languages such as Idris 2 <<brady2021>> and Lean 4 <<demoura2021>>, adapting these ideas to the database query context.
+VCL-DT draws inspiration from proof-carrying code <<necula1997>> and dependent type systems in languages such as Idris 2 <<brady2021>> and Lean 4 <<demoura2021>>, adapting these ideas to the database query context.
 
 === Marr's Three Levels of Analysis
 
@@ -369,14 +369,14 @@ Normalisation results are recorded as telemetry events including the entity ID,
 
 
 // ============================================================================
-// 6. VQL AND VQL-DT
+// 6. VQL AND VCL-DT
 // ============================================================================
 
-== VQL and VQL-DT
+== VQL and VCL-DT
 
 === VQL Syntax and Semantics
 
-The VeriSim Query Language (VQL) is the native query interface for VeriSimDB.
+The VeriSim Consonance Language (VCL) is the native query interface for VeriSimDB.
 Its grammar is specified in ISO/IEC 14977 EBNF notation <<iso14977>> and supports `SELECT`, `INSERT`, `UPDATE`, and `DELETE` operations across octad entities.
 
 A VQL query comprises:
@@ -406,12 +406,12 @@ Key differences include: no table schemas (entities are schema-flexible with typ
 
 === The PROOF Clause and 11 Proof Types
 
-VQL-DT (VQL with Dependent Types) is activated by the presence of a `PROOF` clause.
+VCL-DT (VQL with Dependent Types) is activated by the presence of a `PROOF` clause.
 When a query includes `PROOF`, the query router directs it through the formal verification pipeline rather than the standard (slipstream) execution path.
 
 The `PROOF` clause takes the form `PROOF <TYPE>(<Contract>)` and supports 11 proof types:
 
-.VQL-DT proof types
+.VCL-DT proof types
 [cols="1,3",options="header"]
 |===
 | Proof Type | Guarantee
@@ -462,7 +462,7 @@ PROOF INTEGRITY(DataIntegrityContract)
 
 === Proof Obligation Generation and Certificate Verification
 
-When a VQL-DT query is executed, the proof pipeline generates a _proof obligation_ for each requested proof type.
+When a VCL-DT query is executed, the proof pipeline generates a _proof obligation_ for each requested proof type.
 The obligation specifies:
 
 * The entity (or entities) to verify.
@@ -477,7 +477,7 @@ Clients can independently verify proof certificates without querying VeriSimDB,
 
 === Composition Strategies
 
-VQL-DT supports three composition strategies for multi-proof queries:
+VCL-DT supports three composition strategies for multi-proof queries:
 
 1. **Conjunction (AND)** -- All proofs must succeed for the query to return results. Failure of any proof aborts the query with a proof failure diagnostic.
 
@@ -558,7 +558,7 @@ The Elixir layer coordinates distributed operations using OTP's battle-tested su
 
 - **VeriSim.EntityServer**: A GenServer per entity, managing the entity's lifecycle and serialising concurrent updates. Entity servers are distributed across the cluster using Horde (a distributed DynamicSupervisor).
 - **VeriSim.DriftMonitor**: A GenServer that sweeps entities on a configurable interval, dispatching drift computation to the Rust core and queuing normalisation tasks.
-- **VeriSim.QueryRouter**: Routes VQL queries to the appropriate execution pipeline (slipstream vs VQL-DT) and handles federation decomposition.
+- **VeriSim.QueryRouter**: Routes VQL queries to the appropriate execution pipeline (slipstream vs VCL-DT) and handles federation decomposition.
 - **VeriSim.SchemaRegistry**: Manages entity type schemas and proof contracts, coordinating with the Semantic modality store.
 - **VeriSim.Consensus**: A KRaft-inspired (Kafka Raft) consensus implementation for metadata replication in clustered deployments.
 
@@ -685,12 +685,12 @@ The mean normalisation latency was 23ms for single-modality repairs and 87ms for
 | 5.7
 | 18.9
 
-| VQL-DT with INTEGRITY proof
+| VCL-DT with INTEGRITY proof
 | 8.3
 | 27.4
 |===
 
-VQL-DT queries incur approximately 2-3x the latency of slipstream queries due to proof generation and certificate construction.
+VCL-DT queries incur approximately 2-3x the latency of slipstream queries due to proof generation and certificate construction.
 
 === Federation Overhead
 
@@ -756,7 +756,7 @@ VeriSimDB's INTEGRITY proof type draws on this work, extending it from single-st
 
 **Formal methods in databases.**
 Amazon's use of TLA+ for DynamoDB <<newcombe2015>> demonstrates that formal methods can improve database reliability, but TLA+ is used for protocol verification, not query-level proofs.
-VQL-DT is, to our knowledge, the first query language to support proof-carrying results with dependent-type semantics.
+VCL-DT is, to our knowledge, the first query language to support proof-carrying results with dependent-type semantics.
 
 
 // ============================================================================
@@ -765,9 +765,9 @@ VQL-DT is, to our knowledge, the first query language to support proof-carrying
 
 == Future Work
 
-**Lean 4 integration for VQL-DT type checking.**
-The current VQL-DT type checker is implemented in Elixir with a bridge to the Rust ZKP module.
-We plan to integrate Lean 4 as an external proof assistant, enabling VQL-DT contracts to be expressed as Lean theorems and verified by Lean's kernel.
+**Lean 4 integration for VCL-DT type checking.**
+The current VCL-DT type checker is implemented in Elixir with a bridge to the Rust ZKP module.
+We plan to integrate Lean 4 as an external proof assistant, enabling VCL-DT contracts to be expressed as Lean theorems and verified by Lean's kernel.
 This would provide the highest level of formal assurance for proof certificates.
 
 **GraphRAG application integration.**
@@ -805,7 +805,7 @@ The octad model provides a principled foundation for multimodal entity managemen
 Cross-modal drift detection transforms consistency from an invisible hope into a measurable, actionable metric.
 Self-normalisation automates the most tedious and error-prone aspect of multi-system data management: keeping representations in agreement.
 
-VQL-DT extends this consistency guarantee to the query interface, enabling clients to not merely _hope_ that their data is consistent but to _prove_ it with cryptographic certificates.
+VCL-DT extends this consistency guarantee to the query interface, enabling clients to not merely _hope_ that their data is consistent but to _prove_ it with cryptographic certificates.
 The 11 proof types cover a range of assurance levels from basic existence checking to zero-knowledge proofs, allowing clients to select the appropriate level of verification for their use case.
 
 Federation extends these guarantees across organisational boundaries, enabling multi-institutional data sharing with configurable drift policies that balance consistency against latency and autonomy.
diff --git a/docs/query-optimization-overview.adoc b/docs/query-optimization-overview.adoc
index 13e399b..140c008 100644
--- a/docs/query-optimization-overview.adoc
+++ b/docs/query-optimization-overview.adoc
@@ -475,8 +475,8 @@ LIMIT 10
 
 == References
 
-- link:vql-architecture.adoc[VQL Architecture] - Dual-path router design
-- link:vql-examples.adoc[VQL Examples] - 35+ example queries
+- link:vcl-architecture.adoc[VQL Architecture] - Dual-path router design
+- link:vcl-examples.adoc[VQL Examples] - 35+ example queries
 - link:reversibility-design.adoc[Reversibility Design] - Full technical specification
 - link:../lib/verisim/query_planner_config.ex[Query Planner Config] - Source code
 - link:../lib/verisim/query_planner_bidirectional.ex[Bidirectional Optimization] - Source code
diff --git a/docs/reversibility-design.adoc b/docs/reversibility-design.adoc
index 297cf1f..449ee41 100644
--- a/docs/reversibility-design.adoc
+++ b/docs/reversibility-design.adoc
@@ -412,5 +412,5 @@ end
 
 - link:../WHITEPAPER.md[VeriSimDB White Paper] - Temporal modality design
 - link:technical-specification-kraft-metadata-log.adoc[KRaft Log] - Append-only log
-- link:vql-architecture.adoc[VQL Architecture] - Query execution
+- link:vcl-architecture.adoc[VQL Architecture] - Query execution
 - https://martin.kleppmann.com/2015/05/27/logs-for-data-infrastructure.html[Designing Data-Intensive Applications]
diff --git a/docs/safety-and-fault-tolerance.adoc b/docs/safety-and-fault-tolerance.adoc
index f25fbac..d9fa526 100644
--- a/docs/safety-and-fault-tolerance.adoc
+++ b/docs/safety-and-fault-tolerance.adoc
@@ -1155,7 +1155,7 @@ Invariant:
 
 - link:error-handling-strategy.adoc[Error Handling Strategy]
 - link:reversibility-design.adoc[Reversibility Design]
-- link:vql-architecture.adoc[VQL Architecture]
+- link:vcl-architecture.adoc[VQL Architecture]
 - link:../lib/verisim/supervisor.ex[Supervisor Tree Implementation]
 - https://www.erlang.org/doc/design_principles/des_princ.html[OTP Design Principles]
 - https://doc.rust-lang.org/book/ch04-01-what-is-ownership.html[Rust Ownership System]
diff --git a/docs/vql-architecture.adoc b/docs/vcl-architecture.adoc
similarity index 95%
rename from docs/vql-architecture.adoc
rename to docs/vcl-architecture.adoc
index 9dec88c..864dbed 100644
--- a/docs/vql-architecture.adoc
+++ b/docs/vcl-architecture.adoc
@@ -1,13 +1,13 @@
 // SPDX-License-Identifier: MPL-2.0
 
-= VQL Architecture: Dual-Path Query Router
+= VCL Architecture: Dual-Path Query Router
 :toc: left
 :toclevels: 3
 :sectnums:
 
 == Overview
 
-This document describes the **corrected** VQL (VeriSim Query Language) architecture, aligned with link:../design-decisions.adoc[Architecture Design Decisions] and the link:../WHITEPAPER.md[VeriSimDB White Paper].
+This document describes the **corrected** VCL (VeriSim Consonance Language) architecture, aligned with link:../design-decisions.adoc[Architecture Design Decisions] and the link:../WHITEPAPER.md[VeriSimDB White Paper].
 
 **Key Corrections from Initial Design:**
 
@@ -19,12 +19,12 @@ This document describes the **corrected** VQL (VeriSim Query Language) architect
 
 == 1. Core Architecture: Dual-Path Router
 
-VQL provides two execution paths for queries:
+VCL provides two execution paths for queries:
 
 [source,text]
 ----
                  ┌─────────────────┐
-                 │  VQL Query      │
+                 │  VCL Query      │
                  │  (raw string)   │
                  └────────┬────────┘
                           │
@@ -82,7 +82,7 @@ src/vql/
 
 [source,rescript]
 // VQLRouter.res
-module VQL = {
+module VCL = {
   type queryMetadata = {
     queryId: string,
     timestamp: float,
@@ -361,7 +361,7 @@ end
 defmodule VeriSim.DriftMonitor do
   @moduledoc """
   Detects and repairs drift across federated nodes.
-  Integrates with VQL query path.
+  Integrates with VCL query path.
   """
 
   use GenServer
@@ -419,17 +419,17 @@ end
 module Endpoint = {
   @post("/api/v1/query")
   let queryEndpoint = (req: {body: string, headers: dict<string>}) => {
-    let useDependentTypes = Dict.get(req.headers, "X-VQL-Safe") == Some("true")
+    let useDependentTypes = Dict.get(req.headers, "X-VCL-Safe") == Some("true")
 
     // Parse and route query
-    let result = VQL.handleQuery(req.body, useDependentTypes)
+    let result = VCL.handleQuery(req.body, useDependentTypes)
 
     // Return with appropriate headers
     {
       status: 200,
       headers: {
         "Content-Type": "application/json",
-        "X-VQL-Verified": result.verified ? "true" : "false",
+        "X-VCL-Verified": result.verified ? "true" : "false",
         "X-Query-ID": result.queryId,
       },
       body: JSON.stringify(result),
@@ -443,7 +443,7 @@ module Endpoint = {
 **ReScript Client:**
 
 [source,rescript]
-// Client SDK for VQL
+// Client SDK for VCL
 module VQLClient = {
   type queryOptions = {
     useDependentTypes: bool,
@@ -453,7 +453,7 @@ module VQLClient = {
 
   let query = async (vql: string, options: queryOptions) => {
     let headers = options.useDependentTypes
-      ? {"X-VQL-Safe": "true", "Content-Type": "text/vql"}
+      ? {"X-VCL-Safe": "true", "Content-Type": "text/vql"}
       : {"Content-Type": "text/vql"}
 
     let response = await fetch("/api/v1/query", {
@@ -595,7 +595,7 @@ let searchPapers = async () => {
 
 === Phase 1: Grammar & Slipstream Parser (Week 1-2)
 
-- [ ] Finalize VQL grammar (link:vql-grammar.ebnf[])
+- [ ] Finalize VCL grammar (link:vcl-grammar.ebnf[])
 - [ ] Implement slipstream parser in ReScript
 - [ ] Add basic AST types
 - [ ] Test with simple queries
@@ -616,15 +616,15 @@ let searchPapers = async () => {
 
 === Phase 4: WASM Endpoint (Week 7-8)
 
-- [ ] Compile VQL to WASM
+- [ ] Compile VCL to WASM
 - [ ] Deploy behind Cloudflare SDP
 - [ ] Add rate limiting
 - [ ] Complete audit logging
 
 == 7. References
 
-- link:vql-grammar.ebnf[VQL Grammar (EBNF)]
-- link:vql-examples.adoc[VQL Examples]
+- link:vcl-grammar.ebnf[VCL Grammar (EBNF)]
+- link:vcl-examples.adoc[VCL Examples]
 - link:../WHITEPAPER.md[VeriSimDB White Paper]
 - link:../design-decisions.adoc[Architecture Design Decisions]
 - link:technical-specification-kraft-metadata-log.adoc[KRaft Metadata Log]
diff --git a/docs/vql-examples.adoc b/docs/vcl-examples.adoc
similarity index 98%
rename from docs/vql-examples.adoc
rename to docs/vcl-examples.adoc
index ee5bd45..c0a4091 100644
--- a/docs/vql-examples.adoc
+++ b/docs/vcl-examples.adoc
@@ -1,13 +1,13 @@
 // SPDX-License-Identifier: MPL-2.0
 
-= VeriSim Query Language (VQL) Examples
+= VeriSim Consonance Language (VCL) Examples
 :toc: left
 :toclevels: 3
 :sectnums:
 
 == Overview
 
-This document provides **63 comprehensive examples** of VQL queries and mutations for both **dependent-type** (formally verified) and **slipstream** (fast, unverified) paths, including backwards compatibility (VERSION), drift handling (DRIFT REPAIR), SQL-compatible extensions (ORDER BY, GROUP BY, HAVING, aggregates, column projections), multi-proof composition, cross-modal correlation conditions, and write path mutations (INSERT/UPDATE/DELETE).
+This document provides **63 comprehensive examples** of VCL queries and mutations for both **dependent-type** (formally verified) and **slipstream** (fast, unverified) paths, including backwards compatibility (VERSION), drift handling (DRIFT REPAIR), SQL-compatible extensions (ORDER BY, GROUP BY, HAVING, aggregates, column projections), multi-proof composition, cross-modal correlation conditions, and write path mutations (INSERT/UPDATE/DELETE).
 
 == Basic Queries
 
@@ -498,7 +498,7 @@ WHERE (h)-[:INVALID_SYNTAX
 ----
 {
   "error": "ParseError",
-  "message": "Failed to parse VQL query",
+  "message": "Failed to parse VCL query",
   "details": {
     "line": 3,
     "column": 27,
@@ -606,7 +606,7 @@ LIMIT 100
 
 == Summary
 
-VQL provides two execution paths:
+VCL provides two execution paths:
 
 1. **Dependent-Type Path** (`PROOF` clause present):
    - Formal verification via `proven-library`
@@ -636,7 +636,7 @@ Use slipstream path for:
 
 === Example 36: Version Pinning
 
-**Query with explicit VQL version:**
+**Query with explicit VCL version:**
 [source,vql]
 ----
 VERSION 1.0;
@@ -825,7 +825,7 @@ LIMIT 50
 
 === Example 47: Full SQL-Compatible Query
 
-**Combining all SQL-compatible features with VQL's model:**
+**Combining all SQL-compatible features with VCL's model:**
 [source,vql]
 ----
 SELECT DOCUMENT.name, DOCUMENT.severity, COUNT(*), SUM(DOCUMENT.severity), AVG(DOCUMENT.severity)
@@ -840,7 +840,7 @@ OFFSET 20
 
 === Example 48: SQL-Compatible with Dependent-Type Verification
 
-**Combining aggregates with formal verification (VQL-dt path):**
+**Combining aggregates with formal verification (VCL-dt path):**
 [source,vql]
 ----
 SELECT DOCUMENT.name, COUNT(*)
@@ -1069,7 +1069,7 @@ ensures the deletion is recorded in the audit chain.
 
 == References
 
-- link:vql-grammar.ebnf[VQL Grammar (EBNF)]
+- link:vcl-grammar.ebnf[VCL Grammar (EBNF)]
 - link:backwards-compatibility.adoc[Backwards Compatibility Strategy]
 - link:drift-handling.adoc[Drift Handling Documentation]
 - link:../WHITEPAPER.md[VeriSimDB White Paper]
diff --git a/docs/vql-formal-semantics.adoc b/docs/vcl-formal-semantics.adoc
similarity index 97%
rename from docs/vql-formal-semantics.adoc
rename to docs/vcl-formal-semantics.adoc
index 76a0d35..a9e36d1 100644
--- a/docs/vql-formal-semantics.adoc
+++ b/docs/vcl-formal-semantics.adoc
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: MPL-2.0
 
-= VQL Formal Semantics
+= VCL Formal Semantics
 :toc: left
 :toclevels: 4
 :sectnums:
@@ -8,7 +8,7 @@
 
 == Overview
 
-This document specifies the **formal operational semantics** and **static type system** for VeriSim Query Language (VQL). VQL has two execution paths with different semantic guarantees:
+This document specifies the **formal operational semantics** and **static type system** for VeriSim Consonance Language (VCL). VCL has two execution paths with different semantic guarantees:
 
 1. **Dependent-Type Path** - Queries with `PROOF` clause, formally verified via ZKP
 2. **Slipstream Path** - Queries without `PROOF` clause, fast but unverified
@@ -45,7 +45,7 @@ We use standard mathematical notation for formal semantics:
 
 == Syntax (Abstract)
 
-We define the abstract syntax of VQL (concrete syntax in link:vql-grammar.ebnf[vql-grammar.ebnf]):
+We define the abstract syntax of VCL (concrete syntax in link:vcl-grammar.ebnf[vcl-grammar.ebnf]):
 
 ----
 Query       ::= SELECT Modalities FROM Source [WHERE Condition]
@@ -72,7 +72,7 @@ ProofType   ::= EXISTENCE | CITATION | ACCESS | INTEGRITY | PROVENANCE | CUSTOM
 
 === Base Types
 
-VQL has the following base types:
+VCL has the following base types:
 
 ----
 τ ::= UUID                          -- 128-bit identifier
@@ -421,7 +421,7 @@ For each proof type, we specify the **proposition** stem:[\phi] that must be pro
 
 === Proof Generation
 
-For dependent-type queries, VQL delegates to **proven-library** (external ZKP framework):
+For dependent-type queries, VCL delegates to **proven-library** (external ZKP framework):
 
 [stem]
 ++++
@@ -645,8 +645,8 @@ Where stem:[\phi] is automatically inferred from the query structure.
 
 == References
 
-- link:vql-grammar.ebnf[VQL Grammar (ISO EBNF)]
-- link:vql-type-system.adoc[VQL Type System Specification]
+- link:vcl-grammar.ebnf[VCL Grammar (ISO EBNF)]
+- link:vcl-type-system.adoc[VCL Type System Specification]
 - link:backwards-compatibility.adoc[Backwards Compatibility (VERSION semantics)]
 - link:drift-handling.adoc[Drift Handling (DRIFT semantics)]
 - Pierce, B. C. (2002). *Types and Programming Languages*. MIT Press.
diff --git a/docs/vql-grammar.ebnf b/docs/vcl-grammar.ebnf
similarity index 99%
rename from docs/vql-grammar.ebnf
rename to docs/vcl-grammar.ebnf
index e66aa65..0142a33 100644
--- a/docs/vql-grammar.ebnf
+++ b/docs/vcl-grammar.ebnf
@@ -1,5 +1,5 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
-(* VeriSim Query Language (VQL) Grammar *)
+(* VeriSim Consonance Language (VCL) Grammar *)
 (* Format: Extended Backus-Naur Form (EBNF) *)
 (* Version: 3.0 — Octad (8 modalities), provenance conditions, spatial conditions *)
 (* Date: 2026-02-27 *)
@@ -292,7 +292,7 @@ comment = '--', { ? any character except newline ? }, '\n'  (* Line comment *)
 (* ============================================================================
    12. RESERVED KEYWORDS
    ============================================================================ *)
-(* Keywords are case-insensitive in VQL *)
+(* Keywords are case-insensitive in VCL *)
 keywords = 'SELECT' | 'FROM' | 'WHERE' | 'PROOF' | 'LIMIT' | 'OFFSET'
          | 'GRAPH' | 'VECTOR' | 'TENSOR' | 'SEMANTIC' | 'DOCUMENT' | 'TEMPORAL' | 'PROVENANCE' | 'SPATIAL'
          | 'HEXAD' | 'FEDERATION' | 'STORE'
diff --git a/docs/vql-type-system.adoc b/docs/vcl-type-system.adoc
similarity index 97%
rename from docs/vql-type-system.adoc
rename to docs/vcl-type-system.adoc
index e668d47..92744a0 100644
--- a/docs/vql-type-system.adoc
+++ b/docs/vcl-type-system.adoc
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: MPL-2.0
 
-= VQL Type System Specification
+= VCL Type System Specification
 :toc: left
 :toclevels: 4
 :sectnums:
@@ -8,21 +8,21 @@
 
 == Overview
 
-This document specifies the **static type system** for VQL, including:
+This document specifies the **static type system** for VCL, including:
 
 1. Type syntax and semantics
-2. Typing rules for all VQL constructs
+2. Typing rules for all VCL constructs
 3. Type checking algorithm
 4. Subtyping and type equivalence
 5. Differences between dependent-type and slipstream paths
 
-This complements link:vql-formal-semantics.adoc[VQL Formal Semantics] which covers operational semantics.
+This complements link:vcl-formal-semantics.adoc[VCL Formal Semantics] which covers operational semantics.
 
 == Type Language
 
 === Type Syntax
 
-The VQL type language stem:[\tau] is defined by:
+The VCL type language stem:[\tau] is defined by:
 
 [stem]
 ++++
@@ -683,7 +683,7 @@ Two types are **semantically equal** if they denote the same set of values:
 
 === Bidirectional Type Checking
 
-VQL uses **bidirectional type checking** with two modes:
+VCL uses **bidirectional type checking** with two modes:
 
 1. **Synthesis (stem:[\Uparrow])**: Infer type of an expression
 2. **Checking (stem:[\Downarrow])**: Check expression against expected type
@@ -772,7 +772,7 @@ check_proved_query Γ (SELECT M ... PROOF P) =
 
 === Type Inference
 
-Some VQL constructs support **type inference**:
+Some VCL constructs support **type inference**:
 
 ==== Vector Dimension Inference
 
@@ -914,8 +914,8 @@ Ensure ZKP witnesses are used exactly once:
 
 == References
 
-- link:vql-formal-semantics.adoc[VQL Formal Semantics]
-- link:vql-grammar.ebnf[VQL Grammar]
+- link:vcl-formal-semantics.adoc[VCL Formal Semantics]
+- link:vcl-grammar.ebnf[VCL Grammar]
 - Pierce, B. C. (2002). *Types and Programming Languages*. MIT Press.
 - Pierce, B. C. (ed.) (2005). *Advanced Topics in Types and Programming Languages*. MIT Press.
 - Chlipala, A. (2013). *Certified Programming with Dependent Types*. MIT Press.
diff --git a/docs/vql-vs-sql.adoc b/docs/vcl-vs-sql.adoc
similarity index 85%
rename from docs/vql-vs-sql.adoc
rename to docs/vcl-vs-sql.adoc
index b5f71f7..ba06186 100644
--- a/docs/vql-vs-sql.adoc
+++ b/docs/vcl-vs-sql.adoc
@@ -1,26 +1,26 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
-= VQL vs SQL: A Comparative Guide
+= VCL vs SQL: A Comparative Guide
 :toc: left
 :toclevels: 3
 :sectnums:
 
 == Introduction
 
-VQL (VeriSim Query Language) is the query language for VeriSimDB, a 6-core multimodal database. While VQL borrows familiar keywords from SQL (`SELECT`, `FROM`, `WHERE`, `LIMIT`, `OFFSET`), it serves a fundamentally different purpose.
+VCL (VeriSim Consonance Language) is the query language for VeriSimDB, a 6-core multimodal database. While VCL borrows familiar keywords from SQL (`SELECT`, `FROM`, `WHERE`, `LIMIT`, `OFFSET`), it serves a fundamentally different purpose.
 
-VQL is **read-only**. It does not support `INSERT`, `UPDATE`, or `DELETE` statements. All mutations go through the Octad API (Rust core or Elixir orchestration layer). This is a deliberate design choice: VeriSimDB treats writes as coordinated multi-modal operations that must maintain consistency across all six modality stores (Graph, Vector, Tensor, Semantic, Document, Temporal). A simple `INSERT` statement cannot express the cross-modal invariants that a Octad write requires.
+VCL is **read-only**. It does not support `INSERT`, `UPDATE`, or `DELETE` statements. All mutations go through the Octad API (Rust core or Elixir orchestration layer). This is a deliberate design choice: VeriSimDB treats writes as coordinated multi-modal operations that must maintain consistency across all six modality stores (Graph, Vector, Tensor, Semantic, Document, Temporal). A simple `INSERT` statement cannot express the cross-modal invariants that a Octad write requires.
 
-VQL is **multimodal**. Where SQL selects columns from relational tables, VQL selects _modalities_ from _octad stores_ or _federations_. A single VQL query can retrieve graph edges, vector embeddings, tensor slices, semantic annotations, document text, and temporal versions in one pass.
+VCL is **multimodal**. Where SQL selects columns from relational tables, VCL selects _modalities_ from _octad stores_ or _federations_. A single VCL query can retrieve graph edges, vector embeddings, tensor slices, semantic annotations, document text, and temporal versions in one pass.
 
-VQL is **federation-aware**. Queries can target a local `STORE`, a specific `HEXAD` entity, or a `FEDERATION` of distributed VeriSimDB instances, with configurable drift policies governing cross-instance consistency.
+VCL is **federation-aware**. Queries can target a local `STORE`, a specific `HEXAD` entity, or a `FEDERATION` of distributed VeriSimDB instances, with configurable drift policies governing cross-instance consistency.
 
 == Concept Comparison
 
 [cols="2,3,3",options="header"]
 |===
-|Concept |VQL |SQL
+|Concept |VCL |SQL
 
 |**Column/Field Selection**
 |`SELECT` with _modalities_: `GRAPH`, `VECTOR`, `TENSOR`, `SEMANTIC`, `DOCUMENT`, `TEMPORAL`, or `*` (all six). Modalities can be combined: `SELECT GRAPH, VECTOR, SEMANTIC`.
@@ -39,7 +39,7 @@ VQL is **federation-aware**. Queries can target a local `STORE`, a specific `HEX
 |`JOIN`, `LEFT JOIN`, `RIGHT JOIN`, `FULL OUTER JOIN`, `CROSS JOIN` with `ON` conditions.
 
 |**Mutations**
-|**None.** VQL is strictly read-only. All writes go through the Octad API: `POST /api/octads` (create), `PUT /api/octads/:id` (update), `DELETE /api/octads/:id` (delete). This ensures cross-modal consistency.
+|**None.** VCL is strictly read-only. All writes go through the Octad API: `POST /api/octads` (create), `PUT /api/octads/:id` (update), `DELETE /api/octads/:id` (delete). This ensures cross-modal consistency.
 |`INSERT INTO`, `UPDATE ... SET`, `DELETE FROM`, `MERGE`, `TRUNCATE`.
 
 |**Verification**
@@ -51,13 +51,13 @@ VQL is **federation-aware**. Queries can target a local `STORE`, a specific `HEX
 |`LIMIT n` and `OFFSET n` (or vendor-specific: `TOP`, `FETCH FIRST`).
 |===
 
-== What VQL Lacks That SQL Has
+== What VCL Lacks That SQL Has
 
-VQL is intentionally minimal. The following SQL features have no VQL equivalent:
+VCL is intentionally minimal. The following SQL features have no VCL equivalent:
 
 [cols="2,3",options="header"]
 |===
-|SQL Feature |VQL Status
+|SQL Feature |VCL Status
 
 |`GROUP BY`
 |Not supported. Aggregation is performed application-side or through the Elixir orchestration layer.
@@ -66,7 +66,7 @@ VQL is intentionally minimal. The following SQL features have no VQL equivalent:
 |Not supported. Result ordering is determined by the modality store (e.g., vector similarity ranking, graph traversal order, temporal chronological order).
 
 |Aggregate functions (`COUNT`, `SUM`, `AVG`, `MIN`, `MAX`)
-|Not supported. VQL returns raw data; aggregation is a consumer responsibility.
+|Not supported. VCL returns raw data; aggregation is a consumer responsibility.
 
 |Subqueries
 |Not supported. Queries are flat. Compose results in application code or use the Elixir query router for multi-step workflows.
@@ -90,14 +90,14 @@ VQL is intentionally minimal. The following SQL features have no VQL equivalent:
 |Not supported. Business logic lives in the Elixir orchestration layer.
 |===
 
-== What VQL Has That SQL Lacks
+== What VCL Has That SQL Lacks
 
 [cols="2,3",options="header"]
 |===
-|VQL Feature |Description
+|VCL Feature |Description
 
 |`PROOF` clause
-|Requests a verifiable proof certificate alongside query results. Six proof types cover existence, integrity, consistency, provenance, freshness, and authorization guarantees. Enables dependent-type verification via the VQL-DT path.
+|Requests a verifiable proof certificate alongside query results. Six proof types cover existence, integrity, consistency, provenance, freshness, and authorization guarantees. Enables dependent-type verification via the VCL-DT path.
 
 |Multimodal `SELECT`
 |Select specific modalities (`GRAPH`, `VECTOR`, `TENSOR`, `SEMANTIC`, `DOCUMENT`, `TEMPORAL`) or all (`*`). No SQL equivalent for querying fundamentally different data representations of the same entity.
@@ -133,14 +133,14 @@ FROM entities
 WHERE id = '550e8400-e29b-41d4-a716-446655440000';
 ----
 
-**VQL (Slipstream):**
+**VCL (Slipstream):**
 [source,vql]
 ----
 SELECT *
 FROM HEXAD 550e8400-e29b-41d4-a716-446655440000
 ----
 
-The VQL version returns all six modalities for that octad. The SQL version returns only the columns in the `entities` table.
+The VCL version returns all six modalities for that octad. The SQL version returns only the columns in the `entities` table.
 
 === Finding Related Entities
 
@@ -155,7 +155,7 @@ WHERE e1.id = '550e8400-e29b-41d4-a716-446655440000'
   AND r.type = 'CITES';
 ----
 
-**VQL (graph traversal):**
+**VCL (graph traversal):**
 [source,vql]
 ----
 SELECT GRAPH
@@ -163,7 +163,7 @@ FROM HEXAD 550e8400-e29b-41d4-a716-446655440000
 WHERE (h)-[:CITES]->(target)
 ----
 
-VQL eliminates the triple-table JOIN pattern entirely. Graph relationships are native.
+VCL eliminates the triple-table JOIN pattern entirely. Graph relationships are native.
 
 === Full-Text Search
 
@@ -175,7 +175,7 @@ FROM documents
 WHERE to_tsvector('english', content) @@ to_tsquery('quantum & computing');
 ----
 
-**VQL:**
+**VCL:**
 [source,vql]
 ----
 SELECT DOCUMENT
@@ -195,7 +195,7 @@ ORDER BY embedding <-> '[0.1, 0.2, 0.3, 0.4]'
 LIMIT 10;
 ----
 
-**VQL:**
+**VCL:**
 [source,vql]
 ----
 SELECT VECTOR
@@ -206,7 +206,7 @@ LIMIT 10
 
 === Verified Query (No SQL Equivalent)
 
-**VQL-DT (dependent type path):**
+**VCL-DT (dependent type path):**
 [source,vql]
 ----
 SELECT *
@@ -220,7 +220,7 @@ This returns the octad data _plus_ a cryptographic proof certificate asserting d
 
 [cols="2,1,1",options="header"]
 |===
-|Capability |SQL |VQL
+|Capability |SQL |VCL
 
 |Relational queries |Yes |No
 |Multimodal queries |No |Yes
@@ -237,4 +237,4 @@ This returns the octad data _plus_ a cryptographic proof certificate asserting d
 |Pagination (LIMIT/OFFSET) |Yes |Yes
 |===
 
-VQL is not a replacement for SQL. It is a purpose-built query language for a multimodal database that treats entities as six simultaneous representations rather than rows in flat tables. Use SQL when you need relational algebra. Use VQL when you need to query across modalities with optional formal verification.
+VCL is not a replacement for SQL. It is a purpose-built query language for a multimodal database that treats entities as six simultaneous representations rather than rows in flat tables. Use SQL when you need relational algebra. Use VCL when you need to query across modalities with optional formal verification.
diff --git a/docs/vql-vs-vql-dt.adoc b/docs/vcl-vs-vcl-dt.adoc
similarity index 86%
rename from docs/vql-vs-vql-dt.adoc
rename to docs/vcl-vs-vcl-dt.adoc
index ca7acbc..304e176 100644
--- a/docs/vql-vs-vql-dt.adoc
+++ b/docs/vcl-vs-vcl-dt.adoc
@@ -1,38 +1,38 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
-= VQL Execution Modes & Safety Architecture
+= VCL Execution Modes & Safety Architecture
 :toc: left
 :toclevels: 3
 :sectnums:
 
 == Overview
 
-VQL has two distinct concerns, cleanly separated:
+VCL has two distinct concerns, cleanly separated:
 
-1. **VQL** -- The query language itself. Parsing, basic types, execution. What users write.
-2. **VQL-UT** -- The safety pipeline. Applies 10 progressive type-safety levels behind VQL.
-   Users write VQL; VQL-UT validates it.
+1. **VCL** -- The query language itself. Parsing, basic types, execution. What users write.
+2. **VCL-UT** -- The safety pipeline. Applies 10 progressive type-safety levels behind VCL.
+   Users write VCL; VCL-UT validates it.
 
-Within VQL execution, there are two modes, determined by the presence or absence
+Within VCL execution, there are two modes, determined by the presence or absence
 of a `PROOF` clause:
 
-* **Slipstream** -- Fast, progressive safety (VQL-UT levels apply automatically based
+* **Slipstream** -- Fast, progressive safety (VCL-UT levels apply automatically based
   on query complexity — simple queries exit early at L1-L2, complex queries go deeper).
 * **Proof-carrying** -- Formally verified queries. The `PROOF` clause triggers dependent
   type checking, proof obligation generation, and a proof certificate attached to the
-  result. This corresponds to VQL-UT levels L9-L10.
+  result. This corresponds to VCL-UT levels L9-L10.
 
 Both modes use the same parser and produce the same AST. They diverge at the query
 router, which inspects the AST for a `PROOF` node and selects the appropriate pipeline.
 
-=== Historical Note: VQL-DT
+=== Historical Note: VCL-DT
 
-VQL-DT (Dependent Types) was the original name for the proof-carrying execution mode.
-It is not a separate codebase or product — it is an internal execution path within VQL,
-now folded into VQL-UT's L9 (Proof Attachment) and L10 (Cross-Cutting) levels. All
-references to "VQL-DT" in older documentation should be read as "VQL proof-carrying mode"
-or "VQL-UT L9-L10".
+VCL-DT (Dependent Types) was the original name for the proof-carrying execution mode.
+It is not a separate codebase or product — it is an internal execution path within VCL,
+now folded into VCL-UT's L9 (Proof Attachment) and L10 (Cross-Cutting) levels. All
+references to "VCL-DT" in older documentation should be read as "VCL proof-carrying mode"
+or "VCL-UT L9-L10".
 
 == The Two-Tier Model
 
@@ -40,19 +40,19 @@ or "VQL-UT L9-L10".
 |===
 | Tier | What | How
 
-| **VQL**
+| **VCL**
 | The query language
 | Parser (ReScript) → AST → basic validation. Everyone uses this.
 
-| **VQL-UT**
+| **VCL-UT**
 | The safety pipeline
-| 10 progressive levels. Sits behind VQL. Applies automatically.
+| 10 progressive levels. Sits behind VCL. Applies automatically.
   Simple queries short-circuit at L1-L2. Complex/federated/proof-carrying
-  queries go through L5-L10. No separate syntax — VQL-UT is invisible
+  queries go through L5-L10. No separate syntax — VCL-UT is invisible
   to the user except when they add a `PROOF` clause.
 |===
 
-== VQL-UT Safety Levels (Progressive)
+== VCL-UT Safety Levels (Progressive)
 
 The pipeline is progressive — each query enters at L1 and exits as soon as
 remaining levels don't apply. A simple `SELECT` exits at L2. A `PROOF INTEGRITY`
@@ -75,7 +75,7 @@ query goes all the way to L10.
 |===
 
 Levels L1-L8 apply automatically (slipstream). Levels L9-L10 activate when the
-query includes a `PROOF` clause — this is what was previously called "VQL-DT".
+query includes a `PROOF` clause — this is what was previously called "VCL-DT".
 
 == Slipstream Mode (Default)
 
@@ -94,7 +94,7 @@ WHERE CONTAINS(h.content, "neural network")
 LIMIT 50
 ----
 
-This query enters VQL-UT at L1 (injection prevention), passes L2 (schema
+This query enters VCL-UT at L1 (injection prevention), passes L2 (schema
 check), and exits. L3-L10 don't apply — no connections to leak, no proofs
 requested.
 
@@ -115,7 +115,7 @@ FROM HEXAD 550e8400-e29b-41d4-a716-446655440000
 PROOF INTEGRITY(DataIntegrityContract)
 ----
 
-This query passes through all 10 VQL-UT levels. At L9, proof obligations are
+This query passes through all 10 VCL-UT levels. At L9, proof obligations are
 generated. At L10, the proof certificate is assembled and attached to the result.
 
 == The Six PROOF Types
@@ -198,12 +198,12 @@ that apply — a simple SELECT is essentially free beyond parsing.
 [source,text]
 ----
                   ┌──────────────────┐
-                  │  VQL Query       │
+                  │  VCL Query       │
                   │  (raw string)    │
                   └────────┬─────────┘
                            │
                   ┌────────▼─────────┐
-                  │  VQL Parser      │
+                  │  VCL Parser      │
                   │  (ReScript)      │
                   └────────┬─────────┘
                            │
@@ -212,7 +212,7 @@ that apply — a simple SELECT is essentially free beyond parsing.
                   └────────┬─────────┘
                            │
               ┌────────────▼────────────┐
-              │   VQL-UT Pipeline       │
+              │   VCL-UT Pipeline       │
               │                         │
               │  L1: Construction ──┐   │
               │  L2: Schema ────────┤   │
@@ -243,7 +243,7 @@ that apply — a simple SELECT is essentially free beyond parsing.
 | Phase | Work | Status
 
 | Phase 1
-| VQL parser handles PROOF clauses, AST includes proof nodes, query router branches correctly.
+| VCL parser handles PROOF clauses, AST includes proof nodes, query router branches correctly.
 | Done
 
 | Phase 2
diff --git a/elixir-orchestration/test/verisim/query/vql_e2e_test.exs b/elixir-orchestration/test/verisim/query/vql_e2e_test.exs
index 9c2234a..2f2b51c 100644
--- a/elixir-orchestration/test/verisim/query/vql_e2e_test.exs
+++ b/elixir-orchestration/test/verisim/query/vql_e2e_test.exs
@@ -6,7 +6,7 @@ defmodule VeriSim.Query.VQLE2ETest do
 
     VQL string → parse → typecheck → plan → execute → result
 
-  These tests validate the VQL-SPEC contract by exercising every major
+  These tests validate the VCL-SPEC contract by exercising every major
   language feature through the complete pipeline. They are designed to
   pass both with and without the Rust core running:
 
@@ -18,7 +18,7 @@ defmodule VeriSim.Query.VQLE2ETest do
 
   1. **Full pipeline round-trip** — parse → typecheck → execute for each query shape
   2. **Proof certificate round-trip** — typecheck → generate cert → verify cert
-  3. **VQL-SPEC grammar coverage** — every production in vql-grammar.ebnf tested
+  3. **VCL-SPEC grammar coverage** — every production in vcl-grammar.ebnf tested
   4. **Error paths** — malformed queries, invalid proof types, bad modality combos
   5. **Cross-modal condition evaluation** — drift, consistency, exists checks
   6. **Mutation pipeline** — INSERT/UPDATE/DELETE parse → execute routing
@@ -249,10 +249,10 @@ defmodule VeriSim.Query.VQLE2ETest do
   end
 
   # ===========================================================================
-  # 3. VQL-SPEC grammar coverage
+  # 3. VCL-SPEC grammar coverage
   # ===========================================================================
 
-  describe "VQL-SPEC grammar coverage" do
+  describe "VCL-SPEC grammar coverage" do
     test "SELECT with column projection (not star)" do
       query = "SELECT DOCUMENT.title, DOCUMENT.body FROM HEXAD 'entity-001'"
       ast = H.parse!(query)
diff --git a/formal/VCL.v b/formal/VCL.v
index c111329..21f4e7a 100644
--- a/formal/VCL.v
+++ b/formal/VCL.v
@@ -6,7 +6,7 @@
     Mechanises the foundation-pack theorem V2 (vql_preservation) for
     VCL (the VeriSim Consonance Language; renamed from VQL on
     2026-04-05). The original semantics in
-    [docs/vql-formal-semantics.adoc] use BIG-STEP evaluation
+    [docs/vcl-formal-semantics.adoc] use BIG-STEP evaluation
     [e ⇓ v], which does not compose with preservation as classically
     stated. This module closes #92 by introducing a minimal
     SMALL-STEP calculus and proving preservation against it.
diff --git a/spec/grammar.ebnf b/spec/grammar.ebnf
index 096d0aa..625d3dd 100644
--- a/spec/grammar.ebnf
+++ b/spec/grammar.ebnf
@@ -1,7 +1,7 @@
 (* @taxonomy: spec/grammar *)
 (* SPDX-License-Identifier: MPL-2.0 *)
 (* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> *)
-(* VeriSim Query Language (VQL) Grammar *)
+(* VeriSim Consonance Language (VCL) Grammar *)
 (* Format: Extended Backus-Naur Form (EBNF) *)
 (* Version: 3.0 — Octad (8 modalities), provenance conditions, spatial conditions *)
 (* Date: 2026-02-27 *)
diff --git a/src/vql/VQLTypes.res b/src/vql/VQLTypes.res
index 25c8036..3f0a6a1 100644
--- a/src/vql/VQLTypes.res
+++ b/src/vql/VQLTypes.res
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: MPL-2.0
 // VQL Types — Core type definitions for the bidirectional type checker
 //
-// Implements the type system from vql-type-system.adoc:
+// Implements the type system from vcl-type-system.adoc:
 // - Pi types (dependent function types)
 // - Sigma types (dependent pair types)
 // - Modality types
diff --git a/sync-wiki.sh b/sync-wiki.sh
index 58823bd..f325438 100755
--- a/sync-wiki.sh
+++ b/sync-wiki.sh
@@ -254,12 +254,12 @@ only — they're not wiki-friendly formats. View them at:
 
 ## VQL language
 
-- [VQL-SPEC.adoc](VQL-SPEC.adoc) — full VQL specification
-- [VQL-vql-grammar.ebnf](VQL-vql-grammar.ebnf) — formal EBNF (or browse the file in the repo)
+- [VCL-SPEC.adoc](VCL-SPEC.adoc) — full VCL specification
+- [vcl-grammar.ebnf](vcl-grammar.ebnf) — formal EBNF (or browse the file in the repo)
 - [VQL-getting-started.adoc](getting-started.adoc) — step-by-step setup
-- [VQL-vql-formal-semantics.adoc](vql-formal-semantics.adoc) — operational semantics
-- [VQL-vql-type-system.adoc](vql-type-system.adoc) — dependent types + bidirectional checking
-- [VQL-vql-examples.adoc](vql-examples.adoc) — worked examples
+- [vcl-formal-semantics.adoc](vcl-formal-semantics.adoc) — operational semantics
+- [vcl-type-system.adoc](vcl-type-system.adoc) — dependent types + bidirectional checking
+- [vcl-examples.adoc](vcl-examples.adoc) — worked examples
 
 …and many more under the synced page list — see the sidebar.
 
diff --git a/tests/doc-consonance-gate.sh b/tests/doc-consonance-gate.sh
new file mode 100755
index 0000000..fa7dbf0
--- /dev/null
+++ b/tests/doc-consonance-gate.sh
@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# doc-consonance-gate.sh — fail-closed guard against the query-language
+# misnomer in VeriSimDB documentation.
+#
+# VCL is the VeriSim *Consonance* Language: it expresses propositions
+# (DECLARE/ASSERT/RETRACT) and epistemic requests (INSPECT/VERIFY) over
+# identity-consonance state. "VeriSim Query Language" is a RETIRED misnomer
+# (see README.adoc / EXPLAINME.adoc). This gate stops it creeping back into
+# the docs.
+#
+# Scope: documentation only (*.adoc, *.md, *.a2ml). Code identifiers
+# (vql_executor, /api/v1/vql/execute, VeriSimVql) and the bare "VQL" token in
+# changelog/history are out of scope — they are tracked under the staged #84
+# rename, and this gate must stay green meanwhile.
+set -euo pipefail
+
+GREEN='\033[0;32m'; RED='\033[0;31m'; NC='\033[0m'
+
+# Files that legitimately name the legacy term: this gate, the changelog
+# history, and the cross-thread quarantine directive (which explains it).
+ALLOW='tests/doc-consonance-gate.sh|CHANGELOG|cross-thread-quarantine'
+
+hits=$(git grep -n 'VeriSim Query Language' -- '*.adoc' '*.md' '*.a2ml' 2>/dev/null | grep -vE "$ALLOW" || true)
+
+if [ -n "$hits" ]; then
+  echo -e "${RED}FAIL${NC} doc-consonance: 'VeriSim Query Language' is a retired misnomer."
+  echo "       Use 'VeriSim Consonance Language' (VCL). Offending lines:"
+  echo "$hits" | sed 's/^/         /'
+  exit 1
+fi
+
+echo -e "${GREEN}PASS${NC} doc-consonance: no 'VeriSim Query Language' misnomer in docs"
