aallan/vera

Vera: a programming language designed for LLMs to write

What it solves

LLMs often struggle with code coherence, maintaining invariants across large codebases, and reasoning about state. They are prone to naming errors and losing track of variable identities. Vera addresses these issues by replacing variable names with structural references and requiring explicit, verifiable contracts for every function.

How it works

Vera uses a unique approach to ensure code correctness:

  • Structural References: Instead of variable names, it uses typed De Bruijn indices (e.g., @Int.0) to avoid naming-related errors.
  • Mandatory Contracts: Every function must declare requires (preconditions), ensures (postconditions), and effects (side effects).
  • Static Verification: An SMT solver (Z3) attempts to prove that these contracts hold at compile time.
  • Three-Tier Verification: If a contract cannot be proven statically, the compiler inserts a runtime guard to catch errors before they cause silent failures.
  • Agent-Centric Diagnostics: Errors are designed as instructions for LLMs, providing the rationale and a concrete code example to fix the issue.

Who it’s for

  • LLM Agents: The language is specifically optimized for AI models to write, featuring documentation (SKILL.md) and instructions (AGENTS.md) tailored for agentic workflows.
  • Developers building AI-driven systems: For those needing high-assurance code generated by models.

Highlights"

  • Compiles to WebAssembly for execution in the CLI, browser, or WASI Preview 2 hosts.
  • Features an explicit effect system to track side effects like <Inference> or <Http>.
  • Includes a Language Server Protocol (LSP) for editor support.
  • Includes a benchmark (VeraBench) showing high success rates for models writing Vera compared to traditional languages.