@reader.0 → humans · scroll @reader.1 → agents · SKILL.md · llms.txt · .md
veralang.dev

# A programming language designed for LLMs to write, not humans.

From the Latin veritas — truth. In Vera, verification is a first-class citizen.

GitHub Install For Agents → SKILL.md

v0.1.9

@section.01 · the thesis

## Why?

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 biggest problem models face isn't syntax — it's coherence over scale. Models are pattern matchers optimising for local plausibility, not architects holding the entire system in mind.

The empirical literature shows models are particularly vulnerable to naming-related errors: 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 the compiler verifies against its implementation.

For deeper questions about the design — why no variable names, what gets verified, how Vera compares to Dafny, Lean, and Koka — see the FAQ.

@section.02 · the syntax is the argument

## What Vera Looks Like

Nothing is implicit. The signature declares types, preconditions, postconditions, and effects. The compiler verifies the contract via SMT solver. Division by zero is not a runtime error — it is a type error.

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

Read the slots. `@Int.1` is the first parameter, `@Int.0` is the second — De Bruijn indexing, most-recent first. No variable names means no naming bug is possible. The `requires` clause is what lifts divide-by-zero from a runtime crash to a compile-time error. examples/safe_divide.vera.

    public fn fizzbuzz(@Nat -> @String)
      requires(true)
      ensures(true)
      effects(pure)
    {
      if @Nat.0 % 15 == 0 then {
        "FizzBuzz"
      } else {
        if @Nat.0 % 3 == 0 then {
          "Fizz"
        } else {
          if @Nat.0 % 5 == 0 then {
            "Buzz"
          } else {
            "\(@Nat.0)"
          }
        }
      }
    }

A program everyone knows. Interpolation uses `"\(@Nat.0)"` — the slot reference substitutes in directly with auto-conversion. There are no naming decisions to make, and none to hallucinate. examples/fizzbuzz.vera.

    public fn classify_sentiment(@String -> @Result<String, String>)
      requires(string_length(@String.0) > 0)
      ensures(true)
      effects(<Inference>)
    {
      let @String = string_concat("Classify as Positive, Negative, or Neutral: ", @String.0);
      Inference.complete(@String.0)
    }

LLM calls are effects. Where the two functions above are `effects(pure)`, this one declares `<Inference>`. A caller that does not permit `<Inference>` cannot invoke it. The effect system makes model calls visible in every signature that uses them, all the way up. examples/inference.vera.

    public fn research_topic(@String -> @Result<String, String>)
      requires(string_length(@String.0) > 0)
      ensures(true)
      effects(<Http, Inference>)
    {
      let @String = url_encode(@String.0);
      let @Result<String, String> = Http.get(string_concat("https://api.duckduckgo.com/?format=json&q=", @String.0));
      match @Result<String, String>.0 {
        Ok(@String) -> Inference.complete(string_concat("Summarise this in one paragraph:\n\n", @String.0)),
        Err(@String) -> Err(@String.0)
      }
    }

Effects compose. `<Http, Inference>` is the row — both must be permitted. `Inference` auto-detects the provider (Anthropic, OpenAI, Moonshot, Mistral) from whichever API key is set. Postconditions can constrain model output; Z3 cannot know what a model will return at compile time, so these become runtime assertions that trap on violation.

    public fn find_user(@String -> @Result<Array<Array<Option<String>>>, String>)
      requires(string_length(@String.0) > 0)
      ensures(true)
      effects(<DB>)
    {
      DB.query("SELECT name, email FROM users WHERE name = ?", [Some(@String.0)])
    }

SQL injection won’t compile. Nearly every SQL injection starts the same way — a query assembled from a value that came from outside the program. Vera makes that unwriteable. The SQL text has to be written into the source, so the query is fixed when the program compiles and outside data can only reach the database through the `?` placeholders and the params array. Build the query out of the parameter with `string_concat` instead and the answer is `[E207]`: not a warning, not a lint you can silence, but a type error you cannot configure away. examples/database.vera.

    [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.

      Vera requires all functions to have explicit contracts so that every function's
      behaviour is mechanically checkable.

      Fix:

        Add a contract block after the signature:

          private fn example(@Int -> @Int)
            requires(true)
            ensures(@Int.result >= 0)
            effects(pure)
          {
            ...
          }

      See: Chapter 5, Section 5.2 "Function Declaration Syntax"

Diagnostics as instructions. Every error is an instruction for the model that wrote the code: what went wrong, why, how to fix it, and a spec reference. Parse errors, type errors, effect mismatches, verification failures, and contract violations all produce the same shape.
@section.03 · empirical evidence

## VeraBench

Six of nine frontier models write 100% correct Vera — a language none of them has ever seen before.

A 60-problem benchmark across 5 difficulty tiers — pure arithmetic, strings and arrays, ADTs and exhaustive matching, recursion with termination proofs, multi-function effect propagation. Nine models, three providers, four modes each: Vera written against a full specification, Vera written from a plain English description with the model authoring its own contracts, and the same problems in Python and TypeScript. The table shows three of the four, and reports % solved: the model wrote code, it compiled, it ran, and the output matched. A refusal, a compile failure, a crash and a wrong answer all count alike as not solved.

Model | Vera | Python | TypeScript
--- | --- | --- | ---
Claude Fable 5 ceiling | 100% | 97% | 97%
GPT-5.6 Sol (pro) ceiling | 100% | 95% | 100%
Claude Opus 5 flagship | 100% | 95% | 100%
Claude Opus 4.8 flagship | 93% | 98% | 100%
GPT-5.6 Sol flagship | 98% | 95% | 100%
Kimi K3 flagship | 100% | 100% | 100%
Claude Sonnet 5 workhorse | 97% | 98% | 100%
GPT-5.6 Terra workhorse | 100% | 95% | 100%
Kimi K2.6 workhorse | 100% | 97% | 100%

Frontier models now write Vera as well as they write the languages they were trained on. Vera has the highest score, or level with it, for six of the nine models.

Mandatory contracts and typed slot references appear to provide enough structure to compensate for zero training data. Every successful program came from a single skill file in context, written by a model that had never seen the language before.

The difference between the Python and TypeScript results is probably not random. Python is dynamically typed, so a type error surfaces when the code runs; TypeScript is statically typed and rejects the same error before anything runs. Vera sits with TypeScript but goes further, making `requires`, `ensures` and `effects` mandatory on every function and replacing variable names with typed slot references. Sort the three languages by how much they constrain the model rather than by how much of them it has read, and the ordering stops looking accidental: the two languages that constrain the model finish ahead of the one that doesn't.

TypeScript earns its results due to its inclusion in model training data. Vera earns very nearly the same results without that. Whatever familiarity is buying TypeScript, the additional constraints Vera provides appear to be supplying by other means.

It's still early days. The benchmark is just a single run per model, no pass@k; and with just sixty problems each problem is worth just under two percentage points, so most of the gaps above are only one or two problems wide. However, it looks like language design can, at least sometimes, outweigh sheer volume of training data. Which, if you're in the business of generating code at any scale, is a reasonably interesting thing to be true.

Results from VeraBench v0.0.18 against Vera v0.1.8. Inspired by HumanEval, MBPP, and DafnyBench.

vera-bench

@section.04 · reference

## Design & Features

Design principles

01
Checkability over correctness
Code the compiler can mechanically check. Every diagnostic carries a concrete fix in natural language.
02
Explicitness over convenience
All state changes declared. All effects typed. All contracts mandatory. No implicit behaviour.
03
One canonical form
Every construct has exactly one textual representation. `vera fmt` settles it.
04
Structural references over names
Bindings referenced by type and positional index (`@T.n`), not arbitrary names.
05
Contracts as the source of truth
Every function declares what it requires and guarantees. The compiler verifies statically where possible.
06
Constrained expressiveness
Fewer valid programs means fewer opportunities for the model to be wrong.

Key features

No variable names
Typed De Bruijn indices (`@T.n`) replace variable names: `@Int.0` is the most-recent `Int` binding, `@Int.1` the one before. The whole class of naming hallucinations is removed at the language level, not caught after the fact.
Full contracts
Mandatory preconditions, postconditions, invariants, and effect declarations on every function. Z3 generates test inputs from the contracts and runs them through WASM — no manual test cases.
SQL injection won’t compile
The `<DB>` effect accepts only a literal query string — built from string literals, never spliced from a runtime value. Interpolating user input into SQL is a compile-time error (`E207`); every value flows through a `?` placeholder instead. Injection safety stops being a discipline you remember and becomes one the compiler enforces.
Algebraic effects
IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, Diverge — declared, typed, and handled explicitly. Pure by default.
Refinement types
Types that express constraints like “a list of positive integers of length `n`”.
Three-tier verification
Static via Z3 plus runtime fallback, shipped; the Z3-guided middle tier is specified, not yet implemented.
Language server
A warm Z3 session between keystrokes — proofs re-check at editor latency. Custom methods hand agents proof deltas before an edit lands.
Diagnostics as instructions
Every error is a natural-language explanation with a concrete fix, designed for LLM consumption.
LLM inference as effect
`Inference.complete` is an algebraic effect — typed, contract-verifiable, mockable. Anthropic, OpenAI, Moonshot, Mistral.
Typed stdlib
JSON, HTML, Markdown, HTTP, Regex, Decimal — built-in ADTs with parse/query/serialize.
Async / Future<T>
Futures carry an `<Async>` effect and compose with the rest of the effect system.
Verified HTTP handlers
An `<HttpServer>` effect marks a total `handle(Request -> Response)`. The accept loop lives in the host, so every handler contract is an ordinary proof obligation. `vera serve` runs it.
WASI 0.2 components
`vera compile --target wasi-p2` emits a component any stock wasip2 host runs (experimental; IO and Random surface). `--world server` packages a handler as a `wasi:http` component for `wasmtime serve`.
@section.05 · runtime

## Runs Everywhere

Vera compiles to WebAssembly. The same `.wasm` runs at the command line via wasmtime, in any browser with a self-contained JS runtime, or as a portable WASI 0.2 component under any stock wasip2 host.

### Command line

    $ vera run examples/hello_world.vera
    Hello, World!

    $ vera run examples/factorial.vera --fn factorial -- 10
    3628800

`vera run` compiles to WASM and executes via wasmtime. `--fn` picks any public function; arguments follow `--`.

### Browser

    $ vera compile --target browser \
        examples/hello_world.vera
    Browser bundle: examples/hello_world_browser/
      module.wasm
      runtime.mjs
      index.html

Self-contained — no bundler. Serve with any HTTP server (`python -m http.server`). `IO.print` writes to the page; all other operations work identically to the CLI. Parity tests enforce this on every PR. Note: `Inference.complete` errors in the browser — use a server-side proxy via `Http`.

### WASI components

    $ vera compile --target wasi-p2 --world server \
        examples/http_server.vera
    Compiled (WASI Preview 2 server component
    (run with: wasmtime serve <file>)): examples/http_server.wasm

    $ wasmtime serve examples/http_server.wasm
    Serving HTTP on http://0.0.0.0:8080/

`--target wasi-p2` emits a WASI 0.2 component any stock wasip2 host runs — `wasmtime run module.wasm` needs no flags and no Vera bindings (experimental; the IO and Random surface). `--world server` packages a `handle(Request -> Response)` program as a `wasi:http` component that `wasmtime serve` runs unmodified.

@section.06 · install

## Get Started

Python 3.11+. Everything installs into a virtual environment.

    # Install the toolchain from PyPI
    python -m venv .venv
    source .venv/bin/activate
    python -m pip install veralang
    vera version

    # Optional: the language server for editors and agents
    python -m pip install "veralang[lsp]"

The wheel ships the compiler and the `vera` command. For the full environment — the bundled examples, conformance suite, and specification the agent docs teach from — or for compiler development and unreleased changes, install from source.

    # Clone and install from source
    git clone https://github.com/aallan/vera.git
    cd vera
    python -m venv .venv
    source .venv/bin/activate
    pip install -e ".[dev]"

    # Check, verify, run, compile the bundled examples
    vera check examples/absolute_value.vera
    vera verify examples/safe_divide.vera
    vera run examples/hello_world.vera
    vera compile --target browser examples/hello_world.vera

There is out of the box support for three editors. Vera Language for Visual Studio Code is the fullest — install it from the Marketplace or with `code --install-extension veralang.vera-language`, and it starts `vera lsp` automatically for `.vera` files alongside syntax highlighting and language configuration. A Vim package covers Vim 8+ and Neovim, and a Vera `.tmbundle` covers Sublime Text and other editors that read TextMate grammars.

Live proof-aware diagnostics, hover, slot go-to-definition, and typed-hole completion come from the language server. The source install above (`.[dev]`) already includes it; on the PyPI route add it with `python -m pip install "veralang[lsp]"`, or use `pip install -e ".[lsp]"` for a lighter source checkout. Any editor with a generic LSP client can point at `vera lsp` directly.

@section.07 · for machines

## This page is also a machine-readable specification.

Every document here has an alternate in markdown, served on the same domain, discoverable through standard `<link rel="alternate">`, `llms.txt`, and the Mintlify `llms-txt` / `llms-full-txt` conventions.

SKILL.md
Complete language reference for writing Vera code — syntax, slots, contracts, effects, common mistakes, working examples.
AGENTS.md
Setup instructions for any agent system (Copilot, Cursor, Windsurf, custom). Writing Vera code and working on the compiler.
CLAUDE.md
Project orientation for Claude Code. Key commands, repo layout, workflows, invariants.
LSP_SERVER.md
The language server — live verification, and the custom proof-delta methods agents use to ask “does this edit still prove?” before committing it.
TOOLCHAIN.md
The CLI cookbook — driving the toolchain to write, verify, test, run, and debug Vera, plus the `builtins`/`effects`/`errors` introspection commands.

Claude Code discovers SKILL.md and CLAUDE.md automatically when working inside the repo. For other projects, install the skill manually:

    mkdir -p ~/.claude/skills/vera-language
    cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md

For other models: point them at SKILL.md via system prompt, file attachment, or retrieval. It's self-contained and works with any model that reads markdown.

The documents above are how machines read Vera. The language server is how they interrogate it: `vera lsp` holds a warm, incremental Z3 session between edits, and four custom methods — `vera/speculativeEdit`, `vera/proposeEdit`, `vera/strengthenContract`, `vera/addEffect` — let an agent learn whether an edit keeps, breaks, or strengthens a program's proofs before committing it, then apply it only through the verification gate.

    # vera/speculativeEdit — the proof delta for an in-memory edit
    {
      "ok": true,
      "proof_delta": {
        "newly_discharged": ["..."],
        "newly_undischarged": [],
        "timed_out": [],
        "removed": [],
        "unchanged": 11
      },
      "diagnostics": 0
    }

Vera is under active development

A complete compiler with 164 built-in functions, ten algebraic effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, Diverge), contract-driven testing via Z3, a language server with agent-facing proof deltas, and a 14-chapter specification. A 179-program conformance suite and 42 worked examples are validated against the spec on every pull request. All of it is developed openly on GitHub and released under the MIT licence.