# 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](https://arxiv.org/abs/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.

```vera
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](https://github.com/aallan/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 [[toolbox/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).