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.

Working stance

• Name the failure mode before naming the tool.
• Each tool is additive: Miri does not replace proptest, Kani does not replace Verus.
• Run cheap adversaries on every change; reserve expensive sweeps for code where they pay back.
• The effort is not finished until a deliberate mutation of the production code is caught by it.

Selection by failure mode