Tracking: pulseengine-wide V&V coverage initiative

[avrabe]

Goal

Coordinate adoption of V&V techniques across all pulseengine production repositories so that every safety-critical project has the same baseline coverage and the certification story is consistent end-to-end.

Operating principle: overdo on testing rather than undercommit. Child issues are deliberately granular so per-repo agents can work them independently.

The four-gate pipeline (reference architecture)

Every production push should pass four gates before hardware:

1. Pre-commit hooks — fast shift-left checks (rivet's 21-hook template is the reference)
2. Bazel test //... — hermetic test + proof gate
3. GitHub Actions CI — Miri, sanitizers, proptest, fuzz smoke, differential, mutation, integration
4. cargo-kiln verify-matrix — ASIL profile gate before release

Coverage matrix (current state)

Technique	Coverage today
Verus SMT	kiln, rivet, sigil (partial)
Kani bounded MC	kiln, rivet, z/gale, relay, meld, sigil, wohl (7 repos, 2000+ proofs)
Rocq theorem proving	meld (28 files), synth (24), relay (5), z/gale (partial), loom (partial)
Lean 4 + Mathlib	z/gale (2k lines), spar (592), relay (459), sigil (203)
Aeneas (Rust→Lean)	Scaffolded in rules_lean; blocked on hermetic Charon (see pulseengine/rules_lean#1)
Loom Z3 translation validation	pulseengine/loom (WASM optimizer, bespoke)
proptest	17 repos
tokio-rs/loom concurrency	thrum only (archived)
Miri	rivet (in CI), kiln (tool-versioned)
Sanitizers (ASAN/TSAN/LSAN)	z/gale (wired in .cargo/config.toml)
cargo-fuzz	9 repos, 80+ targets
Differential testing	loom, relay, rivet
Mutation testing (cargo-mutants)	rivet (pre-commit)
criterion benchmarks	9 repos
Rivet traceability	13 repos with rivet.yaml

Phases and child issues

Phase 1 — Stop bleeding (visibility / CI hygiene)

• Resurrect 6 disabled GitHub workflows (kani-verification, kani-regression, capability_tests, status-dashboard, deploy-verification, docs-deploy) kiln#237 — resurrect 6 disabled GitHub workflows
• Re-enable .githooks/pre-commit.disabled and align with rivet's 21-hook template kiln#238 — re-enable .githooks/pre-commit.disabled
• Add GitHub Actions CI surfacing existing Bazel + Kani + proptest + sanitizer verification gale#21 — add GitHub Actions CI
• Add GitHub Actions CI for Lean proofs + proptest + Bazel tests spar#135 — add GitHub Actions CI
• Add GitHub Actions CI for Kani + proptest + fuzz verification wohl#1 — add GitHub Actions CI
• Add GitHub Actions CI for 25 Bazel test targets + fuzz + differential + Rocq/Lean proofs relay#5 — add GitHub Actions CI
• automator: add GitHub Actions CI (repo archived; skipped)

Phase 2 — Formal methods adoption

• Add Kani harnesses for stream-transformer state machines (LC, SCH, SC, HS, CFDP) relay#6 — Kani harnesses for stream-transformer state machines
• Add Kani harnesses for ARINC653 solver invariants (constraint-satisfaction / MILP) spar#136 — Kani for ARINC653 solver invariants
• Add Kani harnesses for crypto parsers (varint, DSSE envelope, signature verification) sigil#88 — Kani for crypto parsers
• Add Kani + proptest harnesses for fusion edges (parser, merger, resolver) meld#102 — Kani + proptest for fusion edges
• automator: Verus contracts for orchestration state machine (repo archived; skipped)

Phase 3a — tokio-rs/loom concurrency

• Add tokio-rs/loom concurrency harnesses for Atomic, RingBuf, PriorityQueue primitives gale#22 — harnesses for Atomic, RingBuf, PriorityQueue
• Add tokio-rs/loom harnesses for stream-channel backpressure relay#7 — harnesses for stream-channel backpressure
• Add tokio-rs/loom concurrency harnesses for async-runtime scheduler kiln#239 — harnesses for async-runtime scheduler

Phase 3b — criterion benchmarks (regression gate)

• Add criterion benchmarks for fusion pipeline (regression gate) meld#103 — fusion pipeline
• Add criterion benchmarks for per-engine throughput (LC, SCH, SC, HS, CFDP) relay#8 — per-engine throughput
• Add criterion benchmarks for signature verification paths sigil#89 — signature verification
• Add criterion benchmarks for scheduling solver (ARINC653) spar#137 — scheduling solver

Phase 3c — cargo-fuzz targets

• Add cargo-fuzz targets for component-model parser meld#104 — component-model parser
• Add cargo-fuzz targets for AADL parser + scheduling solver inputs spar#138 — AADL parser + solver inputs
• Add cargo-fuzz targets for ARM-backend instruction selection synth#82 — ARM-backend instruction selection
• thrum: cargo-fuzz targets for DB query/task protocol (repo archived; skipped)

Phase 3d — mutation testing generalization

• Publish cargo-mutants CI template; adopt in kiln, loom, gale, meld #185 — publish cargo-mutants CI template; adopt in kiln/loom/gale/meld

Phase 4 — Cross-cutting (on rivet)

• Canonicalize 21-hook pre-commit template for adoption across production repos #186 — canonical 21-hook pre-commit template for adoption across production repos
• Enforce rivet-validate as required pre-commit hook wherever rivet.yaml exists #187 — enforce rivet-validate as required pre-commit hook wherever rivet.yaml exists
• V&V coverage matrix dashboard via rivet coverage (per-commit, per-repo, per-technique) #188 — V&V coverage matrix dashboard via rivet coverage

Phase 5 — Abstract interpretation (the third DO-333 technique class)

Three parallel MIRAI prototypes on different code styles (crypto, kernel, data-structure) to understand which property classes abstract interpretation catches on our actual code, followed by a strategic Charon-based value-analysis pass integrated into the hermetic toolchain.

• MIRAI prototype — evaluate abstract interpretation on crypto parser paths (varint + DSSE) sigil#91 — MIRAI prototype on varint + DSSE parser paths
• MIRAI prototype — evaluate abstract interpretation on RTOS kernel primitives (ring_buf, scheduler, atomics) gale#23 — MIRAI prototype on ring_buf / scheduler / atomics
• MIRAI prototype — evaluate abstract interpretation on traceability engine internals (artifact store, link graph) #191 — MIRAI prototype on artifact store / link graph
• Charon-based abstract interpretation pass on LLBC — the third DO-333 technique class rules_lean#3 — Charon-based value analysis pass on LLBC (blocked on rules_lean#1)

Related (pre-existing)

• Finish Aeneas end-to-end pipeline: add hermetic Charon, reuse rules_verus sysroot pattern rules_lean#1 — Finish Aeneas end-to-end pipeline (Rust→LLBC→Lean)

Skipped (repos archived)

• pulseengine/automator — GitHub CI + Verus adoption cannot be filed (archived, read-only)
• pulseengine/thrum — cargo-fuzz cannot be filed (archived). Note: thrum is currently the only repo using tokio-rs/loom; worth considering whether to unarchive if loom-permutation-checking is part of the V&V strategy long-term.

Success metric

Every production repo (kiln, loom, meld, relay, rivet, sigil, spar, synth, gale, wohl) passes all four gates with:

• pre-commit hook parity with rivet's 21-hook config
• Bazel test //... green
• GitHub Actions CI green
• Rivet traceability validated

References

Analysis thread (internal): full V&V inventory across 30 workspaces, DO-332 / DO-333 applicability, cross-domain standards mapping (ISO 26262, IEC 61508, EN 50128, IEC 62304, ECSS-Q-ST-80C, IEC 60880).

Roster summary

Created: 29 issues (1 hub + 28 children) across 10 repos.
Skipped (archived): 3 issues (automator×2, thrum×1).