From 77b23150320806e517d98769a8720f43b5588858 Mon Sep 17 00:00:00 2001
From: leynos <leynos@troubledskies.net>
Date: Fri, 22 May 2026 21:07:13 +0200
Subject: [PATCH 1/6] Add Verus and Stateright boundary plan

Draft the approval-gated ExecPlan for roadmap item `4.1.3` so the
implementation can record Verus as optional and proof-kernel-only while
keeping Stateright deferred until Netsuke has stateful concurrent behaviour.

Capture the expected documentation scope, validation gates, OrthoConfig
boundary guardrails, Wyvern reconnaissance, and CodeRabbit rate-limit status.
---
 ...scope-boundary-for-verus-and-stateright.md | 384 ++++++++++++++++++
 1 file changed, 384 insertions(+)
 create mode 100644 docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md

diff --git a/docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md b/docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md
new file mode 100644
index 00000000..eddb17ff
--- /dev/null
+++ b/docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md
@@ -0,0 +1,384 @@
+# 4.1.3. Record the phase-1 Verus and Stateright boundary
+
+This ExecPlan (execution plan) is a living document. The sections
+`Constraints`, `Tolerances`, `Risks`, `Progress`, `Surprises & Discoveries`,
+`Decision Log`, and `Outcomes & Retrospective` must be kept up to date as work
+proceeds.
+
+Status: DRAFT
+
+## Purpose / big picture
+
+Roadmap item `4.1.3` records the phase-1 boundary for formal-verification tools
+that Netsuke is deliberately not using as mandatory gates yet. After this work
+is implemented, contributors will have one clear policy: Verus is optional and
+reserved for a small proof kernel, while Stateright remains deferred until
+Netsuke has a stateful concurrent subsystem worth model checking.
+
+This matters because Phase 4 is adding stronger checks around Netsuke's
+semantic core without turning every proof tool into a permanent workflow cost.
+The observable result is documentation, not runtime behaviour. A reviewer
+should be able to read `docs/formal-verification-methods-in-netsuke.md`,
+`docs/developers-guide.md`, and `docs/roadmap.md` and see that Kani remains the
+supported phase-1 formal-verification gate, Verus has a narrow optional entry
+point, and Stateright has explicit re-entry criteria.
+
+This plan is approval-gated. It must be reviewed and explicitly approved before
+implementation begins.
+
+## Constraints
+
+- Do not implement this plan until the user explicitly approves it.
+- Keep this work documentation-first. Do not add Verus proofs, Verus install
+  scripts, Stateright models, Stateright dependencies, new Rust modules, new
+  command-line interface (CLI) flags, new configuration fields, new locale
+  keys, or new Continuous Integration (CI) jobs unless the user explicitly
+  expands the scope.
+- Preserve the existing Kani phase-1 contract from roadmap items `4.1.1` and
+  `4.1.2`: `make kani`, `make kani-full`, `make formal-pr`,
+  `tools/kani/VERSION`, `scripts/install-kani.sh`, and the `kani-smoke` CI job
+  remain the supported formal-verification tooling and gating surface.
+- Do not add Verus or Stateright to `make test`, `make lint`,
+  `make check-fmt`, `make all`, `make kani`, `make kani-full`,
+  `make formal-pr`, or CI in this task.
+- Keep Stateright out of scope until Netsuke has an accepted design for a
+  stateful concurrent subsystem such as a daemon, watch service,
+  remote-execution coordinator, actor protocol, or internal scheduler with
+  long-lived mutable control-plane state.
+- Keep Verus out of production Cargo. If future work introduces a proof, it
+  must remain outside the ordinary Cargo build and focus first on a small
+  proof model for `src/ir/cycle.rs` cycle canonicalization.
+- Use `docs/formal-verification-methods-in-netsuke.md` as the design document
+  for this decision. Create an Architecture Decision Record (ADR) only if
+  implementation uncovers a new substantive decision beyond the existing
+  roadmap policy.
+- Update `docs/users-guide.md` only if implementation changes user-facing
+  behaviour. The expected implementation does not change the tool's user
+  interface, so the users' guide should probably remain unchanged.
+- If implementation unexpectedly adds a CLI, configuration, or help surface,
+  use the existing OrthoConfig and localization pipeline: derive configuration
+  from `src/cli/mod.rs` and `src/cli/config.rs`, merge layers in
+  `src/cli/config_merge.rs`, and add localized help in
+  `locales/en-US/messages.ftl`, `locales/es-ES/messages.ftl`, and
+  `src/localization/keys.rs`.
+- Use hexagonal architecture as a boundary check, not as a transplant. Keep
+  verification policy in documentation and, if future code appears, keep pure
+  domain or proof policy separate from adapters, process orchestration and
+  tool-installation concerns.
+- Documentation prose must follow `docs/documentation-style-guide.md` and use
+  en-GB-oxendict spelling and grammar.
+- Run long validation commands sequentially and capture output with `tee`
+  under `/tmp`. Do not run format checks, lints, or tests in parallel.
+- Use `coderabbit review --agent` after each major milestone and clear all
+  concerns before moving to the next milestone.
+- Commit only after gates pass. Use the file-based commit-message workflow
+  with `git commit -F`, not `git commit -m`.
+
+## Tolerances (exception triggers)
+
+- Scope: if implementation requires more than 4 changed files beyond this
+  ExecPlan, stop and escalate. The expected implementation files are
+  `docs/formal-verification-methods-in-netsuke.md`,
+  `docs/developers-guide.md`, and `docs/roadmap.md`.
+- Code: if any Rust production file, test file, Cargo manifest, Makefile, CI
+  workflow, script, locale file, or OrthoConfig surface must change, stop and
+  get explicit approval before continuing.
+- Interface: if a public CLI flag, configuration key, environment variable,
+  structured output field, public Rust API, Make target, or CI job is needed,
+  stop and present options.
+- Dependencies: if a new dependency on `verus`, Stateright, Proptest, Kani,
+  or any other crate is needed for this item, stop and escalate.
+- Proof surface: if recording the boundary appears to require a real Verus
+  proof or Stateright model, stop and split that into a later roadmap item.
+- Documentation decision: if the boundary no longer fits naturally in
+  `docs/formal-verification-methods-in-netsuke.md` and requires an ADR, stop
+  and explain the new decision before creating the ADR.
+- Validation: if `make check-fmt`, `make lint`, or `make test` still fails
+  after two focused fix attempts, stop and escalate with log locations.
+- Review: if `coderabbit review --agent` raises unresolved correctness,
+  scope, or documentation concerns, do not proceed until they are addressed or
+  explicitly waived.
+- Ambiguity: if "stateful concurrent subsystem" could reasonably include a
+  non-concurrent batch workflow, ask for direction before weakening the
+  Stateright deferral rule.
+
+## Risks
+
+- Risk: The existing formal-verification design document already states most
+  of the intended policy, so the implementation could become redundant prose.
+  Severity: medium. Likelihood: high. Mitigation: make the change about
+  phase-1 boundary traceability, re-entry criteria, and developer workflow
+  expectations rather than repeating the executive summary.
+
+- Risk: The planned Verus layout in
+  `docs/formal-verification-methods-in-netsuke.md` mentions future
+  `scripts/install-verus.sh`, `scripts/run-verus.sh`, and `tools/verus/`
+  paths, which could be misread as immediate implementation work. Severity:
+  medium. Likelihood: medium. Mitigation: clarify that phase 1 records the
+  optional proof-kernel boundary and does not create those paths.
+
+- Risk: "Proof kernel" can sound like a new production component. Severity:
+  medium. Likelihood: medium. Mitigation: define it plainly as a small
+  proof-specific model of one mathematical contract, kept outside production
+  Cargo and outside normal user workflows.
+
+- Risk: Stateright is valuable for concurrent protocols, but Netsuke currently
+  emits a static Ninja graph and delegates execution to Ninja. Severity:
+  medium. Likelihood: low. Mitigation: document concrete re-entry triggers so
+  the deferral is revisitable rather than permanent.
+
+- Risk: Over-applying hexagonal architecture could lead to unnecessary module
+  reshaping during a documentation task. Severity: low. Likelihood: medium.
+  Mitigation: use the dependency rule as a review lens only; do not restructure
+  the codebase for this item.
+
+- Risk: Full validation is expensive for a documentation-only change, but the
+  repository instructions require the normal gates before committing. Severity:
+  low. Likelihood: high. Mitigation: run `make check-fmt`, `make lint`, and
+  `make test` sequentially with logs, and add `make markdownlint` and
+  `make nixie` because Markdown changes are expected.
+
+## Progress
+
+- [x] 2026-05-22T19:01:43Z: Loaded the `leta`, `rust-router`,
+      `hexagonal-architecture`, `execplans`, `firecrawl-mcp`,
+      `commit-message`, `pr-creation`, and `en-gb-oxendict-style` skills
+      relevant to this planning task.
+- [x] 2026-05-22T19:01:43Z: Created a `leta` workspace for the repository.
+- [x] 2026-05-22T19:01:43Z: Renamed the branch to
+      `4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright`.
+- [x] 2026-05-22T19:01:43Z: Reviewed `AGENTS.md`, `Makefile`,
+      `docs/roadmap.md`, `docs/formal-verification-methods-in-netsuke.md`,
+      `docs/developers-guide.md`, `docs/users-guide.md`,
+      `docs/ortho-config-users-guide.md`, and the previous `4.1.1` and
+      `4.1.2` ExecPlans.
+- [x] 2026-05-22T19:01:43Z: Used two Wyvern agents for documentation
+      reconnaissance and configuration/test-stack reconnaissance.
+- [x] 2026-05-22T19:01:43Z: Used Firecrawl to check current Verus and
+      Stateright prior-art sources for the boundary rationale.
+- [x] 2026-05-22T19:01:43Z: Drafted this approval-gated ExecPlan.
+- [x] 2026-05-22T19:01:43Z: Ran `make check-fmt`, `make lint`,
+      `make test`, `make markdownlint`, and `make nixie`; all passed for the
+      draft ExecPlan.
+- [x] 2026-05-22T19:01:43Z: Attempted `coderabbit review --agent` three
+      times; all attempts returned a recoverable account rate-limit response
+      before producing review findings.
+- [ ] Stage A: review the draft plan with the user and obtain explicit
+      approval before implementing roadmap item `4.1.3`.
+- [ ] Stage B: update the formal-verification design document with the
+      phase-1 boundary, Verus proof-kernel definition, and Stateright re-entry
+      criteria.
+- [ ] Stage C: update the developers' guide with the phase-1 support matrix:
+      Kani supported and gated, Verus optional and not installed by default,
+      Stateright deferred.
+- [ ] Stage D: run CodeRabbit review, quality gates, and documentation gates.
+- [ ] Stage E: mark roadmap item `4.1.3` and its subitems done only after the
+      approved implementation lands and passes validation.
+- [ ] Stage F: commit, push, and update the pull request for the implemented
+      feature.
+
+## Surprises & Discoveries
+
+- `docs/formal-verification-methods-in-netsuke.md` already states that Verus
+  should remain optional and limited to small proof kernels after Kani and
+  Proptest stabilize, and that Stateright should remain out of scope until
+  Netsuke gains long-lived mutable state, actor-style coordination, or a more
+  complex scheduler than the current Ninja hand-off.
+- `docs/roadmap.md` task `4.4.3` depends on `4.1.3`, so this boundary is a
+  prerequisite for any later evaluation of a minimal Verus proof kernel.
+- The current `Makefile` already exposes `make kani`, `make kani-full`, and
+  `make formal-pr`. There are no Verus or Stateright Make targets today, which
+  supports keeping this task documentation-only.
+- `Cargo.toml` includes `rstest`, `rstest-bdd`, and `rstest-bdd-macros`, but
+  no direct `proptest`, `verus`, or Stateright dependencies at the time this
+  plan was drafted.
+- OrthoConfig is already the active layered configuration mechanism for
+  Netsuke. It should be mentioned as a guardrail only if this task unexpectedly
+  grows a configuration or localized help surface.
+- Firecrawl found the official Verus guide, which describes Verus as using
+  specification, proof, and executable modes, reinforcing that a future Verus
+  boundary should be proof-specific rather than a general runtime feature.
+- Firecrawl found official Stateright documentation and repository material
+  describing it as a Rust model checker and actor library for systems such as
+  actors executing a distributed protocol, reinforcing the deferral until
+  Netsuke has comparable stateful concurrency.
+- `coderabbit review --agent` was available locally but blocked by an
+  account-level rate limit during all three draft validation attempts. No
+  CodeRabbit findings were produced to clear.
+
+## Decision Log
+
+- Decision: Keep this ExecPlan pre-implementation and approval-gated.
+  Rationale: The user explicitly stated that the plan must be approved before
+  implementation. Date/Author: 2026-05-22 / planning agent.
+
+- Decision: Treat the expected implementation as documentation-only.
+  Rationale: Roadmap item `4.1.3` asks to record the scope boundary, not to add
+  toolchain support, executable proof code, runtime behaviour, or CLI surface.
+  Date/Author: 2026-05-22 / planning agent.
+
+- Decision: Record the boundary primarily in
+  `docs/formal-verification-methods-in-netsuke.md`, with developer workflow
+  implications in `docs/developers-guide.md`.
+  Rationale: The formal-verification document is the design source for Phase 4,
+  while the developers' guide already explains the Kani toolchain and local
+  gate policy. Date/Author: 2026-05-22 / planning agent.
+
+- Decision: Do not plan new unit, behavioural, property, Kani, Verus, or
+  Stateright tests for the expected implementation.
+  Rationale: A documentation-only boundary record has no runtime behaviour,
+  externally observable workflow, invariant over program state, or proof
+  obligation. If implementation changes CLI/configuration/code, this decision
+  is invalid and the plan must be revised before proceeding.
+  Date/Author: 2026-05-22 / planning agent.
+
+## Implementation plan
+
+Start from a clean understanding of the branch. Run:
+
+```sh
+git status --short --branch
+git branch --show-current
+```
+
+The branch should be
+`4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright`. If it is not,
+rename it before continuing. Confirm that the working tree contains only
+expected plan changes or user-authored changes that must be preserved.
+
+Next, update `docs/formal-verification-methods-in-netsuke.md`. Keep the
+current conclusion intact, but make the phase-1 boundary explicit. The
+implementation should define "proof kernel" in plain language as a small,
+proof-specific model for one mathematical contract, not a production subsystem.
+It should say that any first Verus work is limited to a cycle canonicalization
+model related to `src/ir/cycle.rs`, kept outside ordinary Cargo and CI until a
+later approved task makes it stable. It should also clarify that phase 1 does
+not create Verus installer scripts, Verus Make targets, or Verus CI.
+
+In the same file, strengthen the Stateright deferral section. The text should
+say that Stateright is deferred because Netsuke currently compiles manifests
+into a static Ninja build graph and delegates execution to Ninja. The re-entry
+criteria should be concrete: reconsider Stateright only after an accepted
+design introduces a stateful concurrent subsystem such as a daemon, watch
+service, remote-execution coordinator, actor protocol, or internal scheduler
+with long-lived mutable control-plane state.
+
+Then update `docs/developers-guide.md` under `## Formal-verification tooling`.
+Add a short phase-1 support matrix in prose or compact bullets. It should state
+that Kani is supported and gated today, Verus is optional and not installed or
+run by default, and Stateright is deferred with no dependency, model, or CI
+surface. Do not duplicate long design rationale here; link back to
+`docs/formal-verification-methods-in-netsuke.md`.
+
+After the documentation changes, review whether `docs/users-guide.md` needs
+changes. It should remain unchanged unless the implementation unexpectedly
+changes a user-facing workflow. Review whether an ADR is needed. It should not
+be needed if the implementation only records the roadmap boundary already
+present in the formal-verification design.
+
+Run CodeRabbit after this documentation milestone:
+
+```sh
+coderabbit review --agent 2>&1 | tee /tmp/coderabbit-netsuke-4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.out
+```
+
+Address every actionable finding before proceeding. If CodeRabbit reports no
+findings, record that in this plan's `Progress` section.
+
+Run formatting and validation sequentially:
+
+```sh
+make check-fmt 2>&1 | tee /tmp/check-fmt-netsuke-4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.out
+make lint 2>&1 | tee /tmp/lint-netsuke-4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.out
+make test 2>&1 | tee /tmp/test-netsuke-4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.out
+make markdownlint 2>&1 | tee /tmp/markdownlint-netsuke-4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.out
+make nixie 2>&1 | tee /tmp/nixie-netsuke-4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.out
+```
+
+The expected result is that all five commands exit successfully. If
+`make check-fmt` fails only because Markdown needs wrapping, run `make fmt`,
+inspect the diff carefully, preserve unrelated user changes, and rerun the
+checks. Do not run these gates in parallel.
+
+Once the implementation has passed CodeRabbit and the gates, update
+`docs/roadmap.md` to mark `4.1.3` and its two subitems done. Do this only at
+the end of the approved implementation, not while this ExecPlan is still only a
+draft. Update this plan's `Progress`, `Surprises & Discoveries`,
+`Decision Log`, and `Outcomes & Retrospective` sections with the validation
+evidence.
+
+Commit with a file-based message:
+
+```sh
+git status --short
+git add docs/formal-verification-methods-in-netsuke.md docs/developers-guide.md docs/roadmap.md docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md
+COMMIT_MSG_DIR=$(mktemp -d)
+cat > "$COMMIT_MSG_DIR/COMMIT_MSG.md" << 'ENDOFMSG'
+Record Verus and Stateright phase-1 boundary
+
+Document the phase-1 formal-verification scope so Kani remains the supported
+gate, Verus stays optional and proof-kernel-only, and Stateright remains
+deferred until Netsuke has stateful concurrent behaviour to model.
+ENDOFMSG
+git commit -F "$COMMIT_MSG_DIR/COMMIT_MSG.md"
+rm -rf "$COMMIT_MSG_DIR"
+```
+
+Push the branch and create or update a draft pull request. The pull request
+title must include `(4.1.3)`, and the summary must mention this ExecPlan:
+`docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md`.
+Include a `## References` section at the end of the pull request body with the
+Lody session link from:
+
+```sh
+echo ${LODY_SESSION_ID}
+```
+
+## Validation strategy
+
+This task's expected implementation changes documentation only. Unit tests with
+`rstest`, behavioural tests with `rstest-bdd`, property tests with Proptest,
+Kani harnesses, Verus proofs, and Stateright models are not applicable unless
+the approved implementation changes code, configuration, CLI behaviour,
+localized help, runtime workflows, or semantic contracts beyond documentation.
+
+The validation evidence for the expected implementation is:
+
+- `coderabbit review --agent` reports no unresolved findings.
+- `make check-fmt` passes.
+- `make lint` passes.
+- `make test` passes.
+- `make markdownlint` passes.
+- `make nixie` passes.
+- `git diff` shows no changes outside the expected documentation files.
+
+## Signposts for implementers
+
+- Use the `leta` skill and workspace for code navigation if implementation
+  unexpectedly touches Rust code.
+- Use the `rust-router` skill before routing any Rust change to a narrower
+  Rust skill.
+- Use the `hexagonal-architecture` skill only as a boundary check: domain and
+  policy remain separated from adapters and tool orchestration.
+- Use the `execplans` skill whenever this plan is revised during
+  implementation.
+- Use the `commit-message` skill for file-based commit messages.
+- Use the `pr-creation` skill for the draft pull request title and body.
+- Use the `en-gb-oxendict-style` skill for documentation prose.
+- Use `docs/roadmap.md` for roadmap acceptance criteria.
+- Use `docs/formal-verification-methods-in-netsuke.md` as the design source
+  for Kani, Proptest, Verus and Stateright scope.
+- Use `docs/developers-guide.md` for contributor-facing workflow details.
+- Use `docs/ortho-config-users-guide.md` and existing `src/cli/*`
+  OrthoConfig code only if the scope unexpectedly grows a configuration or
+  localized CLI help surface.
+- Use `docs/rust-testing-with-rstest-fixtures.md`,
+  `docs/rstest-bdd-users-guide.md`,
+  `docs/rust-doctest-dry-guide.md`, and
+  `docs/reliable-testing-in-rust-via-dependency-injection.md` only if code
+  changes make tests applicable.
+
+## Outcomes & Retrospective
+
+No implementation work has been performed yet. This section must be completed
+after the approved implementation lands and validation passes.

From f4593cbaf2ed25c26c66e7a55a95477042f3a2f0 Mon Sep 17 00:00:00 2001
From: leynos <leynos@troubledskies.net>
Date: Sun, 24 May 2026 18:00:15 +0200
Subject: [PATCH 2/6] Record Verus and Stateright phase-1 boundary

Document the phase-1 formal-verification scope so Kani remains
the supported gate, Verus stays optional and proof-kernel-only,
and Stateright remains deferred until Netsuke has stateful
concurrent behaviour to model.
---
 docs/developers-guide.md                      | 11 +++
 ...scope-boundary-for-verus-and-stateright.md | 93 +++++++++++++++++--
 .../formal-verification-methods-in-netsuke.md | 33 +++++--
 docs/roadmap.md                               |  8 +-
 4 files changed, 124 insertions(+), 21 deletions(-)

diff --git a/docs/developers-guide.md b/docs/developers-guide.md
index 8d5e873a..d275e5a2 100644
--- a/docs/developers-guide.md
+++ b/docs/developers-guide.md
@@ -106,6 +106,17 @@ Use the Make targets for day-to-day formal-verification checks:
 Kani is intentionally not part of `make test`, `make lint`, `make check-fmt`,
 or `make all`.
 
+Phase 1 keeps the rest of the formal-verification surface deliberately narrow.
+Kani is the only supported and gated formal-verification tool today. Verus is
+optional, proof-kernel-only, and not installed or run by default; any first
+Verus work must stay outside ordinary Cargo and focus on a small cycle
+canonicalization model. Stateright is deferred entirely until Netsuke gains an
+accepted stateful concurrent subsystem such as a daemon, watch service,
+remote-execution coordinator, actor protocol, or internal scheduler with
+long-lived mutable control-plane state. See
+[`docs/formal-verification-methods-in-netsuke.md`](formal-verification-methods-in-netsuke.md)
+for the design rationale and re-entry criteria.
+
 Pull requests run a dedicated `kani-smoke` CI job alongside the ordinary
 `build-test` job. The job installs the pinned Kani version with
 `scripts/install-kani.sh` and runs only `make kani`; it does not run
diff --git a/docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md b/docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md
index eddb17ff..c90e0001 100644
--- a/docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md
+++ b/docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md
@@ -5,7 +5,7 @@ This ExecPlan (execution plan) is a living document. The sections
 `Decision Log`, and `Outcomes & Retrospective` must be kept up to date as work
 proceeds.
 
-Status: DRAFT
+Status: COMPLETE
 
 ## Purpose / big picture
 
@@ -163,18 +163,43 @@ implementation begins.
 - [x] 2026-05-22T19:01:43Z: Attempted `coderabbit review --agent` three
       times; all attempts returned a recoverable account rate-limit response
       before producing review findings.
-- [ ] Stage A: review the draft plan with the user and obtain explicit
+- [x] 2026-05-24T15:43:39Z: The user explicitly approved proceeding with
+      implementation from this ExecPlan.
+- [x] 2026-05-24T15:43:39Z: Confirmed the branch is
+      `4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright` and the
+      working tree is clean before implementation.
+- [x] Stage A: review the draft plan with the user and obtain explicit
       approval before implementing roadmap item `4.1.3`.
-- [ ] Stage B: update the formal-verification design document with the
+- [x] 2026-05-24T15:43:39Z: Updated
+      `docs/formal-verification-methods-in-netsuke.md` to define the Verus
+      proof-kernel boundary, exclude Verus from phase-1 build and CI surfaces,
+      and record concrete Stateright re-entry criteria.
+- [x] 2026-05-24T15:43:39Z: Updated `docs/developers-guide.md` with the
+      phase-1 support boundary: Kani supported and gated, Verus optional and
+      not installed by default, and Stateright deferred.
+- [x] Stage B: update the formal-verification design document with the
       phase-1 boundary, Verus proof-kernel definition, and Stateright re-entry
       criteria.
-- [ ] Stage C: update the developers' guide with the phase-1 support matrix:
+- [x] Stage C: update the developers' guide with the phase-1 support matrix:
       Kani supported and gated, Verus optional and not installed by default,
       Stateright deferred.
-- [ ] Stage D: run CodeRabbit review, quality gates, and documentation gates.
-- [ ] Stage E: mark roadmap item `4.1.3` and its subitems done only after the
+- [x] 2026-05-24T15:43:39Z: Ran `make check-fmt`, `make lint`,
+      `make test`, `make markdownlint`, and `make nixie`; all passed before
+      requesting CodeRabbit review.
+- [x] 2026-05-24T15:43:39Z: Ran `coderabbit review --agent`; it completed with
+      zero findings.
+- [x] 2026-05-24T15:43:39Z: Marked `docs/roadmap.md` item `4.1.3` and its two
+      subitems done after documentation and review passed.
+- [x] 2026-05-24T15:59:07Z: Reran the full validation set after the roadmap
+      and ExecPlan updates; all checks passed.
+- [x] 2026-05-24T15:59:07Z: Reran `coderabbit review --agent` on the final
+      documentation diff; it completed with zero findings.
+- [x] Stage D: run CodeRabbit review, quality gates, and documentation gates.
+- [x] Stage E: mark roadmap item `4.1.3` and its subitems done only after the
       approved implementation lands and passes validation.
-- [ ] Stage F: commit, push, and update the pull request for the implemented
+- [x] 2026-05-24T16:00:33Z: Committed and pushed the implementation branch for
+      review.
+- [x] Stage F: commit, push, and update the pull request for the implemented
       feature.
 
 ## Surprises & Discoveries
@@ -205,6 +230,18 @@ implementation begins.
 - `coderabbit review --agent` was available locally but blocked by an
   account-level rate limit during all three draft validation attempts. No
   CodeRabbit findings were produced to clear.
+- Implementation approval arrived on 2026-05-24, so the approval gate is
+  satisfied and the roadmap item can now be implemented within the documented
+  tolerances.
+- The documentation changes stayed inside the expected scope. No user-facing
+  CLI behaviour changed, so `docs/users-guide.md` does not need an update. No
+  new architecture decision beyond the existing roadmap policy was introduced,
+  so no Architecture Decision Record (ADR) is needed.
+- `make fmt` runs `mdformat-all`, which attempted to rewrite many unrelated
+  Markdown files and then failed on pre-existing line-length findings outside
+  this task. The formatter churn was restored because the working tree was
+  clean before the command and those changes exceeded this plan's scope. The
+  required checking gates, including `make markdownlint`, passed afterwards.
 
 ## Decision Log
 
@@ -232,6 +269,24 @@ implementation begins.
   is invalid and the plan must be revised before proceeding.
   Date/Author: 2026-05-22 / planning agent.
 
+- Decision: Proceed with a documentation-only implementation after approval.
+  Rationale: The user approved implementation of this ExecPlan, and the
+  pre-change review found no need to change code, configuration, CI, locale
+  files, OrthoConfig surfaces, or tool dependencies.
+  Date/Author: 2026-05-24 / implementing agent.
+
+- Decision: Leave `docs/users-guide.md` unchanged.
+  Rationale: This implementation records contributor-facing tool boundaries and
+  does not change command-line behaviour, configuration, output, persistence,
+  or any other user-visible workflow.
+  Date/Author: 2026-05-24 / implementing agent.
+
+- Decision: Do not create an ADR for this item.
+  Rationale: The implementation records the phase-1 boundary already requested
+  by the roadmap and design document. It does not introduce a new substantive
+  architecture decision.
+  Date/Author: 2026-05-24 / implementing agent.
+
 ## Implementation plan
 
 Start from a clean understanding of the branch. Run:
@@ -380,5 +435,25 @@ The validation evidence for the expected implementation is:
 
 ## Outcomes & Retrospective
 
-No implementation work has been performed yet. This section must be completed
-after the approved implementation lands and validation passes.
+The approved documentation-only implementation is complete. The formal
+verification design now states that Verus is optional in phase 1,
+proof-kernel-only, outside ordinary Cargo, and outside the normal Make and CI
+gates. It defines the proof kernel as a small proof-specific model and keeps
+the only current Verus entry point to a possible future
+`src/ir/cycle.rs` cycle canonicalization proof.
+
+The Stateright section now records the phase-1 deferral explicitly. Netsuke
+currently compiles manifests into a static Ninja file and delegates execution
+to Ninja, so Stateright remains out of the dependency, model, Make, and CI
+surface until an accepted design introduces a stateful concurrent subsystem.
+
+The developers' guide now gives contributors the same support boundary in
+workflow terms: Kani is supported and gated today, Verus is optional and not
+installed by default, and Stateright is deferred. The users' guide remains
+unchanged because no user-facing behaviour changed, and no ADR was created
+because no new architecture decision was introduced beyond recording the
+roadmap boundary.
+
+Validation passed before the final review with `make check-fmt`, `make lint`,
+`make test`, `make markdownlint`, and `make nixie`. CodeRabbit was run twice
+during implementation and returned zero findings both times.
diff --git a/docs/formal-verification-methods-in-netsuke.md b/docs/formal-verification-methods-in-netsuke.md
index 100a975a..e9de451c 100644
--- a/docs/formal-verification-methods-in-netsuke.md
+++ b/docs/formal-verification-methods-in-netsuke.md
@@ -106,9 +106,17 @@ should lock down these invariants:
 
 ### Optional Verus proof kernel
 
+Verus is optional in phase 1 and remains proof-kernel-only. A proof kernel is
+a small proof-specific model for one mathematical contract; it is not a
+production subsystem, a replacement implementation, or a normal developer
+workflow gate. Netsuke should not add Verus installer scripts, Verus Make
+targets, Verus Continuous Integration (CI), or Verus files under ordinary Cargo
+as part of the phase-1 boundary.
+
 Verus is not the correct first tool for the manifest or command-interpolation
-layers. The code that is most suitable for a later proof is
-`canonicalize_cycle`, because the function exposes a clear mathematical
+layers. The only current entry point worth preserving for later evaluation is a
+cycle canonicalization model related to `src/ir/cycle.rs`. That model is
+appropriate because `canonicalize_cycle` exposes a clear mathematical
 contract:
 
 - output length is preserved,
@@ -116,9 +124,13 @@ contract:
 - the interior node multiset is preserved, and
 - the chosen start node is stable under the repository's ordering rule.[^7]
 
-If Verus is introduced, it should prove only that narrow normalization model at
-first. Production `HashMap` structures, MiniJinja values, filesystem helpers,
-and subprocess orchestration should remain outside the first proof boundary.
+If Verus is introduced by a later approved roadmap item, it should prove only
+that narrow normalization model at first. Production `HashMap` structures,
+MiniJinja values, filesystem helpers, and subprocess orchestration should
+remain outside the first proof boundary. Until the proof kernel is stable and
+reviewed, Verus should remain outside pull-request gates, `make test`,
+`make lint`, `make check-fmt`, `make all`, `make kani`, `make kani-full`, and
+`make formal-pr`.
 
 ### Stateright remains deferred
 
@@ -127,9 +139,14 @@ and orchestrator that emits a static Ninja file and delegates execution to the
 Ninja subprocess.[^4][^10] There is no actor protocol, distributed state
 machine, or internal concurrent scheduler to model check today.
 
-Reconsidering Stateright would make sense only after a future daemon mode,
-watch service, remote-execution coordinator, or another long-lived concurrent
-subsystem exists.
+Stateright is therefore deferred for phase 1. The project should not add a
+Stateright dependency, model directory, Make target, CI job, or documentation
+that implies Stateright is part of the active verification workflow.
+Reconsidering Stateright would make sense only after an accepted design
+introduces a stateful concurrent subsystem: for example a daemon mode, watch
+service, remote-execution coordinator, actor protocol, or internal scheduler
+with long-lived mutable control-plane state. Batch-oriented manifest
+compilation and static Ninja emission are not enough to reopen that decision.
 
 ## Repository integration plan
 
diff --git a/docs/roadmap.md b/docs/roadmap.md
index 989519f8..e8f2469a 100644
--- a/docs/roadmap.md
+++ b/docs/roadmap.md
@@ -330,12 +330,12 @@ and test workflow intact. See
   - [x] Keep the existing `build-test` job unchanged.
   - [x] Run only the bounded smoke harness set on pull requests.
   - [x] Cache Kani tool downloads separately from ordinary Cargo artefacts.
-- [ ] 4.1.3. Record the phase-1 scope boundary for Verus and Stateright. See
+- [x] 4.1.3. Record the phase-1 scope boundary for Verus and Stateright. See
   [formal-verification-methods-in-netsuke.md §Optional Verus proof kernel](formal-verification-methods-in-netsuke.md#optional-verus-proof-kernel)
-   and
+  and
   [formal-verification-methods-in-netsuke.md §Stateright remains deferred](formal-verification-methods-in-netsuke.md#stateright-remains-deferred).
-  - [ ] Document Verus as optional and proof-kernel-only.
-  - [ ] Document Stateright as deferred until Netsuke gains a stateful
+  - [x] Document Verus as optional and proof-kernel-only.
+  - [x] Document Stateright as deferred until Netsuke gains a stateful
     concurrent subsystem.
 
 ### 4.2. Intermediate representation verification

From 2eff8cc6659ef7af8102e380b9bea57534c3e857 Mon Sep 17 00:00:00 2001
From: leynos <leynos@troubledskies.net>
Date: Mon, 25 May 2026 21:07:40 +0200
Subject: [PATCH 3/6] Use rust-prover-tools for prover workflows

Replace repository-local Kani shell scripts with the shared
`rust-prover-tools` CLI pinned in the Makefile.

Route Kani installation and version checks through `uv tool run`, add
optional Verus install/run Make targets, and update the `kani-smoke`
job to install `uv` before running `make install-kani`.
Update the formal-verification docs and roadmap so contributor guidance
points at the shared prover tooling instead of local scripts.
---
 .github/workflows/ci.yml                      |  8 +++-
 Makefile                                      | 20 ++++++++--
 docs/developers-guide.md                      | 29 ++++++++------
 .../formal-verification-methods-in-netsuke.md | 17 ++++++---
 docs/roadmap.md                               |  2 +-
 scripts/check-kani-version.sh                 | 38 -------------------
 scripts/install-kani.sh                       | 38 -------------------
 7 files changed, 53 insertions(+), 99 deletions(-)
 delete mode 100755 scripts/check-kani-version.sh
 delete mode 100755 scripts/install-kani.sh

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 837cb775..a4cd788b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -80,14 +80,18 @@ jobs:
         uses: leynos/shared-actions/.github/actions/setup-rust@e4c6b0e200a057edf927c45c298e7ddf229b3934
         with:
           toolchain: stable
+      - name: Install uv
+        uses: astral-sh/setup-uv@4cda7d73322c50eac316ad623a716f09a2db2ac7  # v3.1.2
+        with:
+          enable-cache: true
       - name: Cache Kani tools
         uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830  # v4.3.0
         with:
           path: |
             .kani-cargo
             .kani-home
-          key: ${{ runner.os }}-kani-${{ hashFiles('tools/kani/VERSION', 'scripts/install-kani.sh') }}
+          key: ${{ runner.os }}-kani-${{ hashFiles('tools/kani/VERSION', 'Makefile') }}
       - name: Install Kani
-        run: scripts/install-kani.sh
+        run: make install-kani
       - name: Kani smoke
         run: make kani
diff --git a/Makefile b/Makefile
index c10a9ab0..cddaefc3 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-.PHONY: help all clean test build release lint fmt check-fmt typecheck markdownlint nixie kani kani-full formal-pr
+.PHONY: help all clean test build release lint fmt check-fmt typecheck markdownlint nixie install-kani kani kani-full install-verus verus formal-pr
 
 APP ?= netsuke
 CARGO ?= $(shell command -v cargo 2>/dev/null || printf '%s' "$$HOME/.cargo/bin/cargo")
@@ -6,10 +6,15 @@ BUILD_JOBS ?=
 CLIPPY_FLAGS ?= --all-targets --all-features -- -D warnings
 KANI ?= cargo kani
 KANI_FLAGS ?=
-KANI_VERSION_CHECK ?= scripts/check-kani-version.sh
+KANI_INSTALL_FLAGS ?=
+KANI_CHECK_FLAGS ?=
 MDLINT ?= $(shell command -v markdownlint-cli2 2>/dev/null || printf '%s' "$$HOME/.bun/bin/markdownlint-cli2")
 NIXIE ?= nixie
+PROVER_TOOLS_SOURCE ?= git+https://github.com/leynos/rust-prover-tools@b07ef696f8373d54ae68e517d39d47a5d27a5bd5
+PROVER_TOOLS ?= uv tool run --from $(PROVER_TOOLS_SOURCE) prover-tools
 RUSTDOC_FLAGS ?= --cfg docsrs -D warnings
+VERUS_FLAGS ?=
+VERUS_INSTALL_FLAGS ?=
 
 export PATH := $(HOME)/.cargo/bin:$(HOME)/.bun/bin:$(PATH)
 
@@ -47,12 +52,21 @@ markdownlint: ## Lint Markdown files
 nixie: ## Validate Mermaid diagrams
 	nixie --no-sandbox
 
+install-kani: ## Install the pinned Kani verifier
+	$(PROVER_TOOLS) kani install $(KANI_INSTALL_FLAGS)
+
 kani: ## Run the Kani local smoke check
-	KANI="$(KANI)" $(KANI_VERSION_CHECK)
+	$(PROVER_TOOLS) kani check-version --kani-command "$(KANI)" $(KANI_CHECK_FLAGS)
 
 kani-full: ## Run the full Kani verification suite
 	$(KANI) $(KANI_FLAGS)
 
+install-verus: ## Install the pinned Verus verifier
+	$(PROVER_TOOLS) verus install $(VERUS_INSTALL_FLAGS)
+
+verus: ## Run the Verus proof entry point
+	$(PROVER_TOOLS) verus run $(VERUS_FLAGS)
+
 formal-pr: ## Run pull-request formal-verification checks
 	$(MAKE) kani
 
diff --git a/docs/developers-guide.md b/docs/developers-guide.md
index d275e5a2..8ffa1c53 100644
--- a/docs/developers-guide.md
+++ b/docs/developers-guide.md
@@ -85,14 +85,15 @@ repository work.
 Install or refresh the pinned Kani tool with:
 
 ```bash
-scripts/install-kani.sh
+make install-kani
 ```
 
-The installer reads `tools/kani/VERSION`, runs
-`cargo install --locked kani-verifier --version <version>`, runs
-`cargo kani setup`, and verifies that `cargo kani` is callable. Kani may manage
-its own supporting Rust nightly toolchain during setup. That toolchain must not
-replace the repository's ordinary stable Rust workflow.
+`make install-kani` delegates to the pinned `rust-prover-tools` CLI through
+`uv tool run`. The prover tool reads `tools/kani/VERSION`, runs
+`cargo install --locked kani-verifier --version <version>`, runs `cargo kani
+setup`, and verifies that `cargo kani` is callable. Kani may manage its own
+supporting Rust nightly toolchain during setup. That toolchain must not replace
+the repository's ordinary stable Rust workflow.
 
 Use the Make targets for day-to-day formal-verification checks:
 
@@ -102,6 +103,9 @@ Use the Make targets for day-to-day formal-verification checks:
 - `make kani-full` is reserved for the full Kani proof suite once harnesses
   exist. Today it invokes `cargo kani` without additional smoke flags.
 - `make formal-pr` aliases the pull-request formal-verification smoke path.
+- `make install-verus` and `make verus` delegate to `rust-prover-tools` for
+  the optional Verus installer and proof runner. These targets are not part of
+  the ordinary pull-request gate.
 
 Kani is intentionally not part of `make test`, `make lint`, `make check-fmt`,
 or `make all`.
@@ -118,12 +122,13 @@ long-lived mutable control-plane state. See
 for the design rationale and re-entry criteria.
 
 Pull requests run a dedicated `kani-smoke` CI job alongside the ordinary
-`build-test` job. The job installs the pinned Kani version with
-`scripts/install-kani.sh` and runs only `make kani`; it does not run
-`make kani-full`, coverage, CodeScene upload, or the normal build matrix. Its
-cache is intentionally separate from ordinary Cargo build artefacts: the job
-uses a Kani-specific cache key derived from `tools/kani/VERSION` and caches the
-job-local Kani Cargo home plus Kani support-file home.
+`build-test` job. The job installs `uv`, installs the pinned Kani version
+through `make install-kani`, and runs only `make kani`; it does not run
+`make kani-full`, `make verus`, coverage, CodeScene upload, or the normal build
+matrix. Its cache is intentionally separate from ordinary Cargo build
+artefacts: the job uses a Kani-specific cache key derived from
+`tools/kani/VERSION` and the Makefile, then caches the job-local Kani Cargo
+home plus Kani support-file home.
 
 ## Test suite map
 
diff --git a/docs/formal-verification-methods-in-netsuke.md b/docs/formal-verification-methods-in-netsuke.md
index e9de451c..2ad2aa24 100644
--- a/docs/formal-verification-methods-in-netsuke.md
+++ b/docs/formal-verification-methods-in-netsuke.md
@@ -158,10 +158,6 @@ The preferred first layout is intentionally lightweight:
 .
 ├── Cargo.toml
 ├── Makefile
-├── scripts/
-│   ├── install-kani.sh
-│   ├── install-verus.sh
-│   └── run-verus.sh
 ├── tools/
 │   ├── kani/
 │   │   └── VERSION        # Update when new stable releases ship
@@ -183,6 +179,12 @@ This layout keeps Kani harnesses close to the internal helpers they exercise,
 which avoids widening the public API solely for proofs. Verus can remain
 outside Cargo until it proves its value.
 
+Kani and Verus installation and execution should be delegated to the
+`rust-prover-tools` CLI rather than repository-local shell scripts. Netsuke
+pins the prover CLI in the Makefile and invokes it through `uv tool run`, so
+the verifier workflows have one maintained implementation while the Rust
+package remains free of Python runtime dependencies.
+
 #### Tool version pinning and updates
 
 The `tools/*/VERSION` files define the exact tool versions used in local
@@ -212,6 +214,10 @@ without disturbing the current developer workflow.[^2]
 
 - `make kani` should run a small smoke-harness set suitable for pull requests.
 - `make kani-full` should run the full Kani suite.
+- `make install-kani` should install the pinned Kani version through
+  `rust-prover-tools`.
+- `make install-verus` and `make verus` should delegate optional Verus
+  installation and proof execution to `rust-prover-tools`.
 - `make formal-pr` should alias the fast pull-request checks.
 - `make formal-nightly` should combine deeper Kani runs with any later Verus
   proofs.
@@ -227,7 +233,8 @@ coverage, and those checks should remain intact.[^3]
 
 The first additional job should be a dedicated `kani-smoke` job that:
 
-- installs the pinned Kani toolchain,
+- installs `uv` and then installs the pinned Kani toolchain through
+  `make install-kani`,
 - runs `make kani`, and
 - caches tool downloads separately from the ordinary Rust build artefacts.
 
diff --git a/docs/roadmap.md b/docs/roadmap.md
index e8f2469a..c167d36f 100644
--- a/docs/roadmap.md
+++ b/docs/roadmap.md
@@ -322,7 +322,7 @@ and test workflow intact. See
 - [x] 4.1.1. Add Kani tooling and local smoke targets. See
   [formal-verification-methods-in-netsuke.md §Repository integration plan](formal-verification-methods-in-netsuke.md#repository-integration-plan).
   - [x] Pin the supported Kani version under `tools/kani/`.
-  - [x] Add `scripts/install-kani.sh`.
+  - [x] Add `rust-prover-tools` backed Kani installation.
   - [x] Add `make kani`, `make kani-full`, and `make formal-pr`.
 - [x] 4.1.2. Add a dedicated `kani-smoke` continuous integration (CI) job.
   Requires 4.1.1. See
diff --git a/scripts/check-kani-version.sh b/scripts/check-kani-version.sh
deleted file mode 100755
index 04f68ced..00000000
--- a/scripts/check-kani-version.sh
+++ /dev/null
@@ -1,38 +0,0 @@
-#!/usr/bin/env bash
-# Verifies that the installed Kani command matches the repository pin.
-set -euo pipefail
-
-fail() {
-  echo "check-kani-version: $*" >&2
-  exit 1
-}
-
-script_dir="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)"
-repo_root="$(cd -- "${script_dir}/.." && pwd)"
-version_file="${repo_root}/tools/kani/VERSION"
-kani_command="${KANI:-cargo kani}"
-
-[[ -f "$version_file" ]] ||
-  fail "version pin '${version_file}' does not exist"
-
-expected_version="$(tr -d '[:space:]' < "$version_file")"
-[[ -n "$expected_version" ]] ||
-  fail "version pin '${version_file}' is empty"
-[[ "$expected_version" =~ ^[0-9]+[.][0-9]+[.][0-9]+$ ]] ||
-  fail "version pin '${expected_version}' must use MAJOR.MINOR.PATCH format"
-
-IFS=' ' read -r -a kani_args <<< "$kani_command"
-((${#kani_args[@]} > 0)) ||
-  fail "KANI command is empty"
-
-version_output="$("${kani_args[@]}" --version)" ||
-  fail "failed to run '${kani_command} --version'"
-
-[[ "$version_output" =~ ([0-9]+[.][0-9]+[.][0-9]+) ]] ||
-  fail "could not parse Kani version from: ${version_output}"
-
-actual_version="${BASH_REMATCH[1]}"
-[[ "$actual_version" == "$expected_version" ]] ||
-  fail "expected Kani ${expected_version} from ${version_file}, found ${actual_version}"
-
-echo "Kani ${actual_version} matches ${version_file}."
diff --git a/scripts/install-kani.sh b/scripts/install-kani.sh
deleted file mode 100755
index 86886232..00000000
--- a/scripts/install-kani.sh
+++ /dev/null
@@ -1,38 +0,0 @@
-#!/usr/bin/env bash
-# Installs the repository-supported Kani verifier version.
-set -euo pipefail
-
-fail() {
-  echo "install-kani: $*" >&2
-  exit 1
-}
-
-require_command() {
-  local command_name="$1"
-  command -v "$command_name" >/dev/null 2>&1 ||
-    fail "required command '${command_name}' was not found on PATH"
-}
-
-script_dir="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)"
-repo_root="$(cd -- "${script_dir}/.." && pwd)"
-version_file="${repo_root}/tools/kani/VERSION"
-
-require_command cargo
-
-[[ -f "$version_file" ]] ||
-  fail "version pin '${version_file}' does not exist"
-
-kani_version="$(tr -d '[:space:]' < "$version_file")"
-[[ -n "$kani_version" ]] ||
-  fail "version pin '${version_file}' is empty"
-[[ "$kani_version" =~ ^[0-9]+[.][0-9]+[.][0-9]+$ ]] ||
-  fail "version pin '${kani_version}' must use MAJOR.MINOR.PATCH format"
-
-echo "Installing kani-verifier ${kani_version} from ${version_file}."
-cargo install --locked kani-verifier --version "$kani_version"
-
-echo "Running cargo kani setup for kani-verifier ${kani_version}."
-cargo kani setup
-
-echo "Verifying cargo kani is callable."
-cargo kani --version

From 7bcb93fe72ec2200617c6f0a412a869a67bd8597 Mon Sep 17 00:00:00 2001
From: leynos <leynos@troubledskies.net>
Date: Tue, 26 May 2026 20:05:34 +0200
Subject: [PATCH 4/6] Disable uv cache in CI setup

Remove `enable-cache: true` from the Kani smoke workflow uv setup.
This job uses uv only as a tool installer, so the default `uv.lock`
cache dependency glob is not applicable to this repository.
---
 .github/workflows/ci.yml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a4cd788b..2caae3dd 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -82,8 +82,6 @@ jobs:
           toolchain: stable
       - name: Install uv
         uses: astral-sh/setup-uv@4cda7d73322c50eac316ad623a716f09a2db2ac7  # v3.1.2
-        with:
-          enable-cache: true
       - name: Cache Kani tools
         uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830  # v4.3.0
         with:

From a3cca330a6416551c9698d408406fa702597dbc3 Mon Sep 17 00:00:00 2001
From: leynos <leynos@troubledskies.net>
Date: Tue, 26 May 2026 20:34:13 +0200
Subject: [PATCH 5/6] Import updated agent instructions

Replace the repository agent guidance with the updated AGENTS.md from
the referenced memoryd branch so local agent rules stay in sync.
---
 AGENTS.md | 121 +++++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 88 insertions(+), 33 deletions(-)

diff --git a/AGENTS.md b/AGENTS.md
index e3f084c2..fdc26d35 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -1,6 +1,6 @@
-# Assistant Instructions
+# Assistant instructions
 
-## Code Style and Structure
+## Code style and structure
 
 - **Code is for humans.** Write code with clarity and empathy—assume a
   tired teammate will need to debug it at 3 a.m.
@@ -22,8 +22,8 @@
 - **Group by feature, not layer.** Colocate views, logic, fixtures, and helpers
   related to a domain concept rather than splitting by type.
 - **Use consistent spelling and grammar.** Comments must use en-GB-oxendict
-  ("-ize" / "-yse" / "-our") spelling and grammar, except for references to
-  external APIs.
+  ("-ize" / "-yse" / "-our") spelling and grammar, with the exception of
+  references to external APIs.
 - **Illustrate with clear examples.** Function documentation must include clear
   examples demonstrating the usage and outcome of the function. Test
   documentation should omit examples where the example serves only to reiterate
@@ -33,22 +33,31 @@
   feature and constituents colocated with targets. Large blocks of test data
   should be moved to external data files.
 
-## Documentation Maintenance
+## Documentation maintenance
 
 - **Reference:** Use the markdown files within the `docs/` directory as a
   knowledge base and source of truth for project requirements, dependency
-  choices, and architectural decisions.
+  choices, and architectural decisions. Start with
+  [documentation contents](docs/contents.md) and
+  [repository layout](docs/repository-layout.md) when orienting within the
+  project.
 - **Update:** When new decisions are made, requirements change, libraries are
   added/removed, or architectural patterns evolve, **proactively update** the
-  relevant file(s) in the `docs/` directory to reflect the latest state.
-  **Ensure the documentation remains accurate and current.**
-- Documentation must use en-GB-oxendict ("-ize" / "-yse" / "-our") spelling
-  and grammar. (EXCEPTION: the LICENSE filename is left unchanged for community
-  consistency.)
-- A documentation style guide is provided at
-  `docs/documentation-style-guide.md`.
-
-## Change Quality & Committing
+  relevant file(s) in the `docs/` directory to reflect the latest state. Ensure
+  the documentation remains accurate and current.
+- **Design decisions:** Record design decisions in the relevant design
+  document. When a decision is substantive, capture it in an Architectural
+  Decision Record (ADR) following the documentation style guide, and reference
+  that ADR from the design document.
+- **User-facing behaviour:** Update [users' guide](docs/users-guide.md) for
+  behaviour or user-interface changes that users should know about.
+- **Internal interfaces:** Document internally facing interfaces in the
+  relevant component architecture document. Document internally facing
+  conventions and practices in [developers' guide](docs/developers-guide.md).
+- **Style:** All documentation must adhere to the
+  [documentation style guide](docs/documentation-style-guide.md).
+
+## Change quality and committing
 
 - **Atomicity:** Aim for small, focused, atomic changes. Each change (and
   subsequent commit) should represent a single logical unit of work.
@@ -78,7 +87,7 @@
       code snippets) within the commit message body.
   - Do not commit changes that fail any of the quality gates.
 
-## Refactoring Heuristics & Workflow
+## Refactoring heuristics and workflow
 
 - **Recognizing Refactoring Needs:** Regularly assess the codebase for potential
   refactoring opportunities. Perform refactoring when observing:
@@ -109,7 +118,7 @@
     pass before and after, unit tests added for new units).
   - Ensure the refactoring commit itself passes all quality gates.
 
-## Rust Specific Guidance
+## Rust specific guidance
 
 This repository is written in Rust and uses Cargo for building and dependency
 management. Contributors should follow these best practices when working on the
@@ -151,26 +160,34 @@ project:
   meaningfully named structs.
 - Where a function is returning a large error, consider using `Arc` to reduce
   the amount of data returned.
-- Write unit and behavioural tests for new functionality. Run both before and
-  after making any change.
+- Ensure that new features are validated with unit tests using `rstest` and
+  behavioural tests using `rstest-bdd` where applicable. Cover happy paths,
+  unhappy paths, and relevant edge cases.
+- Add end-to-end tests where a change affects externally observable workflows,
+  integration contracts, persistence, command-line behaviour, network
+  boundaries, UI flows, or other system-level behaviour.
+- Use property tests with `proptest` or a bounded model checker with `kani`
+  when a change introduces an invariant over a range of inputs, states,
+  orderings, or transitions. Use judgement to choose the appropriate level of
+  rigour.
+- Use an exhaustive proof with `verus` for introduced lemmas or contractual
+  business logic. Proofs must be substantive, rigorous, and well-founded, not
+  merely a restatement of the assumed property.
+- Run relevant unit, behavioural, property, model-checking, proof, and
+  end-to-end suites before and after making any change.
 - Every module **must** begin with a module level (`//!`) comment explaining the
   module's purpose and utility.
 - Document public APIs using Rustdoc comments (`///`) so documentation can be
   generated with cargo doc.
 - Prefer immutable data and avoid unnecessary `mut` bindings.
-- Handle errors with the `Result` type instead of panicking where feasible.
 - Use explicit version ranges in `Cargo.toml` and keep dependencies up-to-date.
 - Avoid `unsafe` code unless absolutely necessary, and document any usage
-  clearly.
+  clearly with a "SAFETY" comment.
 - Place function attributes **after** doc comments.
 - Do not use `return` in single-line functions.
 - Use predicate functions for conditional criteria with more than two branches.
 - Lints must not be silenced except as a **last resort**.
 - Lint rule suppressions must be tightly scoped and include a clear reason.
-- Prefer `expect` over `allow`.
-- Use `rstest` fixtures for shared setup.
-- Replace duplicated tests with `#[rstest(...)]` parameterized cases.
-- Prefer `mockall` for mocks/stubs.
 - Use `concat!()` to combine long string literals rather than escaping newlines
   with a backslash.
 - Prefer single line versions of functions where appropriate. i.e.,
@@ -201,22 +218,36 @@ project:
   consistent without per-type boilerplate. Combine approaches: lean on
   `newt-hype` for the common case, tuple structs for outliers, and
   `the-newtype` to unify behaviour when owning the trait definitions.
+- Use `cap_std` and `cap_std::fs_utf8` / `camino` in place of `std::fs` and
+  `std::path` for enhanced cross platform support and capabilities oriented
+  filesystem access.
+
+### Testing
+
+- Use `rstest` fixtures for shared setup.
+- Replace duplicated tests with `#[rstest(...)]` parameterized cases.
+- Prefer `mockall` for ad hoc mocks/stubs.
+- For testing of functionality depending upon environment variables, dependency
+  injection and the `mockable` crate are the preferred option.
+- If mockable cannot be used, env mutations in tests MUST be wrapped in shared
+  guards and mutexes placed in a shared `test_utils` or `test_helpers` crate.
+  Direct environment mutation is FORBIDDEN in tests.
 
-### Dependency Management
+### Dependency management
 
 - **Mandate caret requirements for all dependencies.** All crate versions
-  specified in `Cargo.toml` must use SemVer-compatible caret requirements
-  (e.g., `some-crate = "1.2.3"`). This is Cargo's default and allows for safe,
+  specified in `Cargo.toml` must use SemVer-compatible caret requirements (e.g.,
+   `some-crate = "1.2.3"`). This is Cargo's default and allows for safe,
   non-breaking updates to minor and patch versions while preventing breaking
   changes from new major versions. This approach is critical for ensuring build
   stability and reproducibility.
 - **Prohibit unstable version specifiers.** The use of wildcard (`*`) or
   open-ended inequality (`>=`) version requirements is strictly forbidden as
-  they introduce unacceptable risk and unpredictability. Tilde requirements
-  (`~`) should only be used where a dependency must be locked to patch-level
+  they introduce unacceptable risk and unpredictability. Tilde requirements (
+  `~`) should only be used where a dependency must be locked to patch-level
   updates for a specific, documented reason.
 
-### Error Handling
+### Error handling
 
 - **Prefer semantic error enums**. Derive `std::error::Error` (via the
   `thiserror` crate) for any condition the caller might inspect, retry, or map
@@ -239,7 +270,31 @@ project:
 - Consume fallible fixtures in `rstest` by **making the test return `Result`**
   and applying `?` to the fixture.
 
-## Markdown Guidance
+### Observability
+
+- Use `tracing` for logging and diagnostics. Prefer structured
+  `tracing::{trace, debug, info, warn, error}` events and spans over `println!`,
+   `eprintln!`, or direct `log` macros. Add fields for identifiers, state, and
+  error context so downstream subscribers can filter and correlate events
+  without parsing message text.
+- Use `#[tracing::instrument]` or explicit spans around request handling,
+  command execution, retries, background jobs, and other meaningful units of
+  work. Do not hold `Span::enter()` guards across `.await`; use
+  `Instrument::instrument` or scoped synchronous spans instead.
+- Use the `metrics` crate for metric emission where usage, uptake, failure,
+  or mitigation metrics are required. Prefer `counter!` for cumulative events,
+  `gauge!` for values that rise and fall, and `histogram!` for distributions
+  such as latency or payload size.
+- Describe emitted metrics with `describe_counter!`, `describe_gauge!`, or
+  `describe_histogram!` where the unit or purpose is not obvious from the
+  metric name. Keep metric names stable and labels low-cardinality; do not put
+  user input, request IDs, paths with unbounded parameters, or raw error
+  strings into labels.
+- Libraries may emit `metrics` and `tracing` instrumentation, but must not
+  install global recorders or subscribers. Applications should initialise
+  exporters/subscribers once, as early as practical in startup.
+
+## Markdown guidance
 
 - Validate Markdown files using `make markdownlint`.
 - Run `make fmt` after any documentation changes to format all Markdown
@@ -291,7 +346,7 @@ The following tooling is available in this environment:
 - `difft` **(Difftastic)** — Semantic diff tool that compares code structure
   rather than just text differences.
 
-## Key Takeaway
+## Key takeaway
 
 These practices help maintain a high-quality codebase and facilitate
 collaboration.

From 19f8eabe675a5571c432c0c31b71fc5429b48b39 Mon Sep 17 00:00:00 2001
From: leynos <leynos@troubledskies.net>
Date: Tue, 26 May 2026 20:47:37 +0200
Subject: [PATCH 6/6] Import updated documentation style guide

Replace the local documentation style guide with the latest version
from the referenced memoryd main branch.
---
 docs/documentation-style-guide.md | 630 +++++++++++++++++++++++-------
 1 file changed, 493 insertions(+), 137 deletions(-)

diff --git a/docs/documentation-style-guide.md b/docs/documentation-style-guide.md
index 92fc7cfc..d4334c3a 100644
--- a/docs/documentation-style-guide.md
+++ b/docs/documentation-style-guide.md
@@ -1,12 +1,14 @@
 # Documentation style guide
 
-This guide outlines conventions for authoring documentation for df12 software.
-Apply these rules to keep the documentation clear and consistent for developers.
+This guide outlines conventions for authoring documentation for software
+created by df12 Productions. Apply these rules to keep documentation clear,
+consistent, and easy to maintain across projects.
 
 ## Spelling
 
 - Use British English based on the
-  [Oxford English Dictionary](https://public.oed.com/) (en-GB-oxendict):
+  [Oxford English Dictionary](https://public.oed.com/) locale `en-GB-oxendict`,
+  which denotes English for the Great Britain market in the Oxford style:
   - suffix -ize in words like _realize_ and _organization_ instead of
      -ise endings,
   - suffix ‑lyse in words not traced to the Greek ‑izo, ‑izein suffixes,
@@ -18,17 +20,15 @@ Apply these rules to keep the documentation clear and consistent for developers.
   - suffix -ogue in words such as _analogue_ and _catalogue_,
   - and so forth.
 - The words **"outwith"** and **"caveat"** are acceptable.
-- Keep United States (US) spelling when used in an external API, command, or
-  library, for example, `color`.
-- The name of the project licence file is spelled `LICENSE` for community
-  consistency.
+- Keep United States (US) spelling when used in an API, for example, `color`.
+- The project uses the filename `LICENSE` for community consistency.
 
 ## Punctuation and grammar
 
 - Use the Oxford comma: "ships, planes, and hovercraft" where it aids
   comprehension.
 - Company names are treated as collective nouns: "df12 Productions are
-  expanding".
+  releasing an update".
 - Avoid first and second person personal pronouns outside the `README.md`
   file.
 
@@ -64,146 +64,295 @@ Apply these rules to keep the documentation clear and consistent for developers.
 - Footnotes must be numbered in order of appearance in the document.
 - Caption every table, and caption every diagram.
 
-## Example snippet
+## Standard document types
+
+Repositories that adopt this documentation style should keep a small set of
+high-value documents with clearly separated audiences and responsibilities.
+These document types are complementary: the contents file helps readers find
+material, the user's guide explains how to use the project, the developer's
+guide explains how to work on the project, the design document explains why the
+system is shaped the way it is, and the repository layout document explains
+where important things live. For discoverability, use canonical filenames
+unless a stronger repository-specific constraint applies. A minimal canonical
+set looks like
+`docs/{contents,users-guide,developers-guide,repository-layout}.md` plus a
+primary design document under `docs/*-design.md`, for example
+`docs/theoremc-design.md` or `docs/query-planner-design.md`.
+
+### Contents file
+
+Use a dedicated contents file, typically `docs/contents.md`, as the index for
+the documentation set.
+
+- Make the document title explicit, for example `# Documentation contents`.
+- Begin with the contents file linking to itself so readers can confirm they
+  are at the index.
+- List each document exactly once with an inline link and a short descriptive
+  phrase explaining why someone would open it.
+- Group related material together, such as decision records, reference
+  documents, guides, and plan directories.
+- Keep the descriptions audience-focused. Explain the purpose of the document,
+  not merely its filename.
+- Prefer stable ordering so repeated readers can scan predictably. Grouping by
+  topic is usually better than strict alphabetic ordering.
+- When listing a directory, add one nested level only where it materially
+  improves navigation, for example to enumerate execution plans beneath an
+  `execplans/` entry.
+- Update the contents file whenever a document is added, renamed, or removed.
+
+### User's guide
+
+Use the user's guide, canonically `docs/users-guide.md`, for readers who need
+to apply the project rather than modify its internals. In a library, this means
+consumers of the application programming interface (API). In an application,
+this means operators, end users, or integrators.
+
+- Open with one short paragraph that states the audience and scope.
+- Organize the guide around user-facing tasks, concepts, and guarantees rather
+  than internal module boundaries.
+- Introduce the primary workflow early, with a minimal working example that a
+  reader can adapt immediately.
+- Put public-facing reference material here when users need it to succeed, for
+  example CLI usage, configuration keys, file-format rules, or API surface
+  summaries.
+- Present rules, constraints, defaults, and error behaviour near the feature
+  they affect, rather than scattering them across the document.
+- Use tables where they clarify field sets, command options, or compatibility
+  matrices.
+- Include concrete examples in code or data form when describing formats,
+  schemas, or command usage.
+- Higher-level user workflows belong here, for example "load a document",
+  "configure the service", or "interpret diagnostics".
+- Link to design documents or maintainer references when deeper rationale would
+  otherwise overload the guide.
+- Exclude maintainer-only concerns such as internal layering debates, future
+  refactor plans, or enforcement tooling unless they directly affect users.
+
+### Developer's guide
+
+Use the developer's guide, canonically `docs/developers-guide.md`, for
+maintainers and contributors. Treat this as the operating manual for working on
+the existing system, not as the place for the project's primary design document.
+
+- Open with one short paragraph that states the audience and the operational
+  scope of the guide.
+- Link early to the design document, repository layout document, accepted
+  decision records, and other normative references that explain architecture or
+  rationale in depth.
+- Put maintainer-facing implementation guidance here, for example build, test,
+  lint, release, debugging, extension, and contribution workflows.
+- Use numbered sections for long-form technical documents to improve
+  cross-referencing in reviews and follow-up discussions.
+- Separate normative rules from informative explanation. Mark source-of-truth
+  sections clearly.
+- Include compact interface maps or workflow diagrams where they materially
+  improve implementation guidance.
+- Keep subsystem descriptions focused on current responsibilities,
+  integration points, and operational expectations. Put design rationale, major
+  trade-offs, and proposed architecture in design documents instead.
+- Do not embed repository-layout guidance here. The canonical location for
+  file-tree and path-responsibility documentation is
+  `docs/repository-layout.md`.
+- Keep the document synchronized with decision records, roadmap items, and the
+  codebase. A stale developer's guide is worse than a shorter one.
+
+### Design document, ADR, and RFC
+
+Use these document types for different jobs. Do not collapse them into one
+catch-all "design note".
+
+- A **design document** explains the shape of a system or subsystem: its
+  architecture, constraints, data flow, rationale, and intended evolution. It
+  is usually a living document and may describe the current implementation, the
+  target implementation, or both.
+- An **Architecture Decision Record (ADR)** captures one accepted decision. It
+  should be narrow, stable, and explicit about context, decision, consequences,
+  and status. Use an ADR when the important thing to preserve is the outcome,
+  not the full exploratory discussion that led to it.
+- A **Request for Comments (RFC)** proposes a change before acceptance. It is
+  the right format for changes that need reviewing, alternatives analysis,
+  migration planning, or cross-team discussion. An RFC may later be accepted,
+  rejected, superseded, or distilled into one or more ADRs.
+
+In short: use a design document to explain the system, an ADR to record a
+decision, and an RFC to propose a change.
+
+### Design document
+
+Use a dedicated design document, conventionally named
+`docs/<product-or-topic>-design.md`, to explain the architecture, constraints,
+rationale, and intended evolution of a system or subsystem. This document is
+the correct location for design intent; that material must not be buried in the
+user's guide or developer's guide.
+
+- Start with a concise front matter section that states status, scope, primary
+  audience, and the decision records or other documents that take precedence.
+- Open the main body with the problem statement, product thesis, or design goal
+  before describing the solution. Readers should understand the problem the
+  design is solving before they inspect the structure.
+- State the non-negotiable constraints explicitly. These are the rules later
+  sections assume rather than re-justify.
+- Separate normative definitions from informative explanation. If another
+  document is the source of truth for a schema, protocol, or naming rule, say
+  so plainly and link to it.
+- Describe the high-level architecture before diving into file-level or
+  module-level details. A reader should understand the major subsystems,
+  boundaries, and data flow early.
+- Use numbered sections for substantial designs so review comments, follow-up
+  changes, and decision records can cite stable anchors.
+- Include diagrams, tables, or pipeline sketches when they materially improve
+  comprehension, especially for flows, layered boundaries, or generated
+  artefacts.
+- Record risks, trade-offs, rejected alternatives, and future extension points.
+  A design document should explain not only what the system looks like, but why
+  it takes that shape.
+- Keep examples concrete and representative. Prefer one realistic example that
+  exercises the important structure over several toy fragments.
+- Keep the design document synchronized with accepted decision records and the
+  implemented system. If the code or the governing decision changes, update the
+  design or mark the divergence explicitly.
+
+### Request for Comments (RFC)
+
+Use RFCs for proposed changes that need technical review before they become
+binding. Store them under `docs/rfcs/`.
+
+### RFC naming convention
+
+Name RFC files using the pattern `0001-short-topic.md`, where `0001` is a
+zero-padded sequence number. Place RFCs in the `docs/rfcs/` directory.
+
+- Number RFCs sequentially in allocation order rather than by date.
+- Do not renumber existing RFCs after publication. Gaps are acceptable when
+  numbers are reserved, drafted on another branch, or intentionally skipped.
+
+### RFC required sections
+
+Every RFC must include the following sections in order:
+
+- **Title:** Start the document with a numbered title in this form:
+  `# RFC 0001: Concise subject`.
+- **Preamble:** Follow the title with a dedicated `## Preamble` section.
+- **RFC number:** Include the allocated sequence number.
+- **Status:** State the document status. Use `Proposed` unless a later process
+  explicitly promotes, rejects, withdraws, or supersedes the RFC.
+- **Created:** The date the RFC was created (format: YYYY-MM-DD).
+- **Opening section:** Keep the first substantive section near the top.
+  `## Summary`, `## Executive summary`, or `## Problem` are all acceptable if
+  used consistently within the document.
+
+### RFC conditional sections
+
+Include these sections as appropriate to the scope and complexity of the
+proposal:
+
+- **Problem:** Describe the deficiency, risk, or missing capability that
+  motivates the RFC.
+- **Current State:** Explain the relevant current behaviour or architecture when
+  the proposal depends on existing constraints.
+- **Goals and Non-goals:** Clarify what the RFC intends to change and what it
+  deliberately leaves out of scope.
+- **Proposed Design / Proposed Change:** Describe the recommended design with
+  enough detail to support implementation review.
+- **Requirements:** Separate functional, technical, safety, or operational
+  requirements when the proposal has multiple kinds of constraints.
+- **Compatibility and Migration:** Explain rollout expectations, compatibility
+  impact, and migration sequencing when adoption is not trivial.
+- **Alternatives Considered:** Record rejected options and the reasons they
+  were not chosen.
+- **Open Questions / Outstanding Decisions:** Identify unresolved issues that
+  still need reviewing before the proposal can be treated as settled.
+- **Recommendation:** End with a clear statement of the preferred direction
+  when the preceding analysis presents multiple viable choices.
+
+### RFC formatting guidance
 
-```rust,no_run
-/// A simple function demonstrating documentation style.
-fn add(a: i32, b: i32) -> i32 {
-    a + b
-}
-```
+- Use second-level headings (`##`) for major sections.
+- Use third-level headings (`###`) for subsections such as phases, options,
+  requirements groupings, or rollout stages.
+- Use numbered major sections for long RFCs when stable review anchors will
+  help discussion.
+- Use tables to compare design alternatives, rollout paths, or capability
+  trade-offs when multiple dimensions matter.
+- Include code snippets with language identifiers when illustrating interfaces,
+  payloads, or implementation seams.
+- Add screen reader descriptions before complex diagrams or code blocks.
+- Update links when RFC filenames change, especially cross-references from one
+  RFC to another.
 
-## API doc comments (Rust)
+### RFC template
 
-Use doc comments to document public APIs. Keep them consistent with the
-contents of the manual.
+```markdown
+# RFC 0001: <title>
 
-- Begin each block with `///`.
-- Keep the summary line short, followed by further detail.
-- Explicitly document all parameters with `# Parameters`, describing each
-  argument.
-- Document the return value with `# Returns`.
-- Document any panics or errors with `# Panics` or `# Errors` as appropriate.
-- Place examples under `# Examples` for public functions.
-- Use examples for private functions only where they assist in understanding
-  the purpose of the function, and mark these as `ignore`.
-- Put function attributes after the doc comment.
+## Preamble
 
-```rust,no_run
-/// Returns the sum of `a` and `b`.
-///
-/// # Parameters
-/// - `a`: The first integer to add.
-/// - `b`: The second integer to add.
-///
-/// # Returns
-/// The sum of `a` and `b`.
-///
-/// # Examples
-///
-/// ```rust,no_run
-/// assert_eq!(add(2, 3), 5);
-/// ```
-#[inline]
-pub fn add(a: i32, b: i32) -> i32 {
-    a + b
-}
-```
+- **RFC number:** 0001
+- **Status:** Proposed
+- **Created:** YYYY-MM-DD
 
-## Diagrams and images
+## Summary
 
-Where it adds clarity, include [Mermaid](https://mermaid.js.org/) diagrams.
-When embedding figures, use `![alt text](path/to/image)` and provide brief alt
-text describing the content. Add a short description before each Mermaid
-diagram, so screen readers can understand it.
+<Concise statement of the proposal and why it matters.>
 
-For screen readers: The following flowchart outlines the documentation workflow.
+## Problem
 
-```mermaid
-flowchart TD
-    A[Start] --> B[Draft]
-    B --> C[Review]
-    C --> D[Merge]
-```
+<Describe the current deficiency, risk, or missing capability.>
 
-_Figure 1: Documentation workflow from draft through merge review._
+## Current state
 
-## Roadmap task writing guidelines
+<Summarize the relevant current implementation or constraints.>
 
-When documenting development roadmap items, write them to be achievable,
-measurable, and structured. This ensures the roadmap functions as a practical
-planning tool rather than a vague wishlist. Do not commit to timeframes in the
-roadmap. Development effort should be roughly consistent from task to task.
+## Goals and non-goals
 
-### Principles for roadmap tasks
+- Goals:
+  - <Goal 1>
+  - <Goal 2>
+- Non-goals:
+  - <Non-goal 1>
+  - <Non-goal 2>
 
-- Define outcomes, not intentions: Phrase tasks in terms of the capability
-  delivered (e.g. “Implement role-based access control for API endpoints”), not
-  aspirations like “Improve security”.
-- Quantify completion criteria: Attach measurable finish lines (e.g. “90%
-  test coverage for new modules”, “response times under 200ms”, “all endpoints
-  migrated”).
-- Break into atomic increments: Ensure tasks can be completed in weeks, not
-  quarters. Large goals should be decomposed into clear, deliverable units.
-- Tie to dependencies and sequencing: Document prerequisites, so tasks can be
-  scheduled realistically (e.g. “Introduce central logging service” before “Add
-  error dashboards”).
-- Bound scope explicitly: Note both in-scope and out-of-scope elements (e.g.
-  “Build analytics dashboard (excluding churn prediction)”).
+## Proposed design
 
-### Hierarchy of scope
+<Describe the recommended design in enough detail for technical review.>
 
-Roadmaps should be expressed in three layers of scope to maintain clarity and
-navigability:
+## Requirements
 
-- Phases (strategic milestones) – Broad outcome-driven stages that represent
-  significant capability shifts. Why the work matters.
-- Steps (epics / workstreams) – Mid-sized clusters of related tasks grouped
-  under a phase. What will be built.
-- Tasks (execution units) – Small, measurable pieces of work with clear
-  acceptance criteria. How it gets done.
+### Functional requirements
 
-### Roadmap formatting conventions
+- <Functional requirement 1>
+- <Functional requirement 2>
 
-- **Dotted numbering:** Number phases, steps, and headline tasks using dotted
-  notation:
-  - Phases: 1, 2, 3, …
-  - Steps: 1.1, 1.2, 1.3, …
-  - Headline tasks: 1.1.1, 1.1.2, 1.1.3, …
-- **Checkboxes:** Precede task and sub-task items with a GitHub-Flavoured
-  Markdown (GFM) checkbox (`[ ]`) to track completion status.
-- **Dependencies:** Note non-linear dependencies explicitly. Where a task
-  depends on another task outside its immediate sequence, cite the dependency
-  using dotted notation (e.g. "Requires 2.3.1").
-- **Success criteria:** Include explicit success criteria only where not
-  immediately obvious from the task description.
-- **Design document citations:** Where applicable, cite the relevant design
-  document section for each task (e.g. "See design-doc.md §3.2").
+### Technical requirements
 
-### Roadmap example
+- <Technical requirement 1>
+- <Technical requirement 2>
 
-```markdown
-## 1. Core infrastructure
+## Compatibility and migration
 
-### 1.1. Logging subsystem
+<Describe compatibility impact, rollout constraints, and migration sequencing.>
 
-- [ ] 1.1.1. Introduce central logging service
-  - [ ] Define log message schema. See design-doc.md §2.1.
-  - [ ] Implement log collector daemon.
-  - [ ] Add structured logging to API layer.
-- [ ] 1.1.2. Add error dashboards. Requires 1.1.1.
-  - [ ] Deploy Grafana instance.
-  - [ ] Create error rate dashboard (target: <1% error rate visible within 5 min).
+## Alternatives considered
 
-### 1.2. Authentication
+### Option A: <Name>
+
+<Description, consequences, and trade-offs.>
+
+### Option B: <Name>
+
+<Description, consequences, and trade-offs.>
+
+## Open questions
+
+- <Open question 1>
+- <Open question 2>
+
+## Recommendation
 
-- [ ] 1.2.1. Implement role-based access control. Requires 1.1.1.
-  - [ ] Define role hierarchy. See design-doc.md §4.3.
-  - [ ] Add RBAC middleware to API endpoints.
-  - [ ] Write integration tests for permission boundaries.
+<State the preferred direction and why it should be adopted.>
 ```
 
-## Architectural Decision Records (ADRs)
+## Architectural decision records (ADRs)
 
 Use ADRs to document significant architectural and design decisions. ADRs
 capture the context, options considered, and rationale behind decisions,
@@ -226,9 +375,6 @@ Every ADR must include the following sections in order:
   the problem or question that prompted the decision. Include enough background
   for readers unfamiliar with the history.
 
-Incorporate Conditional sections (below) as appropriate to the decision's
-complexity.
-
 ### Conditional sections
 
 Include these sections as appropriate to the decision's complexity:
@@ -258,7 +404,7 @@ Include these sections as appropriate to the decision's complexity:
 - Use second-level headings (`##`) for major sections.
 - Use third-level headings (`###`) for subsections (e.g. phases, option names).
 - Use tables to compare options when multiple dimensions are relevant. Include
-  a caption below the table (e.g. "_Table 1: Trade-offs between X and Y._").
+  a caption below the table (e.g. “_Table 1: Trade-offs between X and Y._”).
 - Include code snippets with language identifiers when illustrating technical
   approaches. Use `no_run` for illustrative Rust code that should not be
   executed.
@@ -267,23 +413,18 @@ Include these sections as appropriate to the decision's complexity:
 
 ### ADR template
 
-The following template demonstrates the essential structure of an ADR. For
-complex decisions, expand the template by adding elements from the Formatting
-guidance above (e.g. comparison tables with captions, screen reader
-descriptions, or additional Conditional sections).
-
-```markdown
+```plaintext
 # Architectural decision record (ADR) NNN: <title>
 
 ## Status
 
-Proposed.
+<Proposed | Accepted | Superseded | Deprecated>.
 
 ## Date
 
 YYYY-MM-DD.
 
-## Context and Problem Statement
+## Context and problem statement
 
 <Describe the situation, constraints, and the question being addressed.>
 
@@ -292,7 +433,19 @@ YYYY-MM-DD.
 - <Driver 1>
 - <Driver 2>
 
-## Options Considered
+## Requirements
+
+### Functional requirements
+
+- <Functional requirement 1>
+- <Functional requirement 2>
+
+### Technical requirements
+
+- <Technical requirement 1>
+- <Technical requirement 2>
+
+## Options considered
 
 ### Option A: <Name>
 
@@ -308,21 +461,224 @@ YYYY-MM-DD.
 
 _Table 1: Comparison of options._
 
-## Decision Outcome / Proposed Direction
+## Decision outcome / proposed direction
 
 <State the chosen or recommended approach and summarize the rationale.>
 
-## Known Risks and Limitations
+## Goals and non-goals
+
+- Goals:
+  - <Goal 1>
+  - <Goal 2>
+- Non-goals:
+  - <Non-goal 1>
+  - <Non-goal 2>
+
+## Migration plan
+
+<Use numbered phases with clear goals and deliverables where phased
+implementation is required.>
+
+## Known risks and limitations
 
 - <Risk or limitation 1>
 - <Risk or limitation 2>
 
-## Outstanding Decisions
+## Outstanding decisions
 
 - <Open question 1>
 - <Open question 2>
 ```
 
+### Repository layout document
+
+Use a repository layout document, canonically `docs/repository-layout.md`, to
+explain the shape of the tree and the responsibilities of its major paths. Use
+this standalone document as the canonical location for repository-layout
+guidance rather than embedding that material in the developer's guide.
+
+- Document the top-level directories and any critical subdirectories that a new
+  contributor must understand quickly.
+- Explain the purpose, ownership boundary, and notable conventions of each
+  path, not just its name.
+- Prefer a compact tree, table, or both. Use the tree for orientation and the
+  prose or table for semantics.
+- Distinguish between authoritative structure and illustrative sketches. If the
+  tree is incomplete or simplified, say so explicitly.
+- Highlight where source code, tests, generated artefacts, plans, and
+  long-lived reference documents belong.
+- Call out any directories with unusual constraints, such as generated output,
+  fixtures, snapshots, or capability-restricted paths.
+- Ensure the contents file links directly to `docs/repository-layout.md` so
+  readers can find it without scanning the developer's guide.
+- Update the layout document when the repository structure changes enough that
+  a contributor could otherwise follow outdated guidance.
+
+## Example snippet
+
+```rust,no_run
+/// A simple function demonstrating documentation style.
+fn add(a: i32, b: i32) -> i32 {
+    a + b
+}
+```
+
+## API doc comments (Rust)
+
+Use doc comments to document public APIs. Keep them consistent with the
+contents of the manual.
+
+- Begin each block with `///`.
+- Keep the summary line short, followed by further detail.
+- Explicitly document all parameters with `# Parameters`, describing each
+  argument.
+- Document the return value with `# Returns`.
+- Document any panics or errors with `# Panics` or `# Errors` as appropriate.
+- Place examples under `# Examples` and mark the code block with `no_run`, so
+  they do not execute during documentation tests.
+- Put function attributes after the doc comment.
+
+```rust,no_run
+/// Returns the sum of `a` and `b`.
+///
+/// # Parameters
+/// - `a`: The first integer to add.
+/// - `b`: The second integer to add.
+///
+/// # Returns
+/// The sum of `a` and `b`.
+///
+/// # Examples
+///
+/// ```rust,no_run
+/// assert_eq!(add(2, 3), 5);
+/// ```
+#[inline]
+pub fn add(a: i32, b: i32) -> i32 {
+    a + b
+}
+```
+
+## Diagrams and images
+
+Where it adds clarity, include [Mermaid](https://mermaid.js.org/) diagrams.
+When embedding figures, use `![alt text](path/to/image)` and provide brief alt
+text describing the content. Add a short description before each Mermaid
+diagram, so screen readers can understand it.
+
+For screen readers: The following flowchart outlines the documentation workflow.
+
+```mermaid
+flowchart TD
+    A[Start] --> B[Draft]
+    B --> C[Review]
+    C --> D[Merge]
+```
+
+_Figure 1: Documentation workflow from draft through merge review._
+
+## Roadmap task writing guidelines
+
+When documenting development roadmap items, write them to be achievable,
+measurable, and structured. This ensures the roadmap functions as a practical
+planning tool rather than a vague wishlist. Do not commit to timeframes in the
+roadmap. Development effort should be roughly consistent from task to task.
+
+### Principles for roadmap tasks
+
+- Define outcomes, not intentions: Phrase tasks in terms of the capability
+  delivered (e.g. “Implement role-based access control for API endpoints”), not
+  aspirations like “Improve security”.
+- Quantify completion criteria: Attach measurable finish lines (e.g. “90%
+  test coverage for new modules”, “response times under 200ms”, “all endpoints
+  migrated”).
+- Break into atomic increments: Ensure tasks can be completed in weeks, not
+  quarters. Large goals should be decomposed into clear, deliverable units.
+- Tie to dependencies and sequencing: Document prerequisites, so tasks can be
+  scheduled realistically (e.g. “Introduce central logging service” before “Add
+  error dashboards”).
+- Bound scope explicitly: Note both in-scope and out-of-scope elements (e.g.
+  “Build analytics dashboard (excluding churn prediction)”).
+
+### Hierarchy of scope
+
+Roadmaps should be expressed in three layers of scope to maintain clarity and
+navigability:
+
+- Phases (strategic milestones) – Broad outcome-driven stages that represent
+  significant capability shifts. Why the work matters.
+- Steps (epics / workstreams) – Mid-sized clusters of related tasks grouped
+  under a phase. What will be built.
+- Tasks (execution units) – Small, measurable pieces of work with clear
+  acceptance criteria. How it gets done.
+
+This hierarchy should align with the GIST framework:
+
+- Phases correspond to strategic themes or milestones.
+- Steps correspond to GIST-style workstreams. A step must describe a coherent
+  body of delivery work with one clear objective, explicit sequencing value,
+  and a practical learning loop. A step is not just a heading used to group
+  unrelated tasks.
+- Tasks correspond to implementation-level execution units. A task should be a
+  concrete build activity, not an aspiration, research topic, or status label.
+
+### Roadmap formatting conventions
+
+- **Dotted numbering:** Number phases, steps, and headline tasks using dotted
+  notation:
+  - Phases: 1, 2, 3, …
+  - Steps: 1.1, 1.2, 1.3, …
+  - Headline tasks: 1.1.1, 1.1.2, 1.1.3, …
+- **Checkboxes:** Precede task and sub-task items with a GitHub Flavored
+  Markdown (GFM) checkbox (`[ ]`) to track completion status.
+- **Dependencies:** Note non-linear dependencies explicitly. Where a task
+  depends on another task outside its immediate sequence, cite the dependency
+  using dotted notation (e.g. “Requires 2.3.1”).
+- **Success criteria:** Include explicit success criteria only where not
+  immediately obvious from the task description.
+- **Design document citations:** Where applicable, cite the relevant design
+  document section for each task (e.g. “See design-doc.md §3.2”).
+
+### Roadmap example
+
+```plaintext
+## 1. Core infrastructure
+
+### 1.1. Logging subsystem
+
+- [ ] 1.1.1. Introduce central logging service
+  - Define log message schema. See design-doc.md §2.1.
+  - Implement log collector daemon.
+  - Add structured logging to API layer.
+- [ ] 1.1.2. Add error dashboards. Requires 1.1.1.
+  - Deploy Grafana instance.
+  - Create error rate dashboard (target: <1% error rate visible within 5 min).
+
+### 1.2. Authentication
+
+- [ ] 1.2.1. Implement role-based access control (RBAC). Requires 1.1.1.
+  - Define role hierarchy. See design-doc.md §4.3.
+  - Add RBAC middleware to API endpoints.
+  - Write integration tests for permission boundaries.
+```
+
+### Writing GIST-aligned steps
+
+When writing a roadmap step, make it function as a real workstream:
+
+- Give the step a concrete objective that describes what will exist when the
+  workstream is complete.
+- State the learning opportunity for the step when that learning affects later
+  sequencing or design choices.
+- Group only tasks that serve the same delivery objective. If the tasks do not
+  share one operational purpose, split the step.
+- Sequence steps so each workstream either unlocks the next one or reduces a
+  specific class of delivery risk.
+
+Avoid using steps as passive document structure. Headings such as “Backend
+changes”, “Frontend work”, or “Other tasks” are not sufficient unless they are
+framed as real workstreams with a defined outcome.
+
 ______________________________________________________________________
 
 [^1]: A linter that enforces consistent Markdown formatting.