git:20261016.b71d3ab to git:20261016.0fa40bd

# Vera

> Vera is a statically typed, purely functional programming language designed for large language models to write. It uses typed slot references (`@T.n`) instead of variable names, requires contracts (preconditions, postconditions, effect declarations) on every function, and compiles to WebAssembly. Programs run at the command line via wasmtime or in the browser.

Vera uses De Bruijn indexing for bindings: `@Int.0` is the most recent `Int` binding, `@Int.1` the one before. There are no variable names. Contracts are mandatory — every function must declare `requires(...)`, `ensures(...)`, and `effects(...)`, and every recursive function a `decreases(...)` measure or the `Diverge` effect. The Z3 SMT solver verifies contracts statically where possible; every contract is also compiled as a runtime check where code generation can express it, and most of what can be neither proved nor guarded is disclosed (#1695 tracks the contracts that are not). All side effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, Diverge) are tracked in the type system via algebraic effects.

The reference compiler is written in Python; its releases are listed on [GitHub](https://github.com/aallan/vera/releases) and [PyPI](https://pypi.org/project/veralang/). Install the `veralang` distribution from PyPI, or use `pip install -e ".[dev]"` from the repository — the recommended route for agents, since it includes the examples, conformance programs and specification the language reference teaches from.

## Homepage

- [Vera](https://veralang.dev/index.md): Markdown companion to veralang.dev — project overview, thesis, design principles, key features, quick install, and links to the full documentation set.

## Language Reference

- [SKILL.md](https://veralang.dev/SKILL.md): Complete language reference — syntax, types, slot references, contracts, effects, built-in functions, common mistakes, and working examples. This is the primary document for writing Vera code.

## Quick Start

- [AGENTS.md](https://raw.githubusercontent.com/aallan/vera/main/AGENTS.md): Instructions for AI agents — workflow, commands, error handling, and essential rules for writing correct Vera.

- [FAQ](https://raw.githubusercontent.com/aallan/vera/main/FAQ.md): Design rationale — why no variable names, what gets verified, comparison to Dafny/Lean/Koka, research citations.

- [TOOLCHAIN.md](https://raw.githubusercontent.com/aallan/vera/main/TOOLCHAIN.md): The CLI cookbook — driving the toolchain to write, verify, test, run, and debug Vera, and the `builtins`/`effects`/`errors` introspection commands.

- [DE_BRUIJN.md](https://raw.githubusercontent.com/aallan/vera/main/DE_BRUIJN.md): Typed slot references in depth — worked examples and the commutative-operations trap.

- [ENVIRONMENT.md](https://raw.githubusercontent.com/aallan/vera/main/ENVIRONMENT.md): Every `VERA_*` environment variable — provider keys, runtime knobs, and debug flags.

- [KNOWN_ISSUES.md](https://raw.githubusercontent.com/aallan/vera/main/KNOWN_ISSUES.md): Known bugs and limitations, each with its tracking issue.

- [LSP_SERVER.md](https://raw.githubusercontent.com/aallan/vera/main/LSP_SERVER.md): The language server — live proof-aware diagnostics, hover, slot go-to-definition, hole completion, and the custom proof-delta methods for coding agents (vera/speculativeEdit, vera/proposeEdit, vera/strengthenContract, vera/addEffect).

## Specification

- [Chapter 0: Introduction](https://raw.githubusercontent.com/aallan/vera/main/spec/00-introduction.md): Language philosophy and design goals.

- [Chapter 1: Lexical Structure](https://raw.githubusercontent.com/aallan/vera/main/spec/01-lexical-structure.md): Tokens, literals, keywords, and comments.

- [Chapter 2: Types](https://raw.githubusercontent.com/aallan/vera/main/spec/02-types.md): Primitive types, composite types, type aliases, and generics.

- [Chapter 3: Slot References](https://raw.githubusercontent.com/aallan/vera/main/spec/03-slot-references.md): De Bruijn indexing, binding rules, and resolution.

- [Chapter 4: Expressions](https://raw.githubusercontent.com/aallan/vera/main/spec/04-expressions.md): Arithmetic, comparison, logical, and let expressions.

- [Chapter 5: Functions](https://raw.githubusercontent.com/aallan/vera/main/spec/05-functions.md): Function declarations, closures, generics, and mutual recursion.

- [Chapter 6: Contracts](https://raw.githubusercontent.com/aallan/vera/main/spec/06-contracts.md): Preconditions, postconditions, termination measures, and quantifiers.

- [Chapter 7: Effects](https://raw.githubusercontent.com/aallan/vera/main/spec/07-effects.md): Algebraic effects, handlers, IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, and Diverge.

- [Chapter 8: Modules](https://raw.githubusercontent.com/aallan/vera/main/spec/08-modules.md): Module system, imports, and visibility.

- [Chapter 9: Standard Library](https://raw.githubusercontent.com/aallan/vera/main/spec/09-standard-library.md): All built-in functions — arrays, strings, maps, sets, decimals, JSON, HTML, markdown, regex, numeric, type conversions.

- [Chapter 10: Grammar](https://raw.githubusercontent.com/aallan/vera/main/spec/10-grammar.md): Complete LALR(1) grammar in Lark notation.

- [Chapter 11: Compilation](https://raw.githubusercontent.com/aallan/vera/main/spec/11-compilation.md): Compilation model and WebAssembly code generation.

- [Chapter 12: Runtime](https://raw.githubusercontent.com/aallan/vera/main/spec/12-runtime.md): Runtime execution, memory management, and GC.

- [Chapter 13: WASI Preview 2 Target](https://raw.githubusercontent.com/aallan/vera/main/spec/13-wasi.md): The `wasi-p2` compilation target — experimental WASI 0.2 components, the `--world server` wasi:http backend, and the divergences from the core runtime.

- [Implementation Status](https://veralang.dev/implementation-status.md): Every `Status:` callout in the specification, collected — the boundary between what the reference compiler ships and what the chapters describe.

## Examples

## Compiler and Tooling

- [README](https://raw.githubusercontent.com/aallan/vera/main/README.md): Project overview, installation, and getting started.

- [EXAMPLES](https://raw.githubusercontent.com/aallan/vera/main/EXAMPLES.md): Language tour with code examples.

- [DESIGN](https://raw.githubusercontent.com/aallan/vera/main/DESIGN.md): Technical decisions and prior art.

- [CHANGELOG](https://raw.githubusercontent.com/aallan/vera/main/CHANGELOG.md): Version history and release notes.

- [ROADMAP](https://raw.githubusercontent.com/aallan/vera/main/ROADMAP.md): Forward-looking language roadmap.

- [HISTORY](https://raw.githubusercontent.com/aallan/vera/main/HISTORY.md): How the compiler was built.

- [Compiler Architecture](https://raw.githubusercontent.com/aallan/vera/main/vera/README.md): Compiler internals — pipeline stages, module map, design patterns.

## Optional

- [TESTING.md](https://raw.githubusercontent.com/aallan/vera/main/TESTING.md): Test suite architecture, coverage data, and test conventions.

- [CONTRIBUTING.md](https://raw.githubusercontent.com/aallan/vera/main/CONTRIBUTING.md): Contribution guidelines.