Vera (v-EER-a) is a programming language designed for large language models (LLMs) to write, not humans.

The name comes from the Latin veritas (truth). In Vera, verification is a first-class citizen, not an afterthought.

Programming languages have always co-evolved with their users. Assembly emerged from hardware constraints. C emerged from operating system needs. Python emerged from productivity needs. If models become the primary authors of software, it is consistent for languages to adapt to that.

The evidence suggests the biggest problem models face isn't syntax — 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.

Vera addresses this by making everything explicit and verifiable. The model doesn't need to be right — it needs to be checkable.

1. Checkability over correctness. Code that can be mechanically checked. When wrong, the compiler provides a natural language explanation of the error with a concrete fix — an instruction, not a status report.
2. Explicitness over convenience. All state changes declared. All effects typed. All function contracts mandatory. No implicit behaviour.
3. One canonical form. Every construct has exactly one textual representation. No style choices.
4. Structural references over names. Bindings referenced by type and positional index (@T.n), not arbitrary names.
5. Contracts as the source of truth. Every function declares what it requires and guarantees. The compiler verifies statically where possible.
6. Constrained expressiveness. Fewer valid programs means fewer opportunities for the model to be wrong.

• No variable names — typed De Bruijn indices (@T.n) replace traditional variable names
• Full contracts — mandatory preconditions, postconditions, invariants, and effect declarations on all functions
• Algebraic effects — 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 verification via Z3, guided verification with hints, runtime fallback
• Diagnostics as instructions — every error message is a natural language explanation with a concrete fix, designed for LLM consumption
• Compiles to WebAssembly — portable, sandboxed execution

Every function declares what it requires, what it guarantees, and what effects it performs. Even a one-liner has a full contract. Effects are declared before use, and effect operations use qualified calls (IO.print). effects(<IO>) tells the compiler (and the model) that this function interacts with the outside world.

effect IO {
  op print(String -> Unit);
}

public fn main(@Unit -> @Unit)
  requires(true)
  ensures(true)
  effects(<IO>)
{
  IO.print("Hello, World!")
}

examples/hello_world.vera — run with vera run examples/hello_world.vera

There are no variable names. @Int.0 refers to the most recent Int binding — a typed positional index, like De Bruijn indices but namespaced by type. The ensures clause is a machine-checkable promise: the result is non-negative and equals the absolute value of the input. The compiler verifies this via SMT solver.

public fn absolute_value(@Int -> @Nat)
  requires(true)
  ensures(@Nat.result >= 0)
  ensures(@Nat.result == @Int.0 || @Nat.result == -@Int.0)
  effects(pure)
{
  if @Int.0 >= 0 then {
    @Int.0
  } else {
    -@Int.0
  }
}

examples/absolute_value.vera — run with vera run examples/absolute_value.vera --fn absolute_value -- -42

requires(@Int.1 != 0) means this function cannot be called with a zero divisor. The compiler checks every call site to prove the precondition holds. If it cannot prove it, the code does not compile. 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
}

examples/safe_divide.vera — run with vera run examples/safe_divide.vera --fn safe_divide -- 3 10

Vera is pure by default. State changes must be declared as effects. effects(<State<Int>>) says this function reads and writes an integer. The ensures clause specifies exactly how the state changes: the new value equals the old value plus one. Handlers (not shown) provide the actual state implementation — an in-memory cell in production, a mock in tests.

public fn increment(@Unit -> @Unit)
  requires(true)
  ensures(new(State<Int>) == old(State<Int>) + 1)
  effects(<State<Int>>)
{
  let @Int = get(());
  put(@Int.0 + 1);
  ()
}

examples/increment.vera — this example uses State<Int> effects, which require effect handler compilation (#53) before vera run can execute them

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. The compiler's output is designed to be fed directly back to the model as corrective context.

Error in main.vera at line 12, column 1:

    private fn add(@Int, @Int -> @Int)
    ^

  Function "add" is missing its contract block. Every function in Vera
  must declare requires(), ensures(), and effects() clauses between the
  signature and the body.

  Add a contract block after the signature:

    private fn add(@Int, @Int -> @Int)
      requires(true)
      ensures(@Int.result == @Int.0 + @Int.1)
      effects(pure)
    {
      ...
    }

  See: Chapter 5, Section 5.1 "Function Structure"

This principle applies at every stage: parse errors, type errors, effect mismatches, verification failures, and contract violations all produce natural language explanations with actionable fixes.

Vera is in active development. The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, and runtime contract insertion — is working. Programs compile to WebAssembly and execute via wasmtime. See the roadmap for what's next.

The language specification is in draft across 13 chapters:

• Ch 0: Introduction and Philosophy — Design goals, the LLM-first premise, and the principles behind mandatory contracts, slot references, and algebraic effects.
• Ch 1: Lexical Structure — Source encoding (UTF-8), whitespace handling, indentation-free formatting, and token conventions.
• Ch 2: Types — Primitive types, algebraic data types, parametric polymorphism, refinement types with logical predicates, and function types with effect annotations.
• Ch 3: Slot References — The @T.n binding mechanism where bindings are referenced by type and positional index rather than variable names.
• Ch 4: Expressions and Statements — Expression-oriented design where blocks and nearly all constructs produce values. let bindings are the only statement form.
• Ch 5: Functions — Mandatory parameter types, return types, contracts, effect declarations, and body expressions. Functions are the primary abstraction unit.
• Ch 6: Contracts — Preconditions, postconditions, and decreases clauses as executable specifications that the implementation must satisfy.
• Ch 7: Effects — Pure-by-default semantics with algebraic effects for state, I/O, and exceptions, inspired by Koka.
• Ch 8: Modules — File-based module system with dotted paths, selective and wildcard imports, public/private visibility, and cross-module verification.
• Ch 9: Standard Library — Built-in types (Option, Result, Array), effects (IO, State), and functions that cannot be expressed purely in user code.
• Ch 10: Formal Grammar — Complete EBNF grammar compatible with the Lark LALR(1) parser generator.
• Ch 11: Compilation Model — The pipeline from source to WAT/WASM, including Tier 1 (static) and Tier 3 (runtime) contract classification.
• Ch 12: Runtime and Execution — The wasmtime-based runtime providing effect implementations, linear memory management, and trap handling.

The compiler has 1,209 tests with 88% code coverage, enforced by pre-commit hooks and CI across 6 Python/OS combinations. Every commit validates all 14 example programs and 96 specification code blocks. See TESTING.md for the full testing reference -- coverage tables, test helpers, CI pipeline, and infrastructure details.

Development follows an interleaved spiral — each phase adds a complete compiler layer with tests, docs, and working examples before moving to the next.

C8 addresses the accumulated technical debt and UX gaps before v0.1.0. Open issues are grouped into sub-phases ordered by impact and dependency.

C8a — Refactoring — reduce file sizes to improve maintainability

• #99 decompose checker.py (~1,900 lines) into checker/ submodules (v0.0.40)
• #100 decompose wasm.py (~2,300 lines) into wasm/ submodules (v0.0.41)
• #155 decompose codegen.py (~2,140 lines) into codegen/ submodules (v0.0.46)

C8b — Diagnostics and tooling — improve the developer (human and LLM) experience

• #112 informative runtime contract violation error messages (v0.0.42)
• #80 stable error code taxonomy for diagnostics (v0.0.43)
• #95 LALR grammar fix for module-qualified call syntax (v0.0.44)
• #75 vera fmt canonical formatter (v0.0.45)
• #79 vera test contract-driven testing (v0.0.47)
• #156 improve test coverage for WASM translation modules (v0.0.48)

C8c — Verification depth — expand what the SMT solver can prove

• #136 register Diverge as built-in effect (v0.0.49)
• #13 expand SMT decidable fragment (Tier 2 verification)
• #45 decreases clause termination verification

C8d — Type system — close type-checking gaps

• #20 TypeVar subtyping
• #21 effect row unification and subeffecting
• #55 minimal type inference

C8e — Codegen gaps — extend WASM compilation

• #154 list_ops.vera runtime failure — recursive generic ADT codegen
• #110 name collision detection for flat module compilation
• #131 nested constructor pattern codegen
• #53 Exn<E> and custom effect handler compilation
• #51 garbage collection for WASM linear memory
• #132 arrays of compound types in codegen
• #52 dynamic string construction
• #134 string built-in operations (length, concat, slice)
• #106 universal to-string conversion (Show/Display)
• #56 incremental compilation

Module refinements, lexical extensions, and IO runtime — completing the existing language before adding new features.

• #127 module re-exports
• #135 IO operations (read_line, read_file, write_file)
• #139 scientific notation for float literals
• #169 vera test Float64 and compound type input generation
• #170 vera test hypothesis integration and advanced testing

New effects, types, abilities, and standard library extensions (spec §0.8).

• #60 abilities and type constraints
• #62 standard library collections (Set, Map, Decimal)
• #133 array operations (map, fold, slice)
• #58 JSON standard library type
• #147 Markdown standard library type
• #57 <Http> network access effect
• #59 <Async> futures and promises
• #61 <Inference> LLM inference effect

• #130 package system and registry
• #143 comprehensive example programs

The features on the C9 roadmap -- <Http> (#57), <Inference> (#61), and the Markdown type (#147) -- converge into a single design goal: an LLM should be able to write a short Vera function that searches the web, feeds the results into another model, and returns typed, contract-checked output. No scaffolding, no untyped string wrangling, no unchecked side effects.

A research function that searches YouTube, summarises the results via LLM inference, and returns structured Markdown might look like this:

public fn research_topic(@String -> @MdBlock)
  requires(length(@String.0) > 0)
  ensures(md_has_heading(@MdBlock.result, 1))
  effects(<Http, Inference>)
{
  let @Array<MdBlock> = youtube_search(@String.0, 5);
  let @String = md_render_all(@Array<MdBlock>.0);
  let @String = complete("Summarise this research:\n" ++ @String.0);
  md_parse(@String.0)
}

Five lines of logic. The signature carries all the ceremony -- parameter types, contracts, effect declarations -- so the body reads like a pipeline. The <Http, Inference> effect annotation means a caller that only permits <Http> cannot invoke this function, and an effect handler can mock both effects for deterministic testing. The postcondition md_has_heading(@MdBlock.result, 1) constrains the shape of the LLM response at the type level: if the model produces output that lacks a top-level heading, the contract fails.

This is what "designed for LLMs to write" means in practice: the language makes the intent machine-checkable, the side effects explicit, and the output structurally typed -- in fewer lines than most languages need for a HTTP request.

• Python 3.11+
• Git

The install step pulls in several dependencies via pip — Lark (parser generator), Z3 (SMT solver for contract verification), and wasmtime (WASM runtime for compilation and execution). These all install into the virtual environment and don't require separate system packages.

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

$ vera check examples/absolute_value.vera
OK: examples/absolute_value.vera

vera check parses the file, builds the AST, and runs the type checker. vera typecheck is an explicit alias for the same command.

$ vera verify examples/safe_divide.vera
OK: examples/safe_divide.vera
Verification: 2 verified (Tier 1)

vera verify runs the type checker and then verifies contracts using Z3. Tier 1 contracts (decidable arithmetic, comparisons, Boolean logic) are proved automatically. Contracts that Z3 cannot decide are reported as Tier 3 (runtime checks) with a warning.

vera fmt examples/absolute_value.vera

vera fmt prints the canonical form of a Vera source file to stdout. Add --write to reformat in place, or --check to verify a file is already canonical (exits 1 if not):

vera fmt --write examples/absolute_value.vera   # reformat in place
vera fmt --check examples/absolute_value.vera   # check only (for CI)

$ vera compile examples/hello_world.vera
Compiled: examples/hello_world.wasm (1 function exported)

vera compile runs the full pipeline (parse → typecheck → verify → compile) and writes a .wasm binary. Add --wat to print the human-readable WAT text instead:

vera compile --wat examples/hello_world.vera

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

vera run compiles and executes the program. By default it calls main. Use --fn to call a different function, and pass arguments after --:

$ vera run examples/factorial.vera --fn factorial -- 5
120

vera parse examples/safe_divide.vera

This prints the parse tree, useful for debugging syntax issues.

vera ast examples/factorial.vera

This prints the typed abstract syntax tree. Add --json for JSON output:

vera ast --json examples/factorial.vera

pytest tests/ -v

For contributors, install pre-commit hooks to catch issues before they reach CI:

pre-commit install

This runs mypy, pytest, trailing whitespace checks, and validates all examples on every commit.

Create a file hello.vera:

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

Then check it:

vera check hello.vera

See examples/ for more programs, and the language specification for the full language reference.

Vera ships with three files for LLM agents:

• SKILLS.md — Complete language reference for agents writing Vera code. Covers syntax, slot references, contracts, effects, common mistakes, and working examples.
• AGENTS.md — Instructions for any agent system (Copilot, Cursor, Windsurf, custom). Covers both writing Vera code and working on the compiler.
• CLAUDE.md — Project orientation for Claude Code. Key commands, layout, workflows, and invariants.

If you're working in this repo, Claude Code discovers SKILLS.md and CLAUDE.md automatically. For other projects, install the skill manually:

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

The skill is now available across all your Claude Code projects. Claude will read it automatically when you ask it to write Vera code.

1. Create a folder called vera-language containing a single file named Skill.md (copy SKILLS.md into this folder and rename it to Skill.md)
2. Compress the folder into a ZIP file — the structure should be vera-language.zip → vera-language/ → Skill.md
3. In Claude.ai, go to Settings > Capabilities > Skills and upload the ZIP file
4. The skill is now available in your conversations — Claude will use it automatically when you ask it to write Vera code

from anthropic.lib import files_from_dir

client = anthropic.Anthropic()

skill = client.beta.skills.create(
    display_title="Vera Language",
    files=[("SKILL.md", open("SKILLS.md", "rb"))],
    betas=["skills-2025-10-02"],
)

# Use in a message
response = client.beta.messages.create(
    model="claude-sonnet-4-6",
    max_tokens=4096,
    betas=["code-execution-2025-08-25", "skills-2025-10-02"],
    container={"skills": [{"type": "custom", "skill_id": skill.id, "version": "latest"}]},
    tools=[{"type": "code_execution_20250825", "name": "code_execution"}],
    messages=[{"role": "user", "content": "Write a Vera function that..."}],
)

Point the model at SKILLS.md by including it in the system prompt, as a file attachment, or as a retrieval document. The file is self-contained and works with any model that can read markdown.

If you are an LLM agent, read SKILLS.md for the full language reference. Here is the minimal workflow:

Install (if not already available):

git clone https://github.com/aallan/vera.git && cd vera
python -m venv .venv && source .venv/bin/activate && pip install -e .

Write a .vera file, then check, verify, and run it:

vera check your_file.vera              # type-check
vera verify your_file.vera             # type-check + verify contracts
vera test your_file.vera               # contract-driven testing via Z3 + WASM
vera compile your_file.vera            # compile to .wasm binary
vera run your_file.vera                # compile + execute
vera run your_file.vera --fn f -- 42   # call function f with argument 42
vera fmt your_file.vera                # format to canonical form (stdout)
vera verify --json your_file.vera      # verify with JSON diagnostics

If the check or verification fails, the error message tells you exactly what went wrong and how to fix it. Feed the error back into your context and correct the code. Use --json for machine-readable output that includes structured diagnostics with location, rationale, and fix suggestions.

Essential rules:

1. Every function needs requires(), ensures(), and effects() between the signature and body
2. Use @Type.index to reference bindings — @Int.0 is the most recent Int, @Int.1 is the one before that
3. Declare all effects — effects(pure) for pure functions, effects(<IO>) for IO, etc.
4. Recursive functions need a decreases() clause
5. Match expressions must be exhaustive

vera/
├── SKILLS.md                      # Language reference for LLM agents
├── AGENTS.md                      # Instructions for any AI agent system
├── CLAUDE.md                      # Project orientation for Claude Code
├── TESTING.md                     # Testing reference (single source of truth)
├── CONTRIBUTING.md                # Contributor guidelines
├── CODE_OF_CONDUCT.md             # Contributor Covenant
├── SECURITY.md                    # Security policy
├── CHANGELOG.md                   # Version history
├── LICENSE                        # MIT licence
├── pyproject.toml                 # Package configuration
├── .pre-commit-config.yaml        # Pre-commit hook configuration
├── .github/workflows/             # CI pipeline
│   ├── ci.yml                     #   Tests, type checking, linting
│   └── codeql.yml                 #   GitHub CodeQL analysis
├── spec/                          # Language specification (13 chapters)
│   ├── 00-introduction.md         # Design goals and philosophy
│   ├── 01-lexical-structure.md    # Tokens, operators, formatting rules
│   ├── 02-types.md                # Type system with refinement types
│   ├── 03-slot-references.md      # The @T.n reference system
│   ├── 04-expressions.md          # Expressions and statements
│   ├── 05-functions.md            # Function declarations and contracts
│   ├── 06-contracts.md            # Verification system
│   ├── 07-effects.md              # Algebraic effect system
│   ├── 08-modules.md              # Module system
│   ├── 09-standard-library.md     # Built-in types, effects, functions
│   ├── 10-grammar.md              # Formal EBNF grammar
│   ├── 11-compilation.md          # Compilation model and WASM target
│   └── 12-runtime.md              # Runtime execution and host bindings
├── vera/                          # Reference compiler (Python)
│   ├── __init__.py                # Version constant
│   ├── README.md                  # Compiler architecture docs
│   ├── grammar.lark               # Lark LALR(1) grammar
│   ├── parser.py                  # Parser module
│   ├── ast.py                     # Typed AST node definitions
│   ├── transform.py               # Lark parse tree → AST transformer
│   ├── types.py                   # Internal type representation
│   ├── registration.py            # Function signature registration
│   ├── environment.py             # Type environment and slot resolution
│   ├── checker/                   # Type checker (mixin package)
│   │   ├── core.py                #   Orchestration, diagnostics, contracts
│   │   ├── resolution.py          #   AST TypeExpr → semantic Type
│   │   ├── modules.py             #   Cross-module registration
│   │   ├── registration.py        #   Pass 1 forward declarations
│   │   ├── expressions.py         #   Expression synthesis, operators
│   │   ├── calls.py               #   Function/constructor/module calls
│   │   └── control.py             #   If/match, patterns, handlers
│   ├── smt.py                     # Z3 SMT translation layer
│   ├── verifier.py                # Contract verifier
│   ├── wasm/                     # WASM translation layer (8 modules)
│   │   ├── context.py            #   Composed WasmContext, expression dispatcher
│   │   ├── helpers.py            #   WasmSlotEnv, StringPool, type mapping helpers
│   │   ├── inference.py          #   Type inference and utilities
│   │   ├── operators.py          #   Binary/unary operators, quantifiers
│   │   ├── calls.py              #   Function calls, effect handlers
│   │   ├── closures.py           #   Closures, free variable analysis
│   │   └── data.py               #   Constructors, match, arrays
│   ├── codegen/                    # Code generation orchestrator (11 modules)
│   │   ├── api.py               #   Public API, compile(), execute()
│   │   ├── core.py              #   Composed CodeGenerator class
│   │   ├── modules.py           #   Cross-module call detection
│   │   ├── registration.py      #   Function/ADT registration
│   │   ├── monomorphize.py      #   Generic instantiation
│   │   ├── functions.py         #   Function body compilation
│   │   ├── closures.py          #   Closure lifting
│   │   ├── contracts.py         #   Runtime contract insertion
│   │   ├── assembly.py          #   WAT module assembly
│   │   └── compilability.py     #   Compilability checks
│   ├── tester.py                  # Contract-driven testing engine
│   ├── resolver.py                # Module resolver
│   ├── formatter.py               # Canonical code formatter
│   ├── errors.py                  # LLM-oriented diagnostics
│   └── cli.py                     # Command-line interface
├── examples/                      # 14 example Vera programs
├── tests/                         # Test suite (see TESTING.md)
└── scripts/                       # CI and validation scripts
    ├── check_examples.py          # Verify all .vera examples
    ├── check_spec_examples.py     # Verify spec code blocks parse
    ├── check_readme_examples.py   # Verify README code blocks parse
    └── check_version_sync.py      # Verify version consistency

For compiler architecture, pipeline internals, design patterns, and how to extend the compiler, see vera/README.md.

Vera draws on ideas from (see also Spec Ch 0, Section 0.4):

• Eiffel — Design by Contract, the originator of require/ensure
• Dafny — full functional verification with preconditions, postconditions, and termination measures
• F* — refinement types, algebraic effects, and SMT-based verification
• Koka — row-polymorphic algebraic effects
• Liquid Haskell — refinement types checked via SMT solver
• Idris — totality checking and termination proofs
• SPARK/Ada — contract-based industrial verification ("if it compiles, it's correct")
• bruijn — De Bruijn indices as surface syntax
• TLA+ / Alloy — executable specifications that constrain what implementations can do

See CONTRIBUTING.md for guidelines on how to contribute to Vera. For compiler internals — pipeline architecture, module map, design patterns, and how to extend the compiler — see vera/README.md.

See CHANGELOG.md for a history of changes.

Vera is licensed under the MIT License.

Copyright © 2026 Alasdair Allan

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.