Mandatory contracts on every function. Z3 SMT verification. Typed slot references replace variable names. LLM inference is a first-class typed effect.
Author: Alasdair Allan
Implementation language: Python
Compilation target: WebAssembly
Licence: MIT
First seen: February 2026
Maturity: working compiler
Agent tooling:
- SKILL.md
- AGENTS.md
- CLAUDE.md
- LLM-oriented diagnostics
- stable error codes (E001–E702)
- JSON diagnostic output
Mandatory requires/ensures/effects contracts on every function. Three-tier Z3 SMT verification. Typed De Bruijn slot references (@T.n) instead of variable names — the only language in the space that drops names. LLM inference is a first-class typed effect. The thesis: the model doesn't need to be right, it needs to be checkable.
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 distinctive 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.
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).
@T.n denotes the n-th-most-recent binding of type T.<Inference> effect. A function that doesn't declare it can't make model calls. The effect system tracks model usage up the call graph.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.
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.
<Inference> as one effect, AILANG carves it into IO/FS/Net/Clock/AI.<Inference> effect added as first-class typed effect. Aver becomes first external language integrated into VeraBench.Last modified 15 June 2026