diff --git a/.clusterfuzzlite/build.sh b/.clusterfuzzlite/build.sh
index 6399b28..35dd119 100755
--- a/.clusterfuzzlite/build.sh
+++ b/.clusterfuzzlite/build.sh
@@ -12,20 +12,48 @@
 
 set -euo pipefail
 
+# ── Toolchain floor ──────────────────────────────────────────────────────
+# The OSS-Fuzz base-builder-rust image pins an older nightly (rustc 1.91 at
+# time of writing), but part of the dependency graph — burn / cubecl-zspace,
+# pulled transitively via verisim-tensor (fuzz -> verisim-api) —
+# declares rust-version = 1.92. cargo-fuzz rebuilds the standard library with
+# -Zbuild-std, so all we need is a new-enough nightly with rust-src present.
+# Install one and force it for the whole script via RUSTUP_TOOLCHAIN. This is
+# contained to the fuzz job: it never touches the main workspace toolchain or
+# any other CI job.
+rustup toolchain install nightly --profile minimal \
+    --component rust-src --component llvm-tools-preview
+export RUSTUP_TOOLCHAIN=nightly
+
 # cargo-fuzz drives libfuzzer; install it if missing.
 if ! command -v cargo-fuzz &>/dev/null; then
     cargo install cargo-fuzz --locked
 fi
 
-# ── fuzz_octad_id — top-level fuzz crate ─────────────────────────────────
-cd "${SRC}/verisimdb/fuzz"
-cargo fuzz build --release --sanitizer="${SANITIZER:-address}"
-cp target/*/release/fuzz_octad_id "${OUT}/"
+# Build one named fuzz target from the project's single cargo-fuzz crate
+# (fuzz/) and copy the binary to $OUT. cargo-fuzz resolves ONE fuzz directory
+# per project, so both targets are hosted in fuzz/; building each by name is
+# reliable. We then locate the produced binary wherever cargo-fuzz placed it
+# (not a brittle glob), failing loudly if nothing was produced.
+build_target() {
+    local crate_dir="$1" target="$2"
+    echo "── building fuzz target '${target}' in ${crate_dir} ──"
+    (
+        cd "${crate_dir}"
+        cargo fuzz build --release --sanitizer="${SANITIZER:-address}" "${target}"
+        local bin
+        bin="$(find . -type f -name "${target}" -path '*/release/*' -print -quit)"
+        if [[ -z "${bin}" ]]; then
+            echo "ERROR: no '${target}' binary produced under ${crate_dir}" >&2
+            exit 1
+        fi
+        cp "${bin}" "${OUT}/${target}"
+        echo "── copied ${bin} -> ${OUT}/${target} ──"
+    )
+}
 
-# ── fuzz_vql_parser — rust-core fuzz crate ───────────────────────────────
-cd "${SRC}/verisimdb/rust-core/fuzz"
-cargo fuzz build --release --sanitizer="${SANITIZER:-address}"
-cp target/*/release/fuzz_vql_parser "${OUT}/"
+build_target "${SRC}/verisimdb/fuzz" fuzz_octad_id
+build_target "${SRC}/verisimdb/fuzz" fuzz_vql_parser
 
 # Optional seed corpora — empty for now, will populate as we discover
 # interesting inputs.  Comment in once corpora exist:
diff --git a/.github/workflows/build-validation.yml b/.github/workflows/build-validation.yml
index 24907ed..3439fef 100644
--- a/.github/workflows/build-validation.yml
+++ b/.github/workflows/build-validation.yml
@@ -15,9 +15,9 @@ jobs:
     name: Rust build validation
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo check --workspace
 
   validate-elixir:
@@ -27,8 +27,8 @@ jobs:
       run:
         working-directory: elixir-orchestration
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: erlef/setup-beam@v1
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1
         with:
           elixir-version: "1.17"
           otp-version: "27"
diff --git a/.github/workflows/coq-build.yml b/.github/workflows/coq-build.yml
index d6cd8e7..0c73717 100644
--- a/.github/workflows/coq-build.yml
+++ b/.github/workflows/coq-build.yml
@@ -90,6 +90,12 @@ jobs:
           set -euo pipefail
           coqc -q PlannerSemantic.v | tee PlannerSemantic.out
 
+      - name: Compile Octad.v
+        working-directory: formal
+        run: |
+          set -euo pipefail
+          coqc -q Octad.v | tee Octad.out
+
       - name: Verify Provenance assumptions whitelist
         working-directory: formal
         run: |
@@ -220,3 +226,22 @@ jobs:
             exit 1
           fi
           echo "OK(PlannerSemantic): Q1-full semantic equivalence + membership"
+
+      - name: Verify Octad assumptions whitelist
+        working-directory: formal
+        run: |
+          set -euo pipefail
+          # Whitelist: 2 Parameters (mval, ident) + functional_extensionality_dep
+          # (Coq stdlib). modality is inductive; resolve is an operation
+          # argument — neither is an axiom.
+          UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Octad.out \
+            | sort -u \
+            | grep -vE '^(mval|ident|functional_extensionality_dep)$' || true)
+          if [ -n "$UNEXPECTED" ]; then
+            echo "ERROR(Octad): unexpected axiom(s) in Print Assumptions:"
+            echo "$UNEXPECTED"
+            echo "---"
+            cat Octad.out
+            exit 1
+          fi
+          echo "OK(Octad): O-series + R1-R3 modality algebra whitelisted"
diff --git a/.github/workflows/fuzz.yml b/.github/workflows/fuzz.yml
index bdf64f5..870a9d2 100644
--- a/.github/workflows/fuzz.yml
+++ b/.github/workflows/fuzz.yml
@@ -25,9 +25,9 @@ jobs:
     permissions:
       contents: read
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - name: Run core fuzz compile check
         run: |
           cd rust-core/fuzz
@@ -40,9 +40,9 @@ jobs:
     permissions:
       contents: read
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - name: Run debugger fuzz compile check
         run: |
           cd debugger/fuzz
diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml
index f1ee480..02e1390 100644
--- a/.github/workflows/rust-ci.yml
+++ b/.github/workflows/rust-ci.yml
@@ -28,8 +28,8 @@ jobs:
     name: rustfmt
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
         with:
           components: rustfmt
       - run: cargo fmt --all -- --check
@@ -38,20 +38,20 @@ jobs:
     name: clippy (all-targets)
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
         with:
           components: clippy
-      - uses: Swatinem/rust-cache@v2
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo clippy --workspace --all-targets --no-deps -- -D warnings
 
   test:
     name: cargo test
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo test --workspace --no-fail-fast
 
   doc:
@@ -60,17 +60,17 @@ jobs:
     env:
       RUSTDOCFLAGS: "-D warnings"
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo doc --workspace --no-deps
 
   audit:
     name: cargo audit
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: rustsec/audit-check@v2.0.0
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: rustsec/audit-check@69366f33c96575abad1ee0dba8212993eecbe998 # v2.0.0
         with:
           token: ${{ secrets.GITHUB_TOKEN }}
 
@@ -78,8 +78,8 @@ jobs:
     name: cargo deny
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: EmbarkStudios/cargo-deny-action@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: EmbarkStudios/cargo-deny-action@8f84122a46a358a27cb0625d85ad60ab436a1b87 # v2
         with:
           command: check advisories bans licenses sources
 
@@ -87,24 +87,24 @@ jobs:
     name: benchmarks compile
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo bench --no-run
 
   coverage:
     name: cargo-llvm-cov (≥60%)
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
         with:
           components: llvm-tools-preview
-      - uses: Swatinem/rust-cache@v2
-      - uses: taiki-e/install-action@cargo-llvm-cov
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
+      - uses: taiki-e/install-action@28ba36d36bfc4814f98a469ff9f76b2a41e9aa8a # cargo-llvm-cov
       - name: Generate lcov report
         run: cargo llvm-cov --workspace --lcov --output-path lcov.info
-      - uses: codecov/codecov-action@v6
+      - uses: codecov/codecov-action@e79a6962e0d4c0c17b229090214935d2e33f8354 # v6
         with:
           files: lcov.info
           flags: rust
@@ -122,10 +122,10 @@ jobs:
     runs-on: ubuntu-latest
     if: github.event_name == 'workflow_dispatch' || github.event_name == 'schedule'
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
-      - uses: taiki-e/install-action@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
+      - uses: taiki-e/install-action@25435dc8dd3baed7417e0c96d3fe89013a5b2e09 # v2
         with:
           tool: cargo-mutants
       - name: Run mutation tests on core invariant crates
@@ -140,7 +140,7 @@ jobs:
             --no-shuffle \
             --output mutants-out/
         continue-on-error: true
-      - uses: actions/upload-artifact@v7
+      - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7
         if: always()
         with:
           name: mutants-report
@@ -155,7 +155,7 @@ jobs:
           - fuzz/Cargo.toml
           - rust-core/fuzz/Cargo.toml
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo check --manifest-path ${{ matrix.manifest }}
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
new file mode 100644
index 0000000..e2a94e3
--- /dev/null
+++ b/EXPLAINME.adoc
@@ -0,0 +1,130 @@
+// SPDX-License-Identifier: MPL-2.0
+= EXPLAINME — VeriSimDB Orientation
+:toc:
+:toc-placement!:
+
+[.lead]
+**VeriSimDB does not merely store records. It maintains identity consonance across modal witnesses and federation boundaries. VCL expresses propositions and epistemic requests over that consonance state. VCL-total validates whether proposed identity transitions are admissible.**
+
+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`).
+
+toc::[]
+
+== The one idea to hold onto
+
+If you take away a single thing: a VeriSimDB "entity" is **not a row**. It is a
+**consonance subject** — an identity under continuous maintenance across up to
+eight *modal witnesses* (the octad: graph, vector, tensor, semantic, document,
+temporal, provenance, spatial). The system's job is not storage; it is deciding,
+continuously, whether those witnesses still cohere as one identity — and what to
+do when they do not.
+
+So the verbs are not CRUD. They are **lifecycle transitions** on identity claims:
+declare, assert, inspect, verify, transform, retract, merge, split, normalise,
+tombstone.
+
+== Why "consonance", not "consistency"
+
+Classic databases enforce *consistency* up front (transactions, locks) and treat
+divergence as an error to prevent. VeriSimDB instead expects modal witnesses to
+drift — a document is edited before its embedding is recomputed; a spatial
+coordinate is refined independently of the text — and treats that drift as a
+**first-class, typed condition** to be measured, classified, and repaired. The
+maintained property is *consonance*: the witnesses still refer to the same
+identity, within policy.
+
+A modality failure is therefore **not** automatically an identity failure. These
+are distinct states with distinct proof obligations and repair paths:
+
+[cols="1,1"]
+|===
+|Observation |State
+
+|document changed, vector stale |modal drift (repairable by normalisation)
+|hash chain broken |provenance / integrity failure
+|remote node asserts an incompatible type |federation conflict (needs arbitration)
+|all live witnesses retracted |inactive / tombstoned identity
+|===
+
+== The identity lifecycle
+
+----
+Candidate
+  -> Declared
+  -> Asserted
+  -> Consonant
+  -> Drifting
+  -> Normalised
+  -> Merged / Split
+  -> Retracted
+  -> Tombstoned
+  -> Expunged  (only under explicit policy)
+----
+
+**Retraction is not deletion.** A retracted claim usually stays visible to
+provenance, audit, federation, and proof systems — it is no longer *live*.
+Tombstoning durably retires an identity or claim without pretending it never
+existed. Expungement is a separate, policy-governed operation.
+
+== Core terms
+
+[cols="1,2"]
+|===
+|Term |Meaning
+
+|Consonance Subject |The lifecycle-managed identity under consideration.
+|Identity Claim |A claim that some subject exists, has a property, has a relation, or survives a transition.
+|Modality Witness |One modal presentation of a subject: graph, vector, tensor, semantic, document, temporal, provenance, or spatial.
+|Drift Report |Evidence that one or more modal witnesses no longer cohere.
+|Transition |A proposed identity event: declare, assert, retract, normalise, merge, split, federate, tombstone.
+|Proof Obligation |What must be shown before a transition is admissible.
+|Federation Attestation |A remote or local authority claim about identity, provenance, validity, or trust.
+|Tombstone |A durable marker that an identity claim is no longer live, without pretending it never existed.
+|===
+
+== VCL, VCL-total, and VeriSimDB
+
+[cols="1,3"]
+|===
+|Layer |Role
+
+|**VeriSimDB** |The federated consonance engine. Stores and maintains identity consonance across the octad of modal witnesses; detects drift; repairs under policy.
+|**VCL** |The production consonance language. Statements are *propositions* (`DECLARE`, `ASSERT`, `RETRACT`) or *epistemic requests* (`INSPECT`, `VERIFY`), plus `MERGE` / `SPLIT` / `NORMALISE` — directed at the engine, not queries against a passive store.
+|**VCL-total** |The proof-bearing safety substrate behind VCL (repo: https://github.com/hyperpolymath/vcl-ut[vcl-ut]). It decides whether a proposed identity transition is *admissible* under schema, modality, provenance, authority, freshness, resource, effect, federation, and proof constraints.
+|===
+
+The proof goal is deliberately narrow and useful — **not** "prove the whole
+database correct", but:
+
+----
+prove that THIS identity transition is admissible,
+traceable, authorised, and consonant enough to affect live state.
+----
+
+== What is implemented vs design intent (honest)
+
+* **Implemented today:** the octad stores (graph, vector, tensor, semantic,
+  document, temporal, provenance hash-chain, spatial R-tree); cross-modal drift
+  detection + self-normalisation; the federation coordinator; and a VCL surface
+  whose *current* in-repo grammar (`spec/grammar.ebnf` v3.0) is a read-style,
+  SQL-shaped convenience (`SELECT … FROM HEXAD …`, with `HEXAD` the legacy
+  keyword for the octad source) plus `PROOF`-carrying statements.
+* **The model / direction:** the lifecycle/consonance verbs (`DECLARE` …
+  `NORMALISE`) and full proof-bearing admissibility are the semantic target,
+  carried by **VCL-total** (vcl-ut). Read the SQL-ish read-path as *epistemic
+  inspection of consonance state*, not row retrieval.
+* **Formal core:** invariants are mechanised in Coq under `formal/` (octad
+  modality algebra, provenance hash-chain, drift bounds, planner equivalence,
+  WAL/normaliser idempotence, VCL preservation) — see
+  link:formal/CROSS-REPO-MAP.adoc[the cross-repo map] and
+  link:docs/proof-debt.md[the trusted-base ledger].
+
+== 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`).
+* 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/LICENSE b/LICENSE
index d0a1fa1..a06bf12 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,3 +1,5 @@
+SPDX-License-Identifier: MPL-2.0
+
 Mozilla Public License Version 2.0
 ==================================
 
diff --git a/README.adoc b/README.adoc
index c7171f8..6b1d5b7 100644
--- a/README.adoc
+++ b/README.adoc
@@ -4,10 +4,99 @@
 :toc:
 :toc-placement!:
 
-**Cross-system data consistency that catches drift before it causes damage.**
+[.lead]
+**VeriSimDB does not merely store records. It maintains identity consonance across modal witnesses and federation boundaries. VCL expresses propositions and epistemic requests over that consonance state. VCL-total validates whether proposed identity transitions are admissible.**
+
+_Cross-modal consonance that catches identity drift before it causes damage._
 
 toc::[]
 
+== Conceptual Model: Continuous Identity, Not Passive Storage
+
+VeriSimDB is not primarily a database of records. It is a federated consonance engine for continuously maintained identity claims.
+
+A VeriSimDB "entity" is best understood as a **consonance subject**: an identity under active maintenance across multiple modal witnesses. Those witnesses may include graph structure, vector embeddings, tensor data, semantic annotations, documents, temporal history, provenance chains, and spatial references. Together they form the octad view of an identity.
+
+The central problem VeriSimDB solves is not merely storing these views. The central problem is deciding whether they still refer to the same identity, whether they have drifted, whether a repair or normalisation is justified, whether a federated claim should be accepted, and whether an identity claim should be strengthened, weakened, merged, split, retracted, tombstoned, or expunged under policy.
+
+This means VeriSimDB should be read as a lifecycle system for identity claims:
+
+----
+Candidate
+  -> Declared
+  -> Asserted
+  -> Consonant
+  -> Drifting
+  -> Normalised
+  -> Merged / Split
+  -> Retracted
+  -> Tombstoned
+  -> Expunged only under explicit policy
+----
+
+A modality failure is not automatically an identity failure. For example:
+
+----
+document changed, vector stale        -> modal drift
+hash chain broken                     -> provenance/integrity failure
+remote node asserts incompatible type -> federation conflict
+all live witnesses retracted          -> inactive or tombstoned identity
+----
+
+These states have different proof obligations and different repair paths.
+
+=== Core Terms
+
+[cols="1,2"]
+|===
+|Term |Meaning
+
+|Consonance Subject
+|The lifecycle-managed identity under consideration.
+
+|Identity Claim
+|A claim that some subject exists, has a property, has a relation, or survives a transition.
+
+|Modality Witness
+|One modal presentation of a subject: graph, vector, tensor, semantic, document, temporal, provenance, or spatial.
+
+|Drift Report
+|Evidence that one or more modal witnesses no longer cohere.
+
+|Transition
+|A proposed identity event: declare, assert, retract, normalise, merge, split, federate, tombstone.
+
+|Proof Obligation
+|What must be shown before a transition is admissible.
+
+|Federation Attestation
+|A remote or local authority claim about identity, provenance, validity, or trust.
+
+|Tombstone
+|A durable marker that an identity claim is no longer live, without pretending it never existed.
+|===
+
+=== VCL and VCL-total
+
+VCL is the production consonance language used to propose and inspect identity transitions. VCL statements are not simply queries against a passive store. They are propositions or epistemic requests directed at a consonance engine.
+
+VCL-total / VCL-UT is the proof-bearing safety substrate behind VCL. It validates whether a proposed transition is admissible under the relevant schema, modality, provenance, authority, freshness, resource, effect, federation, and proof constraints.
+
+In short:
+
+----
+VeriSimDB stores and maintains identity consonance.
+VCL expresses identity propositions and epistemic requests.
+VCL-total checks whether those transitions are safe and admissible.
+----
+
+The proof goal is not "prove the whole database correct". The proof goal is narrower and more useful:
+
+----
+prove that this identity transition is admissible,
+traceable, authorised, and consonant enough to affect live state.
+----
+
 == The Problem: Silent Data Drift
 
 Your data lives in multiple systems — graphs, vector stores, document indexes, time-series databases. When one system's view of an entity silently diverges from the others, you get **data drift**: stale embeddings, broken provenance chains, graph edges referencing deleted documents, spatial coordinates that no longer match textual descriptions.
@@ -16,7 +105,7 @@ Traditional tools detect drift _after_ it causes downstream failures. VeriSimDB
 
 == What VeriSimDB Does
 
-VeriSimDB is a **cross-modal consistency engine**. Each entity exists simultaneously across up to 8 representations (the **octad**) with automatic drift detection and self-normalisation:
+VeriSimDB is a **federated consonance engine**. Each consonance subject is maintained across up to 8 modal witnesses (the **octad**), with continuous drift detection and self-normalisation:
 
 ----
 ┌─────────────────────────────────────────────────────────────┐
@@ -103,15 +192,15 @@ Sample output:
 |Partial
 |**Hash-chain verified**
 
-|Query language
+|Consonance language
 |No (Python API)
 |No (UI)
-|**VQL (with dependent types)**
+|**VCL (propositions + epistemic requests)**
 
-|Formal verification
+|Proof-bearing transitions
 |No
 |No
-|**VQL-DT (proof certificates)**
+|**VCL-total (admissibility proofs)**
 |===
 
 == The Octad: Eight Modalities
@@ -241,34 +330,56 @@ VeriSimDB can also operate as a **federation coordinator** over existing databas
 └────────────────────────────────────────────────────────────────┘
 ----
 
-== VQL: VeriSim Query Language
+== VCL: VeriSim Consonance Language
 
-VQL provides unified querying across all eight modalities with two execution paths:
+VCL statements are **propositions and epistemic requests to a consonance engine**, not queries against a passive store. They propose, inspect, verify, transform, retract, merge, split, and normalise identity claims across the eight modal witnesses (see the Conceptual Model section above). The proof-bearing safety substrate behind VCL is **VCL-total** (https://github.com/hyperpolymath/vcl-ut[vcl-ut]), which decides whether a proposed identity transition is _admissible_.
 
-=== Slipstream (Fast, No Proofs)
+The consonance operations:
+
+[cols="1,3"]
+|===
+|Operation |Meaning
+
+|`DECLARE`   |introduce a candidate identity claim
+|`ASSERT`    |strengthen or add evidence to an identity claim
+|`RETRACT`   |revoke, weaken, or retire a live claim (not erasure — see below)
+|`INSPECT`   |observe consonance, drift, provenance, or federation state
+|`VERIFY`    |request proof-bearing validation of a claim or transition
+|`MERGE`     |join identities when consonance evidence supports it
+|`SPLIT`     |separate an over-coalesced identity
+|`NORMALISE` |repair drift when a justified repair path exists
+|===
+
+NOTE: The lifecycle/consonance verbs above are the **semantic model**, carried fully by VCL-total. The current in-repo surface grammar (`spec/grammar.ebnf` v3.0) still exposes a read-style, SQL-shaped convenience (`SELECT … FROM …`, plus legacy `INSERT`/`UPDATE`/`DELETE` mutation forms) and uses `HEXAD` as the legacy keyword for the octad source (8 modal witnesses, retained for backward compatibility). Read the read-path below as **epistemic inspection of consonance state**, not row retrieval from a passive store.
+
+=== Inspection surface — Slipstream (fast, no proofs)
+
+A read-only convenience for inspecting consonance state. `HEXAD <uuid>` names the octad source; `DRIFT(...)` inspects cross-modal divergence:
 
 [source,sql]
 ----
--- Query across modalities
+-- Inspect across modal witnesses
 SELECT GRAPH.*, DOCUMENT.*, VECTOR.* FROM HEXAD 'entity-001'
 
--- Cross-modal drift detection in WHERE clause
+-- Cross-modal drift inspection
 SELECT * FROM HEXAD 'entity-001'
   WHERE DRIFT(VECTOR, DOCUMENT) > 0.3
 
--- Modality existence checks
+-- Modality-witness presence checks
 SELECT * FROM HEXAD 'entity-001'
   WHERE PROVENANCE EXISTS AND TENSOR NOT EXISTS
 
--- Federation queries
+-- Federated inspection
 SELECT * FROM FEDERATION /* WITH DRIFT STRICT
 ----
 
-=== VQL-DT (Dependent Types with Proof Certificates)
+=== Proof-bearing statements — VCL-total (dependent types + proof certificates)
+
+A `PROOF` clause makes a statement proof-bearing: VCL-total must discharge the attached obligation before the result is admissible.
 
 [source,sql]
 ----
--- Query with existence proof
+-- Statement carrying an existence proof obligation
 SELECT GRAPH.* FROM HEXAD 'entity-001'
   PROOF EXISTENCE(entity-001)
 
@@ -276,12 +387,12 @@ SELECT GRAPH.* FROM HEXAD 'entity-001'
 SELECT * FROM HEXAD 'entity-001'
   PROOF EXISTENCE(entity-001) AND PROVENANCE(entity-001)
 
--- Integrity verification with contract
+-- Integrity verification against a contract
 SELECT GRAPH.* FROM HEXAD 'entity-001'
   PROOF INTEGRITY(my_contract)
 ----
 
-VQL-DT queries return a `ProvedResult` with data AND a proof certificate:
+VCL-total proof-bearing statements return a `ProvedResult` with data AND a proof certificate:
 
 [source,elixir]
 ----
@@ -335,7 +446,7 @@ iex -S mix
 ----
 cargo test                    # Rust: 510+ tests
 cd elixir-orchestration
-mix test                      # Elixir: 160+ tests (VQL, consensus, telemetry, federation, hypatia)
+mix test                      # Elixir: 160+ tests (VCL, consensus, telemetry, federation, hypatia)
 ----
 
 === CI & Coverage
@@ -405,7 +516,7 @@ grpcurl -plaintext localhost:50051 list
 # Health check
 grpcurl -plaintext localhost:50051 verisimdb.VeriSimService/Health
 
-# Execute a VQL query
+# Submit a VCL statement
 grpcurl -plaintext -d '{"query": "SELECT * FROM octads LIMIT 10"}' \
   localhost:50051 verisimdb.VeriSimService/Query
 
@@ -436,13 +547,13 @@ verisimdb/
 │   ├── lib/verisim/
 │   │   ├── drift/             # DriftMonitor GenServer
 │   │   ├── entity/            # EntityServer (per-entity GenServer)
-│   │   ├── query/             # VQL parser, executor, bridge
+│   │   ├── query/             # VCL parser, executor, bridge
 │   │   └── rust_client.ex     # HTTP client for Rust core
 │   └── test/
 ├── demos/
 │   └── drift-detection/       # Drift detection demo script
 ├── docs/                      # Specifications and design documents
-│   ├── vql-grammar.ebnf       # VQL formal grammar
+│   ├── vql-grammar.ebnf       # VCL formal grammar
 │   ├── vql-formal-semantics.adoc
 │   └── vql-type-system.adoc
 ├── registry/                  # ReScript federation registry
@@ -461,7 +572,7 @@ Universities and research institutions federate their archives while maintaining
 Vector embeddings and symbolic graphs coexist in the same namespace. AI systems query both modalities without ETL, with formal proof certificates guaranteeing query correctness.
 
 === Verifiable Data Exchange
-ZKP proofs and dependent types enable tamper-evident knowledge exchange. VQL-DT queries return data with cryptographic proof certificates — you can verify the result without trusting the source.
+ZKP proofs and dependent types enable tamper-evident knowledge exchange. VCL-total proof-bearing statements return data with cryptographic proof certificates — you can verify the result without trusting the source.
 
 == Documentation
 
@@ -476,14 +587,14 @@ Quick links:
 * link:SECURITY.md[Security Policy] — threat model and disclosure process
 * link:AUDIT.adoc[Audit Index] — RSR audit-trail index
 
-VQL language:
+VCL language (file paths retain the historical `vql-` / `VQL-` 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[VQL Specification] — normative language spec
-* link:docs/vql-grammar.ebnf[VQL Grammar] — formal EBNF
-* link:docs/vql-formal-semantics.adoc[VQL Formal Semantics] — operational semantics
-* link:docs/vql-type-system.adoc[VQL Type System] — dependent types + bidirectional checking
-* link:docs/vql-examples.adoc[VQL Examples] — worked examples
+* 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
 
 Deployment & operations:
 
diff --git a/docs/proof-debt.md b/docs/proof-debt.md
new file mode 100644
index 0000000..8ce1d7b
--- /dev/null
+++ b/docs/proof-debt.md
@@ -0,0 +1,86 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+# Proof Debt — Trusted Base of the VeriSimDB Formal Development
+
+This document is the authoritative catalogue of **soundness-relevant escape
+hatches** in VeriSimDB's machine-checked proofs, per the estate
+[Trusted-Base Reduction Policy](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc).
+Every Coq `Axiom` (and any `Admitted` / `admit.`, of which there are currently
+**none**) is enumerated here by `file:line`, with its justification.
+
+The Coq corpus lives in [`formal/`](../formal/). Each module is compiled by
+`coqc` and its `Print Assumptions` output is grepped against a per-module
+whitelist in [`formal/Justfile`](../formal/Justfile) and
+[`.github/workflows/coq-build.yml`](../.github/workflows/coq-build.yml), so an
+axiom that is **not** in this ledger cannot silently enter a theorem's trusted
+base — CI fails on any unlisted assumption ("axiom slippage").
+
+## Summary
+
+| Count | Kind | Status |
+|------:|------|--------|
+| 13 | Coq `Axiom` | Documented below; whitelisted; non-`Admitted` |
+| 0 | `Admitted` / `admit.` | None — every theorem closes with `Qed` |
+| 0 | Rust `unsafePerformIO` / `unsafeCoerce` | N/A (Rust core uses neither) |
+
+`formal/Octad.v` (the octad modality algebra) contributes **zero** axioms: it
+closes on two `Parameter`s (`mval`, `ident`) plus the Coq stdlib
+`functional_extensionality_dep`. `Parameter`s are interface points (opaque
+carriers), not soundness escape hatches, and are tracked by the same
+`Print Assumptions` guard.
+
+## Catalogue
+
+### `formal/Drift.v` — drift-score order laws (6 axioms)
+
+Minimal axiomatisation of the abstract `score` order (the Rust source is
+`f64`). These are standard total-order / clamp laws, not domain assumptions.
+
+- `formal/Drift.v:46` — `le_refl` — reflexivity of the score order (`x <= x`).
+- `formal/Drift.v:47` — `clamp_lower` — `clamp lo hi x` is `>= lo`. Mirrors `f64::clamp`.
+- `formal/Drift.v:48` — `clamp_upper` — `clamp lo hi x` is `<= hi`. Mirrors `f64::clamp`.
+- `formal/Drift.v:157` — `le_or_gt` — totality of the order (`s <= t` or `s > t`); faithful to the `f64` total order modulo NaN, which the clamp rules out.
+- `formal/Drift.v:161` — `le_gt_exclusive` — `<=` and `>` are mutually exclusive.
+- `formal/Drift.v:167` — `detector_iff_threshold` — the detector signals iff `score > threshold` (the `if score > threshold` guard at `verisim-drift/src/lib.rs`).
+
+### `formal/Provenance.v` — cryptographic assumption (1 axiom)
+
+- `formal/Provenance.v:59` — `sha256_collision_resistant` — injectivity of SHA-256 on `(content, parent_hash)`. Standard cryptographic assumption; **declared but unused** by the current P2/P3/P4 theorems (reserved for later uniqueness work). `Print Assumptions` confirms it is not in their trusted base.
+
+### `formal/WAL.v` — decidable equality (1 axiom)
+
+- `formal/WAL.v:57` — `eq_entity_dec` — decidable equality on `entity_id`. True for `String` in the Rust source (`store.rs`); axiomatised because the carrier is opaque.
+
+### `formal/Normalizer.v` — normalize spec contract (2 axioms)
+
+Encode the remediated N2 spec (see issue #91): the authoritative source is
+never a drifted modality, and winner selection ignores drifted data.
+
+- `formal/Normalizer.v:73` — `winner_excludes_drifted` — the normalize winner is never a drifted modality ("never copy FROM corrupt sources").
+- `formal/Normalizer.v:80` — `winner_stable_off_drifted` — winner selection depends only on non-drifted modalities ("frozen rank, not `Utc::now()`").
+
+### `formal/Planner.v` / `formal/PlannerSemantic.v` — optimizer contract (3 axioms)
+
+Structural contracts on `Planner::optimize` (a `stable_sort_by`): it permutes
+plan nodes, and per-node filters commute at the set level.
+
+- `formal/Planner.v:63` — `optimize_is_permutation` — the optimizer reorders nodes without adding or dropping any (Q1-lite).
+- `formal/PlannerSemantic.v:94` — `optimize_is_permutation` — same contract, restated for the Q1-full semantic-equivalence development.
+- `formal/PlannerSemantic.v:78` — `exec_node_comm` — per-node set-restrictions commute (filter intersection is order-independent across operator types).
+
+## Discharge paths (future work)
+
+These are deliberate, mathematically-standard assumptions, not gaps in
+reasoning. Where the estate wishes to shrink the trusted base further:
+
+- The `Drift.v` order laws and `WAL.v` `eq_entity_dec` discharge automatically
+  if the abstract carriers are instantiated to concrete Coq types
+  (`R`/`Q`/`bool`-decidable strings) — they exist only because the carriers are
+  kept opaque to mirror the Rust generics.
+- `sha256_collision_resistant` is a genuine cryptographic axiom; it can be
+  re-homed to a CryptHOL/Isabelle development per the issue #77 tool-selection
+  table, but stays an assumption in any first-order model.
+- `optimize_is_permutation` / `exec_node_comm` are checkable by a Rust property
+  test over `Planner::optimize`; that test is the intended runtime corroboration.
+
+See `formal/CROSS-REPO-MAP.adoc` for the echo-types correspondence of each
+theorem these axioms support.
diff --git a/formal/CROSS-REPO-MAP.adoc b/formal/CROSS-REPO-MAP.adoc
index 8756d90..6cebf5e 100644
--- a/formal/CROSS-REPO-MAP.adoc
+++ b/formal/CROSS-REPO-MAP.adoc
@@ -79,6 +79,31 @@ Concretely:
 | `EchoGradedComonadInterface.agda` (existing) — graded comonad for "well-typed at type τ"
 | Type-preservation under reduction is the comonad ε ∘ δ = id property in the graded comonad of "well-typed terms at type τ". Reduction is the comonad action. The V2 mechanisation here is the MINIMUM-VIABLE core (booleans + opaque proof terms + conditional), closing #92 blockers 1 (big-step → small-step) and 2 (proof terms as values, no β-reduction). Full VCL extends mechanically per added expression form. Progress bundled as the type-soundness companion.
 
+| O2 `modality_cardinality` + `modality_exhaustive`
+| `formal/Octad.v`
+| **Direct inductive — no echo-types lift needed** (finite-basis cardinality is structural, like C2)
+| The 8-element `modality` enum mirrors `ModalityStatus`'s eight booleans. Cardinality (= 8) and exhaustiveness are structural facts over a finite inductive; same deliberate non-port rationale as the Transaction.v 3-state automaton.
+
+| O10 `complete_iff_no_missing`
+| `formal/Octad.v`
+| `EchoCharacteristic.agda` (existing) — collapse / echo-true / echo-false
+| `present` partitions modalities into `Echo true` (a value) and `Echo false` (bot). `is_complete` (all present) iff `missing` (the false-fibre) is empty — the same true/false-fibre disjointness as D2. Doubles as a cross-method consistency check between `ModalityStatus::is_complete` and `ModalityStatus::missing`.
+
+| Projection `project_full` + `project_idempotent` + `project_compose`
+| `formal/Octad.v`
+| `EchoTruncation.agda` (existing) — same module N2 cites
+| `pi_M` truncates the modality section `phi` to a mask. `project_compose` (`pi_M . pi_N = pi_{M /\ N}`) is the meet-semilattice law — projections form a bounded meet-semilattice under composition, the "structural modularity" of octads. Direct lift of `EchoTruncation`'s decoupling lemma, restricted to a Boolean modality mask.
+
+| R1-R3 `merge_commutative` + `merge_associative` + `merge_idempotent`
+| `formal/Octad.v`
+| Candidate NEW abstraction — join-semilattice of partial sections (to be established in echo-types per standing directive)
+| The paper's `arcvix-octad-data-model.tex` Proposition "Merge Commutativity" had a one-line pen-and-paper proof; `merge_commutative` is it MECHANISED. Octad merge `(+)` inherits exactly the algebra of its conflict kernel `resolve`: `(+)` is commutative/associative/idempotent iff `resolve` is (R1/R2/R3 stated as implications). This is the honest resolution of verisimdb#77's "R1-R3 likely false as written": a CRDT-shaped `resolve` (join on a semilattice) instantiates all three; AutoMerge does not. Echo-types has no join-semilattice-of-sections module yet — companion issue to file per the standing directive.
+
+| Enrichment `enrich_sets_target` + `enrich_preserves_others` + `enrich_present`
+| `formal/Octad.v`
+| `EchoProvenance.agda` (existing) — for the audit-trail clause, via Provenance.v
+| `enrich_m` is the fundamental write primitive: sets modality `m`, preserves the rest, preserves `id` (`inv:persist`). The `def:enrichment` clause "every enrichment appends to phi(P) and phi(R)" (audit trail) is the hash-chain append already mechanised in `Provenance.v` (`append_preserves_verified`, mapping to `EchoProvenance.agda` above) — not re-modelled here.
+
 | Future: D7 `temporal_drift_zero_iff_monotone_unique`
 | _todo_
 | `EchoLossTaxonomy.agda` + `EchoEntropy.agda`
@@ -104,22 +129,38 @@ Concretely:
 . The verisimdb Coq module's docstring **MUST** name the corresponding echo-types module (or "no direct echo-types analogue, deliberate" with rationale).
 . Update `MEMORY.md` `[[verisimdb-proof-programme-started]]` cross-ref.
 
-== Status (2026-06-01)
+== Status (2026-06-03)
 
-**Foundation pack COMPLETE — 8 of 8 closed.**
+**Foundation pack COMPLETE — 10 of 10 closed** (P2, P3, P4, D1, D2, C2, C7, N2, Q1-lite, Q1-full, V2).
 
 * P2, P3 → `formal/Provenance.v` (PR #87)
 * D1, C2 → `formal/Drift.v`, `formal/Transaction.v` (PR #90)
 * D2, Q1-lite → `formal/Drift.v`, `formal/Planner.v` (PR #93)
 * C7 → `formal/WAL.v` (PR #94, closed #89)
 * N2 → `formal/Normalizer.v` (PR #95, closed #91)
-* **V2 → `formal/VCL.v` (PR #96, closed #92)**
+* V2 → `formal/VCL.v` (PR #96, closed #92)
+* Q1-full → `formal/PlannerSemantic.v` (PR #97)
+* P4 → `formal/Provenance.v` (PR #103)
+
+**Post-foundation — first module landed:**
+
+* **O-series + R1-R3 → `formal/Octad.v`** — the Modality Algebra of
+  `docs/papers/arcvix-octad-data-model.tex` (`sec:modality-algebra`)
+  mechanised: O2 (modality cardinality + exhaustiveness), O10
+  (present-totality / `is_complete` ↔ `missing`), Projection (`pi_M`
+  idempotent + composition-as-meet), the paper's **Merge Commutativity**
+  proposition (`merge_commutative`) plus its R2/R3 companions, and
+  Enrichment (`enrich_*`, `inv:persist`). Closes on `mval`, `ident` and
+  `functional_extensionality_dep` only — Print Assumptions confirms no
+  slippage.
 
 Cross-doc to echo-types established by this file.
 
 Future work:
 
+* File the echo-types companion issue for the merge join-semilattice
+  abstraction (R1-R3 row above) per the standing directive.
 * Port `WAL.v` + `Normalizer.v` + `VCL.v` to Agda within echo-types (refactor on top of `EchoResidue`, `EchoSearchExample`, `EchoGradedComonadInterface`).
 * Extend `VCL.v` from the 4-rule core to full VCL: filter expressions, projections, modality quantifiers, multi-proof composition. Each form adds one congruence step rule + one preservation case.
 * Add a CI check: every new `formal/*.v` module must reference an echo-types module name in its docstring (or `no-echo-types-analogue` with reason).
-* Tackle the post-foundation theorems (D3-D8, C1-C11, F1-F6, Q2-Q9, V1-V8, P1, P4, P5) per the #77 inventory.
+* Tackle the remaining post-foundation theorems (O1/O3-O9, D3-D8, C1/C3-C6/C8-C11, F1-F6, Q2-Q9, V1/V3-V8, P1, P5) per the #77 inventory.
diff --git a/formal/Justfile b/formal/Justfile
index eb5631d..9876c55 100644
--- a/formal/Justfile
+++ b/formal/Justfile
@@ -12,7 +12,7 @@
 COQC := "coqc"
 
 # Compile every proof module.
-all: provenance drift transaction planner wal normalizer vcl planner-semantic
+all: provenance drift transaction planner wal normalizer vcl planner-semantic octad
 
 # --- Per-module compile recipes -------------------------------------------
 
@@ -40,11 +40,14 @@ vcl:
 planner-semantic:
     {{COQC}} -q PlannerSemantic.v | tee PlannerSemantic.out
 
+octad:
+    {{COQC}} -q Octad.v | tee Octad.out
+
 # --- Whitelist guards -----------------------------------------------------
 # Each module declares its own set of Parameters/Axioms; the guard greps
 # Print Assumptions output for any name outside that module's whitelist.
 
-check-assumptions: check-provenance check-drift check-transaction check-planner check-wal check-normalizer check-vcl check-planner-semantic
+check-assumptions: check-provenance check-drift check-transaction check-planner check-wal check-normalizer check-vcl check-planner-semantic check-octad
 
 check-provenance: provenance
     @awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Provenance.out \
@@ -124,6 +127,16 @@ check-planner-semantic: planner-semantic
             echo "OK(PlannerSemantic): Q1-full semantic equivalence + membership"; \
           fi; }
 
+check-octad: octad
+    @awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Octad.out \
+      | sort -u \
+      | grep -vE '^(mval|ident|functional_extensionality_dep)$' \
+      | { if read -r line; then \
+            echo "ERROR(Octad): unexpected axiom: $line"; cat; exit 1; \
+          else \
+            echo "OK(Octad): O-series (cardinality, present-totality, projection) + R1-R3 merge algebra"; \
+          fi; }
+
 # Remove all build artefacts.
 clean:
     rm -f *.vo *.vos *.vok *.glob .*.aux *.out
diff --git a/formal/Octad.v b/formal/Octad.v
new file mode 100644
index 0000000..594081f
--- /dev/null
+++ b/formal/Octad.v
@@ -0,0 +1,368 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
+
+(** * VeriSimDB Octad Modality Algebra (O-series + R1-R3)
+
+    Mechanises the OCTAD DATA MODEL and its MODALITY ALGEBRA as written
+    (on paper) in [docs/papers/arcvix-octad-data-model.tex], section
+    [sec:octad] "The Octad Data Model":
+
+    - [def:modset]     Modality Set        — the fixed eight-element basis.
+    - [def:octad]      Octad               — (id, phi), phi : M -> Sigma_m u {bot}.
+    - [inv:persist]    Identity Persistence — id is immutable under mutation.
+    - [def:projection] Projection  pi_M.
+    - [def:merge]      Merge       (+)      with conflict resolver [resolve].
+    - Proposition      Merge Commutativity  (the paper's one proven claim).
+    - [def:enrichment] Enrichment  enrich_m — the fundamental write primitive.
+
+    ** Why this module exists
+
+    The paper's "Modality Algebra" subsection [sec:modality-algebra] is
+    the octad-modularity experiment. Its sole stated proof — the
+    Proposition "Merge Commutativity" — is a one-line pen-and-paper
+    argument ("follows directly from the symmetry of the case analysis in
+    [def:merge] and the commutativity assumption on resolve").
+    [merge_commutative] below is that proposition MECHANISED. The
+    associativity and idempotence companions ([merge_associative],
+    [merge_idempotent]) close the conditional CRDT-shape laws R1-R3 from
+    the verisimdb#77 inventory.
+
+    ** On verisimdb#77's "honest uncertainty" about R1-R3
+
+    Issue #77 flags R1/R2/R3 ("CRDT-shaped octad merge") as "likely false
+    as currently written", because the concrete AutoMerge heuristic in
+    [verisim-normalizer/src/conflict.rs] is not unconditionally
+    commutative. The honest resolution, mechanised here, is the paper's:
+    the octad merge (+) inherits EXACTLY the algebra of its
+    conflict-resolution kernel [resolve]. (+) is commutative / associative
+    / idempotent precisely WHEN [resolve] is. The laws are therefore
+    stated as implications from [resolve]'s properties — the faithful
+    form. A CRDT-shaped [resolve] (e.g. a join on a semilattice)
+    instantiates all three; AutoMerge does not, and the implication makes
+    that explicit rather than over-claiming.
+
+    ** Faithfulness to the Rust source
+
+    The eight-constructor [modality] enumeration mirrors the eight boolean
+    fields of [ModalityStatus] in [rust-core/verisim-octad/src/lib.rs]
+    (graph, vector, tensor, semantic, document, temporal, provenance,
+    spatial). [is_complete] / [missing] mirror [ModalityStatus::is_complete]
+    and [ModalityStatus::missing]; [complete_iff_no_missing] is the
+    cross-method consistency check between those two independent Rust
+    functions (edit one without the other and this theorem breaks).
+    [resolve] abstracts [RegenerationStrategy] in
+    [rust-core/verisim-normalizer/src/regeneration.rs].
+
+    The [def:enrichment] clause "every enrichment appends a record to
+    phi'(P) and phi'(R)" (the audit-trail invariant) is the hash-chain
+    append modelled separately in [formal/Provenance.v]
+    ([append_preserves_verified]); it is intentionally NOT re-modelled
+    here. This module proves the structural part of enrichment: it sets
+    the target modality and leaves the others untouched.
+
+    ** Abstraction note
+
+    Per-modality value spaces Sigma_m are unified into one opaque [mval]
+    (the algebra laws are parametric in the value type, exactly as
+    [Drift.v] abstracts the score type). The dependently-typed layout
+    phi : forall m, Sigma_m u {bot} specialises this by a sigma-type;
+    that refinement is orthogonal to the algebraic laws proved here.
+
+    ** Cross-doc: echo-types
+
+    Projection pi_M is a TRUNCATION of the modality section phi — the same
+    shape as [EchoTruncation.agda], already cited by N2 in
+    [formal/CROSS-REPO-MAP.adoc]. Merge (+) under a semilattice [resolve]
+    is a JOIN; the conditional CRDT laws (R1-R3) are a candidate NEW
+    echo-types abstraction (join-semilattice of partial sections), flagged
+    for cross-documentation per the standing directive. See CROSS-REPO-MAP.
+
+    Declared parameters: [mval], [ident]. Declared axioms:
+    [functional_extensionality_dep] (Coq stdlib, for octad/function
+    equality — the same whitelist entry as WAL.v and Normalizer.v).
+
+    Build oracle: [just -f formal/Justfile octad]. CI: coq-build.yml.
+
+    Tracking issue: hyperpolymath/verisimdb#77 (O-series + R1-R3).
+*)
+
+Require Import Coq.Lists.List.
+Require Import Coq.Bool.Bool.
+Require Import Coq.Logic.FunctionalExtensionality.
+Import ListNotations.
+
+(** ** [def:modset] — Modality Set
+
+    The fixed eight-element basis M = {G,V,T,S,D,P,R,X}. Mirrors the eight
+    boolean fields of [ModalityStatus]. *)
+Inductive modality : Type :=
+| Graph | Vector | Tensor | Semantic
+| Document | Temporal | Provenance | Spatial.
+
+Definition all_modalities : list modality :=
+  [Graph; Vector; Tensor; Semantic; Document; Temporal; Provenance; Spatial].
+
+(** O2 — modality cardinality: an octad has exactly eight modalities. *)
+Theorem modality_cardinality : length all_modalities = 8.
+Proof. reflexivity. Qed.
+
+(** O2 — exhaustiveness: every modality is one of the eight. The CI
+    tripwire for a ninth modality being added without updating the
+    octad model. *)
+Theorem modality_exhaustive : forall m, In m all_modalities.
+Proof. intros m; destruct m; simpl; tauto. Qed.
+
+(** Decidable equality on the finite modality enumeration. Proved by
+    [decide equality]; introduces no axiom. *)
+Definition modality_eq_dec (a b : modality) : {a = b} + {a <> b}.
+Proof. decide equality. Defined.
+
+(** ** [def:octad] — Octad: identity + modality function *)
+
+(** Opaque per-modality value. Unifies the paper's Sigma_m; [None] models
+    the paper's bot (absence of a representation in that modality). *)
+Parameter mval : Type.
+
+(** Opaque identifier (the paper's UUID). *)
+Parameter ident : Type.
+
+(** An octad: an identifier together with a modality function
+    phi : modality -> option mval, where [None] = bot. *)
+Record octad : Type := mk_octad {
+  oid  : ident;
+  ophi : modality -> option mval;
+}.
+
+(** Extensional octad equality: equal identifiers and equal modality
+    functions imply equal octads. *)
+Lemma octad_ext :
+  forall o1 o2,
+    oid o1 = oid o2 ->
+    ophi o1 = ophi o2 ->
+    o1 = o2.
+Proof.
+  intros [i1 p1] [i2 p2] Hid Hphi; simpl in *; subst; reflexivity.
+Qed.
+
+(** ** Presence, completeness, and the missing-set (O10) *)
+
+Definition present (o : octad) (m : modality) : bool :=
+  match ophi o m with Some _ => true | None => false end.
+
+(** Mirrors [ModalityStatus::is_complete]: all eight modalities present. *)
+Definition is_complete (o : octad) : bool :=
+  forallb (present o) all_modalities.
+
+(** Mirrors [ModalityStatus::missing]: the modalities that are bot. *)
+Definition missing (o : octad) : list modality :=
+  filter (fun m => negb (present o m)) all_modalities.
+
+(** General bridge: a list is [forallb p]-true iff filtering by [negb . p]
+    leaves nothing. *)
+Lemma forallb_iff_filter_negb_nil :
+  forall (A : Type) (p : A -> bool) (l : list A),
+    forallb p l = true <-> filter (fun x => negb (p x)) l = [].
+Proof.
+  induction l as [|x xs IH]; simpl.
+  - split; reflexivity.
+  - destruct (p x); simpl.
+    + exact IH.
+    + split; intro H; discriminate H.
+Qed.
+
+(** O10 — present-totality: an octad is complete iff nothing is missing.
+    Cross-checks [ModalityStatus::is_complete] against
+    [ModalityStatus::missing]. *)
+Theorem complete_iff_no_missing :
+  forall o, is_complete o = true <-> missing o = [].
+Proof.
+  intros o. unfold is_complete, missing.
+  apply forallb_iff_filter_negb_nil.
+Qed.
+
+(** ** [def:projection] — Projection pi_M
+
+    Restrict the modality function to a mask [M : modality -> bool] (the
+    paper's subset M of modality), sending masked-out modalities to bot. *)
+Definition project (M : modality -> bool) (o : octad) : octad :=
+  mk_octad (oid o) (fun m => if M m then ophi o m else None).
+
+(** [inv:persist] for projection — identity is preserved. *)
+Theorem project_preserves_id :
+  forall M o, oid (project M o) = oid o.
+Proof. reflexivity. Qed.
+
+(** Projecting onto every modality is the identity. *)
+Theorem project_full :
+  forall o, project (fun _ => true) o = o.
+Proof.
+  intros o. apply octad_ext; [reflexivity|].
+  apply functional_extensionality; intro m; reflexivity.
+Qed.
+
+(** Projection is idempotent. *)
+Theorem project_idempotent :
+  forall M o, project M (project M o) = project M o.
+Proof.
+  intros M o. apply octad_ext; [reflexivity|].
+  apply functional_extensionality; intro m; simpl.
+  destruct (M m); reflexivity.
+Qed.
+
+(** Projection composes as mask intersection: pi_M . pi_N = pi_{M /\ N}.
+    The meet-semilattice law — the structural "modularity" of
+    projections. *)
+Theorem project_compose :
+  forall M N o,
+    project M (project N o) = project (fun m => andb (M m) (N m)) o.
+Proof.
+  intros M N o. apply octad_ext; [reflexivity|].
+  apply functional_extensionality; intro m; simpl.
+  destruct (M m), (N m); reflexivity.
+Qed.
+
+(** ** [def:merge] — Merge (+)
+
+    [mcombine] is the per-modality merge kernel:
+      bot (+) bot = bot;  v (+) bot = v;  bot (+) v = v;
+      v1 (+) v2 = resolve v1 v2.
+    [resolve] is the policy-dependent conflict resolver (the paper's
+    [resolve]; [RegenerationStrategy] in the Rust source). It is an
+    ARGUMENT of the operation, not a global axiom — the algebra laws below
+    are implications from its properties. *)
+Definition mcombine (resolve : mval -> mval -> mval)
+                    (x y : option mval) : option mval :=
+  match x, y with
+  | None,   None   => None
+  | Some a, None   => Some a
+  | None,   Some b => Some b
+  | Some a, Some b => Some (resolve a b)
+  end.
+
+(** Merge of two same-identifier octads. The result inherits the left
+    operand's identifier; under the paper's precondition [oid o1 = oid o2]
+    the choice of side is immaterial. *)
+Definition merge (resolve : mval -> mval -> mval) (o1 o2 : octad) : octad :=
+  mk_octad (oid o1) (fun m => mcombine resolve (ophi o1 m) (ophi o2 m)).
+
+(** Merge preserves the (shared) identifier — [inv:persist]. *)
+Theorem merge_preserves_id :
+  forall resolve o1 o2, oid (merge resolve o1 o2) = oid o1.
+Proof. reflexivity. Qed.
+
+(** ** Proposition (Merge Commutativity) — MECHANISED
+
+    The paper: "If resolve is commutative, then (+) is commutative."
+    Its proof was one line; this is that proposition fully mechanised.
+    The same-identifier hypothesis [oid o1 = oid o2] is the paper's
+    "sharing the same identifier" precondition. *)
+Theorem merge_commutative :
+  forall resolve o1 o2,
+    oid o1 = oid o2 ->
+    (forall a b, resolve a b = resolve b a) ->
+    merge resolve o1 o2 = merge resolve o2 o1.
+Proof.
+  intros resolve o1 o2 Hid Hcomm.
+  apply octad_ext.
+  - simpl. exact Hid.
+  - apply functional_extensionality; intro m; simpl.
+    destruct (ophi o1 m) as [a|], (ophi o2 m) as [b|]; simpl;
+      try reflexivity.
+    rewrite Hcomm. reflexivity.
+Qed.
+
+(** ** R2 — Merge associativity, under associative [resolve].
+
+    The left-identifier convention makes (+) associative with NO identifier
+    precondition: both nestings inherit [oid o1]. *)
+Lemma mcombine_assoc :
+  forall resolve,
+    (forall a b c, resolve a (resolve b c) = resolve (resolve a b) c) ->
+    forall x y z,
+      mcombine resolve (mcombine resolve x y) z
+      = mcombine resolve x (mcombine resolve y z).
+Proof.
+  intros resolve Hassoc x y z.
+  destruct x as [a|], y as [b|], z as [c|]; simpl; try reflexivity.
+  rewrite Hassoc. reflexivity.
+Qed.
+
+Theorem merge_associative :
+  forall resolve o1 o2 o3,
+    (forall a b c, resolve a (resolve b c) = resolve (resolve a b) c) ->
+    merge resolve (merge resolve o1 o2) o3
+    = merge resolve o1 (merge resolve o2 o3).
+Proof.
+  intros resolve o1 o2 o3 Hassoc.
+  apply octad_ext; [reflexivity|].
+  apply functional_extensionality; intro m; simpl.
+  apply mcombine_assoc. exact Hassoc.
+Qed.
+
+(** ** R3 — Merge idempotence, under idempotent [resolve]. *)
+Theorem merge_idempotent :
+  forall resolve o,
+    (forall a, resolve a a = a) ->
+    merge resolve o o = o.
+Proof.
+  intros resolve o Hidem.
+  apply octad_ext; [reflexivity|].
+  apply functional_extensionality; intro m; simpl.
+  destruct (ophi o m) as [a|]; simpl; [rewrite Hidem|]; reflexivity.
+Qed.
+
+(** ** [def:enrichment] — Enrichment
+
+    [enrich m v o] sets modality [m] to [v] and leaves all others
+    untouched (the paper's fundamental write primitive). *)
+Definition enrich (m : modality) (v : mval) (o : octad) : octad :=
+  mk_octad (oid o)
+           (fun m' => if modality_eq_dec m' m then Some v else ophi o m').
+
+(** [inv:persist]: enrichment never changes the identifier. *)
+Theorem enrich_preserves_id :
+  forall m v o, oid (enrich m v o) = oid o.
+Proof. reflexivity. Qed.
+
+(** Enrichment writes the target modality. *)
+Theorem enrich_sets_target :
+  forall m v o, ophi (enrich m v o) m = Some v.
+Proof.
+  intros m v o; simpl.
+  destruct (modality_eq_dec m m); [reflexivity | congruence].
+Qed.
+
+(** Enrichment leaves every other modality untouched. *)
+Theorem enrich_preserves_others :
+  forall m v o m', m' <> m -> ophi (enrich m v o) m' = ophi o m'.
+Proof.
+  intros m v o m' Hneq; simpl.
+  destruct (modality_eq_dec m' m); [congruence | reflexivity].
+Qed.
+
+(** After enrichment the target modality is present (not bot) — a local
+    present-totality fact. *)
+Theorem enrich_present :
+  forall m v o, present (enrich m v o) m = true.
+Proof.
+  intros m v o. unfold present. rewrite enrich_sets_target. reflexivity.
+Qed.
+
+(** ** Print Assumptions guard
+
+    Allowed: [mval], [ident] (Parameters) and [functional_extensionality_dep]
+    (Coq stdlib). [modality] is inductive and [resolve] is an operation
+    argument — neither is an axiom. Any other name fails the CI guard. *)
+
+Print Assumptions modality_cardinality.
+Print Assumptions modality_exhaustive.
+Print Assumptions complete_iff_no_missing.
+Print Assumptions project_full.
+Print Assumptions project_idempotent.
+Print Assumptions project_compose.
+Print Assumptions merge_commutative.
+Print Assumptions merge_associative.
+Print Assumptions merge_idempotent.
+Print Assumptions enrich_sets_target.
+Print Assumptions enrich_preserves_others.
+Print Assumptions enrich_present.
diff --git a/fuzz/Cargo.toml b/fuzz/Cargo.toml
index a6b35d5..2e8beaf 100644
--- a/fuzz/Cargo.toml
+++ b/fuzz/Cargo.toml
@@ -8,12 +8,19 @@ edition = "2021"
 [package.metadata]
 cargo-fuzz = true
 
+# This is the project's single cargo-fuzz crate. cargo-fuzz resolves ONE fuzz
+# directory per project (it walks up from the cwd to the nearest `fuzz/`, which
+# is always this one), so EVERY target ClusterFuzzLite builds must live here —
+# a target in rust-core/fuzz is unreachable via `cargo fuzz` and silently
+# resolves back to this manifest. fuzz_vql_parser therefore lives here too.
+# rust-core/fuzz is retained only for the native `cargo check` matrix leg in
+# rust-ci.yml; the canonical fuzz harnesses are these.
 [dependencies]
 libfuzzer-sys = "0.4"
 uuid = "1.23"
 
-[dependencies.verisim-octad]
-path = "../rust-core/verisim-octad"
+[dependencies.verisim-api]
+path = "../rust-core/verisim-api"
 
 # Prevent this from interfering with workspaces
 [workspace]
@@ -25,5 +32,11 @@ path = "fuzz_targets/fuzz_octad_id.rs"
 test = false
 doc = false
 
+[[bin]]
+name = "fuzz_vql_parser"
+path = "fuzz_targets/fuzz_vql_parser.rs"
+test = false
+doc = false
+
 [profile.release]
 debug = 1
diff --git a/fuzz/fuzz_targets/fuzz_vql_parser.rs b/fuzz/fuzz_targets/fuzz_vql_parser.rs
new file mode 100644
index 0000000..624cddc
--- /dev/null
+++ b/fuzz/fuzz_targets/fuzz_vql_parser.rs
@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MPL-2.0
+//
+// Fuzz target for the VQL parser.
+// Run with: cargo +nightly fuzz run fuzz_vql_parser
+//
+// This fuzzer feeds arbitrary byte strings to the VQL parser to find
+// panics, hangs, or memory safety issues. The parser should gracefully
+// reject invalid input without crashing.
+
+#![no_main]
+
+use libfuzzer_sys::fuzz_target;
+
+fuzz_target!(|data: &[u8]| {
+    // Only attempt to parse valid UTF-8 strings — the VQL parser
+    // operates on &str, not raw bytes.
+    if let Ok(input) = std::str::from_utf8(data) {
+        // Limit input size to prevent timeouts on extremely long strings
+        if input.len() <= 4096 {
+            // The parser should never panic on any valid UTF-8 input.
+            // We don't care about the result — only that it doesn't crash.
+            let _ = verisim_api::vql::tokenize(input);
+        }
+    }
+});
diff --git a/rust-core/fuzz/Cargo.toml b/rust-core/fuzz/Cargo.toml
index 69cc0c0..977c204 100644
--- a/rust-core/fuzz/Cargo.toml
+++ b/rust-core/fuzz/Cargo.toml
@@ -1,5 +1,8 @@
 # SPDX-License-Identifier: MPL-2.0
 
+# Retained for the native `cargo check` matrix leg in rust-ci.yml. The
+# ClusterFuzzLite build uses the top-level fuzz/ crate (cargo-fuzz resolves a
+# single fuzz dir per project), where fuzz_vql_parser is canonically hosted.
 [package]
 name = "verisimdb-fuzz"
 version = "0.0.0"