diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 7bdeb8e..2e76562 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -5,11 +5,25 @@ on:
     # develop = DEV (build only); main = PRD (build + deploy).
     branches: [develop, main]
     paths:
-      - "docs/**"
+      # Book inputs only. docs/design/ is not part of the book, so editing a design
+      # document must not trigger a site build; its links are checked in quality.yml.
+      - "docs/src/**"
+      - "docs/book.toml"
+      - "docs/preprocessors/**"
+      - "docs/mermaid.min.js"
+      - "docs/mermaid-init.js"
+      - "docs/wrangler.toml"
       - ".github/workflows/docs.yml"
   pull_request:
     paths:
-      - "docs/**"
+      # Book inputs only. docs/design/ is not part of the book, so editing a design
+      # document must not trigger a site build; its links are checked in quality.yml.
+      - "docs/src/**"
+      - "docs/book.toml"
+      - "docs/preprocessors/**"
+      - "docs/mermaid.min.js"
+      - "docs/mermaid-init.js"
+      - "docs/wrangler.toml"
       - ".github/workflows/docs.yml"
   workflow_dispatch:
 
@@ -18,21 +32,6 @@ permissions:
   deployments: write
 
 jobs:
-  links:
-    # Markdown lint moved to the consolidated `pre-commit` job in quality.yml.
-    # This job keeps the offline (deterministic) internal-link check.
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-
-      - name: Check internal links
-        uses: lycheeverse/lychee-action@v2
-        with:
-          # Offline: verify relative/anchor links only — deterministic on PRs.
-          # External links are checked on a schedule by the Quality workflow.
-          args: "--offline --no-progress docs/src"
-          fail: true
-
   build:
     runs-on: ubuntu-latest
     defaults:
diff --git a/.github/workflows/quality.yml b/.github/workflows/quality.yml
index 2e8693b..e13079a 100644
--- a/.github/workflows/quality.yml
+++ b/.github/workflows/quality.yml
@@ -35,10 +35,25 @@ jobs:
         env:
           SKIP: fmt,clippy
 
+  internal-links:
+    # Offline link check on every PR: relative and anchor targets only, so it is
+    # deterministic and cannot be blocked by an external host. Lives here rather than
+    # in docs.yml because that workflow is path-filtered to the book's own inputs,
+    # and docs/design/ is outside them. Skip the scheduled run — that one is online.
+    if: github.event_name != 'schedule'
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Check internal links
+        uses: lycheeverse/lychee-action@v2
+        with:
+          args: "--offline --no-progress docs/src docs/design"
+          fail: true
+
   link-check:
     # Full external link check on a schedule (and on demand) — kept off PRs to avoid
-    # flaky external rate-limits blocking merges. PR-time link checking is the offline
-    # check in the Docs workflow.
+    # flaky external rate-limits blocking merges. PR-time link checking is the
+    # `internal-links` job above.
     if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
     steps:
@@ -46,7 +61,7 @@ jobs:
       - name: Check links
         uses: lycheeverse/lychee-action@v2
         with:
-          args: "--no-progress docs/src README.md ARCHITECTURE.md DOMAIN_MODEL.md STORAGE.md"
+          args: "--no-progress docs/src docs/design README.md CONTRIBUTING.md"
           fail: true
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
index d6378df..3cc7f62 100644
--- a/.pre-commit-config.yaml
+++ b/.pre-commit-config.yaml
@@ -53,13 +53,13 @@ repos:
       - id: typos
 
   # --- Markdown lint (commit stage) — reads .markdownlint.jsonc ---
-  # Scoped to mdBook source, excluding SUMMARY.md (multiple H1 part-titles are by design),
-  # matching the previous Docs workflow step.
+  # Scoped to mdBook source and the design records, excluding SUMMARY.md (multiple H1
+  # part-titles are by design).
   - repo: https://github.com/DavidAnson/markdownlint-cli2
     rev: v0.18.1
     hooks:
       - id: markdownlint-cli2
-        files: ^docs/src/.*\.md$
+        files: ^docs/(src|design)/.*\.md$
         exclude: ^docs/src/SUMMARY\.md$
 
   # --- Rust hooks (local; honour rust-toolchain.toml) ---
diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md
deleted file mode 100644
index 4875a41..0000000
--- a/ARCHITECTURE.md
+++ /dev/null
@@ -1,421 +0,0 @@
-# Verity Architecture
-
-> Status: pre-implementation. This document captures the **architectural intent** derived
-> from the [Design Philosophy](docs/src/design-philosophy.md). No Lean or Rust source exists yet.
-
-Verity is a *provable* consensus client: the verified Lean 4 **Verity Consensus** implementation wrapped in a Rust runtime.
-That two-language split makes Verity structurally different from single-language clients, so its
-first-class architectural axis is **the verification boundary** — what is inside the proven consensus implementation
-and what is outside it. Everything else, including the concurrency model, follows from that axis.
-
-The architecture is organized into three concentric zones, drawn from the proven consensus
-implementation outward. A zone is defined by the **guarantee level** it holds code to — proven-pure,
-trusted-and-panic-free, or concurrent-IO — *not* by the specific components that happen to occupy it
-today. Which component sits in which zone is a **current snapshot**, expected to change as the
-verification frontier moves; see [boundary migration](#boundary-migration).
-
-> **Day-one snapshot — Rust-first.** Implementation starts Rust-first (kickoff decision,
-> 2026-07-22): at kickoff **every capability contract is bound to its native-Rust
-> implementation**, the `verity-consensus-sys` export set is empty, and no FFI call is made.
-> Lean-compiled logic is adopted per capability later — stable, proved, and
-> measured-within-budget first; the state transition and fork choice last, because they track
-> a volatile upstream spec. The zone diagrams and the inbound-block sequence below therefore
-> show the **target** state, with Verity Consensus occupying the Verified Core; on day one the
-> same functions run as native Rust in the Runtime Shell, behind the same contracts.
-
-## Zones
-
-- **Verified Core — Verity Consensus (Lean 4, pure).** The proven-pure zone: pure, total functions only —
-  no hidden state, clocks, locks, or scheduling. This is the surface that Lean proofs defend. Its
-  source is the [formal-leanSpec](https://github.com/NyxFoundation/formal-leanSpec) Lean 4 model,
-  compiled via Lean's C backend into a static library and exposed to Rust over a C ABI (no Aeneas) —
-  see [Formal Verification](docs/src/concepts/formal-verification.md) for the one-model, two-roles
-  split between compiled-and-exported functions and proof-only propositions. Its current
-  occupants are deliberately **minimal** — only the state transition and the fork-choice transition
-  functions — but that export set is a snapshot, not a definition: it contracts if a function leaves for
-  a zkVM artifact, and grows if a function (e.g. `hash_tree_root`) is verified in Lean and pulled in.
-
-- **Runtime Shell — Rust, panic-free.** The trusted, panic-free zone. Manufactures clean,
-  typed, **already-verified** inputs for Verity Consensus, owns the consensus state and fork-choice view
-  as a single writer, and threads immutable values through Verity Consensus. Proofs do not reach here, so
-  it is held to the language-level bar instead: memory-safe, strongly typed, and panic-free. *Today*, SSZ
-  / `hash_tree_root` and signature verification are realized here as native-Rust implementations of their
-  [capability contracts](#capability-contracts), so Verity Consensus receives precomputed roots and
-  verified signatures rather than recomputing or trusting them itself. That is a placement, not a
-  contract: were a Lean-verified serialization to satisfy the same contract across the FFI seam, Verified Core
-  would compute those roots itself and Runtime Shell's consumers would not change.
-
-- **I/O Edge — Rust, concurrent.** The only place where concurrency and the outside world
-  live: networking, the slot clock, validator duties, RPC, metrics, and node orchestration. Bounded
-  queues provide backpressure. The concurrency primitive is settled (2026-08-15, see the
-  [Concurrency Model](CONCURRENCY.md)): the single writer is a dedicated task fed by bounded
-  channels, with signature/proof verification staged in front of it. It remains an I/O-Edge-internal
-  concern — the consensus state has a single owner in Runtime Shell and Verity Consensus is invoked
-  sequentially regardless.
-
-## Component diagram
-
-```mermaid
-flowchart TB
-    subgraph C["I/O Edge — Rust, concurrent"]
-        direction LR
-        NET["P2P networking<br/>gossipsub · req/resp"]
-        CLK["Slot clock / ticker"]
-        VAL["Validator duties<br/>produce · sign · aggregate"]
-        RPC["RPC / HTTP API"]
-        MET["Metrics<br/>verity-metrics"]
-        ORCH["Node orchestrator<br/>lifecycle · bounded queues"]
-    end
-
-    subgraph B["Runtime Shell — Rust, panic-free"]
-        direction LR
-        CODEC["SSZ codec + hash_tree_root<br/>wire bytes ↔ typed values"]
-        CRYPTO["Signature verification<br/>verity-crypto: XMSS · leanVM"]
-        STORE["State + fork-choice store<br/>single writer · threads immutable values"]
-        DB["Database<br/>blocks · states · anchor"]
-        FFI["FFI bindings layer"]
-    end
-
-    subgraph A["Verified Core · Verity Consensus — Lean 4, pure"]
-        direction LR
-        STF["State transition<br/>process_slots · process_block"]
-        FC["Fork choice<br/>on_block · on_vote · get_head"]
-    end
-
-    NET -->|"raw bytes"| CODEC
-    CODEC -->|"typed + roots"| CRYPTO
-    CRYPTO -->|"verified inputs"| STORE
-    CLK --> ORCH --> STORE
-    STORE <-->|"immutable values"| FFI
-    FFI ==>|"C ABI · Lean C backend"| STF
-    FFI ==>|"C ABI"| FC
-    STORE --> DB
-    STORE -->|"head / state"| VAL
-    STORE -->|"head / state"| RPC
-    STORE -->|"head / state"| MET
-    VAL -->|"signed block/vote"| CODEC
-```
-
-## Inbound block — crossing the boundary
-
-The boundary crossing over time, for a block arriving from a peer. Decoding, root computation, and
-signature verification all complete in Runtime Shell *before* Verity Consensus is touched, so each FFI call into
-Verity Consensus receives only clean, typed, verified values.
-
-```mermaid
-sequenceDiagram
-    participant P as Peer
-    participant N as Network (C)
-    participant K as Codec + Crypto (B)
-    participant S as Store (B)
-    participant L as Verity Consensus (A)
-    participant D as DB (B)
-    P->>N: gossip block (bytes)
-    N->>K: SSZ decode + hash_tree_root
-    K->>K: verify XMSS / aggregate signatures
-    K->>S: verified, typed block (+ roots)
-    S->>L: process_block(state, block)  [FFI]
-    L-->>S: new state
-    S->>L: on_block(view, block)  [FFI]
-    L-->>S: new view
-    S->>L: get_head(view)  [FFI]
-    L-->>S: head root
-    S->>D: persist block + state
-```
-
-## Crate layout
-
-This layout is the **target** shape, not the day-one scaffold. Implementation starts with a
-single `verity-consensus` crate (kickoff decision, 2026-07-22): the zone boundaries below
-begin as module boundaries inside that crate, holding the same inward invariant, and split
-into separate crates only when a second crate earns its existence. The workspace description
-that follows is what that split grows into.
-
-The Rust runtime is a Cargo workspace. Crates map onto the zones, and **calls and dependencies flow
-inward, from higher-effect / lower-assurance toward lower-effect / higher-assurance — Verified Core never calls
-outward.** Today that ordering reads `I/O Edge → Runtime Shell → Verified Core` over the current crate snapshot, and the compiler
-enforces it rather than discipline. The invariant is stated over *guarantee levels*, not crate
-identities, so it survives migration: if `hash_tree_root` moves into Verified Core, `verity-types` (Runtime Shell)
-calls inward to Verified Core for it — still `Runtime Shell → Verified Core`, still legal; if the state transition leaves Verified Core, its export
-set shrinks but nothing starts calling outward. Names follow the existing `verity-*` convention
-(`verity-crypto`, `verity-metrics`); the sole exception is the FFI bindings crate, which follows its
-upstream Lean library name per Rust's `-sys` convention.
-
-**Crates Verity must build itself**
-
-- `verity-types` — consensus container definitions (Block, State, Vote, …) and constants. The
-  Serialization capability (SSZ encode / decode, `hash_tree_root`) is *currently* satisfied by an
-  external SSZ library behind an adapter in Runtime Shell; the contract (typed value ↔ bytes / root) is stable
-  whether that implementation is the external Rust library or a Lean implementation reached over FFI.
-  Foundational; depended on by every other crate.
-- `verity-consensus-sys` — raw FFI bindings to Verity Consensus, which is built and proven in
-  [formal-leanSpec](https://github.com/NyxFoundation/formal-leanSpec) and consumed here as a static
-  library: Verity Consensus is the compiled, exported subset of that repository's Lean model — the
-  intended mechanism is a dedicated export target (`VerityConsensus`) holding the `@[export]`
-  wrappers over the model. Confines all `unsafe`. Named after that export target. It is the
-  swappable backend behind the
-  [capability contracts](#capability-contracts): its exported function set is exactly *whatever Verified Core
-  currently hosts*, and is expected to expand or contract as the frontier moves.
-- `verity-chain` — the single writer that owns the consensus state and the fork-choice store, and
-  coordinates the `State` and `Store` aggregates under one consistency boundary. The only caller of
-  Verity Consensus; wraps `verity-consensus-sys` behind a safe API. Reads and writes through `verity-db`.
-- `verity-validator` — validator duties (production only): block and vote production, signing, and
-  aggregation.
-- `verity` (binary) — the executable validators run: orchestrator, slot clock, wiring, backpressure.
-
-**Thin glue over existing libraries**
-
-- `verity-p2p` — gossip and req/resp over libp2p.
-- `verity-crypto` — adapter over the two upstream signature libraries: [`leansig`](https://github.com/leanEthereum/leanSig)
-  for per-validator XMSS sign / verify, and [`leanVM`](https://github.com/leanEthereum/leanVM)
-  (formerly leanMultisig) for aggregation and aggregate-proof verification. One capability
-  contract, two suppliers behind it.
-- `verity-db` — persistence (Repository): blocks, states, aggregate proofs, and the finalized anchor.
-  Keeps the storage concern out of the single-writer aggregate coordinator. See
-  [Storage engine and retention](#storage-engine-and-retention).
-- `verity-rpc` — HTTP API surface.
-- `verity-metrics` — implementation of the leanMetrics contract.
-
-Layer mapping: **Verified Core** = Verity Consensus (the compiled export subset of formal-leanSpec, not a Cargo crate); **Runtime Shell** = `verity-consensus-sys`,
-`verity-types`, `verity-chain`, `verity-crypto`, `verity-db`; **I/O Edge** = `verity-p2p`,
-`verity-validator`, `verity-rpc`, `verity-metrics`, `verity` (binary).
-
-```mermaid
-flowchart TB
-    subgraph ZC["I/O Edge"]
-        BIN["verity (bin)"]
-        VAL["verity-validator"]
-        RPC["verity-rpc"]
-        MET["verity-metrics"]
-        P2P["verity-p2p"]
-    end
-    subgraph ZB["Runtime Shell"]
-        CHAIN["verity-chain"]
-        CRYPTO["verity-crypto"]
-        DB["verity-db"]
-        TYPES["verity-types"]
-        SYS["verity-consensus-sys"]
-    end
-    subgraph ZA["Verified Core · Verity Consensus"]
-        LEAN["Verity Consensus<br/>(Lean repo)"]
-    end
-    BIN --> VAL
-    BIN --> RPC
-    BIN --> MET
-    BIN --> P2P
-    BIN --> CHAIN
-    VAL --> CHAIN
-    VAL --> CRYPTO
-    RPC --> CHAIN
-    MET --> CHAIN
-    P2P --> CHAIN
-    CHAIN --> SYS
-    SYS ==> LEAN
-    CHAIN --> DB
-    CHAIN --> TYPES
-    CRYPTO --> TYPES
-    DB --> TYPES
-```
-
-### Storage engine and retention
-
-`verity-db` stores two workloads with opposite shapes, and the split drives every decision below.
-Sizes are measured from leanSpec's `fixtures-prod-scheme.tar.gz` release asset; at
-`SECONDS_PER_SLOT = 4` a day is 21,600 slots. The table layout that follows from these decisions —
-keys, pruning rules, and the snapshot/diff scheme for state — is in
-[Storage Schema](STORAGE.md).
-
-| Workload | Value size | Volume | Lifetime |
-|---|---|---|---|
-| Blocks, states, indices, finalized anchor | ~100 B – 800 B | ~5 MB/day | permanent |
-| Aggregate proofs (`MultiMessageAggregate`) | 155–236 KB, median 190 KB | ~4.1 GB/day | pruned after ~1 day |
-
-**Engine: RocksDB.** The proof workload — six-figure-byte values written continuously and dropped
-en masse a day later — is what an LSM tree with range tombstones is built for, and the same choice
-is what ethlambda, zeam, and qlean-mini run (gean uses Pebble, the same family). The cost is a C++
-dependency in the runtime's build and trust surface; that cost is accepted for Runtime Shell, where
-the bar is memory-safe, panic-free Rust around a well-exercised store, not proof. It buys nothing in
-Verified Core and reaches nothing there.
-
-**Backend trait.** Storage sits behind a backend trait with an in-memory implementation alongside
-the RocksDB one, following ethlambda's `StorageBackend` split. Tests and ephemeral nodes run
-in-memory; the engine stays replaceable if the proof workload later moves out of the database.
-Anything that leaks one engine's semantics into the trait — range deletes above all — is documented
-at the trait, not assumed.
-
-**Proof retention: 21,600 slots (~1 day).** Proofs live in their own table keyed `slot ‖ root`, so
-pruning is a slot-ordered range delete rather than a scan. They are dropped only below
-`tip_slot − 21,600` and only when that cutoff is already finalized; non-finalized proofs are never
-touched. Blocks and states are never pruned by this path.
-
-The floor is not ours to choose: leanSpec sets `MIN_SLOTS_FOR_BLOCK_REQUESTS = 3600` (4 hours) and
-a responder **MUST** serve `BlocksByRange` over that window. Everything above it is an operational
-choice about how far behind a peer can fall and still catch up over P2P instead of needing a
-checkpoint. One day is that horizon — a node down overnight rejoins by range sync — at 6× the
-mandated floor. Note that leanSpec's own reference node satisfies the requirement in memory and
-persists no proofs at all; Verity persists them so the guarantee survives a restart.
-
-### Capability contracts
-
-The Verified Core ↔ Runtime Shell boundary is expressed not as a fixed list of FFI functions but as a small set of **capability
-contracts** — Rust-side interfaces (traits), one per consensus capability that could be realized on
-either side of the proof boundary:
-
-- `StateTransition` — `state_transition(pre_state, verified_block) -> Result<post_state>`
-- `ForkChoiceDecision` — the pure decision: `fork_choice_decision(view) -> head / safe_target / updated view`
-- `Serialization` / `HashTreeRoot` — `hash_tree_root(value) -> root`, encode / decode
-- `SignatureVerification` — verify aggregate (Type-1 / Type-2) proofs
-
-Each contract admits two implementations: a **native-Rust** implementation (the capability lives in
-Runtime Shell) or an **FFI-into-Lean** implementation provided by `verity-consensus-sys` (the capability lives
-in Verified Core). Consumers such as `verity-chain` depend only on the contract and never learn whether it is
-Lean-backed. Which side hosts a capability is therefore the combination of: (a) which implementation is
-bound — a wiring decision in the `verity` binary, constrained by what is actually proven; (b) where the
-proof obligation sits; and (c) whether that capability's functions appear in the `verity-consensus-sys`
-export set.
-
-**Error model.** Failure is part of the contract, in two strictly separated layers:
-
-- **Protocol rejection** (an invalid block) is a *value*. In the Lean model it is a pure
-  `Except`-style result; in the contract it is the `Err` arm of the shared `Result`. The error
-  type is a plain enum (`ProcessingError`), defined **in the contract crate** alongside the
-  traits, so the native-Rust and FFI-into-Lean implementations return the same type and a
-  migration leaves the error path untouched. At the C ABI the FFI implementation uses the
-  conventional shape — an `int32` status code plus an out-parameter for the result — with the
-  status codes in one-to-one correspondence with the Lean model's rejection reasons; that
-  correspondence table is kept next to the Lean definition it mirrors, and the code→enum
-  conversion is confined to `verity-consensus-sys`. Rejection reasons are a small closed set
-  (the Runtime Shell delivers already-verified inputs, so FFI-level rejection is rare by
-  design), which is why a code enum suffices and no structured error payload crosses the ABI.
-- **Runtime failure** (Lean runtime allocation failure) is *not* a value and is not modeled in
-  the contract. The Lean runtime can abort the process on allocation failure, and Verity
-  designs on the assumption that this cannot be hooked. Such an abort is classed with a
-  Rust-side OOM abort: an availability failure, not a safety failure. The panic-freedom claim
-  is precise on this point — it asserts that **no code path returns an incorrect consensus
-  value**, not that a linked runtime can never abort; the residual abort condition is listed in
-  the [trust base](docs/src/concepts/formal-verification.md).
-
-The contracts' "already-verified inputs" clause has concrete, named content: formal-leanSpec's
-theorems are proved relative to explicit well-formedness predicates — `Store.WellFormed` for the
-fork-choice store, `AnchorWF` (discharged by `Reachable`) for the state, and
-`ValidatorRegistry.WellFormed` for validator keys. Maintaining those predicates across every mutation
-is Runtime Shell's half of the contract: Verified Core's theorems speak only about inputs that satisfy
-them, so the single writer must preserve them, and the boundary harnesses target exactly them (see the
-[Model-Checking Strategy](MODEL_CHECK.md)).
-
-The contracts must be defined **inner to both their consumers and their implementations** — otherwise
-`verity-consensus-sys` implementing a contract defined in `verity-chain` would force a `sys → chain`
-edge and break the inward invariant. The recommended home is a thin contract crate (e.g.
-`verity-consensus-api`) holding only the trait definitions — the minimal expression of a movable
-boundary; folding them into `verity-types` is the alternative but mixes container *shape* with
-capability *behavior*. The final crate placement is an implementation-time decision; what matters
-architecturally is that the boundary is a contract, not a hardcoded call site.
-
-> **Settled (kickoff decision, 2026-07-22).** Proposer selection lives chain-side — a pure
-> function next to the state transition and fork choice, not a `verity-validator` concern.
-> Like everything else it starts as native Rust, and its pure-function shape keeps it a
-> candidate for later adoption into the Verified Core.
->
-> **Open for discussion.** Whether duty scheduling, signing, and aggregation should be
-> separate crates rather than folded into `verity-validator` once the workspace split happens.
-
-### The FFI seam — marshalling cost and verification
-
-When a contract is bound FFI-into-Lean, every call marshals its inputs across the C ABI: the
-Rust value is **promoted** into the Lean object representation on the way in and the result
-**lowered** back on the way out. For `StateTransition` and `ForkChoiceDecision` that means the
-full state or fork-choice view crosses the seam per call. This layer deserves explicit
-attention, because it is the weakest trusted link in the whole chain: the Lean theorems stop
-at Lean values, so a conversion bug (a transposed field, an endianness slip, a truncated
-list) makes the proven function compute *correctly on the wrong input* — and no proof, on
-either side, can see it.
-
-Two obligations follow:
-
-- **Verification.** The promote/lower code is boundary code in the Runtime Shell and is the
-  primary target of the boundary harnesses (round-trip properties, no-panic-on-any-input,
-  range enforcement — see [MODEL_CHECK.md](MODEL_CHECK.md)). Cross-language behavioral
-  equivalence is additionally evidenced by shared leanSpec vectors run on both sides;
-  [verifiable-stf](https://github.com/NyxFoundation/verifiable-stf) demonstrates the
-  strongest form of that evidence — the compiled-Lean and compiled-Rust STF produce
-  **byte-identical outputs** on the same inputs.
-- **Measurement.** Adopting a Lean implementation behind a contract is gated on measured
-  cost, not assumed cost. Two data sets exist today:
-  - [leanSSZ](https://github.com/NyxFoundation/leanSSZ)'s C ABI PoC (Rust-caller round-trip
-    and `hash_tree_root` match): STF+HTR 27.5 ms at V=4096, within budget; per-op on a
-    ~526 KB state, serialize 33 ms / `hash_tree_root` 58 ms / deserialize 54 ms
-    (list-based codec, uncached merkleization).
-  - verifiable-stf's compiled-Lean vs compiled-Rust STF comparison (RISC-V zkVM cycles, a
-    proxy for relative native cost): 26.1 M vs 12.5 M cycles at N=10 and 35.3 M vs 14.4 M at
-    N=100 — the Lean runtime's one-time `Init` accounts for ~15 M of the Lean side, so the
-    steady-state Lean overhead is roughly **1.4× Rust** once initialization is amortized
-    across a long-lived process.
-
-  These numbers are inputs to the migration triggers below: a capability moves into the
-  Verified Core only when its measured seam cost fits the slot-time budget.
-
-**Interchange shape — a conditional design, not an adoption decision.** Nothing here decides
-*whether* any capability is bound to Lean — that remains gated per capability (stable, proved,
-measured-within-budget). What is fixed now is only the **shape** the seam takes *if* a binding
-happens, so that a future adoption is a re-binding rather than a redesign:
-
-- **Long-lived values stay resident.** The consensus state and fork-choice view do not round-trip
-  per call. The Rust side holds an opaque handle to a Lean-resident value
-  (`process_block(state_handle, block) -> new_state_handle`), which fits Lean's immutable,
-  reference-counted values and eliminates the per-call state marshalling cost entirely. The
-  single-writer discipline makes ownership simple: the store is the only holder. Persistence and
-  crash recovery are defined by SSZ export/import at the DB, not by the handle.
-- **Inputs cross as SSZ bytes, decoded by the callee.** Per-call inputs (blocks, votes) are
-  passed in their SSZ wire form and decoded on the Lean side. This deliberately avoids
-  constructing Lean objects field-by-field from Rust (`lean_alloc_ctor`-style), which would
-  couple the shell to the Lean object layout and concentrate `unsafe` exactly where a
-  conversion bug is least detectable. Bytes-as-interchange means the conversion is the
-  consensus-critical wire format itself — already fixture-tested on both sides — and, if the
-  Lean side ever ships a proven decoder, the Lean half of the seam becomes proven code.
-
-Field-by-field construction is not banned outright; it is the last resort, admitted only where
-measurement shows the byte path cannot fit the budget.
-
-## Boundary migration
-
-Because a zone is a guarantee level and placement is a snapshot, components are expected to cross the
-Verified Core ↔ Runtime Shell boundary over the life of the project — the [verification boundary moves](docs/src/design-philosophy.md).
-The [capability contracts](#capability-contracts) are what make this affordable: a migration is a
-**re-binding plus a move of the proof obligation**, not a redesign.
-
-**Cost model — what a migration touches, and what it must not.** A migration may change:
-
-- which implementation is bound behind the capability contract (native-Rust ↔ FFI-into-Lean);
-- where the proof obligation sits (a Lean proof vs. a language-level / external-library guarantee);
-- the `verity-consensus-sys` export set (it grows or shrinks);
-- which crate the implementation lives in.
-
-A migration must **not** change:
-
-- consumer code (`verity-chain`, `verity-validator`) — it depends on the contract, not the placement;
-- consensus container **shapes** (the `verity-types` shared model) — shape is separable from the
-  serialization *behavior* that may move (see [Domain Model](DOMAIN_MODEL.md));
-- the zone **definitions** (the guarantee levels);
-- the inward invariant (calls still flow toward higher assurance; Verified Core still never calls outward).
-
-**Anticipated migrations.** Two are foreseen, in opposite directions, alongside two partial placements
-already in the design:
-
-| Capability | Today | Anticipated move | Trigger | Effect |
-|---|---|---|---|---|
-| State transition | Verified Core | Verified Core → Runtime Shell | An upstream spec for SNARK-proving the consensus STF materializes (none published as of 2026-07; see [Ethlambda notes](memo.md#open-question-unresolved-zk-proving-the-stf-vs-lean4-verification)) | Verified Core export set shrinks; FFI surface contracts; the `StateTransition` contract is bound to a zkVM-friendly (Rust / leanVM) implementation |
-| SSZ / `hash_tree_root` | Runtime Shell | Runtime Shell → Verified Core | A Lean-verified merkleization becomes available | Verified Core computes its own roots; "Verity Consensus receives precomputed roots" no longer holds; `verity-types` calls inward to Verified Core for the `Serialization` contract |
-| Fork choice | Verified Core (decision) + Runtime Shell (`Store`) | — | — | The worked example of a capability split across the boundary: a pure decision in Verified Core over a mutable `Store` owned in Runtime Shell |
-| Proposer selection | Runtime Shell (pure function, chain-side) | Runtime Shell → Verified Core (candidate) | Verified in Lean and pulled into the export set | Same pattern as SSZ: a pure decision whose shape is already what the core requires |
-
-The STF row is **not a decision to move it** — the working position is that the STF stays in Verity
-Consensus (Lean 4). It is recorded so the design is shown to *withstand* the move if the trigger fires;
-the full tension is in [Ethlambda notes](memo.md#open-question-unresolved-zk-proving-the-stf-vs-lean4-verification).
-
-## Notes
-
-- What "proven" means — the artifact chain, the proposition catalog, and the trust base — is defined
-  in [Formal Verification](docs/src/concepts/formal-verification.md).
-- Function names in the diagrams (`process_block`, `on_block`, `get_head`, …) are indicative and will
-  be reconciled with [leanSpec](https://github.com/leanEthereum/leanSpec) (lstar HEAD) when
-  implementation begins.
diff --git a/CLAUDE.md b/CLAUDE.md
index f4ef962..e8ede7d 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -35,7 +35,7 @@ Owner-ratified ground rules for the first Rust code. Do not re-open these withou
 - **Toolchain**: Rust edition 2024, resolver 3, latest stable pinned via `rust-toolchain.toml` (external floor: leanSig requires ≥1.87; no nightly needed).
 - **License**: MIT (Nyx Foundation copyright).
 - **Devnet**: always track the latest devnet generation; never hardcode a generation in docs or code comments.
-- **Verification harness**: NOT wired in from day one (no bolero/proptest in the initial scaffold or CI); introduced later per `MODEL_CHECK.md`'s tool-to-zone mapping.
+- **Verification harness**: NOT wired in from day one (no bolero/proptest in the initial scaffold or CI); introduced later per `docs/design/model-check.md`'s tool-to-zone mapping.
 - Known caveat: leanSig internally depends on `ethereum_ssz`, so two SSZ implementations coexist transitively — harmless, but mind type conversions at the signature boundary.
 
 ## Documentation site (`docs/`)
diff --git a/Cargo.toml b/Cargo.toml
index 061e1ba..e8a0e41 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -11,7 +11,7 @@ repository = "https://github.com/NyxFoundation/verity"
 authors = ["Nyx Foundation"]
 
 # Lints are defined once here and inherited by every crate via `[lints] workspace = true`.
-# `unsafe_code` is denied workspace-wide; per ARCHITECTURE.md the only crate allowed to opt back
+# `unsafe_code` is denied workspace-wide; per docs/src/reference/architecture.md the only crate allowed to opt back
 # in is `verity-consensus-sys` (the FFI boundary), which will override this locally when it lands.
 [workspace.lints.rust]
 unsafe_code = "deny"
@@ -73,7 +73,7 @@ libp2p = { version = "0.56", default-features = false, features = [
 ] }
 
 # --- Storage -------------------------------------------------------------------------------
-# See ARCHITECTURE.md "Storage engine and retention" for why an LSM engine and not a B-tree one.
+# See docs/src/reference/architecture.md "Storage engine and retention" for why an LSM engine and not a B-tree one.
 rocksdb = "0.24"
 
 # --- Workspace members ---------------------------------------------------------------------
@@ -88,7 +88,7 @@ verity-types = { path = "crates/verity-types", version = "0.0.0" }
 # Scoped to SSZ round-trip properties in `verity-types`. This is a deliberate, narrow exception
 # to the kickoff decision that no verification harness ships on day one: a codec is one of the
 # few places where the property is writable directly, and leanSpec's fixtures only ever supply
-# the shapes the spec happened to generate. The graduated harness of MODEL_CHECK.md — bolero,
+# the shapes the spec happened to generate. The graduated harness of docs/design/model-check.md — bolero,
 # Kani, loom — is still introduced later, per its tool-to-zone mapping.
 proptest = "1.9"
 serde = { version = "1.0", features = ["derive"] }
diff --git a/README.md b/README.md
index eeb8ba7..6a0909a 100644
--- a/README.md
+++ b/README.md
@@ -29,6 +29,14 @@ Verity makes a different bet — that the implementation should be *proven* to m
 - https://leanroadmap.org/
 - https://strawmap.org/
 
+## Documentation
+
+Reader-facing documentation is published at
+[docs.verityclient.com](https://docs.verityclient.com), built from `docs/src/` — start
+with the [architecture](./docs/src/reference/architecture.md). The internal design
+records that sit underneath it — domain model, concurrency, sync, storage, key
+management, and verification tooling — are in [`docs/design/`](./docs/design/).
+
 ## Contributing
 
 See [CONTRIBUTING.md](./CONTRIBUTING.md) for local setup — Verity uses
diff --git a/_typos.toml b/_typos.toml
index 6acf992..e967305 100644
--- a/_typos.toml
+++ b/_typos.toml
@@ -18,6 +18,6 @@ ser = "ser"
 symetric = "symetric"
 
 [default.extend-identifiers]
-# Abbreviated git commit SHA of leanEthereum/leanSig cited in KEY_MANAGEMENT.md; the
+# Abbreviated git commit SHA of leanEthereum/leanSig cited in docs/design/key-management.md; the
 # trailing "ba" is not a typo of "by"/"be".
 c08a3ba = "c08a3ba"
diff --git a/crates/verity-chain/src/error.rs b/crates/verity-chain/src/error.rs
index 4347088..b9f8421 100644
--- a/crates/verity-chain/src/error.rs
+++ b/crates/verity-chain/src/error.rs
@@ -1,6 +1,6 @@
 //! Why the spec rejects an input.
 //!
-//! This is the `ProcessingError` of `ARCHITECTURE.md`'s capability contracts — a plain enum,
+//! This is the `ProcessingError` of `docs/src/reference/architecture.md`'s capability contracts — a plain enum,
 //! no structured payload, because rejection reasons are a small closed set and nothing but
 //! the discriminant has to survive a future trip across the C ABI. It is named after the
 //! leanSpec enum it mirrors so the two stay greppable against each other.
diff --git a/crates/verity-chain/src/justification.rs b/crates/verity-chain/src/justification.rs
index acd22ad..6591bda 100644
--- a/crates/verity-chain/src/justification.rs
+++ b/crates/verity-chain/src/justification.rs
@@ -3,7 +3,7 @@
 //! leanSpec defines these as methods on `Slot` and `Checkpoint`. Verity keeps them off the
 //! container types on purpose: they are the leading candidates to move into the Verified
 //! Core, and binding them to `verity-types` would make every crate that merely uses a slot
-//! link the FFI boundary once that move happens. See `ARCHITECTURE.md`, "Capability
+//! link the FFI boundary once that move happens. See `docs/src/reference/architecture.md`, "Capability
 //! contracts".
 //!
 //! Transcribed from leanSpec `src/lean_spec/spec/forks/lstar/slot.py`, read at commit
diff --git a/crates/verity-chain/src/merkle.rs b/crates/verity-chain/src/merkle.rs
index f918966..a94bb9a 100644
--- a/crates/verity-chain/src/merkle.rs
+++ b/crates/verity-chain/src/merkle.rs
@@ -1,6 +1,6 @@
 //! The one place the hash tree root hasher is chosen.
 //!
-//! `hash_tree_root` is a capability contract in `ARCHITECTURE.md`, currently satisfied by the
+//! `hash_tree_root` is a capability contract in `docs/src/reference/architecture.md`, currently satisfied by the
 //! external SSZ library. Routing every call in this crate through one function is what keeps
 //! that swap a one-file change: nothing else names a hasher.
 
diff --git a/crates/verity-chain/src/slot_clock.rs b/crates/verity-chain/src/slot_clock.rs
index f5abaa6..36805b3 100644
--- a/crates/verity-chain/src/slot_clock.rs
+++ b/crates/verity-chain/src/slot_clock.rs
@@ -3,7 +3,7 @@
 //! The clock holds no time source. Every accessor takes the instant it should reason about,
 //! in milliseconds since the Unix epoch, so the arithmetic stays pure and testable against
 //! the spec's vectors. Reading the actual clock belongs to the orchestrator that drives the
-//! node — see `ARCHITECTURE.md`, "I/O Edge".
+//! node — see `docs/src/reference/architecture.md`, "I/O Edge".
 //!
 //! Transcribed from leanSpec `src/lean_spec/node/chain/clock.py`, read at commit
 //! `0588c2d215a955a516378677a92db2a5666802f3`.
diff --git a/crates/verity-types/src/checkpoint.rs b/crates/verity-types/src/checkpoint.rs
index 557ab48..67145bf 100644
--- a/crates/verity-types/src/checkpoint.rs
+++ b/crates/verity-types/src/checkpoint.rs
@@ -2,7 +2,7 @@
 //!
 //! leanSpec puts `Checkpoint.advance_to` and `AttestationData.lies_on_chain` on these
 //! containers. They are consensus decisions, not shape, so they live behind the capability
-//! that owns them rather than here — see `ARCHITECTURE.md`, "Capability contracts".
+//! that owns them rather than here — see `docs/src/reference/architecture.md`, "Capability contracts".
 
 use libssz_derive::{HashTreeRoot, SszDecode, SszEncode};
 
diff --git a/crates/verity-types/src/lib.rs b/crates/verity-types/src/lib.rs
index e9eade9..01c6373 100644
--- a/crates/verity-types/src/lib.rs
+++ b/crates/verity-types/src/lib.rs
@@ -11,7 +11,7 @@
 //! Verity places them behind the capability that owns them instead. The reason is migration
 //! cost: those predicates are the leading candidates to move into the Verified Core, and
 //! binding them here would make every crate that merely uses a type link the FFI boundary.
-//! See `ARCHITECTURE.md`, "Capability contracts".
+//! See `docs/src/reference/architecture.md`, "Capability contracts".
 //!
 //! # Source
 //!
diff --git a/docs/design/README.md b/docs/design/README.md
new file mode 100644
index 0000000..bc85380
--- /dev/null
+++ b/docs/design/README.md
@@ -0,0 +1,31 @@
+---
+title: Design Documents
+last_updated: 2026-08-26
+tags:
+  - design
+  - index
+---
+
+# Design Documents
+
+Internal design records: the decisions behind Verity's implementation, the evidence
+they rest on, and the leanSpec revision each was read against. They are not part of the
+published mdBook — [docs.verityclient.com](https://docs.verityclient.com) carries the
+reader-facing documentation instead.
+
+**The architecture is not here.** It is published, and lives at
+[`docs/src/reference/architecture.md`](../src/reference/architecture.md). Everything below
+elaborates one axis of it.
+
+| Document | What it settles |
+|---|---|
+| [Domain Model](domain-model.md) | The consensus entities, value objects, and aggregates as leanSpec defines them, mapped onto the verification zones |
+| [Concurrency Model](concurrency.md) | Which primitive enforces the single-writer discipline, where verification executes, and how inbound work reaches the consensus state |
+| [Sync Pipeline](sync.md) | The sync mode lifecycle, the block-fetch pipeline, and peer management |
+| [Storage Schema](storage.md) | What `verity-db` persists, how it is keyed, which transitions commit together, and what stays in memory |
+| [Key Management](key-management.md) | The crash-safe XMSS no-reuse guarantee, key material loading, and preparation scheduling |
+| [Verification Tooling](model-check.md) | Which verification technique applies to which zone, classified by assurance strength |
+
+Each document states its own status and the upstream revision it was read at. Where two
+disagree, the one with the later `last_updated` is current — and the disagreement is a
+defect worth reporting.
diff --git a/CONCURRENCY.md b/docs/design/concurrency.md
similarity index 94%
rename from CONCURRENCY.md
rename to docs/design/concurrency.md
index 01fd86a..527cec8 100644
--- a/CONCURRENCY.md
+++ b/docs/design/concurrency.md
@@ -1,13 +1,22 @@
+---
+title: Verity Concurrency Model
+last_updated: 2026-08-26
+tags:
+  - concurrency
+  - runtime
+  - model-checking
+---
+
 # Verity Concurrency Model
 
 > Status: pre-implementation. Decisions ratified 2026-08-15. This document settles the question
-> [ARCHITECTURE.md](ARCHITECTURE.md) left open at the I/O Edge — which concurrency primitive
+> [architecture.md](../src/reference/architecture.md) left open at the I/O Edge — which concurrency primitive
 > enforces the single-writer discipline, where signature and proof verification execute, and how
 > inbound work reaches the consensus state — and records the evidence the decisions rest on.
 
 The selection criterion throughout is **verifiability, not throughput**. The deductive proof
 stops at the FFI seam and structurally cannot reach concurrency (see
-[MODEL_CHECK.md](MODEL_CHECK.md)); the strongest tool available in this zone is exhaustive
+[model-check.md](model-check.md)); the strongest tool available in this zone is exhaustive
 concurrency model checking (Loom), and Loom is only tractable on small interleaving spaces. Every
 choice below either eliminates a concurrency property outright (by making it a type-system fact)
 or confines the surviving interleavings to channel endpoints, where Loom can reach them.
@@ -74,7 +83,7 @@ observe a half-applied mutation and has no way to mutate shared state. What is f
 its **contract**, not its field list: it must carry (a) the current head and the latest
 justified / finalized checkpoints, and (b) enough of the block tree and post-states to resolve
 a validator registry by block root. Those two clauses serve its two consumer groups — the read
-APIs [memo.md](memo.md) assigns to `verity-chain` (head, finalized checkpoint, state views)
+APIs assigned to `verity-chain` (head, finalized checkpoint, state views)
 and the verification stage's key resolution. **The `watch`-published snapshot is the entire
 read path**: there is no query channel into the chain task; RPC, metrics, and validator duties
 answer reads from the snapshot they hold. The exact field layout is an implementation
@@ -82,7 +91,7 @@ decision. Three consequences are fixed alongside the contract:
 
 - **Retention bound.** The snapshot covers the *unfinalized* block tree plus the finalized
   anchor — exactly what fork choice operates on, and the only states verification's registry
-  resolution can name. Anything older is `verity-db`'s job ([STORAGE.md](STORAGE.md) state
+  resolution can name. Anything older is `verity-db`'s job ([storage.md](storage.md) state
   snapshots + diffs): an RPC query for a historical state is a database read, not a snapshot
   miss.
 - **Publication cadence.** At most once per chain-task loop iteration, after an event's import
@@ -126,7 +135,7 @@ flowchart LR
 ```
 
 - **Placement.** Between the network task and the chain task, as its own stage — the
-  `Codec + Crypto` participant in ARCHITECTURE.md's inbound-block sequence, made an execution
+  `Codec + Crypto` participant in architecture.md's inbound-block sequence, made an execution
   unit. The network task performs topic validation and deduplication only: no decode, no
   crypto, so network liveness (mesh maintenance, keep-alives) never waits on a proof. It hands
   raw bytes to the stage with `try_send` on the stage's bounded input channel — the single
@@ -139,9 +148,9 @@ flowchart LR
   `VerifiedBlock` / `VerifiedAttestation` values whose constructors are private to the
   verification stage. An unverified value cannot reach the chain task, and therefore cannot
   reach the FFI: the spec's verify-before-STF ordering holds by construction, and the boundary
-  harnesses (Kani / bolero, per MODEL_CHECK.md) cut exactly at these constructors. A
+  harnesses (Kani / bolero, per model-check.md) cut exactly at these constructors. A
   `Verified*` value wraps the decoded, typed container together with the roots computed during
-  verification — ARCHITECTURE.md's "verified, typed block (+ roots)" — so the chain task
+  verification — architecture.md's "verified, typed block (+ roots)" — so the chain task
   re-computes nothing; the exact fields are an implementation decision.
 - **State supply.** The stage resolves validator registries (parent / target post-state) from
   the `watch`-published `Arc<ChainView>` snapshot — the read side of Decision 1 is the supply
@@ -156,7 +165,7 @@ flowchart LR
   *recoverable* failure — parent post-state not yet in view. Every definitive failure —
   malformed SSZ, a root mismatch, an invalid signature or proof — drops the item on the spot,
   counted in metrics (never peer-punished — see
-  [SYNC.md](SYNC.md#decision-3--peer-management)). Overflow evicts count-bounded, in FIFO
+  [sync.md](sync.md#decision-3--peer-management)). Overflow evicts count-bounded, in FIFO
   order of arrival into the
   buffer, and eviction is silent: nothing re-requests an evicted item. An evicted block is
   peer-recoverable — range sync closes the gap when the chain notices the missing ancestry —
@@ -225,7 +234,7 @@ verification stage.
   the network edge — never a value that verification effort was already spent on. Everything
   dropped there is peer-recoverable by construction: `BlocksByRange` responders MUST serve
   3,600 slots (leanSpec floor) and Verity itself retains proofs for 21,600 slots
-  ([STORAGE.md](STORAGE.md)). Range sync is pull-based, so it cannot flood ③ beyond what the
+  ([storage.md](storage.md)). Range sync is pull-based, so it cannot flood ③ beyond what the
   node itself requested.
 - **Biased ordering cannot starve** ① or ② in practice — their rates are bounded by the slot
   clock, not the network — and the bias is the desired property stated directly: time and the
@@ -234,19 +243,19 @@ verification stage.
 ## Lifecycle
 
 Startup runs the dependency arrows backwards. The `verity` binary — the owner of all wiring —
-opens the database, validates its identity values ([STORAGE.md](STORAGE.md)), and hands the
+opens the database, validates its identity values ([storage.md](storage.md)), and hands the
 chain task its handle; the chain task loads the finalized anchor and reconstructs `Store` and
 `State` (initial values, `Store.time` included, per leanSpec's store initialization), then
 publishes the **first `ChainView`** — that publication is the readiness signal every other
 component waits on; only then do the verification stage, network, validator-duty, and RPC
 tasks **begin serving**. What the first `ChainView` gates is serving, not construction:
 initialization that needs no consensus state — validator key preparation above all
-([KEY_MANAGEMENT.md](KEY_MANAGEMENT.md)) — is spawned by the binary at process start and runs
+([key-management.md](key-management.md)) — is spawned by the binary at process start and runs
 in parallel with this sequence. The first `ChainView` is a *necessary* serving gate for every
 component, not always a *sufficient* one: a component may add its own readiness conditions,
 and the validator-duty loop does — it serves only once its keys are also prepared
-([KEY_MANAGEMENT.md](KEY_MANAGEMENT.md)) and the node is `SYNCED`
-([SYNC.md](SYNC.md)) — a join of three gates. Shutdown inverts it, and **channel closure is the only
+([key-management.md](key-management.md)) and the node is `SYNCED`
+([sync.md](sync.md)) — a join of three gates. Shutdown inverts it, and **channel closure is the only
 signal** — there is no shutdown broadcast. The binary stops the producers at the edge; each
 stopped producer drops its sender; every downstream task exits when its inputs return `None`
 (a closed-and-empty channel), with no side-channel bookkeeping. Concretely: the network task
@@ -273,12 +282,12 @@ Listed so they are not mistaken for omissions:
   above, their struct definitions are not — and internal data structures such as the pending
   buffer's index.
 - **Peer scoring** in response to invalid (verification-failing) input — settled in
-  [SYNC.md](SYNC.md#decision-3--peer-management): counted in metrics, never punished, because
+  [sync.md](sync.md#decision-3--peer-management): counted in metrics, never punished, because
   gossipsub forwards before verification and the deliverer may be an honest relay.
 
 ## Verification obligations introduced by this model
 
-What this document adds to the [MODEL_CHECK.md](MODEL_CHECK.md) map, concretely:
+What this document adds to the [model-check.md](model-check.md) map, concretely:
 
 - **Loom targets:** the chain task's select loop, channel endpoints, and snapshot publication
   — the only interleaving spaces this design leaves alive.
@@ -288,5 +297,5 @@ What this document adds to the [MODEL_CHECK.md](MODEL_CHECK.md) map, concretely:
   no-panic-on-any-input for decode and proof verification, and rejection ⇒ no store effect.
 
 A panic that escapes despite these checks is not caught and continued: consistent with
-ARCHITECTURE.md's error model, it is classed as an availability failure and aborts the
+architecture.md's error model, it is classed as an availability failure and aborts the
 process — never a silently degraded consensus path.
diff --git a/DOMAIN_MODEL.md b/docs/design/domain-model.md
similarity index 96%
rename from DOMAIN_MODEL.md
rename to docs/design/domain-model.md
index 213302d..6ec918b 100644
--- a/DOMAIN_MODEL.md
+++ b/docs/design/domain-model.md
@@ -1,14 +1,23 @@
+---
+title: Verity Domain Model
+last_updated: 2026-08-26
+tags:
+  - domain-model
+  - leanspec
+  - types
+---
+
 # Verity Domain Model
 
 > Status: pre-implementation. This document models the consensus domain that Verity must
 > realize. The single source of truth is **leanSpec** (the Python reference implementation);
-> Verity's Rust/Lean types must match it exactly. Read alongside [Architecture](ARCHITECTURE.md).
+> Verity's Rust/Lean types must match it exactly. Read alongside [Architecture](../src/reference/architecture.md).
 >
 > Grounded in `leanEthereum/leanSpec` `main` @ `57d4339929e4bb8e87a190ea2838408cb9057d82`
 > (2026-07-04; `src/lean_spec/spec/forks/lstar/` — the lstar fork, devnet-4/5 in flight).
 > The Lean 4 formal model of this ground truth is
 > [formal-leanSpec](https://github.com/NyxFoundation/formal-leanSpec); see
-> [Formal Verification](docs/src/concepts/formal-verification.md) for how its proposition
+> [Formal Verification](../src/concepts/formal-verification.md) for how its proposition
 > catalog maps onto the zones.
 
 The domain is the **Lean Ethereum consensus protocol**: a set of validators that vote on a
@@ -25,7 +34,7 @@ straddle the verification boundary**: **Fork Choice** is proven as pure decision
 Verified Core, yet its mutable `Store` and single-writer ownership are realized in Runtime Shell. The
 **Realized in** column is a *current snapshot*, not a fixed assignment — capabilities migrate
 across the Verified Core ↔ Runtime Shell boundary as the verification frontier moves (see
-[boundary migration](ARCHITECTURE.md#boundary-migration)), and the State Transition and Serialization rows are
+[boundary migration](../src/reference/architecture.md#boundary-migration)), and the State Transition and Serialization rows are
 expected to move in opposite directions. The
 *tactical* per-zone view stays in [Mapping to verification zones](#mapping-to-verification-zones)
 below; this section is the *strategic* frame above it.
@@ -38,7 +47,7 @@ below; this section is the *strategic* frame above it.
 | **Serialization** | Supporting | SSZ encode / decode, `hash_tree_root`, merkleization | Runtime Shell | `verity-types` (+ external SSZ lib) |
 | **Validator Duties** | Supporting | proposer / attester duties, production, signing, aggregation scheduling | I/O Edge | `verity-validator` |
 | **Networking** | Generic | gossip topics, req / resp, peers | I/O Edge | `verity-p2p` |
-| **Persistence** | Generic | block / state store, aggregate-proof store with a bounded retention window, finalized anchor; Repository over RocksDB behind a backend trait ([schema](STORAGE.md)) | Runtime Shell | `verity-db` |
+| **Persistence** | Generic | block / state store, aggregate-proof store with a bounded retention window, finalized anchor; Repository over RocksDB behind a backend trait ([schema](storage.md)) | Runtime Shell | `verity-db` |
 | **Node Orchestration** | Generic | lifecycle, slot clock, backpressure | I/O Edge | `verity` (bin) |
 | **API** | Generic | HTTP / RPC surface | I/O Edge | `verity-rpc` |
 | **Telemetry** | Generic | metric contract | I/O Edge | `verity-metrics` (Conformist → leanMetrics) |
@@ -79,7 +88,7 @@ satisfies a capability contract whose implementation may be native-Rust (Runtime
 Verified Core. Persistence is factored out as a **Repository** (`verity-db`) that `verity-chain` reads and
 writes through, keeping storage out of the aggregate coordinator. This matches the inward dependency
 invariant (calls flow toward higher assurance; Verified Core never calls outward) in
-[Architecture](ARCHITECTURE.md).
+[Architecture](../src/reference/architecture.md).
 
 ```mermaid
 flowchart LR
@@ -316,7 +325,7 @@ stateDiagram-v2
 
 ## Mapping to verification zones
 
-This domain model lines up with the [Architecture](ARCHITECTURE.md) zones:
+This domain model lines up with the [Architecture](../src/reference/architecture.md) zones:
 
 - **Verified Core (Verity Consensus, Lean):** the `State` aggregate and the state-transition service —
   pure, total functions that the proofs defend.
diff --git a/KEY_MANAGEMENT.md b/docs/design/key-management.md
similarity index 95%
rename from KEY_MANAGEMENT.md
rename to docs/design/key-management.md
index 608ac3c..00fb03b 100644
--- a/KEY_MANAGEMENT.md
+++ b/docs/design/key-management.md
@@ -1,9 +1,18 @@
+---
+title: Validator Key Management — XMSS Signing State
+last_updated: 2026-08-26
+tags:
+  - xmss
+  - key-management
+  - validator
+---
+
 # Validator Key Management — XMSS Signing State
 
 > Status: pre-implementation. Decisions ratified 2026-08-16. This document settles how Verity
 > manages its validators' XMSS keys: the crash-safe no-reuse guarantee, key material loading,
-> and preparation scheduling. It extends [STORAGE.md](STORAGE.md) with one column family and
-> plugs into the runtime model of [CONCURRENCY.md](CONCURRENCY.md).
+> and preparation scheduling. It extends [storage.md](storage.md) with one column family and
+> plugs into the runtime model of [concurrency.md](concurrency.md).
 
 The stake is unusual and worth stating first. XMSS is a **stateful one-time signature
 scheme**: signing two *different* messages with the same key at the same epoch does not incur
@@ -84,7 +93,7 @@ Three scenarios break the clock-monotonicity bet:
 
 Verity persists a **signing watermark**: the last slot signed, per `(validator, role)`, in a
 dedicated `verity-db` column family (`signing_watermarks`, defined in
-[STORAGE.md](STORAGE.md#column-families)). The signing path enforces, in this order:
+[storage.md](storage.md#column-families)). The signing path enforces, in this order:
 
 1. derive the message for slot `s`;
 2. require `s > watermark(validator, role)` — **equality is refused**, even for a
@@ -101,9 +110,9 @@ duty in a 4-second-slot protocol is negligible, and slot-only state keeps the me
 `u64`s per validator instead of a message-root log.
 
 - **Ownership.** The validator signing path is the sole writer of `signing_watermarks` — the
-  one documented exception to the chain task's write ownership (see STORAGE.md). This keeps
+  one documented exception to the chain task's write ownership (see storage.md). This keeps
   the check-write-sign sequence synchronous inside the signing path; routing it through the
-  chain task would add a query channel that [CONCURRENCY.md](CONCURRENCY.md) deliberately
+  chain task would add a query channel that [concurrency.md](concurrency.md) deliberately
   does not have. One keyspace, one writer still holds — per family, not per database.
 - **Write cost.** At most two fsynced single-row writes per slot per validator; negligible
   against the storage engine's proof workload.
@@ -188,11 +197,11 @@ window boundary) mark the two failure modes to design out.
   each key on `spawn_blocking` until the current slot is inside its prepared interval (which
   may take a while after long downtime — progress is logged). None of this needs consensus
   state, so it runs in parallel with the chain task's own startup — per
-  [CONCURRENCY.md](CONCURRENCY.md#lifecycle), what the first `ChainView` gates is *serving*,
+  [concurrency.md](concurrency.md#lifecycle), what the first `ChainView` gates is *serving*,
   not construction. The duty loop begins serving only when **every serving gate** is open — a join of
   independent conditions, of which this document contributes two: the first `ChainView` has
-  been observed on its `watch` receiver (the CONCURRENCY.md readiness signal, unchanged)
-  *and* key preparation has completed. [SYNC.md](SYNC.md#decision-1--sync-mode-lifecycle)
+  been observed on its `watch` receiver (the concurrency.md readiness signal, unchanged)
+  *and* key preparation has completed. [sync.md](sync.md#decision-1--sync-mode-lifecycle)
   adds the third: the node's sync state is `SYNCED`.
 
 ## Deliberately out of scope
@@ -215,4 +224,4 @@ window boundary) mark the two failure modes to design out.
   no partial registry) and the sign wrapper (leanSig's asserts unreachable given the
   wrapper's pre-checks).
 - **The swap** needs no Loom target: clone and swap happen on one task; the only shared edge
-  is the `spawn_blocking` result channel, already covered by the CONCURRENCY.md targets.
+  is the `spawn_blocking` result channel, already covered by the concurrency.md targets.
diff --git a/MODEL_CHECK.md b/docs/design/model-check.md
similarity index 96%
rename from MODEL_CHECK.md
rename to docs/design/model-check.md
index 8e2f555..0eb5773 100644
--- a/MODEL_CHECK.md
+++ b/docs/design/model-check.md
@@ -1,3 +1,12 @@
+---
+title: Verification Tooling Adoption Strategy
+last_updated: 2026-08-26
+tags:
+  - verification
+  - model-checking
+  - tooling
+---
+
 # Verification Tooling Adoption Strategy
 
 > Internal planning memo — not part of the published mdBook. Strategy level only:
@@ -18,7 +27,7 @@
 Verity's verification path is a **Lean 4 deductive proof of the Verified Core**: the
 consensus logic is written as pure, total Lean functions and proven correct, then
 compiled via Lean's C backend into a static library and consumed by the Rust runtime over
-a C ABI (see `ARCHITECTURE.md`). That deductive proof is the ceiling for the *functional
+a C ABI (see `architecture.md`). That deductive proof is the ceiling for the *functional
 correctness* of the proven core, and nothing here displaces it. Model checking is adopted
 as a **complement**, never a replacement — it earns its place in exactly three situations
 the deductive proof leaves open:
@@ -64,7 +73,7 @@ samples a space, 5 samples inputs, 6 watches one run. Each zone gets the stronge
 its nature allows — a pure sequential core can reach row 1; a concurrent I/O subsystem
 tops out at rows 3–4.
 
-The horizontal axis is the **zone** (per `ARCHITECTURE.md`): Verified Core, the
+The horizontal axis is the **zone** (per `architecture.md`): Verified Core, the
 boundary code that services the moving seam (physically in the Runtime Shell), the rest
 of the Runtime Shell, and the I/O Edge. Crossing the two axes gives the whole plan on
 one grid — a cell is filled only where that technique is both *applicable* and *the
@@ -90,9 +99,9 @@ guarantee there is a deliberate, acknowledged floor — see Honest limits.
 ## The zones, and what checks each
 
 The architecture has exactly **three zones**, defined by guarantee level in
-`ARCHITECTURE.md`: Verified Core, Runtime Shell, and I/O Edge. The **verification
+`architecture.md`: Verified Core, Runtime Shell, and I/O Edge. The **verification
 boundary** is the moving seam between Verified Core and Runtime Shell — a line, not a
-zone of its own (see `docs/src/reference/data-representation.md`). The Rust that
+zone of its own (see `../src/reference/data-representation.md`). The Rust that
 services that seam — promote ↔ lower conversions, range and well-formedness checks,
 SSZ, the FFI wrapper — is **boundary code**, and it lives in the Runtime Shell. Each
 zone is owned by a different primary technique; model checking plays a specific,
@@ -107,7 +116,7 @@ bounded role in each.
 ## Tool-to-zone mapping
 
 Each tool is adopted for a specific zone and tied to a stated belief from the
-[design philosophy](../docs/src/design-philosophy.md). The mapping — not the tool list —
+[design philosophy](../src/design-philosophy.md). The mapping — not the tool list —
 is the decision.
 
 - **Kani** (AWS; bounded model checker, CBMC backend). Verifies absence of panics,
@@ -158,7 +167,7 @@ The properties the tools above check are not invented ad hoc. The
 [formal-leanSpec](https://github.com/NyxFoundation/formal-leanSpec) proposition catalog
 (`docs/lean4-proof-propositions.md`) proves spec-level propositions about the Lean model
 across eight domains, and only part of that model is compiled into the shipped artifact
-(see `docs/src/concepts/formal-verification.md`). The rest — the **proof-only** domains,
+(see `../src/concepts/formal-verification.md`). The rest — the **proof-only** domains,
 whose production implementations are Rust — hand each proposition to this strategy as a
 named implementation obligation:
 
diff --git a/STORAGE.md b/docs/design/storage.md
similarity index 97%
rename from STORAGE.md
rename to docs/design/storage.md
index 951394f..0077237 100644
--- a/STORAGE.md
+++ b/docs/design/storage.md
@@ -1,7 +1,16 @@
+---
+title: Storage Schema
+last_updated: 2026-08-26
+tags:
+  - storage
+  - rocksdb
+  - schema
+---
+
 # Storage Schema
 
 What `verity-db` persists, how it is keyed, which transitions commit together, and which short-lived
-aggregation inputs remain in memory. [Architecture](ARCHITECTURE.md#storage-engine-and-retention)
+aggregation inputs remain in memory. [Architecture](../src/reference/architecture.md#storage-engine-and-retention)
 settles the engine — RocksDB behind a backend trait — and this document fixes the repository layout
 underneath it.
 
@@ -54,7 +63,7 @@ corruption, not an absent value.
 | `fork_choice_blocks` | `slot_be ‖ block_root` | `parent_root` | Processed fork-choice tree; retained |
 | `known_votes` | `validator_index_be` | `SSZ(AttestationData)` | Latest counted vote per validator |
 | `pending_votes` | `validator_index_be` | `SSZ(AttestationData)` | Latest not-yet-counted vote per validator |
-| `signing_watermarks` | `validator_index_be ‖ role` | `SSZ(uint64)` last-signed slot | Local XMSS no-reuse state; retained; see [Key Management](KEY_MANAGEMENT.md) |
+| `signing_watermarks` | `validator_index_be ‖ role` | `SSZ(uint64)` last-signed slot | Local XMSS no-reuse state; retained; see [Key Management](key-management.md) |
 | `metadata` | fixed ASCII key | typed scalar or SSZ value | Database identity and current view pointers |
 
 `role` is one byte: `0x00` attestation, `0x01` proposal. `signing_watermarks` rows exist only
@@ -135,7 +144,7 @@ automatically: an operator must select a new directory and explicitly checkpoint
 `verity-chain` — initially the chain module inside the single `verity-consensus` crate — owns the
 only write capability, with **one documented exception**: `signing_watermarks` is written solely by
 the validator signing path, because its persist-before-sign ordering must stay synchronous inside
-that path (see [Key Management](KEY_MANAGEMENT.md#decision-1--signing-watermark-persist-before-sign)).
+that path (see [Key Management](key-management.md#decision-1--signing-watermark-persist-before-sign)).
 The discipline is one writer per column family, not one writer per database. Watermark writes always
 fsync. P2P, RPC, validator duties, and maintenance otherwise submit requests to the chain writer
 rather than writing the backend directly. Read-only snapshot views may run concurrently.
diff --git a/SYNC.md b/docs/design/sync.md
similarity index 93%
rename from SYNC.md
rename to docs/design/sync.md
index 499d81a..6244be6 100644
--- a/SYNC.md
+++ b/docs/design/sync.md
@@ -1,9 +1,18 @@
+---
+title: Sync Pipeline
+last_updated: 2026-08-26
+tags:
+  - sync
+  - networking
+  - p2p
+---
+
 # Sync Pipeline
 
 > Status: pre-implementation. Decisions ratified 2026-08-16. This document settles how Verity
 > joins the network and catches up: the sync mode lifecycle, the block-fetch pipeline, and
-> peer management. It plugs into the runtime model of [CONCURRENCY.md](CONCURRENCY.md) and
-> pays two debts recorded there and in [KEY_MANAGEMENT.md](KEY_MANAGEMENT.md): the mechanism
+> peer management. It plugs into the runtime model of [concurrency.md](concurrency.md) and
+> pays two debts recorded there and in [key-management.md](key-management.md): the mechanism
 > by which "the chain notices the missing ancestry", and the peer-scoring policy both
 > documents deferred to this design.
 
@@ -23,7 +32,7 @@ Read at leanSpec `main` = `cce7955`.
 - The suite's **one MUST**: a responder serves `BlocksByRange` over the sliding
   `MIN_SLOTS_FOR_BLOCK_REQUESTS = 3600`-slot window; below it, `RESOURCE_UNAVAILABLE`.
   Verity's responder side — retention, `served_from_slot`, refusal below the window — is
-  already fixed in [STORAGE.md](STORAGE.md#retention-and-range-sync) and is not restated
+  already fixed in [storage.md](storage.md#retention-and-range-sync) and is not restated
   here.
 - **Checkpoint sync is HTTP, not libp2p**: a Beacon-API-shaped GET of
   `/lean/v0/states/finalized` and `/lean/v0/blocks/finalized` returning raw SSZ. The spec
@@ -73,15 +82,15 @@ Verity adopts the reference node's three-state machine, with the surveyed refine
   ethlambda/qlean-mini once-per-connection design is the named counterexample.
 - **Duties require `SYNCED`.** The sync service publishes its state over a small `watch`
   channel; the validator duty loop reads it as its **third serving gate**, joining the two
-  from [KEY_MANAGEMENT.md](KEY_MANAGEMENT.md) (first `ChainView` observed, keys prepared) —
-  an application of CONCURRENCY.md's necessary-not-sufficient rule. A validator that
+  from [key-management.md](key-management.md) (first `ChainView` observed, keys prepared) —
+  an application of concurrency.md's necessary-not-sufficient rule. A validator that
   attests while behind broadcasts votes for a stale head and burns one-time signatures
-  (KEY_MANAGEMENT.md) for nothing.
+  (key-management.md) for nothing.
 - **The entry decision tree, exhaustively.** Before the machine starts, the anchor is chosen
   by exactly one of three mutually exclusive paths:
   1. `--checkpoint-sync-url` **given** → checkpoint entry (below). The database and genesis
      are *not* fallbacks on this path.
-  2. Flag absent, **populated database** → resume from the database, subject to STORAGE.md's
+  2. Flag absent, **populated database** → resume from the database, subject to storage.md's
      identity validation (which already fails closed on mismatch).
   3. Flag absent, **empty database** → start from genesis.
 - **Checkpoint entry.** Fetch the finalized state and block over HTTP and verify at the
@@ -115,7 +124,7 @@ flowchart LR
 - **The sync service is its own I/O Edge task** (the reference's `SyncService` placement).
   It owns the state machine of Decision 1, aggregates peer Status, and orchestrates
   requests. It is a peer of the networking and validator tasks in the
-  [CONCURRENCY.md](CONCURRENCY.md) lifecycle: spawned by the binary, serving after the
+  [concurrency.md](concurrency.md) lifecycle: spawned by the binary, serving after the
   first `ChainView`.
 - **Gap noticing is a signal from the verification stage.** When the stage parks an item
   whose parent (or attestation target) post-state is not in view — and when it evicts one —
@@ -123,7 +132,7 @@ flowchart LR
   The slot is the **waiting child's**, not the awaited block's — the awaited block is known
   only by root, and the child's slot is what upper-bounds the gap's head-side edge for the
   by-root/by-range split below. This is
-  the concrete mechanism behind CONCURRENCY.md's "range sync closes the gap when the chain
+  the concrete mechanism behind concurrency.md's "range sync closes the gap when the chain
   notices the missing ancestry": the noticing happens where unknown parents are first
   discovered, not in the chain task.
 - **Small gaps go by root, large gaps by range** (zeam's split). A gap of at most a few
@@ -135,14 +144,14 @@ flowchart LR
   non-overlapping windows are complexity the devnet scale does not justify — revisit on
   measurement). **Pagination terminates on the same condition the state machine watches**:
   the sync service subscribes to the `watch`-published `Arc<ChainView>` like every other
-  consumer (CONCURRENCY.md — the snapshot is the read path; there is no query channel), and
+  consumer (concurrency.md — the snapshot is the read path; there is no query channel), and
   after each completed batch it re-checks `ChainView` head against the network finalized
   slot. Behind → issue the next window; caught up → stop, and the Decision 1 machine
   promotes to SYNCED on the same inputs. ream's everything-by-root design is the
   counterexample for deep sync: a one-day gap is ~21,600 sequential round-trips.
 - **Fetched blocks take the same path as gossip: through the verification stage into
   channel ③.** There is no side door into the chain task; the `Verified*` type invariant
-  of CONCURRENCY.md holds for the sync path without exceptions.
+  of concurrency.md holds for the sync path without exceptions.
 - **Structural response validation happens in the sync service** before handing blocks to
   the stage: slots within the requested window, monotonic order, chunk count within the
   request. Violations are protocol-level failures and feed the peer score (Decision 3);
@@ -196,7 +205,7 @@ precedent:
 
 - **Light-client protocols** — no counterpart exists in leanSpec.
 - **State snap-sync** — unnecessary: checkpoint sync carries the anchor state over HTTP,
-  and all later states are reconstructible from [STORAGE.md](STORAGE.md)'s snapshots and
+  and all later states are reconstructible from [storage.md](storage.md)'s snapshots and
   diffs.
 - **DAS-style data-availability sync** — future-fork machinery with no current spec.
 - **Exact thresholds** (by-root/by-range split, Status refresh cadence, walk caps, gap
@@ -207,10 +216,10 @@ precedent:
 
 - **The state machine is a pure function over Status inputs** — transitions
   (`IDLE→SYNCING→SYNCED`, demotion, no shortcut) are property-tested directly; the duty
-  gate adds a third case to the readiness-join tests from KEY_MANAGEMENT.md.
+  gate adds a third case to the readiness-join tests from key-management.md.
 - **Kani / bolero:** structural response validation (no-panic on arbitrary response bytes,
   out-of-window and non-monotonic chunks always rejected) and checkpoint-state verification
   (every listed check individually falsifiable — qlean-mini's dead error variant is the
   cautionary tale).
 - **Loom:** nothing new — the sync service is one task whose shared edges are bounded
-  channels, the same interleaving surface CONCURRENCY.md already targets.
+  channels, the same interleaving surface concurrency.md already targets.
diff --git a/docs/src/concepts/formal-verification.md b/docs/src/concepts/formal-verification.md
index 0c8b0d7..aa05888 100644
--- a/docs/src/concepts/formal-verification.md
+++ b/docs/src/concepts/formal-verification.md
@@ -1,6 +1,6 @@
 ---
 title: Formal Verification
-last_updated: 2026-08-17
+last_updated: 2026-08-26
 tags:
   - formal-verification
   - lean4
@@ -30,7 +30,7 @@ what carries fidelity at each link:
 | Transcription | [formal-leanSpec](https://github.com/NyxFoundation/formal-leanSpec): a Lean 4 model of leanSpec | **Evidenced, not proven** — every Lean file cites the Python source it mirrors; review and leanSpec-derived vectors keep the gap visible |
 | Proof | The proposition catalog: theorems about the model | **Machine-checked** by the Lean 4 kernel; `sorry`-free |
 | Artifact | Verity Consensus: the compiled, exported subset of the model (Lean C backend → static library → C ABI) | **Trusted** — the C backend and linking sit outside every proof (see [the trust base](#the-trust-base)) |
-| Runtime | The Rust shell around the artifact | **Checked, not proven** — the panic-free bar plus the [model-checking strategy](https://github.com/NyxFoundation/verity/blob/main/MODEL_CHECK.md) |
+| Runtime | The Rust shell around the artifact | **Checked, not proven** — the panic-free bar plus the [model-checking strategy](https://github.com/NyxFoundation/verity/blob/main/docs/design/model-check.md) |
 
 ## One model, two roles
 
@@ -47,7 +47,7 @@ and the distinction *is* the verification boundary:
   **design-basis guarantee**: it fixes what the Rust must uphold. The model-checking
   toolchain (Kani, proptest/bolero, Loom, Miri) is what will carry that obligation onto the
   implementation — it is phased in per the
-  [model-checking strategy](https://github.com/NyxFoundation/verity/blob/main/MODEL_CHECK.md),
+  [model-checking strategy](https://github.com/NyxFoundation/verity/blob/main/docs/design/model-check.md),
   not wired in from day one, so until a harness targets a given proposition, that
   proposition constrains the design but says nothing yet about the running Rust.
 
@@ -139,12 +139,6 @@ either proven or it does not ship.
   ([fradamt/verified-consensus](https://github.com/fradamt/verified-consensus);
   [ssf-mc](https://github.com/freespek/ssf-mc)'s bounded model checking of full 3SF).
   Verity consumes the protocol; those efforts justify it.
-- **ZK execution proofs.** Proving that one execution of the STF was faithful is
-  complementary to proving the STF correct for all inputs.
-  [verifiable-stf](https://github.com/NyxFoundation/verifiable-stf) prototypes that
-  direction for the Lean-written STF (zkVM verification of Lean IR execution traces); the
-  full tension is recorded in the
-  [Ethlambda notes](https://github.com/NyxFoundation/verity/blob/main/memo.md#open-question-unresolved-zk-proving-the-stf-vs-lean4-verification).
 - **Cryptographic primitive algebra**: ArkLib.
 
 ## Tracking a moving specification
diff --git a/docs/src/design-philosophy.md b/docs/src/design-philosophy.md
index 0deb913..b8658f3 100644
--- a/docs/src/design-philosophy.md
+++ b/docs/src/design-philosophy.md
@@ -1,3 +1,12 @@
+---
+title: Design Philosophy
+last_updated: 2026-08-26
+tags:
+  - design-philosophy
+  - formal-verification
+  - verification-boundary
+---
+
 # Design Philosophy
 
 Verity is the Provable Consensus Client. Where other clients test for correctness, Verity proves it. The point of this document is not to list features or pick libraries — it is to state the beliefs that decide every later question. When two reasonable designs compete, the one that keeps Verity *provably* faithful to the specification wins.
@@ -20,7 +29,7 @@ These are the convictions that sit above the design principles. They rarely chan
 
 - **Minimalism in service of verifiability.** Keeping things small is not an aesthetic preference here; it is a precondition for proof. Every abstraction, generic, and indirection that Verity Consensus must account for widens the surface a proof has to cover and loosens the correspondence between the Rust implementation and its Lean 4 model. So Verity keeps the proven surface as small as the protocol allows, and adds structure only when a real protocol requirement demands it — never in anticipation of one.
 
-- **The verification boundary is a first-class part of the architecture — and it moves.** Verity is explicit, at all times, about what lives inside Verity Consensus and what lives outside it. The boundary is designed, documented, and defended — not discovered after the fact. Code crossing into Verity Consensus is held to its standard; code outside it exists to feed it clean, well-typed inputs and to carry its outputs to the network. But where the boundary *sits* is not fixed. As the proof effort matures and the upstream roadmap evolves, components cross it in both directions: serialization may be pulled inside the proven core once it is verified in Lean, and the state transition may be pushed back out toward a zkVM artifact if real-time proving demands a different language. What is invariant is not the placement but the discipline — whatever is inside is held to the proof standard, the boundary is always explicit and defended, and a component's side is decided by the guarantee it currently meets, never assumed permanent. The architecture is therefore designed so that moving a component across the boundary is a re-binding, not a redesign.
+- **The verification boundary is a first-class part of the architecture — and it moves.** Verity is explicit, at all times, about what lives inside Verity Consensus and what lives outside it. The boundary is designed, documented, and defended — not discovered after the fact. Code crossing into Verity Consensus is held to its standard; code outside it exists to feed it clean, well-typed inputs and to carry its outputs to the network. But where the boundary *sits* is not fixed. As the proof effort matures, components cross into the proven core: serialization, for instance, may be pulled inside once it is verified in Lean. What is invariant is not the placement but the discipline — whatever is inside is held to the proof standard, the boundary is always explicit and defended, and a component's side is decided by the guarantee it currently meets, never assumed permanent. The architecture is therefore designed so that moving a component across the boundary is a re-binding, not a redesign.
 
 ## Design principles
 
diff --git a/docs/src/reference/architecture.md b/docs/src/reference/architecture.md
index 104d735..7f9c4e0 100644
--- a/docs/src/reference/architecture.md
+++ b/docs/src/reference/architecture.md
@@ -1,6 +1,6 @@
 ---
 title: Verity Architecture
-last_updated: 2026-08-17
+last_updated: 2026-08-26
 tags:
   - architecture
   - verification-boundary
@@ -9,10 +9,9 @@ tags:
 ---
 
 <!--
-  This page mirrors the repo-root ARCHITECTURE.md, which is canonical.
-  When editing, change the root file first and re-sync this page.
-  Only the links differ: book-internal targets are relative, repo-internal
-  documents not published in the book (DOMAIN_MODEL.md, memo.md) point to GitHub.
+  This page is canonical for the architecture. The design documents it links to
+  live in docs/design/ and are not published in the book, so they are referenced
+  by GitHub URL; book-internal targets stay relative.
 -->
 
 # Verity Architecture
@@ -49,8 +48,8 @@ verification frontier moves; see [boundary migration](#boundary-migration).
   see [Formal Verification](../concepts/formal-verification.md) for the one-model, two-roles
   split between compiled-and-exported functions and proof-only propositions. Its current
   occupants are deliberately **minimal** — only the state transition and the fork-choice transition
-  functions — but that export set is a snapshot, not a definition: it contracts if a function leaves for
-  a zkVM artifact, and grows if a function (e.g. `hash_tree_root`) is verified in Lean and pulled in.
+  functions — but that export set is a snapshot, not a definition: it grows as a function
+  (e.g. `hash_tree_root`) is verified in Lean and pulled in.
 
 - **Runtime Shell — Rust, panic-free.** The trusted, panic-free zone. Manufactures clean,
   typed, **already-verified** inputs for Verity Consensus, owns the consensus state and fork-choice view
@@ -151,8 +150,8 @@ inward, from higher-effect / lower-assurance toward lower-effect / higher-assura
 outward.** Today that ordering reads `I/O Edge → Runtime Shell → Verified Core` over the current crate snapshot, and the compiler
 enforces it rather than discipline. The invariant is stated over *guarantee levels*, not crate
 identities, so it survives migration: if `hash_tree_root` moves into Verified Core, `verity-types` (Runtime Shell)
-calls inward to Verified Core for it — still `Runtime Shell → Verified Core`, still legal; if the state transition leaves Verified Core, its export
-set shrinks but nothing starts calling outward. Names follow the existing `verity-*` convention
+calls inward to Verified Core for it — still `Runtime Shell → Verified Core`, still legal, with the export
+set growing but nothing starting to call outward. Names follow the existing `verity-*` convention
 (`verity-crypto`, `verity-metrics`); the sole exception is the FFI bindings crate, which follows its
 upstream Lean library name per Rust's `-sys` convention.
 
@@ -238,7 +237,7 @@ flowchart TB
 Sizes are measured from leanSpec's `fixtures-prod-scheme.tar.gz` release asset; at
 `SECONDS_PER_SLOT = 4` a day is 21,600 slots. The table layout that follows from these decisions —
 keys, pruning rules, and the snapshot/diff scheme for state — is in
-[Storage Schema](https://github.com/NyxFoundation/verity/blob/main/STORAGE.md).
+[Storage Schema](https://github.com/NyxFoundation/verity/blob/main/docs/design/storage.md).
 
 | Workload | Value size | Volume | Lifetime |
 |---|---|---|---|
@@ -316,7 +315,7 @@ fork-choice store, `AnchorWF` (discharged by `Reachable`) for the state, and
 `ValidatorRegistry.WellFormed` for validator keys. Maintaining those predicates across every mutation
 is Runtime Shell's half of the contract: Verified Core's theorems speak only about inputs that satisfy
 them, so the single writer must preserve them, and the boundary harnesses target exactly them (see the
-[Model-Checking Strategy](https://github.com/NyxFoundation/verity/blob/main/MODEL_CHECK.md)).
+[Model-Checking Strategy](https://github.com/NyxFoundation/verity/blob/main/docs/design/model-check.md)).
 
 The contracts must be defined **inner to both their consumers and their implementations** — otherwise
 `verity-consensus-sys` implementing a contract defined in `verity-chain` would force a `sys → chain`
@@ -350,26 +349,17 @@ Two obligations follow:
 - **Verification.** The promote/lower code is boundary code in the Runtime Shell and is the
   primary target of the boundary harnesses (round-trip properties, no-panic-on-any-input,
   range enforcement — see the
-  [Model-Checking Strategy](https://github.com/NyxFoundation/verity/blob/main/MODEL_CHECK.md)).
+  [Model-Checking Strategy](https://github.com/NyxFoundation/verity/blob/main/docs/design/model-check.md)).
   Cross-language behavioral equivalence is additionally evidenced by shared leanSpec vectors
-  run on both sides;
-  [verifiable-stf](https://github.com/NyxFoundation/verifiable-stf) demonstrates the
-  strongest form of that evidence — the compiled-Lean and compiled-Rust STF produce
-  **byte-identical outputs** on the same inputs.
+  run on both sides.
 - **Measurement.** Adopting a Lean implementation behind a contract is gated on measured
-  cost, not assumed cost. Two data sets exist today:
-  - [leanSSZ](https://github.com/NyxFoundation/leanSSZ)'s C ABI PoC (Rust-caller round-trip
-    and `hash_tree_root` match): STF+HTR 27.5 ms at V=4096, within budget; per-op on a
-    ~526 KB state, serialize 33 ms / `hash_tree_root` 58 ms / deserialize 54 ms
-    (list-based codec, uncached merkleization).
-  - verifiable-stf's compiled-Lean vs compiled-Rust STF comparison (RISC-V zkVM cycles, a
-    proxy for relative native cost): 26.1 M vs 12.5 M cycles at N=10 and 35.3 M vs 14.4 M at
-    N=100 — the Lean runtime's one-time `Init` accounts for ~15 M of the Lean side, so the
-    steady-state Lean overhead is roughly **1.4× Rust** once initialization is amortized
-    across a long-lived process.
-
-  These numbers are inputs to the migration triggers below: a capability moves into the
-  Verified Core only when its measured seam cost fits the slot-time budget.
+  cost, not assumed cost. One data set exists today:
+  [leanSSZ](https://github.com/NyxFoundation/leanSSZ)'s C ABI PoC (Rust-caller round-trip
+  and `hash_tree_root` match): STF+HTR 27.5 ms at V=4096, within budget; per-op on a
+  ~526 KB state, serialize 33 ms / `hash_tree_root` 58 ms / deserialize 54 ms
+  (list-based codec, uncached merkleization). These numbers are inputs to the migration
+  triggers below: a capability moves into the Verified Core only when its measured seam cost
+  fits the slot-time budget.
 
 **Interchange shape — a conditional design, not an adoption decision.** Nothing here decides
 *whether* any capability is bound to Lean — that remains gated per capability (stable, proved,
@@ -412,25 +402,19 @@ A migration must **not** change:
 - consumer code (`verity-chain`, `verity-validator`) — it depends on the contract, not the placement;
 - consensus container **shapes** (the `verity-types` shared model) — shape is separable from the
   serialization *behavior* that may move (see the
-  [Domain Model](https://github.com/NyxFoundation/verity/blob/main/DOMAIN_MODEL.md));
+  [Domain Model](https://github.com/NyxFoundation/verity/blob/main/docs/design/domain-model.md));
 - the zone **definitions** (the guarantee levels);
 - the inward invariant (calls still flow toward higher assurance; Verified Core still never calls outward).
 
-**Anticipated migrations.** Two are foreseen, in opposite directions, alongside two partial placements
+**Anticipated migrations.** One is foreseen — inward — alongside two partial placements
 already in the design:
 
 | Capability | Today | Anticipated move | Trigger | Effect |
 |---|---|---|---|---|
-| State transition | Verified Core | Verified Core → Runtime Shell | An upstream spec for SNARK-proving the consensus STF materializes (none published as of 2026-07; see [Ethlambda notes](https://github.com/NyxFoundation/verity/blob/main/memo.md#open-question-unresolved-zk-proving-the-stf-vs-lean4-verification)) | Verified Core export set shrinks; FFI surface contracts; the `StateTransition` contract is bound to a zkVM-friendly (Rust / leanVM) implementation |
 | SSZ / `hash_tree_root` | Runtime Shell | Runtime Shell → Verified Core | A Lean-verified merkleization becomes available | Verified Core computes its own roots; "Verity Consensus receives precomputed roots" no longer holds; `verity-types` calls inward to Verified Core for the `Serialization` contract |
 | Fork choice | Verified Core (decision) + Runtime Shell (`Store`) | — | — | The worked example of a capability split across the boundary: a pure decision in Verified Core over a mutable `Store` owned in Runtime Shell |
 | Proposer selection | Runtime Shell (pure function, chain-side) | Runtime Shell → Verified Core (candidate) | Verified in Lean and pulled into the export set | Same pattern as SSZ: a pure decision whose shape is already what the core requires |
 
-The STF row is **not a decision to move it** — the working position is that the STF stays in Verity
-Consensus (Lean 4). It is recorded so the design is shown to *withstand* the move if the trigger fires;
-the full tension is in the
-[Ethlambda notes](https://github.com/NyxFoundation/verity/blob/main/memo.md#open-question-unresolved-zk-proving-the-stf-vs-lean4-verification).
-
 ## Notes
 
 - What "proven" means — the artifact chain, the proposition catalog, and the trust base — is defined
diff --git a/memo.md b/memo.md
deleted file mode 100644
index 069581a..0000000
--- a/memo.md
+++ /dev/null
@@ -1,259 +0,0 @@
-# Ethlambda Comparison Notes
-
-This memo focuses on the four ethlambda crates that matter most for Verity's
-Lean/Rust verification boundary:
-
-- `ethlambda-lean-ffi` -> `verity-consensus-sys`
-- `ethlambda-state-transition` -> Verity Consensus / `verity-chain` boundary
-- `ethlambda-fork-choice` -> Verity Consensus / `verity-chain` boundary
-- `ethlambda-blockchain` -> `verity-chain` + `verity-validator` + `verity` binary
-
-## High-Level Difference
-
-Ethlambda is organized around a Rust consensus implementation, with selected
-Lean functions inserted through FFI behind a Cargo feature. Verity should invert
-that emphasis: Verity Consensus is the verified Lean implementation, and Rust is
-the trusted shell that prepares inputs, calls it, owns mutable runtime state, and
-persists results.
-
-In short:
-
-```text
-ethlambda:
-  Rust blockchain implementation first
-  Lean is currently a local replacement for selected functions
-
-Verity:
-  Verity Consensus first
-  Rust coordinates verified calls and owns effects outside the proof boundary
-```
-
-## 1. FFI Boundary
-
-Ethlambda's `ethlambda-lean-ffi` is a narrow FFI crate. In the
-`lean-formalization` branch, the observed switch point is
-`slot_is_justifiable_after`: with the `lean-ffi` feature enabled, Rust calls the
-Lean implementation; without it, Rust uses the native implementation.
-
-Verity's `verity-consensus-sys` should be broader and more explicit. It should
-be the only raw ABI boundary for Verity Consensus. It is the **swappable backend
-behind the capability contracts**: its export set is exactly whatever Verified Core
-currently hosts, and is expected to expand or contract as the verification
-boundary moves (see [boundary migration](ARCHITECTURE.md#boundary-migration)).
-
-Responsibilities:
-
-- declare `extern "C"` functions exported by Verity Consensus
-- initialize and manage the Lean runtime
-- isolate `unsafe`
-- handle ABI-level ownership and representation
-- expose the smallest practical low-level Rust surface for `verity-chain`
-
-Non-responsibilities:
-
-- no chain orchestration
-- no database access
-- no P2P, RPC, metrics, or validator duties
-- no consensus policy beyond raw calls into Verity Consensus
-
-> Open: whether Verity Consensus (and therefore this FFI boundary) should host the
-> STF at all is unsettled — see *Open question (unresolved): ZK-proving the STF vs
-> Lean4 verification* below.
-
-## 2. State Transition Boundary
-
-Ethlambda's `ethlambda-state-transition` owns the Rust implementation of the
-state transition. Its `state_transition(&mut State, &Block)` path is Rust-first:
-it mutates `State`, calls Rust `process_slots`, and calls Rust `process_block`.
-Lean currently replaces only selected helper logic.
-
-Verity should place the state transition itself in Verity Consensus.
-
-Target split:
-
-```text
-Verity Consensus:
-  state_transition(pre_state, verified_block) -> post_state
-
-verity-chain:
-  find parent state
-  accept already-decoded and already-verified block input
-  call Verity Consensus
-  handle result/error
-  persist block and post-state through verity-db
-  coordinate finalized/head updates with Store
-```
-
-`verity-chain` should not reimplement the state transition. If a Rust fallback
-exists, it should implement the same Verity Consensus boundary for testing,
-conformance, or development, not grow as a parallel ad hoc path. That "same
-boundary" is precisely the `StateTransition` capability contract: a native-Rust
-implementation of it *is* the Runtime-Shell placement of the STF, so a development
-fallback and an eventual Verified Core → Runtime Shell migration are the same mechanism, not two (see
-[boundary migration](ARCHITECTURE.md#boundary-migration)).
-
-> Open: this section assumes the STF lives in Lean. The Lean Ethereum roadmap
-> points toward ZK-proving the consensus STF, which pulls the STF toward a
-> zkVM-friendly language — see *Open question (unresolved): ZK-proving the STF vs
-> Lean4 verification* below.
-
-## 3. Fork Choice Boundary
-
-Ethlambda's `ethlambda-fork-choice` is close to the shape Verity wants. Its
-`compute_lmd_ghost_head(start_root, blocks, attestations, min_score)` style is
-mostly pure: it takes a view of blocks and attestations and returns a head plus
-weights.
-
-Verity should keep that purity but move the consensus-critical decision
-function into Verity Consensus.
-
-Target split:
-
-```text
-verity-chain:
-  owns the mutable Store as a single writer
-  extracts StoreView / block graph / latest attestations
-  applies returned head, safe_target, and checkpoint updates
-
-Verity Consensus:
-  fork_choice_decision(view) -> head / safe_target / updated view
-```
-
-The important distinction is ownership versus decision:
-
-- Rust owns the mutable Store and persistence.
-- Lean decides the consensus-critical transition from immutable inputs.
-
-This keeps the proof surface pure while avoiding a large mutable database-backed
-Store inside Lean. Fork choice is therefore the worked example of a capability
-*split* across the boundary — a decision function in Verified Core over a `Store` owned
-in Runtime Shell (see [boundary migration](ARCHITECTURE.md#boundary-migration)).
-
-## 4. Chain Orchestration Boundary
-
-Ethlambda's `ethlambda-blockchain` is a practical integration crate, but it is
-too broad for Verity's verification-boundary-first architecture. It combines:
-
-- Store ownership
-- pending block handling
-- tick handling
-- inbound block import
-- inbound attestation import
-- block proposal
-- attestation production
-- signing
-- P2P publishing
-- key management
-
-Verity should split these responsibilities.
-
-```text
-verity-chain:
-  owns State and Store
-  is the single writer for consensus state
-  processes inbound consensus events
-  handles pending blocks
-  sequences Verity Consensus calls
-  coordinates persistence through verity-db
-  exposes read APIs for head, finalized checkpoint, and state views
-
-verity-validator:
-  owns local validator duties
-  requests chain views or candidate data from verity-chain
-  signs blocks and attestations
-  coordinates aggregation and outbound validator artifacts
-  does not own Store or decide fork choice
-
-verity binary:
-  wires runtime components
-  owns slot clock scheduling and bounded queues
-  starts P2P, RPC, metrics, chain, and validator services
-```
-
-The key rule is that `verity-chain` is the only writer of consensus state, while
-`verity-validator` produces local validator actions from chain views. This keeps
-validator production from leaking into consensus state ownership.
-
-## Design Implication
-
-Ethlambda is valuable as a reference for incremental Lean adoption and a working
-Rust client structure. Verity should borrow the useful crate boundaries, but not
-copy the central `ethlambda-blockchain` aggregation.
-
-The Verity boundary should be defined around these APIs early:
-
-```text
-verity-chain -> verity-consensus-sys -> Verity Consensus
-```
-
-This gives Verity a clear verified implementation boundary while still allowing
-Rust-side fallbacks or test implementations to target the same interface.
-
-## Open question (unresolved): ZK-proving the STF vs Lean4 verification
-
-Sections 1 and 2 assume the consensus state transition lives in Verity Consensus
-(Lean 4) behind `verity-consensus-sys`. That assumption is recorded here as **open,
-not settled**. No decision is changed in this memo — this section only captures the
-tension and the trigger for revisiting it.
-
-The architecture is built to *withstand* this move regardless of how it resolves:
-relocating the STF is a re-binding of the `StateTransition` capability contract from
-an FFI-into-Lean implementation to a native / zkVM one, not a redesign. This is the
-worked Verified Core → Runtime Shell example in [boundary migration](ARCHITECTURE.md#boundary-migration).
-
-### What surfaced it
-
-- ethlambda closed its Lean4-STF formalization PR without merging
-  (`lambdaclass/ethlambda#269`, formalizing `slot_is_justifiable_after`). The stated
-  reason: *"ZK proving the STF is in the roadmap, and moving to Lean4 would get in
-  the way of that."* That PR targeted a 3SF consensus function — the same surface
-  Verity places inside Verity Consensus.
-- The Lean Ethereum roadmap points toward SNARK-proving consensus components. As of
-  2026-07 the public tracker's zkVM track covers PQ signature aggregation
-  (pq-devnet-4/5 block-level aggregation proofs); SNARK-proving the STF itself has no
-  published spec or roadmap phase — the direction is attested by statements like the
-  one above, not by a roadmap item.
-
-### Why it is not a conflict today
-
-- Current lstar proofs (`SignedBlock.proof`, Type-1/Type-2) prove **signature
-  aggregation**, not STF execution. Verity verifying those aggregate proofs in
-  `verity-crypto` is consistent with the current design. STF-proving is the
-  longer-term L* evolution and has **no specification yet**.
-
-### The actual tension (forward-looking)
-
-- Formal verification (Lean 4) and ZK execution proofs answer **different
-  questions**. Lean proves the STF *implementation* is correct for all inputs
-  (static, universal). A ZK proof proves *one* execution was faithful to the program
-  that ran — it does **not** prove that program is correct; a ZK proof of a buggy STF
-  faithfully proves the bug. So ZK-proving does not subsume Verity's "the running
-  client is shown to match the spec" thesis; the two are complementary (cf. the
-  Ethereum Foundation's separate zkEVM formal-verification effort, which exists
-  precisely because ZK circuits still need their correctness proven).
-- The binding constraint is **artifact/language**: a single artifact cannot be both
-  Lean4-proven and efficiently zkVM-proven. Lean's runtime (reference counting,
-  boxed values, GC-style allocation) is hostile to in-zkVM execution; the zkVM path
-  is Rust→RISC-V or a leanVM zkDSL. This is why ethlambda kept the STF in Rust.
-
-### Working position and revisit trigger
-
-- **Working position (unchanged):** the STF stays in Verity Consensus (Lean 4), as
-  in Sections 1 and 2. This is *undecided, not reversed* — Verity's differentiator
-  is formal verification, and the conflicting roadmap item does not exist as a spec
-  yet.
-- **Revisit trigger:** when an L* "real-time CL proofs" specification for the
-  consensus STF materializes upstream, reconsider where the STF lives and what
-  `verity-consensus-sys` is for. Candidate reconciliations to evaluate then:
-  - Lean 4 as the verified source of truth, with a separate, equivalence-checked
-    zkVM artifact for proof generation; or
-  - a zkVM-native STF (Rust / leanVM zkDSL) with Lean 4 proving properties only
-    (the ethlambda shape), accepting the loss of "verified running client matches
-    spec".
-
-  An active prototype of the first reconciliation exists:
-  [NyxFoundation/verifiable-stf](https://github.com/NyxFoundation/verifiable-stf)
-  interprets the Lean 4 IR of the Lean-written STF on the host and verifies each trace
-  step in a RISC Zero guest — keeping Lean as the verified source of truth while a zkVM
-  proves *executions* of it. If that scales, the artifact/language constraint above
-  dissolves rather than forcing a side.