Macro verus_panic 

macro_rules! verus_panic {
    ($($arg:tt)*) => { ... };
}

Available on not (verus_keep_ghost and crate feature verus).

Panics, in a way that Verus proofs of algebraic properties treat as an acceptable outcome. Takes the same arguments as panic!.

A Verus proof (e.g. verus_proof_commutative_fold!) normally requires the closure body to be panic-free for every input, which rejects closures such as *acc += x (which panics on overflow) even though they are commutative whenever they complete. Calling verus_panic!(...) instead tells Verus that this path ends the program: the property only has to hold for executions that do not reach it. That matches Hydro’s requirement, since a panicking closure crashes the process rather than producing a result.

The typical use is to guard an operation that could otherwise panic, so that Verus knows it cannot fail on the paths that continue:

q!(
    |acc, x| {
        if *acc > u32::MAX - x {
            verus_panic!("sum overflowed");
        }
        *acc += x; // cannot overflow here, so Verus accepts it
    },
    commutative = verus_proof_commutative_fold!(acc = u32, item = u32)
)

This is sound because the guard really executes: the closure panics at runtime whenever the guard condition holds, so a guard that is stricter than necessary is still correct. A guard that is too weak is caught by Verus, which reports the operation that may still panic. Unlike assume(...) in a proof script, nothing is taken on faith beyond the fact that verus_panic! never returns.

Under normal compilation, this forwards its arguments to panic!. When verifying with cargo verus verify, the verus feature of hydro_lang must be enabled; Verus then sees a call to a function that never returns (the message arguments are not evaluated by the proof).