How declarations become verification artifacts, and how testing, formal, and mutation compose into evidence. Principles in force: P-7 (claims carry evidence), P-11 (dogfooded on Strata's own components first).

The research landscape validates the platform thesis directly: the strongest existing results (Cascade, TestRIG) each implement one slice of this design bespokely, and the cross-cutting gaps — no maintained PBT-with-shrinking for hardware, no open BMC-witness-as-seed pipeline, no general semantic shrinker, no property-quality scoring loop — are exactly what an integrated, type-driven platform can claim. (D-028)

Committed design

1. Declarations generate infrastructure

A stream/contract declaration (04 §8) generates: payload-stability assertions, transfer-event definitions, outstanding-count tracking, capacity/ordering checks, legal + adversarial generators, cancellation tests, coverage bins, field-aware mutators, and semantic shrink rules. One #[derive(...)] on a payload type yields packed representations, waveform metadata, symbolic values, constrained generators, and shrink rules (02 reflection). Nothing here is hand-maintained; it is compiled from the same judgments the typechecker uses (the vision's claim 3).

2. Property-based testing with integrated shrinking

Strategies are typed, state-aware generator functions (weighted, model-conditioned — rough-1.md §18 stands).
Stateful rule-based testing: state_machine blocks with rules, preconditions, and invariants driving DUT + reference model in lockstep.
Shrinker architecture (D-028): Hypothesis-style integrated shrinking — shrink the generator's choice sequence, not the produced value, so every shrunk case is valid by construction and strategies compose shrinkage for free. This is the state of the art in software PBT and precisely what no hardware framework offers (cocotb+Hypothesis integration is folklore without working shrinking; chiseltest is unmaintained). TestRIG/QuickCheckVEngine proves the concept end-to-end for CPUs — QuickCheck-shrunk instruction sequences diffed over RVFI found real pipeline bugs — but is Haskell- and ISA-bound; Strata generalizes it to any typed interface.
Semantic shrinking preserves dependency structure (data/memory deps, branch preconditions, transaction relationships, privilege/protocol state) during reduction. Cascade's automated program pruning is the nearest precedent and is bespoke to its generator; ours falls out of typed strategies + choice-sequence shrinking.

3. Fuzzing, structured

Field lessons baked in: valid-by-construction, long, control/data-entangled inputs beat byte-stream mutation (Cascade: 28–97× coverage vs prior fuzzers, 37 new bugs — its "asymmetric ISA pre-simulation" trick generalizes to "generate against the reference model's view"); coverage proxies (mux-toggle, control-register) are weak signals to be combined, not trusted individually. Strata's coverage model spans RTL branch/condition/toggle, functional, protocol-state, architectural/microarchitectural novelty, queue occupancy, hazard combinations, assertion proximity, and differential divergence; the corpus manager retains by semantic value.

4. Metamorphic and differential testing

Metamorphic properties (NOP insertion, latency perturbation, burst splitting, speculation-path variation preserve committed state) as first-class #[metamorphic] declarations.
Differential backbone (D-028): commit-level lockstep over an RVFI-class interface. For RISC-V targets: RVFI(-DII)-style per-retired-instruction comparison against Spike/Sail, riscv-dv-compatible trace diffing as the coarse mode; the platform generalizes the interface so non-CPU components (caches, NoCs) get the same treatment against their reference models. This is current best practice (TestRIG, RVVI lockstep) rather than invention — the novelty is generation from types.

5. Formal-assisted testing

Target: queue full ∧ older unresolved store ∧ mispredict ∧ translation fault. Pipeline: encode as reachability cover → BMC produces witness → witness becomes executable prefix/corpus seed → structured mutation of continuations → failure → shrink → generalize. HyPFuzz proved the loop works but is JasperGold-bound; the open-source version of this pipeline effectively does not exist — SymbiYosys cover witnesses exist, using them as fuzz seeds doesn't. That's ours to build on the committed formal backend (SymbiYosys first, circt-bmc when its counterexample extraction lands).

6. Property validation and mutation scoring

Agent-generated (and human-generated) properties are untrusted candidates (09): checked for vacuity, unreachable antecedents, over-strong assumptions, exclusion of legal behavior — and scored by mutation testing: inject dropped responses, duplicated transactions, delayed flushes, arbitration corruption; a property that catches no mutants is flagged. Open tooling precedent: MCY (mutations + formal filtering of equivalent mutants); emerging pattern: mutation as assertion-quality oracle (VERT). Mutation results feed the evidence lattice as MutationValidated<mutant-classes>.

7. Dogfood targets (P-11)

Phase order of verification targets mirrors the roadmap: Strata's own stdlib FIFOs/arbiters/CDC bridges first (their contracts are the catalog schemas' reference implementations), then a cache + memory controller, then a small pipelined core with the full differential + formal-assisted loop.

8. Systems-safety contract compilers

Each optional contract family generates a different artifact package; none is silently treated as a type proof:

Contract family	Generated artifacts	Honest result boundary
Fault/health	occurrence→detection monitors, containment windows, stale-value rejection, ECC/parity/lockstep/replay campaigns, permanent/transient mutants	coverage is over declared fault classes and injection sites, not arbitrary physical failure
Mapping leases	DMA/IOMMU/interrupt lifecycle tests, issue-time authorization monitors, unmap-drain and stale-descriptor campaigns	assumes modeled hardware mediation and owner validation
Progress	finite wait-for graph, SCC/ranking/escape checks, arbitration starvation tests	`proved / refuted / obligation`; weak fairness never manufactures finite `N`
Memory model	event-relation export, completeness checks, litmus generation, herd/model-adapter comparison	bounded suites are evidence, not all-program refinement; full RVWMO awaits mixed-size/per-byte validation
Observer security	two-run harnesses, declassification-authority checks, cache/contention/debug observation comparisons	model-relative noninterference; power observations require physical evidence
Power/reconfiguration	lifecycle monitors, isolation/retention/quiescence checks, stale-generation tests, replacement-ABI/authenticity obligations	digital protocol proof assumes characterized electrical behavior
Numeric accuracy	unit/scale checks, range campaigns, transformation error certificates, calibration-expiry tests	correlation and approximation models are explicit assumptions
DFT/debug	authenticated-mode reachability, scan/trace policy checks, functional and security-observer translation validation	insertion proof is conditional on fuse/mode/power/isolation premises
Assurance	deterministic hazard→guarantee→assumption→artifact graph, release diff, expiry and residue report	the graph summarizes evidence and never counts as evidence

Campaigns are declaration-derived but remain scored like any other verification artifact: mutation adequacy, coverage, boundedness, target/tool pins, and expiry are visible. Missing ownership, incomplete event relations, stale artifacts, and unsupported backend semantics produce obligations or release failures—not optimistic defaults.

North star

Coverage-novelty metrics learned from traces (microarchitectural-state novelty beyond hand-defined bins).
Formal generalization of shrunk counterexamples into proven property strengthenings.
Cross-run corpus transfer between design variants via architectural-IR-level mapping (an experiment-database service, 09 §4).
Standard-model adapters for RVWMO/Arm-style mixed-size memory behavior, commercial fault/safety tools, power-aware simulation, and DFT/signoff flows; adapters import evidence without placing those tools in Strata's semantic trusted base.
Independent-checker diversity for high-consequence certificates and assurance claims.

Open problems touching this doc

None owned; consumes OP-3 obligation stability (summaries drive which properties re-verify) and feeds OP-5 (failure explanations reuse the diagnostic vocabulary).