# proposal/11-roadmap.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/6e774a8a98ad63868774cf1558e6159b6a8b6593/proposal/11-roadmap.md)

Repository: [versecafe/strata](https://git.cafe/versecafe/strata)

Visibility: public

Requested revision: 6e774a8a98ad63868774cf1558e6159b6a8b6593

Requested commit: 6e774a8a98ad63868774cf1558e6159b6a8b6593

Commit: 6e774a8a98ad63868774cf1558e6159b6a8b6593

Blob: 980c43446a9dfbf7739ebc10e4b6e2e5273684a5

Size: 9623 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/6e774a8a98ad63868774cf1558e6159b6a8b6593/proposal/11-roadmap.md?format=markdown)

```
# Roadmap

Phases sized for an agent-amplified team of 1–3 humans (D-008): strictly serial in their load-bearing dependencies, each producing something independently useful, each with a gate that must hold before the next phase stacks on it. Calendar estimates are deliberately absent; ordering and gates are the commitments.

## Phase 0 — Foundations on paper

**Build:** the core-calculus note for the phase-1/2 judgment set ([OP-7](open-problems.md) down-payment); the architectural-IR node catalog with laws; the diagnostic object schema (P-9); CI skeleton with pinned firtool.
**Gate:** the phase-1 feature set has written typing rules someone has adversarially reviewed (this is what the probing phase of this proposal begins).

## Phase 1 — Typed structural language

**Build:** widths + numeric domains ([02 §4](02-type-system-core.md)); nominal clock/reset domains + opaque newtypes ([02 §5](02-type-system-core.md)); `{0,1,ω}` grades + phase modalities ([02 §2–3](02-type-system-core.md)); explicit iteration forms; typestate-over-linearity pattern; single-clock `later` for registers/feedback ([03 §5](03-time-and-resources.md)); budgeted deterministic comptime ([07 §7](07-compiler-architecture.md)); architectural IR with the ledger's identity/representation/temporal categories; lowering to hw/comb/seq → SV ([07 §2](07-compiler-architecture.md)); arcilator simulation; structure reports (P-2); the language module system and forge v0 — manifest, lockfile, workspaces, path resolution ([13 §2, §6–7](13-package-system.md)); `strata fmt` with its CI-fuzzed invariants and the provenance-stability rule ([14 §1–5](14-toolchain.md)); `strata lint` v0 over the phase-1 ledger categories, with `expect`-only suppression ([14 §7–10](14-toolchain.md)); `strata-ls` at Tier A — resident daemon, bound-level diagnostics/completion/hover, R-LS-1's no-second-frontend invariant with its CI diff oracle, plus the tree-sitter grammar and Zed reference extension with corpus conformance ([14 §15–19](14-toolchain.md)).
**Designs:** counters, FIFOs, arbiters, simple pipelines — the stdlib that later phases verify.
**Gate:** an experienced hardware engineer ports a nontrivial FIFO/arbiter design; generated SV is reviewably equivalent to hand-written; the CDC/width/reset bug class is demonstrably rejected with P-9-quality diagnostics.

## Phase 2 — Time, resources, contracts

**Build:** events + static-interval temporal capabilities with conflict-freedom checking ([03 §3](03-time-and-resources.md)); schedule witnesses ([03 §4](03-time-and-resources.md)); capacity/credit tokens ([03 §6](03-time-and-resources.md)); Tier-1/Tier-2 refinements with stable obligations ([06 §1](06-refinements-and-evidence.md)); protocol catalog (ready_valid, credit, burst, request_response) with duality checking ([04 §1](04-protocols-and-streams.md)); first-class `arbitrate`; typed CDC bridges with contracts; contract declarations compiling to assertions; component summaries + incremental composition ([07 §6](07-compiler-architecture.md)); mechanical summary semver on top of them ([13 §3](13-package-system.md)).
**Designs:** packet router, DMA engine, memory interface.
**Gate:** the OP-4 line holds (obligation generation vs scheduling stays crisp on the router's shared-resource paths); Tier-2 outcomes are reproducibly stable across solver versions on the test corpus ([OP-3](open-problems.md) evidence); ledger coverage on the elaborate→schedule→emit path stays useful ([OP-6](open-problems.md) metric).

## Phase 3 — Verification generation

**Build:** declaration-generated assertions/monitors/generators ([08 §1](08-verification-platform.md)); typed strategies + stateful rule testing with integrated choice-sequence shrinking ([08 §2](08-verification-platform.md)); coverage model + corpus manager; metamorphic properties; differential lockstep harness (RVFI-class interface, Spike/Sail bindings) ([08 §4](08-verification-platform.md)); mutation scoring via MCY-style flow ([08 §6](08-verification-platform.md)); SymbiYosys integration; evidence lattice wired end-to-end ([06 §3](06-refinements-and-evidence.md)).
Also: forge registry v1 — immutable versions, summary indexing, contract search, proof-artifact dependencies, config-coverage publication gate ([13 §2, §4](13-package-system.md)); the stdlib publishes through it (P-11).
**Targets:** the phase-1 stdlib first (P-11), then a cache and memory controller.
**Gate:** a seeded-bug study on the cache: the generated verification catches ≥ an agreed fraction of mutation classes with zero hand-written testbench code; shrunk counterexamples are human-readable.

## Phase 4 — Formal + speculation + agents

**Build:** symbolic values + BMC integration with witness-to-seed pipeline ([08 §5](08-verification-platform.md)); speculation epochs + authority capabilities with the squash-boundary rule ([05 §2–3](05-speculation-authority-effects.md)); reset epochs with ambient containment ([05 §4](05-speculation-authority-effects.md)); Rast-lineage user protocols ([04 §2](04-protocols-and-streams.md)); agent workspace protocol + experiment database + diagnostics-driven repair loop ([09](09-agent-system.md)); FPGA HIL v1 ([10](10-fpga-loop.md)).
**Targets:** an in-order pipelined RISC-V core with full differential + formal-assisted loop; agents closing simple repair loops unsupervised.
**Gate:** OP-1's firewall rule survives contact with a real speculative load queue; OP-2's containment holds (measure epoch-index appearance rate in user signatures); the OP-5 metric (agent repair success from structured diagnostics alone) is tracked and improving.

## Phase 5 — Optimization under contracts + scale

**Build:** equivalence-classed optimizer passes with proof-carrying levels A–D ([07 §4](07-compiler-architecture.md)); translation-validated agent rewrites; schedule search; synthesis feedback loop closed ([10 §2](10-fpga-loop.md)); out-of-order core as the forcing target.
**Gate:** an agent-proposed retiming/topology change lands with zero human RTL review — admitted purely by translation validation + contract checks — on the OoO core.

## Deferred (north star, revisit each phase boundary)

Per D-023 and per-doc north-star sections: dynamic-latency capabilities ([OP-8](open-problems.md); entry criterion in [03](03-time-and-resources.md)); revocable intervals ([OP-1](open-problems.md)); menu semirings / dependent multiplicities; multi-clock guarded modality; four-state typing; multiparty protocols; and full mechanized core calculus — staging fixed by the wave-2 probe ([OP-7](open-problems.md)): the λ-strata⁰ checker (`probes/core-calculus/`) stays green as a **phase-2 gate** with per-feature break-hunt reruns; **full mechanization (est. 2–4 person-months, Lean/Coq) is the phase-3 entry gate**. Observer projections and digital power/reconfiguration lifecycle schemas may enter under the systems-safety staging below; full information-flow closure, analog leakage, and electrical power semantics remain deferred.

### Systems-safety expansion, probe-staged

The 2026-07-21 systems-safety wave (`probes/fault-health`, `dma-iommu`, `progress-waitfor`, `memory-consistency`, `observer-flow`, `physical-constraints`, `power-reconfig`, `numeric-error`, `dft-debug`, `assurance-cases`) supports extension through existing seams rather than new top-level judgments:

- **Phase 2 candidates:** factor the generic invalidation kernel; add finite wait-for summaries with stable `proved/refuted/obligation`; define enforced mapping leases/borrows and opaque owner-validated generations. Promotion requires larger multi-entry/ATS/parameterized re-probes.
- **Phase 3 candidates:** generated fault campaigns and recovery monitors; partial memory-event summaries with explicit completeness; deterministic assurance dependency graphs. Full RVWMO remains out until checked against a standard model with mixed-size/per-byte behavior.
- **Phase 4 candidates:** component-local health invalidation and observer-projection support in the reference semantics, with noninterference remaining Tier-3 relational verification.
- **Phase 5 candidates:** approximation-aware transforms and DFT insertion certificates. Timing-exception generation is corrected now: source facts produce candidates, and exact post-synthesis binding/precedence validation is mandatory before admission (D-086).
- **Remain deferred:** analog power leakage, electrical power intent, multi-region reconfiguration liveness, full coherence-model composition, probabilistic noninterference, and general numeric error algebra. The bounded probes establish interfaces, not those global claims.

Promotion is per family, never as one “systems safety” feature flag. Each candidate must preserve the sparse-summary rule, show P-9 diagnostics, define artifact invalidation, and pass an integrated target—not merely its small model. The first integrated proving wave is: (1) fault-contracted MSHR; (2) CHI/NoC wait-for corpus; (3) DMA–IOMMU–interrupt slice; (4) netlist-bound timing-constraint generator. Later families cannot bypass those gates by citing the assurance graph.

## Staging map for refine-1's recommendations

For traceability: refine-1 §§1–3,5,6,11,14,31,32,34 → Phases 0–1. §§4,15,16,18–20,25,26,36,42 → Phase 2. §§40 (evidence), 21–22 partially → Phases 2–3. §§7,13,23,35,49 → Phase 4. §§21–24,41,48 fully → Phase 5. §§17,27,28,29(four-state),37 + dependent multiplicities → Deferred. §§43,44,50 are absorbed into principles and this staging itself.

```