pulseengine · avrabe · Apr 22, 2026 · Apr 22, 2026
diff --git a/docs/design/doc-reality-audit.md b/docs/design/doc-reality-audit.md
@@ -0,0 +1,194 @@
+# Documentation-Reality Audit
+
+Date: 2026-04-19
+Scope: README, docs/, CHANGELOG, AGENTS.md, CLAUDE.md, vscode-rivet/README.md,
+schemas, CLI help strings. Evidence only; no fixes applied.
+
+## 1. TL;DR
+
+28 mismatches found. 4 HIGH, 14 MEDIUM, 10 LOW. Top offenders: (1) Kani
+CI job and Verus/Rocq are soft-gated (`continue-on-error: true`) while the
+v0.4.0 CHANGELOG bullet reads "wired into CI" without qualification on the
+Kani line; (2) `docs/schemas.md` documents 5 schemas while `schemas/` ships
+27; (3) `docs/audit-report.md` (dated 2026-03-09) still claims fuzz and
+mutation testing are "NOT IMPLEMENTED" — both shipped months ago; (4) README
+dogfood block hard-codes "447 artifacts across 19 types", while the regenerated
+AGENTS.md managed section reports 518, and raw ID counts in `artifacts/` and
+`safety/` are higher still. Systemic pattern: every hand-maintained count in
+prose is out of date, because the project has no CI check that numbers in
+prose match `rivet stats` / `rivet list` output.
+
+## 2. The Register
+
+| File:line | Claim (short) | Reality | Type | Severity |
+|---|---|---|---|---|
+| README.md:53 | "235+ Playwright E2E tests" | `tests/playwright/*.spec.ts` has 29 files, ~326 `test(` calls | Out-of-date | LOW |
+| README.md:177 | "447 artifacts across 19 types" | AGENTS.md managed block says 518; rivet.yaml still pins project version 0.1.0 | Out-of-date | MEDIUM |
+| README.md:188 | "uca 57" in dogfood block | AGENTS.md and `.rivet/agent-context.md` both say 59 | Out-of-date | LOW |
+| README.md:172 | "Built-in domain schemas (8 schemas)" | `ls schemas/` → 27 files incl. do-178c, iec-61508, iec-62304, en-50128, iso-pas-8800, sotif, score, safety-case, eu-ai-act, and 9 bridge schemas | Out-of-date | MEDIUM |
+| README.md:199 | "cargo test --all  # 500+ tests" | Unverified from outside; count is not CI-published anywhere | Implementation-hidden | LOW |
+| README.md:47 | "`rivet export --gherkin` generates .feature files" | CLI takes `--format gherkin`, not `--gherkin` (rivet-cli/src/main.rs:4230) | Out-of-date | LOW |
+| README.md:51 | "`rivet init --agents` generates AGENTS.md (25+ tools)" | Accurate (36+ CLI subcommands in `enum Command` at rivet-cli/src/main.rs:162-715) | Accurate | — |
+| CHANGELOG.md:7 | "Verus + Rocq jobs wired into CI via Bazel" on main feature bullet | `.github/workflows/ci.yml:392,404,423` all `continue-on-error: true`; Kani job also soft-gated | Silent-fail | HIGH |
+| CHANGELOG.md:36-37 | CI section admits "marked `continue-on-error: true` pending toolchain stabilization" — but only for Verus/Rocq | Kani is *also* `continue-on-error: true` (ci.yml:392). CHANGELOG implies Kani is hard-gated ("enabled — previously commented out"). | Silent-fail | HIGH |
+| CHANGELOG.md:29 | "27 Kani BMC harnesses" | `grep -c "#[kani::proof]" rivet-core/src/proofs.rs` → 27 exact | Accurate | — |
+| CHANGELOG.md:82 | "235+ Playwright E2E tests across 22 spec files" | 29 files, ~326 tests today | Out-of-date | LOW |
+| docs/schemas.md:11-17 | Schema table lists 5 schemas (common, dev, stpa, aspice, cybersecurity) | 27 schema files present incl. 10+ domain schemas and 9 bridge schemas not documented | Out-of-date | HIGH |
+| docs/schemas.md | No section for `feature-model` YAML (user issue #3) | `rivet-core/src/feature_model.rs` loads kind:feature-model YAML; `examples/variant/feature-model.yaml` is the only example | Implementation-hidden | MEDIUM |
+| docs/audit-report.md:130 | "Fuzz Testing — Status: NOT IMPLEMENTED" | `fuzz/fuzz_targets/` has 5 targets (yaml, reqif, schema merge, needs-json, document) | Out-of-date | HIGH |
+| docs/audit-report.md:150 | "Mutation Testing — Status: NOT IMPLEMENTED" | `.github/workflows/ci.yml:288-333` runs cargo-mutants on both rivet-core and rivet-cli | Out-of-date | HIGH |
+| docs/audit-report.md:220 | "MSRV 1.89" | Matches Cargo.toml:14 (`rust-version = "1.89"`) | Accurate | — |
+| docs/verification.md:137 | "msrv 1.85" in CI gate table | Cargo.toml says 1.89; CI uses dtolnay/rust-toolchain@1.89.0 | Out-of-date | MEDIUM |
+| docs/srs.md:85 | "[[REQ-011]] pins Rust edition 2024 with MSRV 1.85" | MSRV is 1.89 | Out-of-date | MEDIUM |
+| docs/getting-started.md:465 | "Supported formats: `reqif`, `generic-yaml`" | `cmd_export` accepts reqif, generic-yaml, generic, html, gherkin, zola (rivet-cli/src/main.rs:4225-4232) | Out-of-date | MEDIUM |
+| docs/getting-started.md:863 | "MCP Server — exposes 15 tools" | Count matches (mcp.rs `fn rivet_*` count: validate, list, stats, get, coverage, schema, embed, snapshot_capture, add, query, modify, link, unlink, remove, reload) | Accurate | — |
+| docs/getting-started.md:839-840 | Only `rivet_artifact` and `rivet_stats` Zola shortcodes listed | Unverified; Zola shortcodes generated by `--shortcodes` flag — doc does not list the full set | Implementation-hidden | LOW |
+| docs/architecture.md:85 | "`oslc` — OSLC client for discovery, query, CRUD, and sync (feature-gated)" | `rivet-core/src/oslc.rs` is 1911 lines and *not* feature-gated in rivet-core/Cargo.toml (builds unconditionally); there is no `rivet oslc` or `rivet sync --oslc` subcommand | Aspirational | MEDIUM |
+| docs/architecture.md:269-275 | Schema table lists same 5 schemas as schemas.md | Same mismatch — 27 files exist | Out-of-date | MEDIUM |
+| docs/stpa-sec.md:120 | "Current mitigations in place as of v0.2.0-dev" | Workspace is v0.4.0 | Version-stale | MEDIUM |
+| docs/stpa-sec.md:127-129 | "SSC-1 Provenance check — Phase 3 / Planned" | Phase 3 features largely shipped in v0.4.0; status unverified but banner stale | Version-stale | LOW |
+| docs/roadmap.md:104-116 | "Phase 3 — Sync & Extensibility (Planned)" | v0.4.0 shipped variant/PLE, MCP, Zola export, rowan/salsa, Kani, sphinx-needs import; roadmap document itself never updated past Phase 3 section | Out-of-date | MEDIUM |
+| vscode-rivet/README.md:46 | "`cargo install rivet-cli`" | rivet-cli depends on rivet-core as a path dep; never published to crates.io; no publish CI for it | Aspirational | HIGH |
+| vscode-rivet/package.json:6 | `"version": "0.3.0"` | Workspace is 0.4.0 | Version-stale | MEDIUM |
+| CLAUDE.md:4 | "A Claude Code pre-commit hook runs `rivet validate` before each commit (configured in `.claude/settings.json`)" | Hook exists but `rivet init --hooks` installs one that requires `python3` to parse JSON (rivet-cli/src/main.rs:2480). Not documented as a dependency. | Implementation-hidden | MEDIUM |
+| docs/getting-started.md:720-752 | S-expression predicates/quantifiers listed | Matches `rivet-core/src/sexpr_eval.rs`; `(reachable-from ...)`, `forall`, `exists` present | Accurate | — |
+| docs/getting-started.md:722 | "s-expressions — one syntax for CLI, API, constraints, and queries" | Query engine in `rivet-core/src/query.rs` uses a *separate* `Query` struct (type/status/tags); only `--filter` on CLI takes s-expressions | Implementation-hidden | LOW |
+| (various) | `{{query:...}}` and `{{group:...}}` embed tokens referenced in session prompt | No such tokens in code. `embed.rs` supports stats, coverage, diagnostics, matrix, artifact, links, table. No query/group. | N/A (never claimed in repo docs) | — |
+
+Tokens `{{query:...}}`, `{{group:...}}`, `rivet discover`, `rivet gaps`,
+`rivet variant check-all` do **not** appear anywhere in the repo's doc files
+(grep of `docs/`, `README.md`, `CHANGELOG.md`, `AGENTS.md` produced zero
+matches for each). They were hypothesised in the audit prompt but the repo
+is clean of those specific aspirational terms.
+
+## 3. Top 3 most-misleading
+
+### 3.1 Kani/Verus/Rocq "wired into CI" (CHANGELOG.md:7, 36)
+
+Claim (CHANGELOG.md:7): "Kani BMC expanded from 15 to 27 harnesses
+covering the core public API, Verus/Rocq jobs wired into CI via Bazel".
+Claim (CHANGELOG.md:36): "Kani job enabled — previously commented out".
+
+Reality (.github/workflows/ci.yml:392, 404, 423): all three jobs are
+`continue-on-error: true`. Proof regressions cannot block merge.
+CHANGELOG.md:37 discloses this for Verus/Rocq in a parenthetical but
+omits Kani, and the headline bullet omits all three.
+
+Why misleading: a reader evaluating rivet for ISO 26262 / TCL 3 tool
+qualification will conclude formal verification is hard-gated — the
+headline v0.4.0 feature — when in practice regressions are silent.
+
+Remediation: either flip jobs to hard-gate or add "(soft-gated, pending
+toolchain stabilization)" to every CHANGELOG mention including Kani.
+Effort S.
+
+### 3.2 audit-report.md says fuzz + mutation "NOT IMPLEMENTED" (docs/audit-report.md:130, 150)
+
+Claim (130, 150): "**Status: NOT IMPLEMENTED**" for both fuzz and
+mutation testing.
+
+Reality: `fuzz/fuzz_targets/` has 5 targets (yaml, reqif, schema-merge,
+document, needs-json). `.github/workflows/ci.yml:288-333` runs
+`cargo mutants` on both crates and uploads reports.
+
+Why misleading: this 2026-03-09 doc is the canonical "quality audit".
+An auditor consulting it will misjudge test-effectiveness posture; the
+"Overall 73%" score is calibrated against the missing-fuzz/mutation
+lines.
+
+Remediation: delete or stamp "superseded by v0.4.0 verification
+pyramid". Effort S.
+
+### 3.3 schemas.md documents 5 of 27 schemas (docs/schemas.md:11-17)
+
+Claim: table listing common, dev, stpa, aspice, cybersecurity.
+
+Reality: `ls schemas/` → 27 files. Missing from docs: do-178c,
+en-50128, iec-61508, iec-62304, iso-pas-8800, sotif, stpa-sec, stpa-ai,
+safety-case, score, aadl, eu-ai-act, research, supply-chain, and 9
+`.bridge.yaml` files. The feature-model YAML kind (issue #3) is also
+undocumented apart from a code block in getting-started.md.
+
+Why misleading: a user adopting rivet for IEC 61508 or DO-178C will
+see no mention in docs/schemas.md that these schemas exist, and will
+likely write their own. The schemas ship but silently.
+
+Remediation: regenerate from `rivet schema list` + `rivet schema show
+<name>`; add feature-model section. Effort M.
+
+## 4. Systemic Patterns
+
+1. **Prose counts drift.** Every hand-coded number in `.md` files
+   (447 artifacts, 500+ tests, 235+ Playwright tests, MSRV 1.85) is
+   stale. Regenerated sections (AGENTS.md managed block,
+   `.rivet/agent-context.md`) are correct; free-form prose isn't.
+   No CI check compares prose to `rivet stats` output.
+
+2. **Soft-gate semantics hidden from CHANGELOG.** Three of four
+   verification pyramid jobs (kani, verus, rocq) use
+   `continue-on-error: true`; CHANGELOG qualifies only two, only
+   in a parenthetical, not in the headline bullet.
+
+3. **Stale snapshot docs never superseded.** audit-report.md,
+   roadmap.md, architecture.md §8, verification.md were written
+   for earlier releases and never refreshed. No "superseded"
+   marker, no `last-verified` frontmatter date, no CI that fails
+   when a doc references a deleted module/subcommand.
+
+4. **Cross-file divergence on identical facts.** README vs AGENTS.md
+   cite different UCA counts (57 vs 59) and artifact totals
+   (447 vs 518). No authoritative source.
+
+5. **Unverified "feature-gated" claims.** architecture.md marks
+   oslc and wasm_runtime as feature-gated; only `wasm` is actually
+   a Cargo feature; `oslc` builds unconditionally.
+
+## 5. Remediation Plan for v0.4.1
+
+Ranked by impact/effort:
+
+| # | File | Change | Effort |
+|---|---|---|---|
+| 1 | CHANGELOG.md:7, 36 | Add "(soft-gated, pending toolchain stabilization)" to Kani and headline Verus/Rocq bullets, or hard-gate Kani | S |
+| 2 | docs/audit-report.md | Either delete (stale point-in-time) or rewrite to reflect fuzz/mutants/Kani/Verus/Rocq that now ship | M |
+| 3 | docs/schemas.md | Regenerate from `rivet schema list` for all 27 schemas; add feature-model section | M |
+| 4 | docs/architecture.md:269-275, §8 | Update schema table; rewrite "Phase 3 Architecture Extensions" into a "what-shipped-in-v0.4.0" section | M |
+| 5 | docs/roadmap.md | Reflect that Phase 3 and much of Phase 3 extensions shipped | S |
+| 6 | docs/verification.md:137 | MSRV 1.85 → 1.89 | S |
+| 7 | docs/srs.md:85 | MSRV 1.85 → 1.89 | S |
+| 8 | README.md:177-193 | Replace hand-coded 447 / per-type counts with a note: "Run `rivet stats` for live counts." Remove 57 UCAs. | S |
+| 9 | README.md:172 | "8 schemas" → "25+ domain schemas" or live count | S |
+| 10 | README.md:47 | `rivet export --gherkin` → `rivet export --format gherkin` | S |
+| 11 | README.md:53, 199, 203 | "235+ Playwright", "500+ tests" → strip numbers or link to CI badge | S |
+| 12 | vscode-rivet/package.json:6 | Bump to 0.4.0 (align with workspace) | S |
+| 13 | vscode-rivet/README.md:46 | Replace `cargo install rivet-cli` with `cargo install --path rivet-cli --git ...` or link to releases | S |
+| 14 | docs/stpa-sec.md:120-129 | Remove "v0.2.0-dev" banner; refresh SSC implementation status table | S |
+| 15 | docs/getting-started.md:465 | "Supported formats: reqif, generic-yaml" → add html, gherkin, zola | S |
+| 16 | docs/architecture.md:85 | oslc: drop "(feature-gated)" wording or actually gate it | S |
+| 17 | CLAUDE.md | Note `rivet init --hooks` requires python3 at runtime | S |
+| 18 | (new) `docs/design/json-output-schema.md` | Publish the stable JSON envelope schema FEAT-025 claims | L |
+| 19 | (new CI check) | Lint that fails when `.md` contains a count that differs from live `rivet stats` | L |
+
+## 6. What the Docs Should STOP Claiming
+
+Until genuinely shipped and hard-gated:
+
+- **"Verus + Rocq wired into CI"** / **"Kani job enabled"** without a
+  "(soft-gated)" qualifier on every mention.
+- **"NOT IMPLEMENTED" banners on fuzz/mutation** in audit-report.md.
+- **"OSLC feature-gated"** in architecture.md (gate in Cargo.toml or
+  drop the qualifier).
+- **Hand-coded artifact counts** in README, CHANGELOG v0.2.0 subsection
+  claims (e.g. "31 adversarial threat artifacts"), docs/srs.md STPA ID
+  ranges. Replace with a single "live counts via `rivet stats`".
+- **`cargo install rivet-cli`** in vscode-rivet/README.md — not possible
+  without crates.io publish. Use `--git` install form or publish.
+- **Stable JSON output envelope** (FEAT-025) — claimed shipped but no
+  schema is published in docs/.
+
+---
+
+Evidence: README.md, CHANGELOG.md, AGENTS.md, CLAUDE.md, docs/{schemas,
+verification, srs, architecture, audit-report, getting-started, stpa-sec,
+roadmap}.md, vscode-rivet/{README.md,package.json}, .github/workflows/ci.yml,
+rivet-core/src/{proofs,embed}.rs, rivet-cli/src/main.rs, Cargo.toml.