Vow — A Programming Language for Agentic Coding

// 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.

// begin

Get started

Vow is open source. The compiler is self-hosted and verified to produce byte-identical binaries.

View on GitHub