From d495498f9df264480cdf5f5241e14c05b30b8a57 Mon Sep 17 00:00:00 2001
From: leynos <leynos@rohga>
Date: Thu, 2 Jul 2026 01:51:09 +0200
Subject: [PATCH 1/5] Convert roadmap footnotes to inline links

The mapsplice roadmap grammar rejects footnote references
("unsupported inline node `footnoteReference`"). Replace every [^N]
footnote reference in docs/roadmap.md with an inline link at the
reference site (as a parenthetical "see ..." or a direct link on the
existing phrase) and remove the footnote definition block at the end of
the file. All link targets are preserved. No wording beyond the link
conversions, no ordering, numbering, or checkbox states change.
---
 docs/roadmap.md | 71 ++++++++++++++++++++++---------------------------
 1 file changed, 32 insertions(+), 39 deletions(-)

diff --git a/docs/roadmap.md b/docs/roadmap.md
index 4df4bd28..a869d933 100644
--- a/docs/roadmap.md
+++ b/docs/roadmap.md
@@ -207,10 +207,12 @@ stream.
 
 - [x] 6.3.1. Provide a helper (for example `Response::with_channel`) that
   returns a bounded channel sender alongside a `Response::MultiPacket` so
-  handlers can opt into streaming ergonomically.[^adr-0001]
+  handlers can opt into streaming ergonomically (see
+  [ADR 0001](adr-001-multi-packet-streaming-response-api.md)).
 - [x] 6.3.2. Update the multi-packet design documentation and user guide with
   tuple return examples that explain initial-frame handling, back-pressure, and
-  graceful termination.[^adr-0001]
+  graceful termination (see
+  [ADR 0001](adr-001-multi-packet-streaming-response-api.md)).
 - [x] 6.3.3. Add an example handler (or test fixture) demonstrating spawning a
   background task that pushes frames through the returned sender while the
   connection actor manages delivery.
@@ -258,7 +260,8 @@ into a single frame, making the process transparent to the application logic.
 
 ## 8. Streaming requests and shared message assembly
 
-This phase implements the decisions from ADR 0002,[^adr-0002] adding
+This phase implements the decisions from
+[ADR 0002](adr-002-streaming-requests-and-shared-message-assembly.md), adding
 first-class streaming request bodies, a generic message assembly abstraction,
 and standardized per-connection memory budgets.
 
@@ -371,7 +374,8 @@ integration boundaries.
 ### 9.2. Fragment adaptor alignment
 
 - [x] 9.2.1. Introduce a `FragmentAdapter` trait as described in the
-  fragmentation design.[^fragmentation-design] Fragmentation behaviour must
+  [fragmentation design](generic-message-fragmentation-and-re-assembly-design.md).
+  Fragmentation behaviour must
   explicitly define duplicate handling, out-of-order policies, and ownership of
   purge scheduling.
   - [x] Make fragmentation opt-in by requiring explicit configuration on the
@@ -389,7 +393,8 @@ integration boundaries.
 ### 9.3. Unified codec handling
 
 - [x] 9.3.1. Unify codec handling between the app router and the `Connection`
-  actor.[^outbound-design]
+  actor (see
+  [outbound messaging design](asynchronous-outbound-messaging-design.md)).
   - [x] Route app-level request and response handling through the
     `FramePipeline` so fragmentation and metrics apply consistently.
   - [x] Remove duplicate codec construction in `src/app/inbound_handler.rs`; the
@@ -398,8 +403,8 @@ integration boundaries.
     fragmentation, sequential requests, disabled fragmentation).
   - [x] Add BDD behavioural tests exercising the unified codec path.
   - [x] Note: protocol hooks (`before_send`) are deferred to a follow-up
-    stage because `F::Frame` and `Envelope` types may
-    differ.[^streaming-design]
+    stage because `F::Frame` and `Envelope` types may differ (see
+    [streaming responses design](multi-packet-and-streaming-responses-design.md)).
 
 ### 9.4. Property-based codec tests
 
@@ -412,12 +417,15 @@ integration boundaries.
 ### 9.5. Serializer boundaries and protocol metadata
 
 - [x] 9.5.1. Decouple message encoding from `bincode`-specific traits to
-  support alternative serializers.[^router-design][^adr-005]
+  support alternative serializers (see
+  [rust-binary-router-library-design.md](rust-binary-router-library-design.md)
+  and [adr-005-serializer-abstraction.md](adr-005-serializer-abstraction.md)).
   - [x] Introduce a serializer-agnostic message trait or adaptor layer for
     `Message` types.
   - [x] Provide optional wire-rs or Serde bridges to reduce manual boilerplate.
   - [x] Define how frame metadata is exposed to the deserialization context to
-    enable version negotiation.[^message-versioning]
+    enable version negotiation (see
+    [message-versioning.md](message-versioning.md)).
   - [x] Add migration guidance covering existing `bincode` users.
 
 ### 9.6. Codec performance benchmarks
@@ -436,7 +444,8 @@ integration boundaries.
   invalid frames, including oversized payloads and correlation metadata.
 - [x] 9.7.3. Introduce a test observability harness in `wireframe_testing` that
   captures logs and metrics per test run for asserting codec failures and
-  recovery policies.[^adr-006]
+  recovery policies (see
+  [adr-006-test-observability.md](adr-006-test-observability.md)).
 - [x] 9.7.4. Add regression tests backed by `wireframe_testing` for the
       `CodecError`
   taxonomy and recovery policy behaviours defined in 9.1.2. Requires 9.1.2.
@@ -617,21 +626,26 @@ Wireframe's protocol, framing, and message assembly layers.
 - [ ] 15.2.1. Support a determined set of length-prefix widths (either `1`,
   `2`, `4`, and `8`, or the full `1..=8` range) and enforce them in
   constructors, conversions, and tests; record the decision in an ADR. Requires
-  15.1.1. See the formal verification guide[^fv-guide] §"What widths does
-  Wireframe actually support for length prefixes?". Success criteria: an ADR
+  15.1.1. See the
+  [formal verification guide](formal-verification-methods-in-wireframe.md)
+  §"What widths does Wireframe actually support for length prefixes?".
+  Success criteria: an ADR
   records the decision, constructors enforce the chosen set, and existing tests
   cover rejected widths.
 - [ ] 15.2.2. Treat `total_body_len` as either authoritative or advisory and
   enforce or rename it consistently across the message assembly path; record
   the decision in an ADR and add tests for both conforming and violating
-  inputs. Requires 15.1.1. See the formal verification guide[^fv-guide] §"Is
-  `total_body_len` authoritative or advisory?". Success criteria: an ADR
+  inputs. Requires 15.1.1. See the
+  [formal verification guide](formal-verification-methods-in-wireframe.md)
+  §"Is `total_body_len` authoritative or advisory?". Success criteria: an ADR
   records the decision, runtime code enforces the chosen semantics, and tests
   verify both conforming and violating inputs.
 - [ ] 15.2.3. Publish named fairness and priority guarantees for
   `ConnectionActor` and encode them as model properties for Stateright checks.
-  Requires 15.1.1. See the formal verification guide[^fv-guide] §"What fairness
-  guarantee does `ConnectionActor` actually make?". Success criteria: the
+  Requires 15.1.1. See the
+  [formal verification guide](formal-verification-methods-in-wireframe.md)
+  §"What fairness guarantee does `ConnectionActor` actually make?".
+  Success criteria: the
   design document enumerates each guarantee as a named property that can be
   referenced by Stateright model checks.
 
@@ -801,7 +815,8 @@ ecosystem.
 - [ ] 18.2.1. Implement a formal message versioning system to allow for
   protocol evolution.
 - [ ] 18.2.2. Ensure version negotiation can consume codec metadata without
-  leaking framing details into handlers.[^message-versioning]
+  leaking framing details into handlers (see
+  [message-versioning.md](message-versioning.md)).
 
 ### 18.3. Security
 
@@ -832,25 +847,3 @@ and usability.
 - [ ] 19.4.1. Ensure all public items have clear, useful documentation
   examples.
 - [ ] 19.4.2. Publish documentation to `docs.rs`.
-
-[^adr-0001]: Refer to
-[ADR 0001](adr-001-multi-packet-streaming-response-api.md).
-[^adr-0002]: Refer to
-[ADR 0002](adr-002-streaming-requests-and-shared-message-assembly.md).
-[^fragmentation-design]: See
-  [fragmentation doc](generic-message-fragmentation-and-re-assembly-design.md).
-[^outbound-design]: See
-  [outbound messaging design](asynchronous-outbound-messaging-design.md).
-[^streaming-design]: See
-  [streaming responses design](multi-packet-and-streaming-responses-design.md).
-[^router-design]: See
-[rust-binary-router-library-design.md](rust-binary-router-library-design.md).
-[^message-versioning]: See
-[message-versioning.md](message-versioning.md).
-[^adr-005]: See
-[adr-005-serializer-abstraction.md](adr-005-serializer-abstraction.md).
-[^adr-006]: See
-[adr-006-test-observability.md](adr-006-test-observability.md).
-
-[^fv-guide]: See
-[formal-verification-methods-in-wireframe.md](formal-verification-methods-in-wireframe.md).

From 29a3b8960a9e1a0188643d0b93ac96b34d90870c Mon Sep 17 00:00:00 2001
From: leynos <leynos@rohga>
Date: Sat, 25 Jul 2026 17:50:50 +0200
Subject: [PATCH 2/5] Standardize roadmap link text and note mapsplice
 exception
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Address review feedback on the footnote-to-inline-link conversion in
docs/roadmap.md:

- Standardize the visible link text: cite ADRs as `ADR NNNN` and design
  documents by a short descriptive name rather than a raw filename, so
  the inline references read consistently.
- Reference the formal verification guide once in the §15.2 introduction
  and let each task cite only its specific section, removing the
  repeated full guide link.
- Keep every changed line within the 80-column limit by linking the
  distinguishing keyword and leaving "design" in the surrounding prose.

Document why the roadmap cannot use GitHub-flavoured footnotes: the
mapsplice roadmap grammar rejects footnote references, so roadmap-shaped
Markdown must cite references inline. Record this scoped exception in
AGENTS.md and the documentation style guide.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 AGENTS.md                         |  5 +++
 docs/documentation-style-guide.md |  4 ++
 docs/roadmap.md                   | 61 +++++++++++++++----------------
 3 files changed, 38 insertions(+), 32 deletions(-)

diff --git a/AGENTS.md b/AGENTS.md
index 4f2b6bf6..c6d856b0 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -307,6 +307,11 @@ project:
 - Use dashes (`-`) for list bullets.
 - Use GitHub-flavoured Markdown footnotes (`[^1]`) for references and
   footnotes.
+  - Exception: roadmap-shaped Markdown edited with `mapsplice` (for example
+    `docs/roadmap.md`) must use inline links instead, because the `mapsplice`
+    roadmap grammar rejects footnote references (`unsupported inline node
+    footnoteReference`). Cite references inline, either as a parenthetical
+    `(see [target](path))` or by linking an existing phrase.
 
 ## Additional tooling
 
diff --git a/docs/documentation-style-guide.md b/docs/documentation-style-guide.md
index d4334c3a..a6fc9a31 100644
--- a/docs/documentation-style-guide.md
+++ b/docs/documentation-style-guide.md
@@ -62,6 +62,10 @@ consistent, and easy to maintain across projects.
 - Do not wrap tables.
 - Use GitHub-flavoured numeric footnotes referenced as `[^1]`.
 - Footnotes must be numbered in order of appearance in the document.
+- Exception: roadmap-shaped Markdown edited with `mapsplice` (for example
+  `docs/roadmap.md`) must cite references with inline links instead of
+  footnotes, because the `mapsplice` roadmap grammar rejects footnote
+  references.
 - Caption every table, and caption every diagram.
 
 ## Standard document types
diff --git a/docs/roadmap.md b/docs/roadmap.md
index a869d933..429920b2 100644
--- a/docs/roadmap.md
+++ b/docs/roadmap.md
@@ -374,10 +374,9 @@ integration boundaries.
 ### 9.2. Fragment adaptor alignment
 
 - [x] 9.2.1. Introduce a `FragmentAdapter` trait as described in the
-  [fragmentation design](generic-message-fragmentation-and-re-assembly-design.md).
-  Fragmentation behaviour must
-  explicitly define duplicate handling, out-of-order policies, and ownership of
-  purge scheduling.
+  [fragmentation](generic-message-fragmentation-and-re-assembly-design.md)
+  design. Fragmentation behaviour must explicitly define duplicate handling,
+  out-of-order policies, and ownership of purge scheduling.
   - [x] Make fragmentation opt-in by requiring explicit configuration on the
     `WireframeApp` builder.
   - [x] Expose a public purge API, so callers can drive timeout eviction.
@@ -403,8 +402,9 @@ integration boundaries.
     fragmentation, sequential requests, disabled fragmentation).
   - [x] Add BDD behavioural tests exercising the unified codec path.
   - [x] Note: protocol hooks (`before_send`) are deferred to a follow-up
-    stage because `F::Frame` and `Envelope` types may differ (see
-    [streaming responses design](multi-packet-and-streaming-responses-design.md)).
+    stage because `F::Frame` and `Envelope` types may differ; see the
+    [streaming responses](multi-packet-and-streaming-responses-design.md)
+    design.
 
 ### 9.4. Property-based codec tests
 
@@ -417,15 +417,15 @@ integration boundaries.
 ### 9.5. Serializer boundaries and protocol metadata
 
 - [x] 9.5.1. Decouple message encoding from `bincode`-specific traits to
-  support alternative serializers (see
-  [rust-binary-router-library-design.md](rust-binary-router-library-design.md)
-  and [adr-005-serializer-abstraction.md](adr-005-serializer-abstraction.md)).
+  support alternative serializers (see the
+  [binary router library design](rust-binary-router-library-design.md) and
+  [ADR 0005](adr-005-serializer-abstraction.md)).
   - [x] Introduce a serializer-agnostic message trait or adaptor layer for
     `Message` types.
   - [x] Provide optional wire-rs or Serde bridges to reduce manual boilerplate.
   - [x] Define how frame metadata is exposed to the deserialization context to
-    enable version negotiation (see
-    [message-versioning.md](message-versioning.md)).
+    enable version negotiation (see the
+    [message versioning design](message-versioning.md)).
   - [x] Add migration guidance covering existing `bincode` users.
 
 ### 9.6. Codec performance benchmarks
@@ -444,8 +444,7 @@ integration boundaries.
   invalid frames, including oversized payloads and correlation metadata.
 - [x] 9.7.3. Introduce a test observability harness in `wireframe_testing` that
   captures logs and metrics per test run for asserting codec failures and
-  recovery policies (see
-  [adr-006-test-observability.md](adr-006-test-observability.md)).
+  recovery policies (see [ADR 0006](adr-006-test-observability.md)).
 - [x] 9.7.4. Add regression tests backed by `wireframe_testing` for the
       `CodecError`
   taxonomy and recovery policy behaviours defined in 9.1.2. Requires 9.1.2.
@@ -623,31 +622,29 @@ Wireframe's protocol, framing, and message assembly layers.
 
 ### 15.2. Protocol contract decisions
 
+Each decision below is analysed in the
+[formal verification guide](formal-verification-methods-in-wireframe.md); the
+cited section names the specific question it answers.
+
 - [ ] 15.2.1. Support a determined set of length-prefix widths (either `1`,
   `2`, `4`, and `8`, or the full `1..=8` range) and enforce them in
   constructors, conversions, and tests; record the decision in an ADR. Requires
-  15.1.1. See the
-  [formal verification guide](formal-verification-methods-in-wireframe.md)
-  §"What widths does Wireframe actually support for length prefixes?".
-  Success criteria: an ADR
-  records the decision, constructors enforce the chosen set, and existing tests
-  cover rejected widths.
+  15.1.1. See §"What widths does Wireframe actually support for length
+  prefixes?". Success criteria: an ADR records the decision, constructors
+  enforce the chosen set, and existing tests cover rejected widths.
 - [ ] 15.2.2. Treat `total_body_len` as either authoritative or advisory and
   enforce or rename it consistently across the message assembly path; record
   the decision in an ADR and add tests for both conforming and violating
-  inputs. Requires 15.1.1. See the
-  [formal verification guide](formal-verification-methods-in-wireframe.md)
-  §"Is `total_body_len` authoritative or advisory?". Success criteria: an ADR
-  records the decision, runtime code enforces the chosen semantics, and tests
-  verify both conforming and violating inputs.
+  inputs. Requires 15.1.1. See §"Is `total_body_len` authoritative or
+  advisory?". Success criteria: an ADR records the decision, runtime code
+  enforces the chosen semantics, and tests verify both conforming and violating
+  inputs.
 - [ ] 15.2.3. Publish named fairness and priority guarantees for
   `ConnectionActor` and encode them as model properties for Stateright checks.
-  Requires 15.1.1. See the
-  [formal verification guide](formal-verification-methods-in-wireframe.md)
-  §"What fairness guarantee does `ConnectionActor` actually make?".
-  Success criteria: the
-  design document enumerates each guarantee as a named property that can be
-  referenced by Stateright model checks.
+  Requires 15.1.1. See §"What fairness guarantee does `ConnectionActor`
+  actually make?". Success criteria: the design document enumerates each
+  guarantee as a named property that can be referenced by Stateright model
+  checks.
 
 ### 15.3. Kani bounded model checks
 
@@ -815,8 +812,8 @@ ecosystem.
 - [ ] 18.2.1. Implement a formal message versioning system to allow for
   protocol evolution.
 - [ ] 18.2.2. Ensure version negotiation can consume codec metadata without
-  leaking framing details into handlers (see
-  [message-versioning.md](message-versioning.md)).
+  leaking framing details into handlers (see the
+  [message versioning design](message-versioning.md)).
 
 ### 18.3. Security
 

From 76b840da9d6857af248dd494738955ba4136d503 Mon Sep 17 00:00:00 2001
From: leynos <leynos@troubledskies.net>
Date: Sun, 2 Aug 2026 21:18:51 +0200
Subject: [PATCH 3/5] Drop comma before restrictive "because" clause

Review feedback: in the mapsplice footnote-exception note the `because`
clause is restrictive (essential to the meaning), so it takes no preceding
comma. Remove the comma in both AGENTS.md and the documentation style guide.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 AGENTS.md                         | 2 +-
 docs/documentation-style-guide.md | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/AGENTS.md b/AGENTS.md
index c6d856b0..db6bb5a5 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -308,7 +308,7 @@ project:
 - Use GitHub-flavoured Markdown footnotes (`[^1]`) for references and
   footnotes.
   - Exception: roadmap-shaped Markdown edited with `mapsplice` (for example
-    `docs/roadmap.md`) must use inline links instead, because the `mapsplice`
+    `docs/roadmap.md`) must use inline links instead because the `mapsplice`
     roadmap grammar rejects footnote references (`unsupported inline node
     footnoteReference`). Cite references inline, either as a parenthetical
     `(see [target](path))` or by linking an existing phrase.
diff --git a/docs/documentation-style-guide.md b/docs/documentation-style-guide.md
index a6fc9a31..d67ab84a 100644
--- a/docs/documentation-style-guide.md
+++ b/docs/documentation-style-guide.md
@@ -64,7 +64,7 @@ consistent, and easy to maintain across projects.
 - Footnotes must be numbered in order of appearance in the document.
 - Exception: roadmap-shaped Markdown edited with `mapsplice` (for example
   `docs/roadmap.md`) must cite references with inline links instead of
-  footnotes, because the `mapsplice` roadmap grammar rejects footnote
+  footnotes because the `mapsplice` roadmap grammar rejects footnote
   references.
 - Caption every table, and caption every diagram.
 

From 8847ce64e9e5b07ae52d1bc516334f58cc212e4f Mon Sep 17 00:00:00 2001
From: leynos <leynos@troubledskies.net>
Date: Mon, 3 Aug 2026 01:05:39 +0200
Subject: [PATCH 4/5] Standardize formal-verification guide link text
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Review feedback: the roadmap still mixed clean labels (ADR numbers, design
names) with the raw filename `formal-verification-methods-in-wireframe.md`
used as visible link text across the §15 references, right beside the
`formal verification guide` label used in §15.2 for the same document.

Rename that visible text to the descriptive `formal verification guide`
(matching the §15.2 introduction and the ADR/design-name convention) so
link text reads consistently throughout the roadmap. The link targets
(URLs) and section anchors are unchanged.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 docs/roadmap.md | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/docs/roadmap.md b/docs/roadmap.md
index 429920b2..6b138a39 100644
--- a/docs/roadmap.md
+++ b/docs/roadmap.md
@@ -590,19 +590,19 @@ Wireframe's protocol, framing, and message assembly layers.
 
 - [x] 15.1.1. Convert the root manifest into a hybrid workspace while keeping
   the root package as the default member. See
-  [formal-verification-methods-in-wireframe.md §Root `Cargo.toml` changes](formal-verification-methods-in-wireframe.md#root-cargotoml-changes).
+  [formal verification guide §Root `Cargo.toml` changes](formal-verification-methods-in-wireframe.md#root-cargotoml-changes).
   Success criteria: `cargo build` and `cargo test --workspace` pass with the
   new layout.
 - [x] 15.1.2. Add `crates/wireframe-verification` as an internal crate for
   Stateright models and shared verification harnesses. Requires 15.1.1. See
-  [formal-verification-methods-in-wireframe.md §Why Stateright belongs in a separate verification crate](formal-verification-methods-in-wireframe.md#why-stateright-belongs-in-a-separate-verification-crate)
+  [formal verification guide §Why Stateright belongs in a separate verification crate](formal-verification-methods-in-wireframe.md#why-stateright-belongs-in-a-separate-verification-crate)
   and
   [§Suggested Stateright file layout](formal-verification-methods-in-wireframe.md#suggested-stateright-file-layout).
   Success criteria: the crate compiles, is included as a workspace member, and
   contains a placeholder Stateright model that passes `cargo test`.
 - [x] 15.1.3. Add pinned Kani and Verus tool metadata plus repo-local Makefile
   install and run entry points. See
-  [formal-verification-methods-in-wireframe.md §Recommended repository layout](formal-verification-methods-in-wireframe.md#recommended-repository-layout)
+  [formal verification guide §Recommended repository layout](formal-verification-methods-in-wireframe.md#recommended-repository-layout)
   and
   [§Verus should *not* live inside the main build](formal-verification-methods-in-wireframe.md#why-verus-should-not-live-inside-the-main-build).
   Success criteria: a contributor can run `make install-kani` and
@@ -611,12 +611,12 @@ Wireframe's protocol, framing, and message assembly layers.
 - [ ] 15.1.4. Add `make test-verification`, `make kani`, `make kani-full`,
   `make verus`, `make formal-pr`, and `make formal-nightly` Makefile targets.
   Requires 15.1.2 and 15.1.3. See
-  [formal-verification-methods-in-wireframe.md §Recommended Makefile changes](formal-verification-methods-in-wireframe.md#recommended-makefile-changes).
+  [formal verification guide §Recommended Makefile changes](formal-verification-methods-in-wireframe.md#recommended-makefile-changes).
   Success criteria: each target is accepted by `mbake validate Makefile` and
   returns exit 0 on a clean tree.
 - [ ] 15.1.5. Add separate CI jobs for Stateright, Kani smoke, and Verus
   proofs without changing the existing `build-test` coverage flow. See
-  [formal-verification-methods-in-wireframe.md §Recommended CI changes](formal-verification-methods-in-wireframe.md#recommended-ci-changes).
+  [formal verification guide §Recommended CI changes](formal-verification-methods-in-wireframe.md#recommended-ci-changes).
   Success criteria: CI pipelines pass on the default branch with the new jobs
   visible and green.
 
@@ -650,20 +650,20 @@ cited section names the specific question it answers.
 
 - [ ] 15.3.1. Add smoke harnesses for supported length-prefix round-trips and
   unsupported-width rejection in `src/frame/*`. See
-  [formal-verification-methods-in-wireframe.md §Phase 1 smoke harnesses](formal-verification-methods-in-wireframe.md#phase-1-smoke-harnesses).
+  [formal verification guide §Phase 1 smoke harnesses](formal-verification-methods-in-wireframe.md#phase-1-smoke-harnesses).
   Requires 15.1.3 and 15.2.1. Success criteria: `make kani` completes with all
   harnesses verified.
 - [ ] 15.3.2. Add harnesses for `FragmentSeries`, `Reassembler`, and
   `MessageSeries` covering duplicates, gaps, completion, and oversize cleanup.
   See
-  [formal-verification-methods-in-wireframe.md §Phase 1 smoke harnesses](formal-verification-methods-in-wireframe.md#phase-1-smoke-harnesses)
+  [formal verification guide §Phase 1 smoke harnesses](formal-verification-methods-in-wireframe.md#phase-1-smoke-harnesses)
   and
   [§Phase 2 full harnesses](formal-verification-methods-in-wireframe.md#phase-2-full-harnesses).
   Requires 15.1.3 and 15.2.2. Success criteria: `make kani-full` completes
   with all fragment and assembly harnesses verified.
 - [ ] 15.3.3. Extend existing Proptest coverage for fragment round-trips and
   mixed actor action traces where Kani bounds would be too small. See
-  [formal-verification-methods-in-wireframe.md §Second priority: `src/fragment/*`](formal-verification-methods-in-wireframe.md#second-priority-srcfragment)
+  [formal verification guide §Second priority: `src/fragment/*`](formal-verification-methods-in-wireframe.md#second-priority-srcfragment)
   and
   [§How Proptest and Loom fit after these changes](formal-verification-methods-in-wireframe.md#how-proptest-and-loom-fit-after-these-changes).
   Requires 15.3.1. Success criteria: `make test` includes the new Proptest
@@ -674,19 +674,19 @@ cited section names the specific question it answers.
 - [ ] 15.4.1. Model queue arrivals, active response and multi-packet outputs,
   shutdown races, fairness state, and terminal markers in
   `crates/wireframe-verification`. See
-  [formal-verification-methods-in-wireframe.md §Model scope](formal-verification-methods-in-wireframe.md#model-scope).
+  [formal verification guide §Model scope](formal-verification-methods-in-wireframe.md#model-scope).
   Requires 15.1.2 and 15.2.3. Success criteria: the model compiles and a
   bounded BFS run completes without panics or assertion failures.
 - [ ] 15.4.2. Add a shared checker harness that separates safety properties
   from reachability properties and reports both deterministically. See
-  [formal-verification-methods-in-wireframe.md §Properties to encode](formal-verification-methods-in-wireframe.md#properties-to-encode)
+  [formal verification guide §Properties to encode](formal-verification-methods-in-wireframe.md#properties-to-encode)
   and
   [§Shared checker harness](formal-verification-methods-in-wireframe.md#shared-checker-harness).
   Requires 15.4.1. Success criteria: `make test-verification` exercises the
   checker and reports property results.
 - [ ] 15.4.3. Gate a bounded breadth-first search (BFS) model run in pull
   request CI and a deeper run in scheduled or manual workflows. See
-  [formal-verification-methods-in-wireframe.md §Shared checker harness](formal-verification-methods-in-wireframe.md#shared-checker-harness)
+  [formal verification guide §Shared checker harness](formal-verification-methods-in-wireframe.md#shared-checker-harness)
   and
   [§Recommended CI changes](formal-verification-methods-in-wireframe.md#recommended-ci-changes).
   Requires 15.1.5 and 15.4.2. Success criteria: the PR CI job completes within
@@ -696,21 +696,21 @@ cited section names the specific question it answers.
 
 - [ ] 15.5.1. Enforce the chosen `total_body_len` contract in runtime code
   before relying on proofs. See
-  [formal-verification-methods-in-wireframe.md §"Is `total_body_len` authoritative or advisory?"](formal-verification-methods-in-wireframe.md#2-is-total_body_len-authoritative-or-advisory)
+  [formal verification guide §"Is `total_body_len` authoritative or advisory?"](formal-verification-methods-in-wireframe.md#2-is-total_body_len-authoritative-or-advisory)
   and
   [§"What Verus should prove in Wireframe"](formal-verification-methods-in-wireframe.md#what-verus-should-prove-in-wireframe).
   Requires 15.2.2. Success criteria: runtime assertions or checks enforce the
   contract, and existing tests confirm the enforcement.
 - [ ] 15.5.2. Add proof-only modules under `verus/` for declared-total and
   buffered-byte accounting invariants. See
-  [formal-verification-methods-in-wireframe.md §Proof style recommendation](formal-verification-methods-in-wireframe.md#proof-style-recommendation)
+  [formal verification guide §Proof style recommendation](formal-verification-methods-in-wireframe.md#proof-style-recommendation)
   and
   [§Representative proof tree](formal-verification-methods-in-wireframe.md#representative-proof-tree).
   Requires 15.1.3 and 15.5.1. Success criteria: `make verus` verifies all
   proof modules without errors.
 - [ ] 15.5.3. Document proof trigger discipline and contributor expectations
   for running `make verus`. See
-  [formal-verification-methods-in-wireframe.md §Trigger discipline](formal-verification-methods-in-wireframe.md#trigger-discipline)
+  [formal verification guide §Trigger discipline](formal-verification-methods-in-wireframe.md#trigger-discipline)
   and
   [§Recommended Makefile changes](formal-verification-methods-in-wireframe.md#recommended-makefile-changes).
   Requires 15.5.2. Success criteria: a contributor guide section explains

From 679cba1a1526550810ace5bdac052bf8dcf732d2 Mon Sep 17 00:00:00 2001
From: leynos <leynos@troubledskies.net>
Date: Tue, 18 Aug 2026 00:51:00 +0200
Subject: [PATCH 5/5] Document mapsplice roadmap editing for developers

Review feedback: this branch introduces the rule that roadmap references use
inline links rather than footnotes, but recorded it only in AGENTS.md and the
documentation style guide, leaving the developers' guide silent on it.

Add a concise "Roadmap editing with mapsplice" section covering the roadmap
grammar (phase, step, and task shapes), the footnote limitation that motivates
the inline-link rule, the link-text convention, and how to use a stdout preview
as a grammar check. Link to the documentation style guide for the underlying
style rule.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 docs/developers-guide.md | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/docs/developers-guide.md b/docs/developers-guide.md
index 25cdb7e7..602937a3 100644
--- a/docs/developers-guide.md
+++ b/docs/developers-guide.md
@@ -509,6 +509,35 @@ a fresh handle without explicitly calling the constructor.
 while holding the logger lock, `new()` recovers the guard via `into_inner()`
 and drains any buffered log records, so the next test starts from a clean state.
 
+## Roadmap editing with mapsplice
+
+[The combined roadmap](roadmap.md) is roadmap-shaped Markdown: `mapsplice`
+parses it to append, insert, delete, and replace numbered items, so it must
+stay within that tool's grammar. Phases are level-2 headings
+(`## 9. Phase title`), steps are level-3 headings (`### 9.2. Step title`), and
+tasks are numbered checklist items (`- [ ] 9.2.1. Task title`).
+
+That grammar rejects footnote references, failing with `unsupported inline
+node footnoteReference`. Roadmap references must therefore use inline links
+instead of the GitHub-flavoured `[^1]` footnotes used elsewhere in the
+documentation set: cite a target either as a parenthetical
+`(see [target](path))` or by linking an existing phrase. This is a scoped
+exception to the footnote rule recorded in the
+[documentation style guide](documentation-style-guide.md).
+
+Keep the visible link text consistent: cite ADRs by number (for example
+`ADR 0005`) and design documents by a short descriptive name, rather than by
+raw filename.
+
+`mapsplice` fails closed when the target does not match the supported grammar,
+so previewing an edit to stdout doubles as a grammar check:
+
+```bash
+MAPSPLICE_IN_PLACE=false mapsplice append docs/roadmap.md fragment.md >/dev/null
+```
+
+Run `make fmt` to reformat and rewrap after editing, then `make markdownlint`.
+
 ## Spelling policy
 
 The `make spelling` gate enforces en-GB-oxendict spelling across tracked text.