diff --git a/docs/roadmap.md b/docs/roadmap.md
index 6589709..002de20 100644
--- a/docs/roadmap.md
+++ b/docs/roadmap.md
@@ -506,6 +506,34 @@ work progresses.
     convergence). CLOSED — audited + drift-resolved; hard gate
     enforces the honesty spirit.
 
+- [~] **\[milestone\]** Formal cross-links in the `design/` ledger
+  (browsable wiki) — IN FLIGHT 2026-05-19. The positive completion
+  of DESIGN.md → `design/`: informal prose cross-references between
+  contracts/models (`(see "Str ABI" below)`, bare-path-in-prose,
+  `§"Section"`) become **formal file-relative Markdown links**
+  `[label](./sibling.md)` / `[label](../../crates/.../x.rs)`
+  resolved relative to the containing file, plus a new RED-first
+  `design_index_pin.rs` **clause-5** that fails the build on any
+  body link that does not resolve into the durable tier (`design/`
+  + `crates/**` + `runtime/**` only — never `docs/`, never a
+  `#fragment`). clause-5 ∘ clause-3 = complete invariant: every
+  contract cross-reference is a resolving durable file-link or
+  clause-3-forbidden history prose. The INDEX **spine stays
+  repo-root-relative** (registry tier, clause-1 byte-unchanged) —
+  the move-fragility rationale that drives body prose to
+  file-relative is absent for the file that never moves.
+  No authoring surface (no `.ail`; precedent: the split spec,
+  audited clean). Out of scope (recon-forced): intra-file
+  "above/below" within one document (no file-link form; the
+  file-split is a separate concern).
+  - context: spec `docs/specs/2026-05-19-design-ledger-formal-links.md`
+    (grounding-check PASS, 7/7 ratified); origin this session's
+    six-turn design conversation following the split close;
+    precedent slice already shipped in the split's tidy
+    (`float-semantics.md` `(see "Str ABI" below)` →
+    `(see design/contracts/str-abi.md)`, now to be brought to the
+    final `[Str ABI](str-abi.md)` form). Awaiting plan.
+
 - [ ] **\[milestone\]** Flat array/slice primitive — performance
   follow-up to the Embedding ABI arc, *not* a capability gap.
   AILang's only sequence is the recursive `List` ADT (one RC cell
diff --git a/docs/specs/2026-05-19-design-ledger-formal-links.md b/docs/specs/2026-05-19-design-ledger-formal-links.md
new file mode 100644
index 0000000..3a6a364
--- /dev/null
+++ b/docs/specs/2026-05-19-design-ledger-formal-links.md
@@ -0,0 +1,362 @@
+# Formal Cross-Links in the design/ Ledger — Design Spec
+
+**Date:** 2026-05-19
+**Status:** Draft — awaiting user spec review
+**Authors:** Brummel (orchestrator) + Claude
+
+## Goal
+
+Make the `design/` ledger a browsable wiki: replace informal prose
+cross-references between contracts/models (`(see "Str ABI" below)`,
+`(see design/contracts/str-abi.md …)`, `see §"Data model"`) with
+**formal, machine-checkable, file-level Markdown links**, and add an
+in-tree hard gate that turns a broken cross-link into a same-commit
+test failure instead of silent rot.
+
+This is the positive completion of the DESIGN.md → design/ split.
+That milestone established the negative half — *history prose must
+not live in a contract* (`contracts_carry_no_decision_record_prose`,
+clause-3). This milestone establishes the positive half — *what
+cross-reference prose remains must resolve to a durable file*.
+Together they form a complete invariant: every cross-reference in a
+contract is **either** a resolving file-relative link into
+`design/`-or-source, **or** decision-record prose that clause-3
+already forbids.
+
+The milestone has **no authoring surface**: it changes no `.ail`
+program, no language construct, no compiler/checker/codegen path. It
+is a documentation-form + Rust-test-infrastructure milestone, the
+same category as the immediately-preceding DESIGN.md → design/ split
+(`docs/specs/2026-05-19-design-md-rolesplit.md`), whose concrete code
+was likewise the structural Rust pin plus the ledger shape, audited
+clean. The no-`.ail` disposition is therefore precedent-governed and
+reasoned, not an omission (see Concrete code shapes §"No authoring
+surface").
+
+## Architecture
+
+Four locked design commitments (converged interactively this
+session; the INDEX sub-choice was resolved by user MC during
+brainstorm Step 2). They are the spec's input contract, not open
+forks:
+
+1. **File-level granularity, no in-file anchors.** A link addresses a
+   whole file. Finer reference granularity is achieved by *splitting
+   a file*, never by a `#fragment`. A link whose target is a pure
+   `#anchor`, or carries a `#fragment` suffix, is a contract
+   violation the hard gate rejects.
+
+2. **Durable-tier targets only.** A formal link may target a file
+   under `design/` (contracts + models) **or** a source file
+   (`crates/**`, `runtime/**`). It may **never** target `docs/`
+   (specs, plans, journals, or standing docs like
+   `docs/PROSE_ROUNDTRIP.md`) — that is the *potentially ephemeral
+   tracking* tier; linking the durable ledger into it re-couples
+   exactly what the split decoupled.
+
+3. **Standard relative Markdown link syntax** `[label](path)`. Not
+   Obsidian `[[wikilinks]]`: wikilink name-fuzzy resolution is the
+   prose-reference problem in another costume (it contradicts
+   content-addressing), is not native on Gitea (the platform we
+   actually use, self-hosted) nor in GitHub repo view, and does not
+   uniformly address source files.
+
+4. **File-relative path form for body prose; the INDEX spine stays
+   repo-root-relative.** Body cross-links are
+   `[label](./sibling.md)` / `[label](../models/x.md)` /
+   `[label](../../crates/ailang-core/src/desugar.rs)`, resolved
+   relative to the *containing file*. This is the universal standard
+   (resolves in Gitea blob, GitHub, VS Code preview, Obsidian,
+   static generators), serving the named primary goal (browsability)
+   on every platform; its move-fragility is real but mechanically
+   bounded by the resolve-check. The earlier "root-relative = the
+   content-addressing thesis" argument was retracted as
+   principle-overreach (the thesis kills name-fuzzy wikilinks;
+   between two deterministic path forms it is an engineering trade).
+   The **INDEX registry table** (`design/INDEX.md`) is a
+   *deliberately-distinct structured tier*: it is machine-parsed as
+   a table, and it is the one `design/` file whose path is
+   structurally invariant (it is THE spine — it does not move). The
+   move-fragility rationale that drove body prose to file-relative is
+   *absent* for the spine, so the INDEX keeps its repo-root-relative
+   cells and `design_index_pin.rs` clause-1 is **unchanged**.
+   Forcing the body rule onto the spine would itself be the
+   principle-overreach pattern this session already retracted once.
+
+Derived scope boundaries (forced by the commitments + Step-1 recon,
+not forks):
+
+- **Intra-file directional prose is out of scope.** "the constraints
+  below", "Direction 1 above", "see §X below" *within the same
+  document* is not a cross-*file* reference; it has no file-link
+  form (same file) and anchors are forbidden by commitment 1.
+  These stay as prose. The remedy for "this file is too big for
+  'above' to be clear" is commitment 1's file-split — a separate
+  future concern, explicitly NOT this milestone.
+- **Homeless references resolve or die.** A prose reference whose
+  referent has no durable home (e.g.
+  `design/models/pipeline.md` → `(see docs/PROSE_ROUNDTRIP.md)`)
+  is retargeted to the durable file that carries the content today
+  (here: `../contracts/roundtrip-invariant.md`) if one exists, else
+  deleted as decision-record-class prose (clause-3 already forbids
+  the relitigation form). Enumerating them is a recon/plan-time
+  scan, not a spec byte-decision.
+- **A cross-*file* `§"Section"` reference becomes a file-link.**
+  `(see §"Data model" …)` pointing at content in *another* file
+  becomes `[Data model](data-model.md)` — the section title may
+  survive only as the human link *label*, never as a `#fragment`
+  (commitment 1). The reader lands on the file and finds the section
+  by reading; that is file-level granularity working as designed,
+  not a loss. (A `§"Section"` that names a section of the *same*
+  file is intra-file directional prose — the bullet above — and is
+  untouched.)
+
+## Concrete code shapes
+
+### No authoring surface — the delivered concrete code
+
+There is no `.ail` because the milestone touches nothing in the
+language: no construct, no type rule, no codegen, no fixture. Per
+the brainstorm infra clause, the rationalisation to refuse is "no
+surface so no code to show"; the honest response is to show the
+concrete code the milestone *does* deliver. For a docs-form +
+test-infra milestone that is (a) the new Rust hard-gate clause,
+(b) the real prose-reference before→after, (c) the explicit
+no-change statement for clause-1. All three are shown below. The
+governing precedent is the immediately-preceding same-category
+milestone (DESIGN.md → design/ split), whose spec led its concrete
+code with the Rust pin and the ledger shape and was audited clean —
+this milestone follows that precedent exactly.
+
+### (a) The new hard gate — `design_index_pin.rs` clause-5
+
+A new test in the existing `crates/ailang-core/tests/design_index_pin.rs`
+(sibling of clauses 1–4; reuses the file's `root()` helper and the
+clause-3 `fs::read_dir` walk idiom verbatim). It is RED-first via an
+embedded synthetic-vector self-check before it asserts the live tree
+(a tree-scan test cannot be RED-first by tree state alone — the tree
+is GREEN-vacuous until the first ref is converted — so the RED proof
+is an in-test malformed-link vector, the honest mechanism for
+"scan-the-tree" gates).
+
+```rust
+#[test]
+fn design_body_links_are_durable_and_resolve() {
+    // clause 5 — every inline Markdown link in design/ body prose
+    // (contracts/ + models/, NOT INDEX.md — the spine is the
+    // structured registry tier resolved by clause-1, commitment 4)
+    // resolves, relative to its CONTAINING file, to an existing
+    // file under design/ or source (crates/** | runtime/**); never
+    // under docs/; never an in-file #anchor. Composes with clause-3:
+    // a surviving cross-reference is a resolving durable file-link
+    // or it is clause-3-forbidden decision-record prose.
+
+    // link target := first capture of  \]\(([^)]+)\)
+    // (matches [x](y) and the ](y) of image ![x](y) alike — every
+    //  parenthesised target must resolve; conservative on purpose)
+    fn targets(md: &str) -> Vec<String> {
+        let mut out = Vec::new();
+        let b = md.as_bytes();
+        let mut i = 0;
+        while i + 1 < b.len() {
+            if b[i] == b']' && b[i + 1] == b'(' {
+                if let Some(end) = md[i + 2..].find(')') {
+                    out.push(md[i + 2..i + 2 + end].trim().to_string());
+                }
+            }
+            i += 1;
+        }
+        out
+    }
+
+    // classify a repo-relative resolved path
+    fn is_durable(repo_rel: &str) -> bool {
+        repo_rel.starts_with("design/")
+            || repo_rel.starts_with("crates/")
+            || repo_rel.starts_with("runtime/")
+    }
+
+    // RED-first synthetic vectors (proves the gate bites before it
+    // is pointed at the live tree).
+    {
+        let t = targets("see [x](../docs/specs/foo.md) and [y](#sec) and [z](./gone.md)");
+        assert_eq!(t, vec!["../docs/specs/foo.md", "#sec", "./gone.md"]);
+        assert!(!is_durable("docs/specs/foo.md"));   // durable-tier reject
+        assert!("#sec".starts_with('#'));            // in-file anchor reject
+    }
+
+    let bases = ["design/contracts", "design/models"];
+    for base in bases {
+        let dir = root().join(base);
+        for entry in fs::read_dir(&dir).expect("design/ subdir exists") {
+            let p = entry.unwrap().path();
+            if p.extension().and_then(|e| e.to_str()) != Some("md") {
+                continue;
+            }
+            let raw = fs::read_to_string(&p).unwrap();
+            let fname = format!("{base}/{}", p.file_name().unwrap().to_string_lossy());
+            for tgt in targets(&raw) {
+                if tgt.starts_with("http://")
+                    || tgt.starts_with("https://")
+                    || tgt.starts_with("mailto:")
+                {
+                    continue; // external — out of the ledger's scope
+                }
+                let file_part = tgt.split('#').next().unwrap_or(&tgt);
+                assert!(
+                    !file_part.is_empty(),
+                    "clause-5: in-file #anchor link {tgt:?} in {fname:?} \
+                     — commitment 1 forbids fragments; split the file"
+                );
+                // resolve RELATIVE TO THE CONTAINING FILE
+                let resolved = p.parent().unwrap().join(file_part);
+                let canon = resolved
+                    .canonicalize()
+                    .unwrap_or_else(|e| panic!(
+                        "clause-5: link {tgt:?} in {fname:?} does not resolve: {e}"
+                    ));
+                let repo_rel = canon
+                    .strip_prefix(root().canonicalize().unwrap())
+                    .unwrap_or(&canon)
+                    .to_string_lossy()
+                    .replace('\\', "/");
+                assert!(
+                    is_durable(&repo_rel),
+                    "clause-5: link {tgt:?} in {fname:?} targets the \
+                     non-durable tier ({repo_rel:?}); commitment 2 \
+                     permits design/ + crates/ + runtime/ only"
+                );
+            }
+        }
+    }
+}
+```
+
+`#[test]` count in the file goes 4 → 5; clauses 1–4 are byte-
+unchanged. The exact byte form of the extractor/regex is the
+planner's to finalise against this shape; the *contract* is the
+three predicates (resolves-from-containing-file; durable-tier;
+no-fragment) and the RED-first synthetic vector.
+
+### (b) Real prose-reference before → after
+
+Three real, in-tree references (recon-confirmed line numbers; exact
+bytes are the planner's):
+
+```
+design/contracts/float-semantics.md:100  (the tidy precedent, still
+  half-formal: bare root path in prose, not a Markdown link)
+- before:  … a fresh heap-Str slab at the call site (see
+           design/contracts/str-abi.md for the dual realisation).
+- after:   … a fresh heap-Str slab at the call site (see
+           [Str ABI](str-abi.md) for the dual realisation).
+           # float-semantics.md and str-abi.md are siblings in
+           # design/contracts/ ⇒ file-relative target is `str-abi.md`
+
+design/contracts/embedding-abi.md:45  (informal AND stale-direction
+  — the exact wart class motivating the milestone: "below" but the
+  target is a different file)
+- before:  … layout is **frozen as of M3** (see "Frozen value
+           layout" below); …
+- after:   … layout is **frozen as of M3** (see
+           [Frozen value layout](frozen-value-layout.md)); …
+
+design/models/pipeline.md:61  (the canonical HOMELESS reference —
+  points into docs/, the non-durable tier)
+- before:  … (see docs/PROSE_ROUNDTRIP.md)
+- after:   … (see [round-trip invariant](../contracts/roundtrip-invariant.md))
+           # retargeted to the durable home that carries the
+           # content; if recon finds no durable home, the clause-6
+           # rule deletes it as decision-record-class prose instead
+```
+
+### (c) clause-1 is unchanged (commitment 4, INDEX = spine)
+
+```
+crates/ailang-core/tests/design_index_pin.rs
+  fn link_target_exists(cell) { … root().join(path).exists() }   // UNCHANGED
+  fn every_index_link_resolves() { … }                            // UNCHANGED
+```
+
+The INDEX table cells stay repo-root-relative
+(`design/contracts/str-abi.md`); clause-1 keeps resolving them via
+`root().join`. No INDEX content edit, no clause-1 resolver edit.
+One resolution rule per *tier* (registry-spine: root-relative;
+movable body prose: file-relative), each locally justified — not
+one rule everywhere, by deliberate design.
+
+## Components
+
+| Component | Disposition |
+|---|---|
+| `crates/ailang-core/tests/design_index_pin.rs` | **Modify** — add clause-5 (`design_body_links_are_durable_and_resolve`); clauses 1–4 byte-unchanged; module `//!` extended one sentence to name clause-5. |
+| `design/contracts/*.md`, `design/models/*.md` | **Modify** — every genuine cross-*file* prose reference rewritten to a file-relative Markdown link; homeless refs retargeted-or-deleted; intra-file "above/below" untouched (out of scope). |
+| `design/INDEX.md` | **Untouched** — spine tier, commitment 4. |
+| `docs/journals/2026-05-19-design-decision-records.md` | **Untouched** — monolithic append-only relitigation archive; never a link target (commitment 2/7). |
+| `design/contracts/honesty-rule.md` | **Modify (prose only)** — one sentence stating cross-references are formal file-relative links into the durable tier (the positive-half companion to the clause-3 sentence it already carries). Pin-safe: the two `docs_honesty_pin.rs` phrases stay verbatim+contiguous. |
+| `bench/architect_sweeps.sh` | **Untouched** — clause-5 ("does every link resolve into the durable tier?") and Sweep-1 ("does any line carry a history anchor: `Iter <n>`, a date, `**Status:`?") are orthogonal predicates over the same files. A Markdown link `[label](file.md)` contains no Sweep-1 anchor token, so converting prose to links cannot trip Sweep-1; clause-5 shares no regex or scope with it. No sweep change. |
+
+## Data flow
+
+`cargo test` → clause-5 reads each `design/contracts/*.md` and
+`design/models/*.md` → extracts every `](…)` target → for each:
+external? skip. `#`-fragment or empty file-part? fail (commitment
+1). Else resolve against the *containing file's directory*,
+canonicalize, strip the repo root → repo-relative path → assert
+under `design/`|`crates/`|`runtime/` (commitment 2). The synthetic
+vector runs first and unconditionally (RED-first proof). clause-1
+independently resolves INDEX cells root-relative (unchanged).
+
+## Error handling
+
+Every failure is a `panic!`/`assert!` naming the file, the offending
+target, and which commitment it violates ("non-durable tier",
+"in-file #anchor — split the file", "does not resolve"). No silent
+skips except the three external schemes. A homeless reference that
+recon cannot map to a durable home is not worked around in the test
+— it is deleted from the prose as clause-3-class content (the test
+then passes because the reference is gone, which is the correct
+outcome, not a dodge).
+
+## Testing strategy
+
+- **RED-first:** clause-5's embedded synthetic-vector block asserts
+  the extractor + durable classifier reject a `docs/specs/…` target
+  and recognise a `#anchor` *before* the tree walk. Planner scripts
+  the first task as: add clause-5 (RED on the synthetic vector if
+  the classifier is stubbed wrong) → make the vector GREEN → then
+  convert prose refs until the tree walk is GREEN.
+- **Composition with clause-3:** a per-milestone assertion (journal,
+  not code) that on the post-milestone tree, for every
+  `design/contracts/*.md`, clause-3 GREEN ∧ clause-5 GREEN — i.e.
+  every cross-reference is a resolving durable link or it is gone.
+- **Whole-suite gate:** `cargo test --workspace` GREEN, count
+  unchanged except +1 test. `design_index_pin` 5/5.
+- **No bench surface:** zero codegen/runtime change ⇒ the regression
+  trio is expected pristine; any firing is the tracked-P2 noise,
+  causally exonerable as in the M2/M3/M5 and the just-closed split.
+
+## Acceptance criteria
+
+1. `crates/ailang-core/tests/design_index_pin.rs` has a 5th test
+   `design_body_links_are_durable_and_resolve`; clauses 1–4 are
+   byte-identical to HEAD `2ee4087`.
+2. clause-5 is demonstrably RED-able (the synthetic vector fails if
+   the durable classifier or the anchor check is wrong) and GREEN on
+   the final tree.
+3. Every genuine cross-*file* prose reference in `design/contracts/`
+   and `design/models/` is a file-relative `[label](path)` Markdown
+   link resolving (from its containing file) to an existing
+   `design/`-or-source file. The float-semantics, embedding-abi, and
+   pipeline references above are converted exactly as shown (modulo
+   recon's homeless-home confirmation).
+4. No reference in `design/` targets `docs/` (any subtree) or
+   carries a `#fragment`.
+5. `design/INDEX.md` and clause-1 are byte-unchanged; the
+   decision-records journal is byte-unchanged and unlinked.
+6. Intra-file "above/below" directional prose is untouched
+   (recon-enumerated as out of scope, not missed).
+7. `cargo test --workspace` GREEN; bench trio exit 0 or
+   causally-exonerated per the standing P2 disposition.
+8. `honesty-rule.md` carries the positive-half sentence; its two
+   `docs_honesty_pin.rs` pinned phrases remain verbatim+contiguous.