Vera: a programming language designed for machines to write

Vera (v-ERR-a) is a programming language designed for large language models to write. The name comes from the Latin veritas (truth). Programs compile to WebAssembly and run at the command line or in the browser.

public fn safe_divide(@Int, @Int -> @Int)
requires(@Int.1 != 0)
ensures(@Int.result == @Int.0 / @Int.1)
effects(pure)
{
@Int.0 / @Int.1
}

There are no variable names. @Int.0 is the most recent Int binding; @Int.1 is the one before. The requires clause is a precondition the compiler checks at every call site. The ensures clause is a postcondition the SMT solver proves statically. The function is pure — no side effects of any kind. If any of this is wrong, the code does not compile.

Programming languages have always co-evolved with their users. Assembly emerged from hardware constraints. C from operating systems. Python from productivity needs. If models become the primary authors of code, it follows that languages should adapt to that too.

The evidence suggests the biggest problem models face isn't syntax, instead it's coherence over scale. Models struggle with maintaining invariants across a codebase, understanding the ripple effects of changes, and reasoning about state over time. They're pattern matchers optimising for local plausibility, not architects holding the entire system in mind. The empirical literature shows that models are particularly vulnerable to naming-related errors like choosing misleading names, reusing names incorrectly, and losing track of which name refers to which value.

Vera addresses this by making everything explicit and verifiable. The model doesn't need to be right, it needs to be checkable. Names are replaced by structural references. Contracts are mandatory. Effects are typed. Every function is a specification that the compiler can verify against its implementation.

Traditional compilers produce diagnostics for humans: expected token '{'. Vera produces instructions for the model that wrote the code. Every error includes what went wrong, why, how to fix it with a concrete code example, and a spec reference. Every diagnostic has a stable error code (E001–E702) and is available as structured JSON via the --json flag.

vera check parses and type-checks. vera verify adds contract verification via Z3 — Tier 1 contracts (decidable arithmetic, comparisons, Boolean logic, ADTs, termination) are proved automatically. vera run compiles to WebAssembly and executes. vera compile --target browser produces a self-contained bundle (wasm + JS runtime + HTML) that runs in any browser.

Vera ships with specific files for LLM agents: SKILL.md (Complete language reference), AGENTS.md (Instructions for agent systems), and CLAUDE.md (Project orientation for Claude Code). Vera is in active development at v0.0.127 with 3,638 tests and 96% code coverage.