Vow.

The 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
}

Distinctive moves.

• ESBMC over SMT or theorem provers. Contracts lower to verification obligations the bounded model checker discharges before codegen. The C emitter exists only to feed that pipeline; native code comes from Cranelift directly.
• Blame is structured. requires violations fault the Caller; ensures and invariant violations fault the Callee. The JSON violation record carries the verdict explicitly ({"error":"VowViolation","vow_id":N,"blame":"Caller"|"Callee",...}).
• Compiler-bundled agent skill. Running vowc build in a project that already has a .claude/ directory writes the skill to .claude/skills/vow/ the first time, sourced from the running compiler binary. The repository describes the bundle as “the source of truth for any harness writing Vow code… it cannot drift from the toolchain you are running.” Non-Claude harnesses get the same bundle via vowc skill print --bundle.
• Canonical form as a compiler pass. The printer is a stage, not a formatter; parse → print → parse is enforced to be idempotent by tests. There is one preferred way to write each construct.
• Linear types and checked arithmetic at the grammar level. linear struct values must be consumed exactly once; the type checker tracks the obligation. +!, -! and the rest are distinct token kinds from +, - — checked and wrapping arithmetic are not library functions but grammar productions.
• What is deliberately absent. No generics, no traits, no closures, no higher-order functions, no macros, no garbage collector. The CLAUDE.md design rule rejects any feature that “introduces a new type-system axis.”

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.