Contracts

Contracts let you state intent next to the function. The body — often AI-written — is checked against that intent at run time (Tier 1). Static / SMT proving is not implemented.

Shape

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

requires — evaluated before the body
ensures — evaluated after a successful return; result is the return value
Multiple clauses are allowed

Try it

vow run tests/lang/withdraw.vow        # ok (repo clone)
vow run tests/lang/withdraw_bad.vow    # traps on violation

A violation aborts with a structured message, for example:

contract violation: requires amount <= balance
  at line …

Machine-readable compile errors

Unused Result values are a type error (strictness), independent of contracts:

vow check tests/lang/ignored_result.vow --json

What contracts are not

Next