diff --git a/content/blog/2026-04-22-overdoing-the-verification-chain.md b/content/blog/2026-04-22-overdoing-the-verification-chain.md index cd40875..85ea377 100644 --- a/content/blog/2026-04-22-overdoing-the-verification-chain.md +++ b/content/blog/2026-04-22-overdoing-the-verification-chain.md @@ -148,6 +148,7 @@ A one-line gloss for each technique in the matrix below — skip if these read l - **tokio-rs/loom** — permutation-checks every possible thread interleaving in a bounded concurrent program. - **Sanitizer · Miri** — runtime instrumentation that detects undefined behaviour, memory errors, and data races (ASAN, TSAN, LSAN, UBSAN, Miri). - **Mutation testing** — inject small plausible bugs into the source and check whether the test suite catches them; empirical test-suite adequacy. +- **Structural coverage (Wasm IR)** — branch / MC/DC coverage measured on the post-compile WebAssembly module rather than at source. Closes the §FM.6.7(f) / MC/DC-shaped cell that source-level lcov has long pretended to satisfy across DO-178C, ISO 26262, IEC 61508. Shipping as [witness](https://github.com/pulseengine/witness); the credit-template work for the other four standards is the next post's hook. - **Traceability** — requirement ↔ design ↔ code ↔ test ↔ proof chain, validated on every commit (rivet). At a glance, all seven domains against the core chain techniques: @@ -166,6 +167,7 @@ At a glance, all seven domains against the core chain techniques: