// manifesto
The syntax is not for you. The semantics is not for you. The language is not for you. Yours is only the product.
Vow is designed for the agent that writes the code. Humans review the artifact, not the keystroke.
// 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 bisect(lo: i64, hi: i64) -> i64 vow {
requires: lo >= 0,
requires: hi >= lo,
requires: hi <= 100
} {
let mut lo: i64 = lo;
let mut hi: i64 = hi;
while lo + 1 < hi vow {
invariant: lo >= 0,
invariant: hi >= lo,
invariant: hi <= 100
} {
let mid: i64 = lo + (hi - lo) / 2;
lo = mid;
}
lo
}ESBMC proves the loop preserves every invariant on the back-edge across any inputs that satisfy the preconditions. vowc verify returns {"status":"Verified"}.
// reference
Language reference
A curated tour of Vow's surface. The complete spec lives in the main repo.
§1 Module declaration
Every file begins with a module declaration in PascalCase. Imports use dot-separated paths.
module BinarySearch
use std.io§2 Functions and effects
Pure functions need no annotation. Effects appear in brackets after the return type: [io], [read, write], [panic]. Calling an effectful function from a pure context is a type error.
fn add(x: i64, y: i64) -> i64 {
x + y
}
fn main() -> i32 [io] {
print_str("hello");
0
}§3 Contracts: requires, ensures, invariant
The vow block carries the contract. requires is a precondition (blame: caller). ensures is a postcondition over result (blame: callee). Multiple clauses are comma-separated.
fn clamp(x: i64, lo: i64, hi: i64) -> i64 vow {
requires: lo <= hi,
ensures: result >= lo,
ensures: result <= hi
} {
if x < lo { lo } else { if x > hi { hi } else { x } }
}§4 Refinement types on parameters
where clauses on parameters become additional preconditions. Each clause may only reference its own parameter.
fn safe_sub(a: i64 where a >= 0, b: i64 where b >= 0) -> i64 vow {
requires: a >= b,
ensures: result >= 0
} {
a - b
}§5 Types
Primitives: i32, i64, u8, u64, f32, f64, bool, (), !. Built-in parameterised types cover the common containers; user-defined types are structs and enums.
let n: i64 = 42;
let v: Vec<i64> = Vec::new();
let name: String = "vow";
let maybe: Option<i64> = Option::Some(7);
let map: BTreeMap<i64, i64> = BTreeMap::new();§6 Control flow
if/else is an expression. Loops can carry invariants the verifier checks at every back-edge.
let mut i: i64 = 0;
while i < n vow {
invariant: i >= 0,
invariant: i <= n
} {
v.push(i);
i = i + 1;
}
for x in v vow {
invariant: total >= 0
} {
total = total + x;
}§7 Structs and linear structs
Regular structs are heap-allocated and pass by reference. linear struct values must be consumed exactly once — resource leaks become compile errors.
struct Point {
x: i64,
y: i64,
}
linear struct FileHandle {
fd: i64,
}
let p: Point = Point { x: 1, y: 2 };§8 Enums and pattern matching
Enum variants can be unit, tuple, or struct. match is an expression; arms must be exhaustive and share a type.
enum Shape {
Circle(i64),
Rect(i64, i64),
Empty,
}
let area: i64 = match s {
Shape::Circle(r) => 3 * r * r,
Shape::Rect(w, h) => w * h,
Shape::Empty => 0,
};§9 Error propagation
The ? operator on Option or Result short-circuits to the caller. The calling function's return type must match.
fn first_line_len(s: String) -> Option<i64> {
let nl: i64 = s.find_byte("\n".byte_at(0))?;
Option::Some(nl)
}§10 CEGIS workflow
Write → build → parse JSON → on VerifyFailed, read the counterexample → fix → repeat. The compiler emits structured output for every status; no log-scraping required.
$ vowc build hello.vow
{
"status": "Verified",
"executable": "./hello",
"diagnostics": [],
"counterexamples": []
}No generics. No traits. No closures. No macros. No garbage collection. The verification surface stays small on purpose.
// release
Vow 0.3.0
July 16, 2026Version 0.3.0 is a foundations release. Two threads run through it: making verification honest, and making the type system sound. The compiler now fails closed when it cannot prove a contract, rejects contracts that pass only by being trivially true, and closes a family of signed/unsigned holes that let unsound programs slip past the checker. Full changelog →
Verification that fails closed
Contract verification no longer lets unproven work pass as proven. An unprovable contract, a verifier worker that panics, and effect or linear-type errors now each fail the build instead of slipping through silently. ESBMC's memory use is bounded so runs stay predictable, and user-defined structs are now modelled through a heap model — widening the set of programs the verifier can reason about.
No contracts that prove nothing
A contract can lie by being vacuously true. A new static contract-quality classifier, backed by per-clause checking (ESBMC --multi-property), flags contracts that are vacuous or trivially satisfiable — the kind of ensures any implementation would pass. Every weak bit-packer contract was rewritten, bringing the CI weak-contract gate to zero.
A sounder type checker
The checker now enforces mut: mutating an immutable binding is a compile error. A family of u64/i64 soundness holes is closed — mixing signed and unsigned is rejected, and unsignedness is preserved through pattern matches, loop back-edges, and coercions. Linear types can no longer be smuggled in as map values.
New analysis tooling
A new complexity subcommand reports per-function complexity, including the weight of contracts and parameter refinements. --perfetto emits a Chrome/Perfetto trace of the build-and-verify pipeline, so you can see where the time goes. --replay-cex differentially tests the verifier's model against the real runtime by replaying counterexamples.
Standard library and runtime
The standard library is unified and now has its own documentation site. Arbitrary-precision integers arrive as a base-232 bignum with u64 interop, bitwise operations, and truncated subtraction, plus a small-integer fast path. On the runtime side: checked arithmetic in Vec growth, reclaimed small-Vec leaks in loop arenas, and exit code 134 reserved for aborts.
// begin
Get started
Vow is open source. The compiler is self-hosted and verified to produce byte-identical binaries.
View on GitHub