Rust verification: choosing the right adversary

Tests show a program works on the inputs you tried. Verification tools attack the program with adversaries chosen by failure mode: UB, unexpected inputs, schedule chaos, logic gaps, exhaustive state, or unbounded reasoning. Pick the smallest adversary that fits the property at risk.

Use this skill when the required evidence is unclear or the task has outgrown ordinary examples and a lightweight property. Do not insert a selector ceremony between a clear, cheap invariant and a ten-line proptest! block; load proptest directly for that case.

The tools here answer different questions. They form an escalation map, not a single scale from weak to strong.

Before escalating