# 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(...)`. The Z3 SMT solver verifies contracts statically where possible; remaining contracts become runtime assertions. All side effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, Diverge) are tracked in the type system via algebraic effects.

Current version: 0.1.9. The reference compiler is written in Python. Install the `veralang` distribution from PyPI or use `pip install -e ".[dev]"` from the repository.

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

## Examples

- [examples/](https://github.com/aallan/vera/tree/main/examples): 42 verified example programs covering closures, generics, effects, pattern matching, string operations, async, markdown, JSON, HTML, HTTP, inference, regex, modules, and more.

## 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.
- [KNOWN_ISSUES.md](https://raw.githubusercontent.com/aallan/vera/main/KNOWN_ISSUES.md): Known bugs and limitations.
- [CONTRIBUTING.md](https://raw.githubusercontent.com/aallan/vera/main/CONTRIBUTING.md): Contribution guidelines.
- [Conformance Suite](https://github.com/aallan/vera/tree/main/tests/conformance): 179 programs validating every language feature against the spec.
