vera

Vera is a programming language designed to be written by LLMs rather than humans. The premise is that the failure mode of LLM-generated code is mostly not syntax — it's coherence over scale: invariants drifting across files, naming-related errors (misleading names, reused names, lost references — see arXiv:2307.12488), and incorrect reasoning about state over time. Vera tries to make those errors compile-time failures.

The compiler is a Python reference implementation that emits WebAssembly and runs at the CLI or in the browser. It's authored by Alasdair Allan (the IoT/maker writer; also a physicist by background).

Three design choices that shape everything else

No variable names. Bindings are referred to by typed De Bruijn index — @Int.0 is the most recent Int binding in scope, @Int.1 is the one before. The name-as-source-of-confusion failure mode goes away because there are no names to confuse. See typed-de-bruijn-for-llms for the concept on its own.

Mandatory contracts. Every function has requires(), ensures(), and effects() clauses between the signature and the body. The signature is a specification, not just a type. Z3 proves Tier-1 contracts (decidable arithmetic, comparisons, booleans, ADTs, termination) statically; contracts the solver can't decide become Tier-3 runtime checks.

Algebraic effects in signatures. A function that calls an LLM declares effects(<Inference>); one that does HTTP declares effects(<Http>). Callers must permit the full effect row. Pure functions are effects(pure) and the compiler enforces it. This is closer to Koka or F* than to Haskell's IO — the effect row is on the function arrow, not in the return type.

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 isn't a runtime error in Vera — it's a type error caught at every call site.

Errors are written for the model that wrote the code

Diagnostics include what went wrong, why, a concrete fixed example, and a spec reference. Every error has a stable code (E001–E702) and is available as structured JSON via --json for agent feedback loops:

[E001] Error at main.vera, line 14, column 1:
  Function is missing its contract block. Every function in Vera must declare
  requires(), ensures(), and effects() clauses between the signature and the body.
  Fix: ...
  See: Chapter 5, Section 5.1 "Function Structure"

That --json flag is the design tell. The whole language treats the LLM as the primary user — error output is shaped for an autonomous loop, not for a human reading a terminal.

Tooling for agents

The repo ships SKILL.md, AGENTS.md, CLAUDE.md, and DE_BRUIJN.md — separate documents for Claude Code, generic agent systems, and the academic background of the slot system. Claude Code auto-discovers the skill in-repo; for other projects, it installs to ~/.claude/skills/vera-language/SKILL.md.

Workflow

vera check    # parse + type-check
vera verify   # add Z3 contract verification
vera run      # compile to WASM + execute
vera test     # contract-driven testing
vera fmt      # canonical formatter

vera compile --target browser emits a self-contained bundle (wasm + JS runtime + HTML), and the build system runs parity tests so CLI and browser behaviour stay identical.

VeraBench

The author's companion benchmark (vera-bench) is 50 problems × 5 difficulty tiers across 6 models / 3 providers. Reported headline: Kimi K2.5 hits 100% run_correct on Vera, vs 86% on Python and 91% on TypeScript; three models beat TypeScript on Vera; flagship-tier average is 93% Vera vs 93% Python. Single-run, high-variance — not a settled result, but the early signal is "purpose-built constraints lift correctness without bottoming out fluency."

Status and watchlist

v0.0.127 at time of ingest, repo created 2026-02-22 (~10 weeks old), 810+ commits, 127 releases, 261 stars, MIT, single author. The compiler covers parser, type checker, Z3 contract verifier, WASM codegen, module system, browser runtime, and runtime contract insertion. The 13-chapter spec is in draft. The roadmap calls out a verified MCP tool server as the flagship goal.

Added to watchlist — single author, very young, deliberately swimming against ecosystem gravity (no variable names is a hard sell). The next-check question is whether anyone besides Alasdair ships nontrivial Vera code, whether VeraBench gains independent reproductions, and whether the verified-MCP-server milestone lands.

Cross-references

• typed-de-bruijn-for-llms — the slot-references concept, isolated from Vera.
• vamp-ai-frontend — same idea on the frontend side: explicit, AI-friendly-by-design language surfaces beat conventional ones for generated code.
• clippy-stricter-config — the retrofit version: tightening an existing language with lints rather than rebuilding the surface.
• clean-code-coding-agents — context-window economics that motivate AI-friendly language design.

Repo

https://github.com/aallan/vera — 261 stars, MIT, Python (compiler) / WASM (runtime).