Validate requires/ensures specs at runtime using the check_contracts! macro from vstd. Wraps functions with check_contracts! {}, generates
Validate requires/ensures specifications at runtime using the check_contracts!
macro from vstd::contrib::exec_spec. The macro wraps function bodies and generates
check_<fn>() wrappers that return Result<T, ContractError>.
Reference: verus/source/vstd/contrib/exec_spec/README.md
check_contracts! from vstdvstd is already a dependency. No extra Cargo feature needed. At the top of the file being tested, add:
use vstd::contrib::exec_spec::check_contracts;
check_contracts! {}Move the function (or entire impl block) OUT of any existing block and into a block. The macro wraps it in verus internally.
verus! {}check_contracts! {}Critical rules:
check_contracts! {} must be at the crate top level — NOT inside verus! {}spec fn referenced in requires/ensures must live inside the same
check_contracts! {} block (they get compiled to exec_* versions at runtime)old() must derive Cloneobj.check_method(args); free functions generate check_fn(args)// ❌ WRONG — nested inside verus!
verus! { check_contracts! { fn foo() ensures ..., { } } }
// ✅ CORRECT — top level
check_contracts! {
impl Block {
spec fn value(self) -> usize { self.0 } // spec fn referenced in ensures
pub fn is_empty(self) -> (result: bool)
ensures result == (self.value() == 0),
{
self.0 == 0
}
}
}
If the function uses old(), the struct must derive Clone:
check_contracts! {
#[derive(Clone)] // required for old(self) captures
impl Counter {
fn increment(&mut self)
requires old(self).value < old(self).max,
ensures self.value == old(self).value + 1,
{ self.value += 1; }
}
}
#[test] functions calling the generated wrappersPlace inline as #[cfg(test)] mod tests { ... } or in tests/contract_tests.rs.
No feature gate needed — check_contracts! is always active.
Postcondition test (happy path):
#[test]
fn contract_<fn_name>_postcondition() {
// Arrange valid state satisfying the precondition
let obj = ...;
// Call the check_ wrapper
match obj.check_<fn_name>(<valid_arg>) {
Ok(result) => {
// Assert the postcondition holds
assert!(<postcondition_expression>, "Postcondition violated: <spec text>");
}
Err(e) => panic!("Unexpected contract violation: {:?}", e),
}
}
Precondition test (boundary / invalid input):
#[test]
fn contract_<fn_name>_precondition() {
let mut obj = ...;
match obj.check_<fn_name>(<invalid_arg>) {
Ok(_) => panic!("Expected PreconditionViolated for <reason>"),
Err(e) => assert!(
matches!(e, ContractError::PreconditionViolated { .. }),
"Expected PreconditionViolated, got {:?}", e
),
}
}
Value selection:
len - 1, len, len + 1insert(bit) with requires bit < self.len(): test bit = 0, bit = len-1
(valid) and bit = len, bit = len + 100 (invalid)cd <project_root> && cargo test 2>&1
No --features flag is needed.
After tests pass, verify the spec is not vacuously satisfied. A test that always passes regardless of the postcondition value indicates a weak spec.
Method A — mutate the test input:
cargo test; the assert! inside Ok(_) should now fail (or a
different value should be returned)ensures clauseMethod B — negate one ensures clause (temporary):
ensures result == X to ensures result == X + 1 in the sourcecargo test; expect PostconditionViolated { condition: "result == X + 1" }check_<fn> wrapper is not being called or the
ensures is not constraining enough; investigate and strengthen| Failure | Cause | Fix |
|---|---|---|
PreconditionViolated in happy-path test | requires too strict | Relax the clause |
PostconditionViolated | ensures wrong or impl doesn't satisfy it | Fix spec or impl |
Regular assert! failure | Expected postcondition expression is wrong | Fix the test assertion |
| Spec-strength mutation passes silently | ensures is too weak / not exercised | Strengthen the spec |
Report the failing test name, the error variant, and the condition string.
python3 scripts/verus-log.py event --type verus_run --data '{
"phase": "contract_tests",
"command": "cargo test",
"result": "pass|fail",
"failing_tests": [...],
"spec_strength_confirmed": true,
"project_root": "<project_root>"
}'