Pick the first level whose evidence matches the question:
- Named unit test: one scenario, regression, exact output, or error contract matters.
- Parameterized
rstesttable: a finite truth table, standards corpus, or set of cases whose rows each carry semantic meaning. - Lightweight
proptest: one round trip, invariant, oracle, or metamorphic relation should hold across many cheap, repeatable inputs. A growing set of representative#[case]rows is the usual signal, and the estate's reviewers flag it as such. - Structured or stateful
proptest: valid data has dependent or recursive structure, or failures depend on operation history. - Kani: a small bounded function needs exhaustive exploration of every reachable path within a stated bound.
- Verus: the property must hold with no bound, over a small stable pure kernel.
cargo-mutants sits beside the hierarchy. Use it when the question is whether
the current suite would notice a plausible defect. Miri sits below it, on the
tests that already touch unsafe.
Leave the hierarchy for scheduling, integration, load, performance, or
foreign-code failures. Those need loom, shuttle, or turmoil, real or
simulated boundaries, benchmarks and profilers, or sanitizers.
rust-verification is the escalation selector when the rung is unclear; a
clear lightweight invariant goes straight to proptest.