Verus deductive verification for Rust

Verus uses the Z3 SMT solver to statically verify that executable Rust code satisfies user-provided specifications, with zero runtime cost. Load the rust-verification skill first for the selection rules; load this skill once Verus is the chosen tool.

When to apply

Apply when:

• a property holds over unbounded domains (arbitrary-length sequences, any number of layers, all possible orderings),
• a pure function must satisfy algebraic properties (reflexivity, antisymmetry, transitivity, totality),
• extraction or transformation logic that must preserve structure needs verification,
• a Kani harness keeps growing because the bounded state space is too large — extract the pure helper and prove it in Verus instead.