Roadmap to 2.0 (rivet-tracked): reality track → capability track

[avrabe]

Roadmap to 2.0 — planning only (no feature implementation)

Adds the typed-traceability backing for the 2.0 line + the narrative.
Left open for review rather than self-merged: this is a plan to
approve, not a release to ship.

What's in it

• artifacts/roadmap-2.0.yaml — 15 new rivet artifacts (rivet validate PASS):
  • Research (deep-research 2026-05-30, verified primary sources): TE-008 TrustInSoft+Rust (GA 2025-11-04), TE-009 Polyspace, TE-010 Frama-C EVA (Zinc 30.0), MF-005 (no commercial sound analyzer offers mechanized soundness; none targets Wasm — scry's niche). Academic-frontier / Wasm-ecosystem citations were flagged thin by the research and are deliberately not fabricated.
  • DD-011 — close the analyzer↔composed-artifact decoupling (the v1.0.1 open finding); the foundational reality-track decision.
  • REQ-009 (shipped artifact embeds + runs the analyzer), REQ-010 (analyzer decision logic carries MC/DC evidence).
  • Feature ladder (status: proposed): reality FEAT-013/014/015 (v1.1–1.3), capability FEAT-016..020 (v1.4–2.0).
  • G-005 — scry is itself qualifiable to the commercial bar, differentiated by mechanized soundness.
• docs/roadmap-2.0.md — narrative: the three v1.0 structural gaps, the competitive thesis, the per-minor capability ladder.

The thesis

v1.0 added breadth (domains + proofs) but the shipped //:scry is hollow (4.6 KB, analyzer not embedded, analyze() never runs). 2.0 = depth: make the shipped artifact actually do — and be measured doing — what the dossier claims (reality track), then add capability on a real foundation (capability track). scry's defensible niche per the research: the only sound Wasm analyzer whose soundness is a machine-checked theorem, not a vendor design claim.

Verification

rivet validate PASS — 86 artifacts, the new doc + 15 artifacts load clean; the only warning is the pre-existing roadmap.md (no frontmatter), unrelated.

Out of scope / flagged separately

A pre-existing uncommitted ci.yml change (scry-taint lint/test steps never landed on main) was found during this work and deliberately excluded from this planning PR — see PR discussion.

🤖 Generated with Claude Code

[avrabe]

Correction to the PR description above (honest record): when I opened this PR the description said "rivet validate PASS — only the pre-existing roadmap.md warning." That was wrong — at open there were 26 rivet warnings (≈18 from this branch's new artifacts' un-linked prose mentions, plus 8 pre-existing on main from the v1.0 capstone).

Both are now fixed (commit f3c0bbc):

1. Added the typed links the new roadmap artifacts' prose names.
2. Restored typed links dropped from FEAT-011 / Sn-005 / Sn-006 during the v1.0 PR (FEAT-011: v1.0 capstone — full-stack mechanized soundness + six-domain credit dossier #25) — on disk FEAT-011 had only REQ-002/AC-005/AC-003; the REQ-001/REQ-005/TE-004/FEAT-010/G-001/G-002 edges its prose references had silently failed to land that turn. That means v1.0 shipped with 8 rivet warnings — a real prior-turn miss, corrected here.

rivet validate is now PASS (0 warnings). Still planning-only; no feature code.

[avrabe]

Follow-up correction (keeping the record honest): commit aa58066 — the one I described above as bringing rivet to PASS (0 warnings) — actually regressed it to FAIL (8 errors). The typed links I added to clear the bidirectional-mention warnings used type-invalid predicates (a technology-evaluation may only traces-to requirement/design-decision; a market-finding only requirement/feature — I pointed them at sibling TEs and features). I committed that without checking the result line — my mistake.

Fixed forward in 9aa6f30: removed the invalid links (the MF↔TE edges still exist via each TE's valid addresses-finding → MF-005), reworded the prose that bare-cited un-linkable sibling IDs, and dropped an unschema'd field on FEAT-016.

rivet validate is now genuinely PASS (0 warnings, 0 errors) — verified the result line before committing this time.

[github-actions]

📐 rivet artifact delta

PR: #27 Base SHA: 4b686048

Validation

head — `rivet validate` result

Loaded 8 documents with 123 artifact references

Diagnostics:
  INFO: [G-005] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped

  INFO: [G-001] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped

  INFO: [G-002] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped

  INFO: [G-003] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped

  INFO: [G-004] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped

  INFO: [G-005] Top-level safety goals should have context defining scope and assumptions
  INFO: [G-001] Top-level safety goals should have context defining scope and assumptions
  INFO: [G-002] Top-level safety goals should have context defining scope and assumptions
  INFO: [G-003] Top-level safety goals should have context defining scope and assumptions
  INFO: [G-004] Top-level safety goals should have context defining scope and assumptions

Result: PASS (0 warnings)

base — `rivet validate` result (for comparison)

  WARN: [FEAT-011] prose mentions 'TE-004' but no typed link to it; add a link in `links:` or remove the mention
  WARN: [FEAT-011] prose mentions 'REQ-001' but no typed link to it; add a link in `links:` or remove the mention
  WARN: [FEAT-011] prose mentions 'REQ-005' but no typed link to it; add a link in `links:` or remove the mention
  WARN: [FEAT-011] prose mentions 'G-002' but no typed link to it; add a link in `links:` or remove the mention
  WARN: [FEAT-011] prose mentions 'FEAT-010' but no typed link to it; add a link in `links:` or remove the mention
  WARN: [Sn-006] prose mentions 'TE-004' but no typed link to it; add a link in `links:` or remove the mention
  INFO: [G-001] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped

  INFO: [G-002] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped

  INFO: [G-003] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped

  INFO: [G-004] Every safety goal must be supported by evidence (solution) or decomposed into sub-goals (via strategy), unless marked undeveloped

  INFO: [G-001] Top-level safety goals should have context defining scope and assumptions
  INFO: [G-002] Top-level safety goals should have context defining scope and assumptions
  INFO: [G-003] Top-level safety goals should have context defining scope and assumptions
  INFO: [G-004] Top-level safety goals should have context defining scope and assumptions

Result: PASS (8 warnings)

Artifact stats

	base	head
Total artifacts	69	85

full stats — head

Artifact summary:
  academic-reference               11
  design-decision                  11
  feature                          20
  market-finding                    5
  requirement                      10
  safety-context                    3
  safety-goal                       5
  safety-justification              3
  safety-solution                   6
  safety-strategy                   1
  technology-evaluation            10
  TOTAL                            85

Diagnostics: 0 error(s), 0 warning(s), 10 info(s)

Diff (base → head)

+ DD-011  Close the analyzer↔composed-artifact decoupling so the shipped artifact embeds and runs the analyzer
+ FEAT-013  v1.1 — Composition-gap fix: shipped artifact embeds and runs the analyzer
+ FEAT-014  v1.2 — witness MC/DC on the analyzer (closes the long-standing structural-coverage gap)
+ FEAT-015  v1.3 — Live end-to-end soundness oracle (un-skip the abstract-vs-concrete harness)
+ FEAT-016  v1.4 — Analyzer loop-carried octagon relational fixpoint (use the octagon, not just ship it)
+ FEAT-017  v1.5 — SpecTec soundness-by-construction backend (promote the deferred prototype)
+ FEAT-018  v1.6 — Component-Model handle-state / use-after-drop (deferred FEAT-002 slice)
+ FEAT-019  v1.7 — Differential precision corpus vs Wanilla / Wassail (falsify precision externally)
+ FEAT-020  v2.0 — Tool-qualification dossier: match the commercial bar, differentiated by mechanized soundness
+ G-005  scry is itself qualifiable to the commercial sound-analyzer bar, differentiated by mechanized soundness
+ MF-005  No commercial sound analyzer offers mechanized soundness, and none targets Wasm — scry's niche
+ REQ-009  The shipped scry artifact shall embed and execute its analyzer
+ REQ-010  The analyzer's decision logic shall carry structural (MC/DC) coverage evidence
+ TE-008  TrustInSoft Analyzer — sound analysis adds Rust (2025.10, with Ferrous Systems)
+ TE-009  MathWorks Polyspace Code Prover — sound abstract-interpretation prover (commercial bar)
+ TE-010  Frama-C EVA — open-source sound C value analysis (Zinc 30.0, 2024-12-06)
~ FEAT-011
  link: + depends-on -> FEAT-010
  link: + evaluates-tech -> TE-004
  link: + traces-to -> G-001
  link: + traces-to -> G-002
  link: + traces-to -> REQ-001
  link: + traces-to -> REQ-005
~ Sn-005
  link: + traces-to -> REQ-001
~ Sn-006
  link: + evaluates-tech -> TE-004

16 added, 0 removed, 3 modified, 66 unchanged

+ RESOLVED    WARN: [Sn-006] prose mentions 'TE-004' but no typed link to it; add a link in `links:` or remove the mention
+ RESOLVED    WARN: [FEAT-011] prose mentions 'G-001' but no typed link to it; add a link in `links:` or remove the mention
+ RESOLVED    WARN: [FEAT-011] prose mentions 'TE-004' but no typed link to it; add a link in `links:` or remove the mention
+ RESOLVED    WARN: [FEAT-011] prose mentions 'REQ-001' but no typed link to it; add a link in `links:` or remove the mention
+ RESOLVED    WARN: [FEAT-011] prose mentions 'REQ-005' but no typed link to it; add a link in `links:` or remove the mention
+ RESOLVED    WARN: [FEAT-011] prose mentions 'G-002' but no typed link to it; add a link in `links:` or remove the mention
+ RESOLVED    WARN: [FEAT-011] prose mentions 'FEAT-010' but no typed link to it; add a link in `links:` or remove the mention
+ RESOLVED    WARN: [Sn-005] prose mentions 'REQ-001' but no typed link to it; add a link in `links:` or remove the mention
0 new errors, 0 resolved errors, 0 new warnings, 8 resolved warnings

AADL model — head

spar/scry.aadl: OK

---

Posted by the rivet-delta workflow. Informational only — does not gate the PR.