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.
- **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](https://arxiv.org/abs/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
- **[Vera](https://agentlanguages.dev/languages/vera.md)** *(Verification)* — Closest design relative. Both ship mandatory contracts on every function and treat the agent as the primary author. Vera dispatches to Z3 SMT and drops parameter names via typed DeBruijn slots; Vow dispatches to the ESBMC bounded model checker, keeps names, and adds linear types plus distinct checked/wrapping arithmetic tokens at the grammar level.
- **[Intent](https://agentlanguages.dev/languages/intent.md)** *(Verification)* — Same camp, same era, different checker. Intent commits to Z3 SMT with runtime enforcement on three backends (Rust, JavaScript, WebAssembly); Vow commits to ESBMC bounded model checking with a single Cranelift native backend and a C emitter that exists only because the verification pipeline needs it.
- **[Aver](https://agentlanguages.dev/languages/aver.md)** *(Verification)* — Same diagnosis, different upper-bound check. Aver exports