refactor(docs): consolidate design docs under docs/design

.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:

.github/workflows/quality.yml

@@ -35,18 +35,33 @@ 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:
       - uses: actions/checkout@v4
       - 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 }}

.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) ---

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/`)

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"] }

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

_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"

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.

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

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.
 

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`.

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};
 

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
 //!

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.