Vow

AI-first language whose stated audience is not human readers.

Website | Source

Every function carries machine-checked vows. ESBMC bounded model checking discharges them at compile time. The compiler binary ships its own Claude Code skill, generated from the same source as the toolchain.

Camp: Verification
Author: Paulo Matos
Implementation language: Rust (stage 0); self-hosted in Vow
Compilation target: Native (via Cranelift); C (for the ESBMC verification pipeline only)
Licence: MIT
First seen: February 2026
Maturity: working compiler

Agent tooling:
- CLAUDE.md
- compiler-bundled Claude Code skill (auto-installed to .claude/skills/vow/)
- vowc skill print --bundle (self-contained markdown for non-Claude harnesses)
- structured JSON diagnostics with counterexamples and blame

Key idea

Every function declares a vow block of requires/ensures; loops carry invariant. The compiler lowers these to obligations for the ESBMC bounded model checker before any code ships. Diagnostics emit JSON in parallel with human text, with explicit Caller/Callee blame on every violation. The compiler binary embeds and auto-installs a Claude Code skill generated from the same compiler version — "the source of truth for any harness writing Vow code; cannot drift from the toolchain you are running."

Thesis

Vow is a verification-camp project whose stated audience is not human readers. The homepage announces it directly: "The syntax is not for you. The semantics is not for you. The language is not for you. Yours is only the product." Every module makes vows — preconditions, postconditions, and loop invariants — that the compiler lowers to obligations for the ESBMC bounded model checker. The CLI emits JSON in parallel with human text on every invocation; counterexamples come back as structured records the agent can read. The intended workflow is CEGIS: write, compile, verify, read counterexamples, fix, iterate.

The syntax is not for you. The semantics is not for you. The language is not for you. Yours is only the product.

The distinctive move is the choice of checker. Vera and Intent dispatch contracts to Z3 SMT; Aver exports them as Lean 4 theorems or Dafny lemmas; NanoLang proves the core type system in Coq from below. Vow chooses ESBMC, a bounded model checker, and accepts the trade that comes with it — counterexamples are concrete inputs the agent can re-run against, but soundness holds only up to the unwinding bound chosen for each verification call. The repository's CLAUDE.md is explicit about the consequence: "Bounds like n <= 10 (to fit within --unwind 10) or a <= 100 (to help the SMT solver) are verification artefacts. They do not belong in requires/ensures clauses... If ESBMC can't prove a correct contract, that's ESBMC's problem."

What it looks like.

module Bisect

fn bisect(lo: i64, hi: i64) -> i64 vow {

requires: hi >= lo

} {

let mut lo: i64 = lo;

let mut hi: i64 = hi;

while lo + 1 < hi vow {

invariant: hi - lo >= 0

} {

let mid: i64 = lo + (hi - lo) / 2;

lo = mid;

}

lo

}


fn main() -> i32 [io] {

let r: i64 = bisect(0, 64);

print_i64(r);

0

}

A vow block follows the function signature; loop vows carry invariant clauses. The [io] effect set on main declares the only impurity in the program — pure functions carry no annotation, and calling an effectful function from a pure one is a type error.

Distinctive moves.

Maturity.

v0.2.0 released 20 May 2026 on a repository created 25 February 2026, MIT-licensed under the vow-lang GitHub organisation. The Rust workspace splits across nine crates (vow-syntax, vow-types, vow-ir, vow-codegen, vow-verify, vow-runtime, vow-diag, vow-clif-shim, vow) feeding a Pizlo-style SSA IR and a Cranelift backend. The self-hosted compiler in compiler/ (13 modules) compiles itself to a byte-identical binary under the project's bootstrap triple test — stage 0 produces compiler A, compiler A produces compiler B, compiler B produces compiler C, and sha256sum of B and C must match. Mutation testing ships as a vowc mutants subcommand with a tiered oracle and structured JSON output.

Three substantial programs ship in examples/ alongside the small contract demonstrations: a deterministic CDCL SAT solver (watched literals, first-UIP learning, non-chronological backtracking, Luby restarts), a UCI-compatible chess engine, and a Lean 4 kernel checker (vow-lean-kernel) targeting the Lean Kernel Arena. The author's announcement names the standing gap explicitly: "ESBMC integration is in place and discharges contracts for the example programs, but the corners are still being found... The compiler is written in Vow but its own vows are not all verified end-to-end. Closing that loop is the single most important piece of work ahead." The benchmarks/ directory holds Vow's implementation of vericoding (arXiv:2509.22908) — 40 problems across 15 Easy, 15 Medium, and 10 Hard tiers, with a Python harness in bench/ that runs frontier models against paper baselines (Dafny 82%, Verus/Rust 44%, Lean 27%). Published numbers for Vow itself sit on the roadmap rather than in a release.

Agent tooling.

CLAUDE.md runs to ~20 KB and addresses the language design rules to Claude directly; AGENTS.md is a nine-byte placeholder. The substantive agent surface is the compiler-emitted skill: vowc skill install --local writes SKILL.md plus reference/, examples/, and schemas/ to .claude/skills/vow/; vowc build auto-installs the same payload the first time it runs in a project that already has .claude/; vowc skill print --bundle emits a single self-contained markdown document for raw-API harnesses. Diagnostics from every crate flow through vow-diag, which always emits JSON and human text in parallel — "this is by design, not a flag." vowc --help returns a structured JSON capability description by default and human text under --human.

Design DNA

Timeline

Tags: ai   language   verification  

Last modified 15 June 2026