When to reach for verification

Use the verification cluster when example-based tests cover the obvious cases but the bug class is broader than the corpus.

• Hypothesis — when a property should hold across an input space (round-trip, oracle, invariant). Mirrors the rust-skill proptest deep dive.
• CrossHair — when symbolic execution can prove or disprove an assertion over a small pure function. Best on parsers, codecs, finance code, and refactors validated with diffbehavior.
• mutmut — when the suite passes consistently and the question is whether the tests would notice a regression.

Run Hypothesis on every CI run; run CrossHair and mutmut on slower cadences.