Contracts

Use case: money must not go negative

fn withdraw(balance: int, amount: int) -> int
    requires amount > 0
    requires amount <= balance
    ensures result >= 0
{
    return balance - amount
}

fn main(caps: Caps) -> int {
    return withdraw(100, 30)
}

vow run tests/lang/withdraw.vow          # ok → exit 70
vow run tests/lang/withdraw_bad.vow      # traps on violation

requires — preconditions (checked on entry)
ensures — postconditions; result is the return value
Runtime checks on the native path (not SMT proving)

Use case: pair with capabilities

Generate or accept a tool that needs a narrow path, then wrap critical math in contracts so edge cases fail closed.

Next