// properties
Contracts as First-Class
Every function carries requires and ensures clauses. Every loop carries invariant. These are fed to a bounded model checker — not comments, not assertions.
Compile-Time Verification
ESBMC bounded model checking proves your contracts hold or returns structured counterexamples. No runtime overhead in release builds.
Blame Semantics
requires violations blame the caller. ensures violations blame the callee. Diagnostics tell you exactly who is at fault.
Structured Output
JSON diagnostics, counterexamples, and build results everywhere. No human-readable-only output to parse. Built for agent consumption.
Linear Types
linear struct values must be consumed exactly once, enforced by the type checker. Resource leaks are compile errors.
Explicit Effects
Pure functions have empty effect sets. Calling an effectful function from a pure context is a type error. No hidden side effects.
// proof
Write contracts. Get proofs.
module BinarySearch
fn binary_search(arr: Vec<i64>, target: i64) -> i64 vow {
requires: arr.len() > 0,
ensures: result == -1 || arr[result] == target
} {
let mut lo: i64 = 0;
let mut hi: i64 = arr.len() - 1;
while lo <= hi vow {
invariant: lo >= 0,
invariant: hi < arr.len()
} {
let mid: i64 = lo + (hi - lo) / 2;
if arr[mid] == target {
return mid;
} else if arr[mid] < target {
lo = mid + 1;
} else {
hi = mid - 1;
}
}
-1
}The compiler proves the postcondition: if a result is returned, it's either -1 or the element at that index equals the target.
// begin
Get started
Vow is open source. The compiler is self-hosted and verified to produce byte-identical binaries.
View on GitHub