11 · SMT Verification

@verify tells the compiler to discharge function contracts using an SMT solver (Z3 by default) at compile time. @precondition states what must be true when the function is called; @postcondition states what the function guarantees about its return value. Verification failures are compile errors — not test failures, not runtime panics.

verify.cssl

// The compiler proves these contracts hold for all valid inputs.
@verify
@precondition(n >= 0)
@postcondition(result >= 1)
fn factorial(n: i32) -> i32 {
    if n == 0 { 1 }
    else      { n * factorial(n - 1) }
}

// Contract on a numeric range utility.
@verify
@precondition(lo <= hi)
@postcondition(result >= lo && result <= hi)
fn clamp_i32(value: i32, lo: i32, hi: i32) -> i32 {
    if value < lo { lo }
    else if value > hi { hi }
    else { value }
}

// Integer square root — verified to return the floor.
@verify
@precondition(n >= 0)
@postcondition(result * result <= n && (result + 1) * (result + 1) > n)
fn isqrt(n: i32) -> i32 {
    let mut r = 0;
    while (r + 1) * (r + 1) <= n { r += 1; }
    r
}

fn main() !io {
    println!("5!         = {}", factorial(5));   // 120
    println!("clamp      = {}", clamp_i32(200, 0, 100)); // 100
    println!("isqrt(17)  = {}", isqrt(17));     // 4
}

Output

5!         = 120
clamp      = 100
isqrt(17)  = 4

What the compiler sees

Before emitting any code, the compiler encodes each function as an SMT formula and asks the solver whether a precondition violation or postcondition failure is reachable. If the solver finds a counterexample, it reports the specific input values that break the contract — at compile time. Verification is zero runtime overhead: the produced binary contains no contract checks, only the verified logic. Calling factorial(-1) from code that doesn’t satisfy the precondition is itself a compile error.

---

Next → 12 · Vec and Collections