The thesis.
Vera takes the verification camp’s diagnosis literally. If LLMs make semantic errors faster than humans can catch them by reading code, the compiler has to do the catching. Every function declares preconditions and postconditions; the compiler discharges them via the Z3 SMT solver in a three-tier scheme (compile-time, runtime guard, runtime check) before any code runs.
The model doesn't need to be right. It needs to be checkable.
The provocative move is replacing variable names with typed slot references. A function safe_divide(@Int, @Int -> @Int) has no parameter names — its arguments are referred to as @Int.0 (most recent) and @Int.1 (next most recent) using De Bruijn indexing. The empirical literature shows models are particularly vulnerable to naming-related errors: choosing misleading names, reusing names incorrectly, losing track of which name refers to which value. Vera’s answer is to remove names from the language entirely.
What it looks like.
public fn safe_divide(@Int, @Int -> @Int) requires(@Int.1 != 0) ensures(@Int.result == @Int.0 / @Int.1) effects(pure) { @Int.0 / @Int.1 }
Division by zero is not a runtime error — it is a type error. A caller that can't prove the denominator is non-zero won't compile. @Int.1 is the first parameter (next-most-recent binding); @Int.0 is the second (most-recent).
Distinctive moves.
- Mandatory contracts. Every function carries requires/ensures/effects clauses. There’s no opt-out; the grammar rejects functions without them.
- De Bruijn slot references. No variable names at the parameter level.
@T.ndenotes the n-th-most-recent binding of typeT. - Typed effects, including inference. LLM calls are an
<Inference>effect. A function that doesn’t declare it can’t make model calls. The effect system tracks model usage up the call graph. - Three-tier verification. Some contracts discharge at compile time via Z3; some become runtime guards; some become runtime checks. The tier is determined by which fragment of arithmetic the clause lives in.
- LLM-oriented diagnostics. Every error code is stable (E001–E702); every diagnostic carries a fix hint and a spec reference. The CLI emits JSON for tooling.
Maturity.
Vera is at v0.0.157+ with 300+ stars, 3,400+ tests at 96% coverage, 76 conformance programs validating every language feature, and a 13-chapter specification. The reference compiler is Python; programs compile to WebAssembly via wasmtime and run in the browser. Published VeraBench results report 93% flagship correctness on zero training data, matching Python.
Current focus is standard-library breadth. Open questions remain in monomorphisation reindexing and GC-rooting around inference calls. The language is usable but the surrounding ecosystem (LSP, package registry, IDE plug-ins) is still building.
Agent tooling.
Three documents in the repo target agent authors directly: SKILL.md (complete language reference for agents writing Vera), AGENTS.md (setup for any agent system), and CLAUDE.md (project orientation for Claude Code specifically). All three are rendered into llms.txt and llms-full.txt for ingestion by agent frameworks. The diagnostics output JSON when asked, with stable error codes that can be referenced from agent prompts.
- Aver verification Closest design relative. Co-located verify blocks, Lean 4 proof export, decision blocks. Different syntax for the same diagnosis. Now integrated into VeraBench.
- Prove verification Same verification diagnosis, opposite politics. Licence explicitly prohibits AI training use. Refinement types, verb-based IO tracking.
- AILANG verification Capability-based effects with row polymorphism. Where Vera tracks
<Inference>as one effect, AILANG carves it into IO/FS/Net/Clock/AI. - Magpie syntactic Cross-camp foil. Magpie strips ambiguity at the surface (SSA form); Vera adds a layer of mechanical checks. Different bets on where the error budget should be spent.