llms-full.txt@docs · git:20261016.1805432 · 2026-10-16 · sha256 01fb8b3b18673d92
llms-full.txt@docs git:20261016.1805432B
Immutable. This exact content never changes and is served at /api/v1/blob/01fb8b3b18673d92.
# Vera — Language Reference Documentation
> 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 on every function, and compiles to WebAssembly.
This file contains the core Vera language documentation — language reference, agent instructions, FAQ, error codes, and formal grammar — compiled into a single document. For the full documentation index, including the specification and the supplementary docs, see llms.txt.
========================================================================
# Language Reference (SKILL.md)
========================================================================
# Vera Language Reference
Vera is a programming language designed for LLMs to write. It uses typed slot references instead of variable names, requires contracts on every function, and makes all effects explicit.
## Installation
Vera requires Python 3.11 or later. Node.js 22+ is optional (only needed for `vera compile --target browser` and browser parity tests).
**Recommended — install from the GitHub source checkout.** The checkout is the full environment this file teaches from: alongside the compiler and the `vera` CLI it carries the bundled `examples/`, the conformance suite in `tests/conformance/` (minimal working programs, named by spec chapter and feature), and the specification in `spec/`:
```bash
git clone https://github.com/aallan/vera.git && cd vera
python -m venv .venv && source .venv/bin/activate # Windows: .venv\Scripts\activate
python -m pip install -e .
```
For an editable source install with the language server, use `python -m pip install -e ".[lsp]"` — see [LSP_SERVER.md](https://github.com/aallan/vera/blob/main/LSP_SERVER.md). Verify the install end to end with the bundled example:
```bash
vera check examples/hello_world.vera # prints "OK: examples/hello_world.vera"
vera run examples/hello_world.vera # prints "Hello, World!"
```
**Toolchain only — install the released `veralang` distribution from PyPI.** This installs the `vera` command and all runtime dependencies (Lark parser, Z3 solver, wasmtime), but **not** the examples, conformance programs, or specification — those exist only in the checkout:
```bash
python -m venv .venv && source .venv/bin/activate # Windows: .venv\Scripts\activate
python -m pip install veralang
vera version
```
For the language server on this route, install `python -m pip install "veralang[lsp]"`.
If you are working on the compiler itself, install development dependencies too:
```bash
python -m pip install -e ".[dev]"
```
> **Platform support**: [README §Supported platforms](https://github.com/aallan/vera/blob/main/README.md#supported-platforms) lists the platforms and Python versions CI tests on, the ones that are out of scope (where install fails at dependency resolution), the workarounds, and the data behind the baseline.
>
> **For agents running in a sandbox** (Claude.ai, Code Interpreter, container-based execution environments, etc.): the steps above work. Sandboxes typically have Python, `git`, `pip`, and outbound network access — that's all Vera needs. **Run the install commands and verify with `vera run examples/hello_world.vera` before concluding that Vera "isn't available." Don't assume the sandbox lacks the toolchain — try it.**
>
> `pip install vera` installs a *different* package from PyPI (an ERAV citizen-science library — unrelated to this Vera). Use the `veralang` distribution or the GitHub source clone shown above; both install the `vera` command.
## Toolchain
See [TOOLCHAIN.md](https://github.com/aallan/vera/blob/main/TOOLCHAIN.md) for the CLI cookbook — driving the toolchain to write, verify, test, run, and debug Vera, plus the `builtins`/`effects`/`errors` introspection commands.
```bash
vera check file.vera # Parse and type-check (or "OK")
vera check --json file.vera # Type-check with JSON diagnostics
vera check --quiet file.vera # Type-check, suppress success output (errors still shown)
vera typecheck file.vera # Same as check (explicit alias)
vera verify file.vera # Type-check and verify contracts via Z3
vera verify --json file.vera # Verify with JSON diagnostics
vera verify --quiet file.vera # Verify, suppress success output (errors still shown)
vera verify --timeout-ms 60000 file.vera # Per-query Z3 budget in ms (default 10000; env VERA_Z3_TIMEOUT_MS)
vera compile file.vera # Compile to .wasm binary
vera compile --wat file.vera # Print WAT text (human-readable WASM)
vera compile --json file.vera # Compile with JSON diagnostics
vera compile --target browser file.vera # Compile + emit browser bundle (wasm + JS + html)
vera compile --target wasi-p2 file.vera # Emit a WASI Preview 2 component (IO+Random only)
vera compile --target wasi-p2 --world server file.vera # wasi:http server component (wasmtime serve)
vera run file.vera # Compile and execute (calls main)
vera run file.vera --fn f -- 42 # Call function f with Int argument
vera run file.vera --fn f -- 3.14 # Call function f with Float64 argument
vera run file.vera --fn f -- true # Call function f with Bool argument
vera run file.vera --fn f -- "hello" # Call function f with String argument
vera run --json file.vera # Run with JSON output
vera serve file.vera # Serve handle(Request -> Response) over HTTP (default :8000)
vera serve --port 8080 file.vera # Serve on a specific port
vera test file.vera # Contract-driven testing via Z3 + WASM
vera test --json file.vera # Test with JSON output
vera test --trials 50 file.vera # Limit trials per function (default 100)
vera test --distrust file.vera # Also execute proved functions; a failed proved check refutes the proof (E703)
vera test file.vera --fn f # Test a single function
vera parse file.vera # Print the parse tree
vera ast file.vera # Print the typed AST
vera ast --json file.vera # Print the AST as JSON
vera fmt file.vera # Format to canonical form (stdout)
vera fmt --write file.vera # Format in place
vera fmt --check file.vera # Check if already canonical
vera version # Print the installed version (also --version, -V)
vera lsp # Serve LSP over stdio: live diagnostics, hover, slot goto,
# hole completion + agent proof-delta methods (LSP_SERVER.md)
vera builtins [--json] # List the built-in function registry (no file needed)
vera effects [--json] # List the effect and ability registry (no file needed)
vera errors [--json] # List the diagnostic-code registry (no file needed)
pytest tests/ -v # Run the test suite
```
Errors are natural language instructions explaining what went wrong and how to fix it. Feed them back into your context to correct the code.
`vera test` generates Z3 inputs for `Int`, `Nat`, `Bool`, `Byte`, `String`, and `Float64` parameters. The decision is made on each parameter's **resolved** type, not its spelling: a type alias or refinement that resolves to one of those six is generated for like any other, so a parameter spelled `@Count` under `type Count = Nat;` is not skipped for its parameter type, and an alias-spelled `requires` still constrains the inputs. (Trials are what a *Tier 3* contract gets; a signature the verifier proves reports `VERIFIED (Tier 1)` instead, unless `vera test --distrust` runs it too, and one with only trivial contracts is skipped as `trivial contracts only`.) A parameter resolving to an ADT or a function type is skipped with a message naming that resolved type — `type MaybeCount = Option<Nat>` skips with `cannot generate Option<Nat> inputs`. A generic function is skipped as `generic function` before its parameter types are considered at all, so a `forall<T>` signature never reports a per-parameter reason even when every parameter is generable. A generable signature is also skipped when a `requires` conjunct — or a refined parameter's predicate — is outside the SMT layer's decidable fragment, since Z3 could not constrain the generated inputs by it; the skip names the conjunct (`cannot generate inputs satisfying `` `string_length(@String.0) > 0` ``), because running trials the precondition never shaped would report the function's own entry-guard trap as a broken contract. `string_length` over a non-literal is the usual trigger — Vera counts UTF-8 bytes and Z3's string theory has no byte-length operator — so compare a `string_length` against a literal where you want the function trialled. Float64 uses Z3's mathematical reals (NaN, ±∞, and subnormals are not generated). Strings are capped at 50 characters.
### Browser compilation
`vera compile --target browser` produces a ready-to-serve browser bundle:
```bash
vera compile --target browser file.vera # Output to file_browser/
vera compile --target browser file.vera -o dist/ # Output to dist/
```
This generates three files: `module.wasm` (the compiled binary), `runtime.mjs` (self-contained JavaScript runtime with all host bindings), and `index.html` (loads and runs the program). Serve the output directory with any HTTP server (`python -m http.server`) and open `index.html` — ES module imports require HTTP, not `file://`.
The JavaScript runtime provides browser-appropriate implementations: `IO.print` writes to the page, `IO.read_line` uses `prompt()`, `IO.stderr` captures into a separate buffer, `IO.time` uses `Date.now()`, `IO.sleep` busy-waits (main-thread blocking — best kept short in the browser), file IO returns `Result.Err`, and `IO.read_char` returns `Result.Err`, since the browser runtime has no JSPI suspend/resume support. All other operations (State, contracts, Markdown) work identically to the Python runtime.
#### IO model: terminal vs browser
Vera's "write once, run anywhere" claim has a real seam at the IO boundary, and writing for one target without thinking about the other will produce a program that compiles cleanly to both but only *runs* meaningfully on one:
- **Terminal target** assumes a synchronous IO loop: `IO.sleep(120)` blocks the program for 120 ms (fine), ANSI escape codes (`"\u{1B}[2J\u{1B}[H"` to clear screen + home cursor) drive cursor and colour, and the program drives its own pacing.
- **Browser target** assumes "Vera = pure simulation core, JS = timing and rendering driver". `IO.sleep` still works numerically but busy-waits on the main thread (freezing the tab); ANSI escape codes render as literal control bytes in the DOM rather than mutating a virtual screen; `IO.print` writes to the page (good) but the program has no way to *yield* between writes.
The recommended pattern for browser-targeted Vera programs is to **expose pure update functions** (`@State<T>, @Input -> @State<T>`) that JavaScript drives via `requestAnimationFrame`, with Vera computing the next state and JS handling timing + DOM updates. Two runtime gaps make the recommended pattern less ergonomic than it should be — both are tracked on [#603](https://github.com/aallan/vera/issues/603):
- implement `IO.sleep` against the WebAssembly JavaScript Promise Integration (JSPI) proposal so the WASM call suspends on `setTimeout` instead of busy-waiting.
- interpret a minimal ANSI escape subset in the browser runtime so terminal-style programs (clear-screen, cursor-home, colour) render unchanged.
Terminal Vera programs (animation via `IO.sleep` + cursor control via ANSI) need either a terminal target or a deliberate browser-shaped variant. The design point ("pure core, effects at the boundary") is unchanged; the boundary just differs between targets.
### WASI Preview 2 compilation
`vera compile --target wasi-p2` emits a binary WebAssembly *component* that runs under any stock wasip2 host with no Vera bindings — `wasmtime run file.wasm` just works. The target covers the **IO and Random host families only**; a program using any other host family (Http, Decimal, Json, Html, Md, Regex, Math, Inference, State, Async, DB) is rejected with a diagnostic naming the family. `Map` and `Set` are not host families: the module carries their operations, so both worlds run every instance code generation builds; a function that builds a `Map` or `Set` with an `Array` key, value or element is dropped by code generation on every target (`E602`, [#1680](https://github.com/aallan/vera/issues/1680)). `vera run --target wasi-p2 file.vera` executes the component under the built-in wasip2 host with the usual output/trap reporting. Divergences inherent to WASI 0.2 (exit codes collapse to 0/1; no structured trap frames) are documented in [spec chapter 13](https://github.com/aallan/vera/blob/main/spec/13-wasi.md). `--world server` packages a `handle(Request -> Response)` program (the `<HttpServer>` effect) as a `wasi:http/incoming-handler` component that stock `wasmtime serve` runs — headers work via in-guest String maps; of the IO operations that world implements `IO.print`, `IO.stderr`, `IO.time` and `IO.sleep`, and rejects stdin (`IO.read_line`, `IO.read_char`), the filesystem (`IO.read_file`, `IO.write_file`, `IO.read_bytes`, `IO.write_bytes`), `IO.args`, `IO.get_env` and `IO.exit` (spec §13.7).
To run the WASM directly in Node.js:
```bash
node --experimental-wasm-exnref vera/browser/harness.mjs module.wasm
```
### JSON diagnostics
Use `--json` on `check` or `verify` for machine-readable output:
```json
{"ok": true, "file": "...", "diagnostics": [], "warnings": []}
```
On error, each diagnostic includes `severity`, `description`, `location` (`file`, `line`, `column`), `source_line`, `rationale`, `fix`, `spec_ref`, and `error_code`. The `verify --json` output also includes a `verification` summary (`tier1_verified`, `tier3_runtime` and `total` counts, `assumptions` — the number of unverified `assume` statements, each a W003 — and the `timeout_ms` budget the run used) and an `obligations` array, one entry per obligation with `kind`, `status`, `description`, `location` and, when present, `error_code`. The counts are derived from `status`: `verified` counts as Tier 1, `tier3` and `timeout` as Tier 3, and `violated` and `tier3_unguarded` in neither, since each surfaces as a diagnostic instead.
### Error codes
Every diagnostic has a stable code grouped by compiler phase — the `W` series is warnings, the `E` series errors:
- **W001** — Typed hole (`?`) — expected type and available bindings reported (warning, not error)
- **W002** — `async()` argument evaluates eagerly: its effects fall outside the commutative set (`Http`), so the future is computed sequentially at the `async()` site rather than concurrently (warning, not error)
- **W003** — Unverified assumption: an `assume` statement is taken on trust, not proved (warning, not error)
- **W004** — `vera verify --reconcile` found a runtime check in the compiled module that no verification record accounts for: the check still runs, and the summary omits it (warning, not error)
- **E001–E009** — Parse errors (missing contracts, unexpected tokens, malformed slot references, bad string escapes)
- **E011–E013** — Import errors (circular import, unresolvable import, a module that fails to parse)
- **E020, E021, E023** — Malformed comments: unterminated `{-` (E020) or `/*` (E021), or a `/*` nested inside another (E023 — only `{- -}` nests). Each names the delimiter at fault and how to close it.
- **E030–E032** — Contract syntax: an `old()`/`new()` argument that is not an effect reference (E030, E031), or a contract clause written after `effects` (E032)
- **E040** — A pipe whose right operand is not a call: `a |> b` needs `b` to be a call with an argument list, such as `a |> f()`
- **E010** — Transform errors (internal)
- **E1xx** — Type check: core + expressions (type mismatches, slot resolution, operators, declarations, termination)
- **E2xx** — Type check: calls (unresolved functions, argument mismatches, module calls, ability operations)
- **E3xx** — Type check: control flow (if/match, patterns, effect handlers)
- **E5xx** — Verification (contract violations, undecidable fallbacks, primitive-operation safety incl. arithmetic overflow, premise satisfiability, and E541: a runtime-check claim `vera verify --reconcile` found no check for in the compiled module)
- **E6xx** — Codegen (unsupported features, name collisions, typed holes block compilation); **E699** is an internal compiler error
- **E7xx** — Testing (contract violations, input generation, execution errors, a proof a test run refutes)
In diagnostic messages, a `?` inside a printed type (`Array<?>`, `Map<String, ?>`) marks a component the checker could not infer. That is a rendering marker for an unknown type, not the typed-hole expression `?` (W001) you write in source.
Common codes you'll encounter:
- **W001** — Typed hole: fill `?` with an expression of the stated type
- **E130** — Unresolved slot reference (`@T.n` has no matching binding)
- **E121** — Function body type doesn't match return type
- **E200** — Unresolved function call
- **E300** — If condition is not Bool
- **E001** — Missing contract block (requires/ensures/effects)
- **E614** — Program contains typed holes; compile rejected until holes are filled
## Function Structure
Every function has this exact structure. No part is optional except `decreases` and `where`. Visibility (`public` or `private`) is mandatory on every top-level `fn` and `data` declaration.
```vera
private fn function_name(@ParamType1, @ParamType2 -> @ReturnType)
requires(precondition_expression)
ensures(postcondition_expression)
decreases(measure_expression)
effects(effect_row)
{
body_expression
}
```
The order is fixed: every contract clause first (`requires`, `ensures` and
`decreases` — in any order among themselves, and each may appear more than
once), then exactly one `effects` clause, then the body. A contract clause
written after `effects` is a parse error (`E032`) naming the move.
(`invariant` is a `data` declaration's clause, not a function's.)
Complete example:
```vera
public fn safe_divide(@Int, @Int -> @Int)
requires(@Int.1 != 0)
ensures(@Int.result == @Int.0 / @Int.1)
effects(pure)
{
@Int.0 / @Int.1
}
```
### Nullary and Unit-taking functions
Vera accepts two equivalent shapes for functions that take no meaningful argument:
```vera
public fn a(-> @Int) requires(true) ensures(true) effects(pure) { 42 }
public fn b(@Unit -> @Int) requires(true) ensures(true) effects(pure) { 42 }
```
At every call site the arity must match the declaration: `a()` calls the nullary form, `b(())` passes a `Unit` value to the Unit-taking form. They cannot be mixed — `a(())` and `b()` are both type errors. Use the nullary form for constants and computations that have no conceptual input; use the Unit-taking form when you want to match the shape of a combinator that expects a `fn(T -> U)` (the callee side of `apply_fn`, see below). Write `main` as `main(@Unit -> @Unit)` with `effects(<IO>)`, the shape spec §5.11 requires; the toolchain does not enforce it, and runs a `main` of any signature.
### Stored function values and `apply_fn`
Functions passed as arguments or stored in `let` bindings use the type form `fn(T -> U) effects(...)` — plain types, no `@`, and the `effects` clause is required. To invoke such a stored value, use `apply_fn`:
```vera
type IntToInt = fn(Int -> Int) effects(pure);
private fn use_fn(@IntToInt, @Int -> @Int)
requires(true) ensures(true) effects(pure)
{
apply_fn(@IntToInt.0, @Int.0)
}
```
`apply_fn(f, x)` is the only way to call a function that's stored as a value — direct application syntax (`f(x)`) is reserved for declared names. The prelude uses this pattern for `option_map`, `option_and_then`, `result_map` etc., where the mapping function is a parameter. See `examples/closures.vera` and `tests/conformance/ch05_closures.vera` for worked examples.
## Function Visibility
Every top-level `fn` and `data` declaration **must** have an explicit visibility modifier. There is no default visibility -- omitting it is an error.
- `public` -- the declaration is visible to other modules that import this one. Only `public` functions are exported as WASM entry points (callable via `vera run`). Use for library APIs, exported functions, and program entry points.
- `private` -- the declaration is only visible within the current file/module. Private functions compile but are not WASM exports. Use for internal helpers.
```vera
public fn exported_api(@Int -> @Int)
requires(true)
ensures(true)
effects(pure)
{
@Int.0
}
private fn internal_helper(@Int -> @Int)
requires(true)
ensures(true)
effects(pure)
{
@Int.0 + 1
}
public data Color {
Red,
Green,
Blue
}
private data InternalState {
Ready,
Done(Int)
}
```
For generic functions, visibility comes before `forall`:
```vera
private forall<T> fn identity(@T -> @T)
requires(true)
ensures(true)
effects(pure)
{
@T.0
}
```
Visibility does **not** apply to: type aliases (`type Foo = ...`), effect declarations (`effect E { ... }`), module declarations, or import statements. Functions inside `where` blocks also do not take visibility.
Multiple `requires` and `ensures` clauses are allowed. They are conjunctive (AND'd together):
```vera
private fn clamp_to_range(@Int, @Int, @Int -> @Int)
requires(@Int.1 <= @Int.0)
ensures(@Int.result >= @Int.1)
ensures(@Int.result <= @Int.0)
effects(pure)
{
if @Int.2 < @Int.1 then {
@Int.1
} else {
if @Int.2 > @Int.0 then {
@Int.0
} else {
@Int.2
}
}
}
```
## Slot References (`@T.n`)
**De Bruijn slot ordering is the most common source of bugs in Vera programs.** Before writing contracts, `ensures` clauses, or body expressions that involve multiple parameters of the same type, run `vera check --explain-slots` to confirm which index maps to which parameter. Do not rely on intuition.
Vera has no variable names. Every binding is referenced by type and index. See [`DE_BRUIJN.md`](https://github.com/aallan/vera/blob/main/DE_BRUIJN.md) for the academic background, deeper examples, and the commutative-operations trap.
```
@Type.index
```
- `@` is the slot reference prefix (mandatory)
- `Type` is the exact type of the binding, starting with uppercase
- `.index` is the zero-based De Bruijn index (0 = most recent binding of that type)
### Parameter ordering
Parameters bind left-to-right. The **rightmost** parameter of a given type is `@T.0`:
```vera
private fn add(@Int, @Int -> @Int)
requires(true)
ensures(@Int.result == @Int.0 + @Int.1)
effects(pure)
{
@Int.0 + @Int.1
}
-- @Int.0 = second parameter (rightmost Int)
-- @Int.1 = first parameter (leftmost Int)
```
### Mixed types
Each type has its own index counter:
```vera
private fn repeat(@String, @Int -> @String)
requires(@Int.0 >= 0)
ensures(true)
effects(pure)
{
string_repeat(@String.0, @Int.0)
}
-- @String.0 = first parameter (only String)
-- @Int.0 = second parameter (only Int)
```
### Let bindings push new slots
```vera
private fn example(@Int -> @Int)
requires(true)
ensures(true)
effects(pure)
{
let @Int = @Int.0 * 2; -- @Int.0 here refers to the parameter
let @Int = @Int.0 + 1; -- @Int.0 here refers to the first let (param * 2)
@Int.0 -- refers to the second let (param * 2 + 1)
}
```
### `@T.result`
Only valid inside `ensures` clauses. Refers to the function's return value:
```vera
private fn absolute(@Int -> @Nat)
requires(true)
ensures(@Nat.result >= 0)
effects(pure)
{
if @Int.0 >= 0 then {
@Int.0
} else {
-@Int.0
}
}
```
### Index is mandatory
`@Int` alone is not a valid reference. Always write `@Int.0`, `@Int.1`, etc.
### Debugging slot indices with --explain-slots
**Always run `vera check --explain-slots` before writing contracts or function calls that
involve multiple parameters of the same type.** This is the single most reliable way to avoid
De Bruijn ordering mistakes.
```bash
vera check --explain-slots your_file.vera
```
Output:
```text
Slot environments (index 0 = last occurrence in signature):
fn divide(@Int, @Int -> @Int)
@Int.0 parameter 2 (last @Int)
@Int.1 parameter 1 (first @Int)
```
`where`-block helpers get their own table, indented under their parent:
```text
fn is_even(@Nat -> @Bool)
@Nat.0 parameter 1 (only @Nat)
where fn is_odd(@Nat -> @Bool)
@Nat.0 parameter 1 (only @Nat)
```
**Read this table before writing any contract or recursive call.** The ordering only matters
when a function has multiple parameters of the same type — but that is exactly when bugs occur.
Example: for `fn divide(@Int, @Int -> @Int)`, the contract `requires(@Int.1 != 0)` guards the
*first* parameter (the divisor). Confirm this by checking the table: `@Int.1 = parameter 1
(first @Int)`.
**Workflow:**
1. Write the function signature.
2. Run `vera check --explain-slots` to get the slot table.
3. Use the table to write contracts and body expressions with correct `@T.n` indices.
4. If `vera check` reports E130 (unresolved slot), read the `Available bindings:` table in its
own fix text — it lists the slot bindings in scope *at that reference* with their `@T.n`,
including the `let` and `match`-arm ones the signature table cannot show. The table renders
at most twelve rows and then `; … and K more`, so a scope wider than that shows its first
twelve bindings and names how many it withheld. `@T.result` is not a slot binding, so it
never appears there, not even inside `ensures`.
The `--json` flag also works: `vera check --explain-slots --json` emits a `slot_environments`
array, useful when processing diagnostics programmatically.
## Types
### Primitive types
- `Bool` — `true`, `false`
- `Int` — signed 64-bit integer; arithmetic overflow traps (and `INT_MIN / -1` traps with no verifier obligation)
- `Nat` — natural number, the non-negative half of the 64-bit `Int` (`0` to `2^63 - 1`)
- `Float64` — 64-bit IEEE 754 floating-point
- `Byte` — unsigned 8-bit integer (0–255)
- `String` — text
- `Unit` — singleton type, value is `()`. Zero-size and **declaration-only**: a `@Unit` parameter (function or handler-clause op) is legal but reading it (`@Unit.0`) is a checker error (E182) — write the literal `()` instead — and a `let` of a zero-size type (`let @Unit = put(5);`) is a checker error (E183) — call the expression as a statement (`put(5);`). Applies to anything with no runtime representation, including `Future<Unit>`.
- `Never` — bottom type (used for non-terminating expressions like `throw`)
**`Int` and `Nat` are interchangeable in both directions.** `@Nat <: @Int` is a formal subtyping rule at the *type* level (use a `@Nat` anywhere `@Int` is expected, no `nat_to_int` call), and `@Int <: @Nat` is permitted by the type checker with a verifier-discharged obligation (`@Int.0 >= 0`). This means `array_length` (declared `@Int`) flows freely into `@Nat` positions without explicit conversion — the verifier proves non-negativity from context or falls back to a runtime check. Only narrowing carries a *value*-level obligation: a `@Nat` is the non-negative half of the i64 an `@Int` is, so widening is the identity, and narrowing requires `>= 0` (`E503`/`E504`). Runtime guards and verifier obligations correspond at every closure depth (nested closure returns included). Every `@Int` -> `@Nat` narrowing at a PATTERN BIND or a BOUNDARY is runtime-guarded. One ARGUMENT site is not, and is disclosed instead: `string_slice`, whose `@Nat` index arguments code generation deliberately does not guard because the builtin CLAMPS them to `[0, len]` (#475), so a negative becomes a valid `0` and no invalid `@Nat` propagates — the disclosure is `E504` and the roster is `_NAT_ARG_UNGUARDED_BUILTINS`. A user-declared effect operation's argument is never reached: a row naming the effect, and a call of the operation where no row names it, are refused at check (`E340`). An array element and a `Map` value take the SIGN guard at their store too. The refinement PREDICATE (`E505`/`E506`) is a different obligation over an arbitrary predicate rather than a sign, and it is guarded at every construction-position component — a constructor field, a tuple component, an array element, a `Map` value ([#1426](https://github.com/aallan/vera/issues/1426)) — and at the `State` write boundaries ([#1439](https://github.com/aallan/vera/issues/1439)), by the same lowering the pattern binds use. It stays unguarded only where no guard can be lowered at all: a refinement whose BASE is itself a refinement (the guard would silently drop the inner membership predicate), or one whose base ERASES at run time. At an internal bind that is disclosed with an `E506` warning; at a function BOUNDARY it is refused outright with `E618`, because there the verifier would otherwise be promising a runtime check it cannot deliver. Every other site is guarded: the pattern binds at any depth, the function and closure boundaries, the generic-instantiated constructor field, the conversion builtins, a BUILT-IN effect operation's argument, and — of the two write boundaries — the `Exn` `throw` payload, which takes the refinement-predicate guard beside the sign guard ([#1268](https://github.com/aallan/vera/issues/1268)). A user-declared effect operation's argument is never reached, as above. **Do not** insert `nat_to_int` defensively; `@Nat` already flows to `@Int`. Keep a value that may be negative as `@Int`, or use `int_to_nat` (which returns `Option`) when an explicit narrowing must handle the failure case. See spec §2.2.1 for the formal rule.
### Composite types
```vera
@Array<Int> -- array of ints
@Array<Option<Int>> -- array of ADT (compound element type)
@Array<String> -- array of strings
@Tuple<Int, String> -- tuple
@Option<Int> -- Option type (Some/None)
@Map<String, Int> -- key-value map (keys: Eq + Hash)
@Set<Int> -- unique elements, insertion order (Eq + Hash)
@Decimal -- exact decimal arithmetic
@Json -- JSON data (parse/query/serialize)
@HtmlNode -- HTML document node (parse/query/serialize)
fn(Int -> Int) effects(pure) -- function type
{ @Int | @Int.0 > 0 } -- refinement type
```
### Array literals
Write `[1, 2, 3]` for a populated array and `[]` for an empty one. The element type is inferred from the elements when present, and from the surrounding type annotation when the literal is empty:
```vera
let @Array<Int> = [1, 2, 3]; -- populated: elements determine type
let @Array<Bool> = [true, false]; -- populated, any element type
let @Array<Int> = []; -- empty: annotation determines type
let @Array<Array<Int>> = [[1, 2], [3, 4]]; -- nested arrays
let @Array<Json> = [JNumber(1.0), JNull]; -- ADT elements
```
Empty arrays **must** appear in a position with a known type — a `let` binding with a type annotation, a function argument whose parameter type is known, or the branch of a match arm whose type is fixed by another arm. An empty literal with no surrounding type context is a type error. When the element type is polymorphic in the context (e.g. returning `Array<T>` from a `forall<T>` function body), annotate the `let` or thread through a concrete instantiation.
`[` and `]` are context-disambiguated: in expression position (`let @Array<Int> = []`) they delimit an array literal; in postfix position (`@Array<Int>.0[@Int.0]`) they are the index operator — see the operator precedence table at the bottom of this file. The parser resolves the two by lookahead; there is no ambiguity you need to work around.
### Tuples
Tuples are constructed with the `Tuple(...)` constructor and destructured with the same shape inside `match`:
```vera
let @Tuple<Int, String> = Tuple(42, "hello");
match @Tuple<Int, String>.0 {
Tuple(@Int, @String) -> @Int.0 -- => 42
}
```
`Tuple` is just an upper-case constructor — there is no special tuple-literal syntax (no `(1, 2, 3)` form). The empty tuple `Tuple<>` is equivalent to `Unit`. The name is reserved in both the data and the constructor namespace: `data Tuple { ... }` and `data Box { Tuple(Bool) }` are each rejected at `vera check` with **E158** (see below), because the compiler recognises `Tuple` by name when it renders and lays out a value. A `type Tuple = ...` alias is unaffected.
### Type aliases
```vera
type PosInt = { @Int | @Int.0 > 0 };
type Name = String;
```
An alias is **opaque as the head** of a slot name and **transparent inside type arguments**
(spec §3.8.1). A parameter written `@PosInt` is referenced `@PosInt.0`, never `@Int.0` — the
two are separate namespaces. A parameter written `@Option<Name>` binds `Option<String>`, so it
is referenced `@Option<String>.0`. When in doubt, run `vera check --explain-slots`: it prints
the resolved name of every parameter.
## Data Types (ADTs)
```vera
private data Color {
Red,
Green,
Blue
}
private data List<T> {
Nil,
Cons(T, List<T>)
}
private data Option<T> {
None,
Some(T)
}
```
> `Option<T>`, `Result<T, E>`, `Ordering`, and `UrlParts` are provided by the standard prelude and available in every program without explicit `data` declarations. You only need to define them locally if you want to shadow the prelude definition.
With an invariant *(not implemented; use a refinement type instead, shown below)*:
```vera
private data Positive invariant(@Int.0 > 0) {
MkPositive(Int)
}
```
The `invariant(...)` clause on `data` declarations is specified but does not work in the reference compiler — every documented form fails with `[E130] no <DataName> bindings in scope`. Express the same constraint with a refinement type:
```vera
type Positive = { @Int | @Int.0 > 0 };
```
## Pattern Matching
```vera
private fn to_int(@Color -> @Int)
requires(true)
ensures(true)
effects(pure)
{
match @Color.0 {
Red -> 0,
Green -> 1,
Blue -> 2
}
}
```
Patterns can bind values:
```vera
private fn unwrap_or(@Option<Int>, @Int -> @Int)
requires(true)
ensures(true)
effects(pure)
{
match @Option<Int>.0 {
None -> @Int.0,
Some(@Int) -> @Int.0
}
}
```
Available patterns: constructors (`Some(@Int)`), nullary constructors (`None`, `Red`), literals (`0`, `"x"`, `true`), wildcard (`_`).
Match must be exhaustive.
## Conditional Expressions
```vera
if @Bool.0 then {
expr1
} else {
expr2
}
```
Both branches are mandatory. Braces are mandatory. Each branch is always multi-line (closing brace on its own line).
## Block Expressions
Blocks contain statements followed by a final expression:
```vera
{
let @Int = @Int.0 + 1;
let @String = to_string(@Int.0);
IO.print(@String.0);
@Int.0
}
```
Statements end with `;`. The final expression (no `;`) is the block's value.
## Typed Holes
**When you do not know the right expression to write, use `?` rather than guessing.** A typed hole tells you immediately what type is needed and what bindings are available — it is always faster than writing the wrong thing and debugging the type error.
```vera
public fn double(@Int -> @Int)
requires(true) ensures(true) effects(pure)
{
?
}
```
`vera check` reports a `W001` warning (not an error):
```text
Warning [W001]: Typed hole: expected Int.
Fix: Replace ? with an expression of type Int. Available bindings: @Int.0: Int.
```
The program type-checks successfully (`ok: true`) — holes are warnings, not errors. This means you can check the *rest* of a function for type errors while one expression is still incomplete.
`vera check --json` includes hole warnings in the `warnings` array with the full expected type and binding context, making them machine-readable for agent workflows.
**Programs with holes cannot be compiled.** `vera compile` and `vera run` reject any program containing `?` with an `E614` error.
### Workflow
Use holes to build programs incrementally:
```vera
public fn safe_div(@Int, @Int -> @Option<Int>)
requires(true) ensures(true) effects(pure)
{
if ? then { -- W001: expected Bool. Bindings: @Int.0: Int; @Int.1: Int
Some(?) -- W001: expected Int. Bindings: @Int.0: Int; @Int.1: Int
} else {
None
}
}
```
Check this, read the `W001` fix hints, then fill in the holes:
```vera
if @Int.0 != 0 then {
Some(@Int.1 / @Int.0)
} else {
None
}
```
### Multiple holes
Multiple holes in one program each produce their own `W001` warning with independent context. You can fill them one at a time and re-check between iterations.
### Conformance
See `tests/conformance/ch03_typed_holes.vera` for a minimal working example.
## Iteration
Vera has no `for` or `while` loops. Iteration is always expressed as tail-recursive functions. The standard pattern for counted iteration:
```vera
private fn loop(@Nat, @Nat -> @Unit)
requires(@Nat.0 <= @Nat.1)
ensures(true)
decreases(@Nat.1 - @Nat.0)
effects(<IO>)
{
IO.print(string_concat(fizzbuzz(@Nat.0), "\n"));
if @Nat.0 < @Nat.1 then {
loop(@Nat.1, @Nat.0 + 1)
} else {
()
}
}
```
Here `@Nat.0` is the counter (De Bruijn index 0 = most recent, i.e. the second parameter) and `@Nat.1` is the limit (the first parameter). The contract `requires(@Nat.0 <= @Nat.1)` ensures the counter never exceeds the limit — and since the recursive call passes `@Nat.0 + 1` where `@Nat.0 < @Nat.1`, the precondition is maintained at every step. The function prints, then either recurses with an incremented counter or returns `()`.
The measure `decreases(@Nat.1 - @Nat.0)` is the number of steps left. It shrinks by one on every recursive call and never goes below zero, which is what proves the loop ends; the `requires` is what makes the subtraction safe at entry. Every recursive function needs a measure, whatever its effect row, `<IO>` included (see [decreases](#decreases-termination)). A loop that is not meant to end declares `Diverge` instead.
Call with the limit first and counter second: `loop(100, 1)`.
## Closures and captured bindings
Anonymous functions are written `fn(@ParamType1, @ParamType2 -> @ReturnType) effects(effect_row) { body_expression }`. They are first-class values and can be passed to higher-order built-ins (`array_map`, `array_filter`, `array_fold`, `array_any`, `array_find`, `array_sort_by`, …) or stored in `let` bindings.
```vera
let @Array<Int> = [1, 2, 3, 4, 5];
let @Array<Int> = array_map(
@Array<Int>.0,
fn(@Int -> @Int) effects(pure) { @Int.0 * 2 }
);
-- Result: [2, 4, 6, 8, 10]
```
Inside the closure body, `@Int.0` is the closure's own parameter (index 0 = most recent binding). This matches how slot indices work in top-level `fn` declarations.
### Capturing outer bindings
**Closures can capture any outer binding** — primitives (`Int`, `Nat`, `Bool`, `Byte`, `Float64`), pair types (`String`, `Array<T>`), single-pointer ADTs (`Option<T>`, `Result<T, E>`, user-defined `data` types), and the opaque-handle ADTs (`Map<K, V>`, `Set<T>`, `Decimal`).
Outer bindings are available at higher De Bruijn indices — the closure's own parameters are pushed on top of the slot stack, so outer `@T` bindings shift up by the number of inner `@T` parameters.
```vera
-- WORKS: capturing a primitive @Int.
public fn sum_plus_offset(@Unit -> @Int)
requires(true) ensures(true) effects(pure)
{
let @Int = 100; -- outer binding: @Int.0 = 100
let @Array<Int> = [1, 2, 3];
array_fold(
@Array<Int>.0,
0,
-- array_fold's closure shape is fn(@Acc, @Elem -> @Acc) — accumulator
-- first. By the rightmost = .0 rule, that puts the element at .0
-- and the accumulator at .1 inside the body.
fn(@Int, @Int -> @Int) effects(pure) {
-- Inside this closure body, two @Int params are in scope:
-- @Int.0 = element (most recent, the iterator's current value)
-- @Int.1 = accumulator
-- @Int.2 = outer `let @Int = 100` (captured — primitive, OK)
@Int.1 + @Int.0 + @Int.2
}
)
}
-- 0+1+100 + 2+100 + 3+100 = 306
```
The rule when capture IS safe: count the closure's own `@T` parameters, and the outermost captured `@T` binding sits at that index. A closure with no `@Int` parameters of its own would see the outer `let @Int` as `@Int.0`; a closure with two `@Int` parameters sees it as `@Int.2`. Types are independent — a closure's `@Int` parameter does not shift outer `@String` bindings.
Use `vera check --explain-slots file.vera` if you need the resolved index table printed for a specific function (including closures).
### Capturing a pair-typed value
Capturing a `String` or `Array<T>` works the same way as capturing any other outer binding — the closure-struct layout serialises both halves of the (ptr, len) pair, so `array_length` / `string_length` / element-access all see the captured value correctly inside the closure body.
```vera
-- Capture an outer Array<Int> and read its length inside the closure.
let @Array<Int> = [10, 20, 30]; -- captured (outer) @Array<Int>.0 = this
let @Array<Int> = [1, 2, 3]; -- iterated (inner) @Array<Int>.0 = this
-- outer shifts to .1
array_fold(
@Array<Int>.0,
0,
fn(@Int, @Int -> @Int) effects(pure) {
-- Inside the closure: @Int.0 = element, @Int.1 = acc.
-- @Array<Int>.1 refers to the OUTER (captured) array.
@Int.1 + @Int.0 + nat_to_int(array_length(@Array<Int>.1))
}
)
-- 0+1+3 + 2+3 + 3+3 = 15
```
The same applies to `String` captures. ADT captures (`Option<T>`, `Result<T, E>`, user `data` types, `Json`, `HtmlNode`, `MdBlock`, opaque handles `Map<K, V>` / `Set<T>` / `Decimal`) work too — they're single-i32 pointers that the closure-struct layout handles directly.
### When to use recursion instead
Closures cover pure, self-contained transformations and simple captured constants. Prefer a top-level recursive function when any of these hold:
- The body needs an effect row other than `pure` that doesn't match the combinator's expected effect signature.
- The body needs to early-return or short-circuit in a way the combinator doesn't provide (`array_find` / `array_any` / `array_all` short-circuit; `array_map` / `array_fold` do not).
- The iteration shape isn't one-pass left-to-right (e.g. you need to look ahead, or process in reverse while mutating a different data structure).
- Termination requires a `decreases` clause that proves non-trivial progress — closures cannot carry `decreases`.
For counted iteration with IO, use the recursive `loop` pattern from the Iteration section above; for array transformations, use the array combinators with closures.
### Nested closures
Closures inside closure bodies work end-to-end — the natural 2D `array_map(rows, fn(row) { array_map(cols, fn(col) { ... }) })` shape compiles, validates, and runs at any return type. Captures from the outer scope flow through nested closures correctly for every type that can be captured at the top level (primitives, pair types, ADTs, opaque handles). Three or more levels of nesting work the same way; the lifting pass uses a worklist that handles arbitrary depth.
```vera
public fn build_grid(@Unit -> @Array<Array<Int>>)
requires(true) ensures(true) effects(pure)
{
-- 2D array of products via nested array_map.
array_map(
array_range(0, 3),
fn(@Int -> @Array<Int>) effects(pure) {
array_map(
array_range(0, 3),
fn(@Int -> @Int) effects(pure) { @Int.0 + @Int.1 }
)
}
)
}
```
## Built-in Functions
### Naming convention
All built-in functions follow predictable naming patterns. When guessing a function name you haven't seen, apply these rules:
| Pattern | When | Examples |
|---------|------|----------|
| `domain_verb` | Most functions | `string_length`, `array_append`, `regex_match`, `md_parse` |
| `source_to_target` | Type conversions | `int_to_float`, `float_to_int`, `nat_to_int` |
| `domain_is_predicate` | Boolean predicates | `float_is_nan`, `float_is_infinite` |
| Prefix-less | Math universals and float constants only | `abs`, `min`, `max`, `floor`, `ceil`, `round`, `sqrt`, `pow`, `nan`, `infinity` |
**String operations always use `string_` prefix** — `string_contains`, `string_starts_with`, `string_split`, `string_join`, `string_strip`, `string_upper`, `string_lower`, `string_replace`, `string_index_of`, `string_char_code`, `string_from_char_code`, `string_chars`, `string_lines`, `string_words`, `string_reverse`, `string_trim_start`, `string_trim_end`, `string_pad_start`, `string_pad_end`. **Character classifiers use `is_` prefix** — `is_digit`, `is_alpha`, `is_alphanumeric`, `is_whitespace`, `is_upper`, `is_lower`. **First-character conversion uses `char_` prefix** — `char_to_upper`, `char_to_lower`. **JSON typed accessors use `json_as_` and `json_get_` prefixes** — `json_as_string`/`number`/`bool`/`int`/`array`/`object` for Layer-1 coercions; `json_get_string`/`number`/`bool`/`int`/`array` for Layer-2 compound field accessors. **Float64 predicates use `float_` prefix** — `float_is_nan`, `float_is_infinite`. **Type conversions use `source_to_target`** — `int_to_float` (not `to_float`), `float_to_int`, `int_to_nat`. Math functions (`abs`, `min`, `max`, etc.) and float constants (`nan`, `infinity`) are the **only** exceptions — they need no prefix because they are universally understood mathematical names.
**If `vera check` reports an unresolved function name, apply these patterns to derive the correct name before giving up.** The convention is strict and consistent — the right name is always derivable. Do not invent names that don't follow the pattern; they will not exist.
### Option and Result Combinators
The standard prelude provides `Option<T>` and `Result<T, E>` along with combinator functions that are always available:
```vera
-- Option: unwrap with default
option_unwrap_or(Some(42), 0) -- returns 42
option_unwrap_or(None, 0) -- returns 0
-- Option: transform the value inside Some
option_map(Some(10), fn(@Int -> @Int) effects(pure) { @Int.0 + 1 })
-- returns Some(11)
-- Option: chain fallible operations (flatmap)
option_and_then(Some(5), fn(@Int -> @Option<Int>) effects(pure) {
if @Int.0 > 0 then { Some(@Int.0 * 2) } else { None }
})
-- returns Some(10)
-- Result: unwrap with default
result_unwrap_or(Ok(42), 0) -- returns 42
result_unwrap_or(Err("oops"), 0) -- returns 0
-- Result: transform the Ok value
result_map(Ok(10), fn(@Int -> @Int) effects(pure) { @Int.0 + 1 })
-- returns Ok(11)
```
These are generic functions that follow the `domain_verb` naming convention. They are automatically injected and undergo normal monomorphization. If you define a function with the same name, your definition takes precedence, inside the prelude's own bodies as well as your code: the prelude's `json_get_string` calls `json_get` by bare name, so a user `json_get` changes its answer or, with a different signature, stops the module loading. Pick a distinct name unless you mean to replace the prelude's everywhere.
### Array operations
```vera
array_length(@Array<Int>.0) -- returns Int (the array length, flows to either Nat or Int positions)
array_append(@Array<Int>.0, @Int.0) -- returns Array<Int> (new array with element appended)
array_range(@Int.0, @Int.1) -- returns Array<Int> (integers [start, end))
array_concat(@Array<Int>.0, @Array<Int>.1) -- returns Array<Int> (merge two arrays)
array_slice(@Array<Int>.0, @Int.0, @Int.1) -- returns Array<Int> (elements [start, end))
array_map(@Array<Int>.0, fn(@Int -> @Int) effects(pure) { ... }) -- returns Array<Int>
array_filter(@Array<Int>.0, fn(@Int -> @Bool) effects(pure) { ... }) -- returns Array<Int>
array_fold(@Array<Int>.0, 0, fn(@Int, @Int -> @Int) effects(pure) { @Int.1 + @Int.0 }) -- returns Int
array_mapi(@Array<Int>.0, fn(@Int, @Nat -> @Int) effects(pure) { ... }) -- returns Array<Int> (map with index)
array_reverse(@Array<Int>.0) -- returns Array<Int> (element order reversed)
array_find(@Array<Int>.0, fn(@Int -> @Bool) effects(pure) { ... }) -- returns Option<Int> (first match)
array_any(@Array<Int>.0, fn(@Int -> @Bool) effects(pure) { ... }) -- returns Bool (at least one match)
array_all(@Array<Int>.0, fn(@Int -> @Bool) effects(pure) { ... }) -- returns Bool (every element matches)
array_flatten(@Array<Array<Int>>.0) -- returns Array<Int> (one level)
array_sort_by(@Array<Int>.0, fn(@Int, @Int -> @Ordering) effects(pure) { ... }) -- returns Array<Int>
```
`array_map` / `array_mapi` are generic: the element type can change (e.g. `array_map(@Array<Int>.0, fn(@Int -> @String) ...)`).
`array_fold` is generic: the accumulator type can differ from the element type.
`array_mapi` passes the zero-based index as a `@Nat` second argument — use this rather than hand-rolling a recursive accumulator with an index counter.
`array_find` short-circuits on the first match; `array_any` and `array_all` do the same and observe the standard vacuous-truth convention on empty input (`any([], _) == false`, `all([], _) == true`).
`array_sort_by`'s comparator returns `@Ordering` (`Less` / `Equal` / `Greater`); insertion sort, stable.
`array_sort<T> where Ord<T>`, `array_contains<T> where Eq<T>`, and `array_index_of<T> where Eq<T>` (operations that would dispatch on the element type's built-in ability) are not implemented — use `array_sort_by` with an explicit comparator, or `array_any` / `array_find` with an equality predicate.
### Map operations
`Map<K, V>` is a key-value collection. Keys must satisfy `Eq` and `Hash` abilities (primitive types: `Int`, `Nat`, `Bool`, `Float64`, `String`, `Byte`). Values may be any type with a runtime representation — a zero-size key or value type (`Unit`, or a `Future` wrapping one) is rejected at check time with E135. All operations are pure — insert and remove return new maps, sharing what they do not change, so an insert costs the depth of the map's trie, not its size. `map_keys` and `map_values` return the keys and values in insertion order: a key inserted again keeps its first position, and a removed key loses it. `-0.0` and `0.0` are one key, and so are any two NaNs.
```vera
map_insert(map_new(), "hello", 42) -- returns Map<String, Nat>
map_insert(@Map<String, Nat>.0, "world", 7) -- returns Map<String, Nat> (new map with entry added)
map_get(@Map<String, Nat>.0, "hello") -- returns Option<Nat> (Some(42) or None)
map_contains(@Map<String, Nat>.0, "hello") -- returns Bool
map_remove(@Map<String, Nat>.0, "hello") -- returns Map<String, Nat> (new map without key)
map_size(@Map<String, Nat>.0) -- returns Int (number of entries)
map_keys(@Map<String, Nat>.0) -- returns Array<String>
map_values(@Map<String, Nat>.0) -- returns Array<Nat>
```
> `map_new()` is a zero-argument generic function. Nest it inside `map_insert(map_new(), k, v)` so that type inference can resolve the key and value types from the arguments. Using `option_unwrap_or(map_get(...), default)` is the idiomatic way to extract values with a fallback.
### Set operations
`Set<T>` is a collection of unique elements, which `set_to_array` returns in insertion order. Elements must satisfy `Eq` and `Hash` abilities (primitive types: `Int`, `Nat`, `Bool`, `Float64`, `String`, `Byte`); a zero-size element type (`Unit`, or a `Future` wrapping one) is rejected at check time with E135. All operations are pure — add and remove return new sets.
```vera
set_add(set_add(set_new(), "hello"), "world") -- returns Set<String>
set_contains(@Set<String>.0, "hello") -- returns Bool (true)
set_remove(@Set<String>.0, "hello") -- returns Set<String> (new set without element)
set_size(@Set<String>.0) -- returns Int
set_to_array(@Set<String>.0) -- returns Array<String>
```
> `set_new()` is a zero-argument generic function. Nest it inside `set_add(set_new(), elem)` so that type inference can resolve the element type. Adding a duplicate element is a no-op (sets enforce uniqueness).
### Decimal operations
`Decimal` provides exact decimal arithmetic for financial and precision-sensitive applications. It is an opaque type (i32 handle) backed by the runtime's decimal implementation. All operations are pure.
```vera
decimal_from_int(42) -- returns Decimal (exact conversion)
decimal_from_float(3.14) -- returns Decimal (via str conversion)
decimal_add(@Decimal.0, @Decimal.1) -- returns Decimal (addition)
decimal_sub(@Decimal.0, @Decimal.1) -- returns Decimal (subtraction)
decimal_mul(@Decimal.0, @Decimal.1) -- returns Decimal (multiplication)
decimal_neg(@Decimal.0) -- returns Decimal (negation)
decimal_abs(@Decimal.0) -- returns Decimal (absolute value)
decimal_round(@Decimal.0, 2) -- returns Decimal (round to N places)
decimal_eq(@Decimal.0, @Decimal.1) -- returns Bool (equality)
decimal_compare(@Decimal.0, @Decimal.1) -- returns Ordering (Less/Equal/Greater)
decimal_to_string(@Decimal.0) -- returns String
decimal_to_float(@Decimal.0) -- returns Float64 (potentially lossy)
```
`decimal_from_string` and `decimal_div` return `Option<Decimal>` — use `option_unwrap_or` or `match` to extract the value. `decimal_compare` returns `Ordering` — use `match` to dispatch on `Less`, `Equal`, `Greater`.
### JSON operations
`Json` is a built-in ADT for structured data interchange. Parse JSON strings, query fields and array elements, and serialize back to strings. All operations are pure.
The `Json` type has six constructors: `JNull`, `JBool(Bool)`, `JNumber(Float64)`, `JString(String)`, `JArray(Array<Json>)`, `JObject(Map<String, Json>)`. It is provided by the standard prelude — no `data` declaration needed.
**What `json_parse` accepts.** Exactly RFC 8259-valid text that decodes to finite numbers and strings of Unicode scalar values (spec §9.7.1). Anything else is `Err`, at the parse, with the same message on the CLI and in the browser — Vera defines this domain rather than inheriting whichever one the host parser implements. Two consequences bear on the `Err` arm:
- A **non-finite number** never parses, however it is written. The constants `NaN`, `Infinity` and `-Infinity` are not JSON at all; a number that merely *overflows*, like `1e999`, is syntactically fine and still refused, because what it decodes to is an infinity. Underflow is different — `1e-999` gives you `0` and parses. If a producer you do not control emits any of these, fix the producer or pre-process the text; there is no flag to admit them.
- A **lone surrogate** escape (`\ud800` with no matching partner) never parses either: its decoded value is not a Unicode scalar, and a Vera `String` is. A *matched* pair is ordinary — `"\ud83d\ude00"` parses fine and gives you the astral character.
Everything else that fails is a plain syntax error, and that message is the host parser's own.
```vera
json_parse("{\"name\":\"Vera\"}") -- returns Result<Json, String>
json_stringify(@Json.0) -- returns String (JSON text)
json_get(@Json.0, "name") -- returns Option<Json> (field lookup)
json_has_field(@Json.0, "name") -- returns Bool
json_keys(@Json.0) -- returns Array<String> (object keys)
json_array_get(@Json.0, 0) -- returns Option<Json> (element at index)
json_array_length(@Json.0) -- returns Int (array length, 0 if not array)
json_type(@Json.0) -- returns String ("null"/"bool"/"number"/"string"/"array"/"object")
```
Pattern match on `Json` constructors to extract values:
```vera
match json_parse("{\"x\":42}") {
Err(@String) -> Err(@String.0),
Ok(@Json) -> match json_get(@Json.0, "x") {
None -> Err("missing x"),
Some(@Json) -> match @Json.0 {
JNumber(@Float64) -> Ok(float_to_int(@Float64.0)),
_ -> Err("x is not a number")
}
}
}
```
#### Typed accessors (Layer 1 and Layer 2)
For the common case of "unwrap `Option<Json>` and match on a specific constructor", use the typed accessors instead of the two-level match above:
```vera
-- Layer 1: Json -> Option<T>. Some when the constructor matches.
json_as_string(@Json.0) -- Option<String>
json_as_number(@Json.0) -- Option<Float64>
json_as_bool(@Json.0) -- Option<Bool>
json_as_int(@Json.0) -- Option<Int> (truncates; None for NaN/inf/|f| >= 2^63)
json_as_array(@Json.0) -- Option<Array<Json>>
json_as_object(@Json.0) -- Option<Map<String, Json>>
-- Layer 2: json_get + json_as_* composed (the common pattern).
json_get_string(@Json.0, "name") -- Option<String>
json_get_number(@Json.0, "score") -- Option<Float64>
json_get_bool(@Json.0, "active") -- Option<Bool>
json_get_int(@Json.0, "age") -- Option<Int>
json_get_array(@Json.0, "tags") -- Option<Array<Json>>
```
The Layer-2 accessors return `None` both when the field is missing AND when the field is present but of the wrong type — exactly what 90% of real API-consuming code wants. The example above collapses to:
```vera
match json_parse("{\"x\":42}") {
Err(@String) -> Err(@String.0),
Ok(@Json) -> match json_get_int(@Json.0, "x") {
Some(@Int) -> Ok(@Int.0),
None -> Err("x missing or not a number")
}
}
```
### String operations
```vera
string_length(@String.0) -- returns Nat
string_concat(@String.0, @String.1) -- returns String
string_slice(@String.0, @Nat.0, @Nat.1) -- returns String (start, end)
string_char_code(@String.0, @Int.0) -- returns Nat (ASCII code at index)
string_from_char_code(@Nat.0) -- returns String (single char from code point)
string_repeat(@String.0, @Nat.0) -- returns String (repeated N times)
parse_nat(@String.0) -- returns Result<Nat, String>
parse_int(@String.0) -- returns Result<Int, String>
parse_float64(@String.0) -- returns Result<Float64, String>
parse_bool(@String.0) -- returns Result<Bool, String>
base64_encode(@String.0) -- returns String (RFC 4648)
base64_decode(@String.0) -- returns Result<String, String>
base64_encode_bytes(@Array<Byte>.0) -- returns String (RFC 4648, over bytes)
base64_decode_bytes(@String.0) -- returns Result<Array<Byte>, String>
string_to_bytes(@String.0) -- returns Array<Byte> (the string's UTF-8 bytes)
bytes_to_string(@Array<Byte>.0) -- returns Result<String, String> (UTF-8 decode)
url_encode(@String.0) -- returns String (RFC 3986 percent-encoding)
url_decode(@String.0) -- returns Result<String, String>
url_parse(@String.0) -- returns Result<UrlParts, String> (RFC 3986 decomposition)
url_join(@UrlParts.0) -- returns String (reassemble URL from UrlParts)
md_parse(@String.0) -- returns Result<MdBlock, String> (parse Markdown)
md_render(@MdBlock.0) -- returns String (render to canonical Markdown)
md_has_heading(@MdBlock.0, @Nat.0) -- returns Bool (check if heading of level exists)
md_has_code_block(@MdBlock.0, @String.0) -- returns Bool (check if code block of language exists)
md_extract_code_blocks(@MdBlock.0, @String.0) -- returns Array<String> (extract code by language)
html_parse(@String.0) -- returns Result<HtmlNode, String> (parse HTML)
html_to_string(@HtmlNode.0) -- returns String (serialize to HTML)
html_query(@HtmlNode.0, @String.0) -- returns Array<HtmlNode> (CSS selector query)
html_text(@HtmlNode.0) -- returns String (extract text content)
html_attr(@HtmlNode.0, @String.0) -- returns Option<String> (get attribute value)
regex_match(@String.0, @String.1) -- returns Result<Bool, String> (test if pattern matches)
regex_find(@String.0, @String.1) -- returns Result<Option<String>, String> (first match)
regex_find_all(@String.0, @String.1) -- returns Result<Array<String>, String> (all matches)
regex_replace(@String.0, @String.1, @String.2) -- returns Result<String, String> (replace first match)
async(@T.0) -- returns Future<T> (requires effects(<Async>))
await(@Future<T>.0) -- returns T (requires effects(<Async>))
to_string(@Int.0) -- returns String (integer to decimal)
int_to_string(@Int.0) -- returns String (alias for to_string)
bool_to_string(@Bool.0) -- returns String ("true" or "false")
nat_to_string(@Nat.0) -- returns String (natural to decimal)
byte_to_string(@Byte.0) -- returns String (single character)
float_to_string(@Float64.0) -- returns String (decimal; nan/inf/-inf for non-finite; traps if finite and |x| >= 2^63)
string_strip(@String.0) -- returns String (trim whitespace)
```
#### String interpolation
```vera
"hello \(@String.0)" -- embeds a String value
"x = \(@Int.0)" -- auto-converts Int to String
"a=\(@Int.1), b=\(@Int.0)" -- multiple interpolations
"\(@String.0)" -- interpolation-only (no literal text)
"len=\(string_length(@String.0))" -- function call inside interpolation
```
Expressions inside `\(...)` are auto-converted to String for types: Int, Nat, Bool, Byte, Float64. Other types produce error E148. Expressions cannot contain string literals (use `let` bindings instead).
#### String search
```vera
string_contains(@String.0, @String.1) -- returns Bool (substring test)
string_starts_with(@String.0, @String.1) -- returns Bool (prefix test)
string_ends_with(@String.0, @String.1) -- returns Bool (suffix test)
string_index_of(@String.0, @String.1) -- returns Option<Nat> (first occurrence)
```
`string_contains` checks whether the needle appears anywhere in the haystack. `string_starts_with` and `string_ends_with` test prefix and suffix matches. `string_index_of` returns `Some(i)` with the byte offset of the first match, or `None` if not found. An empty needle always matches (returns `true` or `Some(0)`).
#### String transformation
```vera
string_upper(@String.0) -- returns String (ASCII uppercase)
string_lower(@String.0) -- returns String (ASCII lowercase)
string_replace(@String.0, @String.1, @String.2) -- returns String (replace all)
string_split(@String.0, @String.1) -- returns Array<String> (split by delimiter)
string_join(@Array<String>.0, @String.0) -- returns String (join with separator)
```
`string_upper` and `string_lower` convert ASCII letters only (a-z ↔ A-Z). `string_replace` substitutes all non-overlapping occurrences; an empty needle returns the original string unchanged. `string_split` returns an array of segments; an empty delimiter returns a single-element array. `string_join` concatenates array elements with the separator between each pair.
#### String utilities and character classification
```vera
-- Splits (bridge to the array combinators)
string_chars(@String.0) -- returns Array<String> (one byte each)
string_lines(@String.0) -- returns Array<String> (\n, \r\n, \r)
string_words(@String.0) -- returns Array<String> (whitespace runs)
-- Transformations
string_reverse(@String.0) -- returns String (byte reverse)
string_trim_start(@String.0) -- returns String (lstrip whitespace)
string_trim_end(@String.0) -- returns String (rstrip whitespace)
string_pad_start(@String.0, @Nat.0, @String.1) -- returns String (left-pad to length, JS padStart)
string_pad_end(@String.0, @Nat.0, @String.1) -- returns String (right-pad to length)
-- Case conversion (first byte only)
char_to_upper(@String.0) -- returns String
char_to_lower(@String.0) -- returns String
-- Character classifiers (first byte; false for empty)
is_digit(@String.0) -- returns Bool ('0'..'9')
is_alpha(@String.0) -- returns Bool ('A'..'Z', 'a'..'z')
is_alphanumeric(@String.0) -- returns Bool
is_whitespace(@String.0) -- returns Bool (tab, LF, VT, FF, CR, space — Python isspace() ASCII)
is_upper(@String.0) -- returns Bool
is_lower(@String.0) -- returns Bool
```
`string_chars` is the canonical bridge from `String` to `Array<String>` — combine with `array_map`, `array_filter`, `array_fold` to thread per-byte logic through the array combinators. `string_lines` follows Python's `splitlines()` (trailing `\n` does not add an empty segment). `string_words` follows Python's `split()` with no args (runs collapse, empty segments discarded).
`string_pad_start` and `string_pad_end` cycle the fill left-to-right and truncate to exactly the padding length, matching JavaScript's `padStart` / `padEnd`. If the input is already at least `n` bytes, the input is returned unchanged. An empty `fill` is a no-op.
`char_to_upper` / `char_to_lower` convert only the **first byte** of the string; remaining bytes pass through unchanged. Useful for title-casing a token. The six classifiers all inspect only the first byte and return `false` for the empty string. All sixteen are ASCII-only — no Unicode awareness.
String functions use the heap allocator (`$alloc`). Memory is managed automatically by a conservative mark-sweep garbage collector — there is no manual allocation or deallocation. All four parse functions return `Result<T, String>`: `parse_nat`, `parse_int`, `parse_float64`, and `parse_bool`. They return `Ok(value)` on valid input and `Err(msg)` on empty or invalid input; leading and trailing spaces are tolerated. `parse_int` accepts an optional `+` or `-` sign. `parse_bool` is strict: only `"true"` and `"false"` (lowercase) are valid. `base64_encode` encodes a string to standard Base64 (RFC 4648); `base64_decode` returns `Result<String, String>`, failing on invalid length or characters. `url_encode` percent-encodes a string for use in URLs (RFC 3986), leaving unreserved characters (`A-Z`, `a-z`, `0-9`, `-`, `_`, `.`, `~`) unchanged; `url_decode` returns `Result<String, String>`, failing on invalid `%XX` sequences. `url_parse` decomposes a URL into its RFC 3986 components, returning `Result<UrlParts, String>` where `UrlParts(scheme, authority, path, query, fragment)` is a built-in ADT with five String fields; it returns `Err("missing scheme")` if no `:` is found. `url_join` reassembles a `UrlParts` value into a URL string. `UrlParts` is in every program, so match on it directly (`UrlParts(@String, @String, @String, @String, @String) -> ...`) with no local declaration.
#### Bytes
An `Array<Byte>` holds bytes, one to an element. `string_to_bytes` gives a string's UTF-8 bytes, and `bytes_to_string` decodes bytes to a string: `Ok` for well-formed UTF-8, otherwise `Err("invalid UTF-8 at byte N")`, where `N` is the offset of the first byte of the first sequence that is not well formed. `base64_encode_bytes` and `base64_decode_bytes` are Base64 (RFC 4648) over bytes, so a payload that is not text, such as an image, decodes to what it is. `IO.read_bytes` and `IO.write_bytes` read and write a file's bytes unchanged.
```vera
private fn decoded(@Array<Byte> -> @String)
requires(true)
ensures(true)
effects(pure)
{
match bytes_to_string(@Array<Byte>.0) {
Ok(@String) -> @String.0,
Err(@String) -> @String.0
}
}
public fn main(@Unit -> @Unit)
requires(true)
ensures(true)
effects(<IO>)
{
let @Array<Byte> = string_to_bytes("héllo");
IO.print(string_concat(int_to_string(array_length(@Array<Byte>.0)), " bytes, "));
IO.print(string_concat(base64_encode_bytes(@Array<Byte>.0), ", "));
match base64_decode_bytes("aMOpbGxv") {
Ok(@Array<Byte>) -> IO.print(decoded(@Array<Byte>.0)),
Err(@String) -> IO.print(@String.0)
}
}
```
### Markdown operations
```vera
md_parse(@String.0) -- returns Result<MdBlock, String>
md_render(@MdBlock.0) -- returns String
md_has_heading(@MdBlock.0, @Nat.0) -- returns Bool
md_has_code_block(@MdBlock.0, @String.0) -- returns Bool
md_extract_code_blocks(@MdBlock.0, @String.0) -- returns Array<String>
```
`md_parse` parses a Markdown string into a typed `MdBlock` document tree. Returns `Ok(MdDocument(...))` on success. `md_render` converts an `MdBlock` back to canonical Markdown text. `md_has_heading` checks whether the document contains a heading at the given level (1–6). `md_has_code_block` checks for a fenced code block with the given language tag (use `""` for untagged blocks). `md_extract_code_blocks` returns an array of code content strings for all blocks matching the language.
Two built-in ADTs represent the Markdown document structure:
**MdInline** — inline content within blocks:
- `MdText(String)` — plain text
- `MdCode(String)` — inline code
- `MdEmph(Array<MdInline>)` — emphasis (*italic*)
- `MdStrong(Array<MdInline>)` — strong (**bold**)
- `MdLink(Array<MdInline>, String)` — link with text and URL
- `MdImage(String, String)` — image with alt text and source
**MdBlock** — block-level content:
- `MdParagraph(Array<MdInline>)` — paragraph
- `MdHeading(Nat, Array<MdInline>)` — heading with level (1–6)
- `MdCodeBlock(String, String)` — fenced code block (language, code)
- `MdBlockQuote(Array<MdBlock>)` — block quote
- `MdList(Bool, Array<Array<MdBlock>>)` — list (ordered?, items)
- `MdThematicBreak` — horizontal rule
- `MdTable(Array<Array<Array<MdInline>>>)` — table (rows of cells)
- `MdDocument(Array<MdBlock>)` — top-level document
All Markdown functions are pure and available without imports. Pattern match on `MdBlock` and `MdInline` constructors to traverse the document tree.
### HTML operations
`HtmlNode` is a built-in ADT for parsing and querying HTML documents. Parse HTML strings, query elements with CSS selectors, and extract text content. All operations are pure.
```vera
html_parse(@String.0) -- returns Result<HtmlNode, String> (parse HTML)
html_to_string(@HtmlNode.0) -- returns String (serialize to HTML)
html_query(@HtmlNode.0, @String.0) -- returns Array<HtmlNode> (CSS selector query)
html_text(@HtmlNode.0) -- returns String (extract text content)
html_attr(@HtmlNode.0, @String.0) -- returns Option<String> (get attribute value)
```
`html_parse` is lenient (like browsers) — malformed HTML produces a best-effort tree, not an error. `html_query` supports simple CSS selectors: tag name (`div`), class (`.classname`), ID (`#id`), attribute presence (`[href]`), and descendant combinator (`div p`). `html_text` recursively concatenates all text content, excluding comments. `html_attr` returns `None` for non-element nodes or missing attributes.
**HtmlNode constructors:**
- `HtmlElement(String, Map<String, String>, Array<HtmlNode>)` — element (tag name, attributes, children)
- `HtmlText(String)` — text content
- `HtmlComment(String)` — HTML comment
```vera
let @Result<HtmlNode, String> = html_parse("<div><a href=\"url\">link</a></div>");
match @Result<HtmlNode, String>.0 {
Ok(@HtmlNode) -> {
let @Array<HtmlNode> = html_query(@HtmlNode.0, "a");
IO.print(int_to_string(array_length(@Array<HtmlNode>.0)))
},
Err(@String) -> IO.print(@String.0)
}
```
All HTML functions are pure and available without imports. Pattern match on `HtmlNode` constructors to traverse the document tree.
### Regular expressions
```vera
regex_match(@String.0, @String.1) -- returns Result<Bool, String>
regex_find(@String.0, @String.1) -- returns Result<Option<String>, String>
regex_find_all(@String.0, @String.1) -- returns Result<Array<String>, String>
regex_replace(@String.0, @String.1, @String.2) -- returns Result<String, String>
```
All four regex functions take the input string as the first argument and the regex pattern as the second. `regex_replace` takes a third argument for the replacement string. All return `Result` types — `Err(msg)` for invalid patterns, `Ok(value)` on success.
`regex_match` tests whether the pattern matches anywhere in the input (substring match, not full-string). `regex_find` returns the first matching substring wrapped in `Option`. `regex_find_all` returns all non-overlapping matches as an `Array<String>` — always returns full match strings (group 0), even when the pattern contains capture groups. `regex_replace` replaces only the **first** match.
```vera
let @Result<Bool, String> = regex_match("hello123", "\\d+");
match @Result<Bool, String>.0 {
Ok(@Bool) -> if @Bool.0 then { IO.print("found digits") } else { IO.print("no digits") },
Err(@String) -> IO.print(string_concat("Error: ", @String.0))
}
```
All regex functions are pure and implemented as host imports (Python `re` / JavaScript `RegExp`).
### Numeric operations
```vera
abs(@Int.0) -- returns Nat (absolute value)
min(@Int.0, @Int.1) -- returns Int (smaller of two)
max(@Int.0, @Int.1) -- returns Int (larger of two)
floor(@Float64.0) -- returns Int (round down)
ceil(@Float64.0) -- returns Int (round up)
round(@Float64.0) -- returns Int (banker's rounding)
sqrt(@Float64.0) -- returns Float64 (square root)
pow(@Float64.0, @Int.0) -- returns Float64 (exponentiation)
```
`abs` returns `Nat` because absolute values are non-negative. `floor`, `ceil`, and `round` convert `Float64` to `Int`; they trap as `float_conversion` on NaN, an infinity, or a value outside the `Int` range `[-2^63, 2^63)`. `round` uses IEEE 754 roundTiesToEven (banker's rounding): `round(2.5)` is `2`, not `3`. `pow` takes an `Int` exponent — negative exponents produce reciprocals (`pow(2.0, -1)` is `0.5`). The integer builtins (`abs`, `min`, `max`) are fully verifiable by the SMT solver (Tier 1). The float builtins fall to Tier 3 (runtime).
### Logarithmic, trigonometric, and numeric utility functions
```vera
log(@Float64.0) -- natural logarithm (base e)
log2(@Float64.0) -- base-2 logarithm
log10(@Float64.0) -- base-10 logarithm
sin(@Float64.0) -- sine (radians)
cos(@Float64.0) -- cosine (radians)
tan(@Float64.0) -- tangent (radians)
asin(@Float64.0) -- inverse sine, returns [-π/2, π/2]
acos(@Float64.0) -- inverse cosine, returns [0, π]
atan(@Float64.0) -- inverse tangent, returns (-π/2, π/2)
atan2(@Float64.0, @Float64.1) -- quadrant-correct angle from (y, x)
pi() -- 3.141592653589793
e() -- 2.718281828459045
sign(@Int.0) -- returns Int: -1, 0, or 1
clamp(@Int.0, @Int.1, @Int.2) -- clamp(v, lo, hi) -> Int
float_clamp(@Float64.0, @Float64.1, @Float64.2) -- Float64 clamp
```
All log and trig functions follow IEEE 754 semantics: `NaN` for out-of-domain inputs (e.g. `log(-1.0)`, `asin(2.0)`), `±Infinity` for overflow. The logarithms' zero pole is not a domain error: `log(0.0)` / `log2(0.0)` / `log10(0.0)` return `-Infinity` in both runtimes (#790). The argument order for `atan2` is `(y, x)`, matching POSIX / Python / JavaScript — `atan2(1.0, 1.0)` is `π/4`. `sign` and `clamp` are inlined as WAT (no host call). `pi()` and `e()` inline as `f64.const` constants. The log and trig functions fall to Tier 3 verification (they're uninterpreted in Z3's real-arithmetic fragment).
### Type conversions
```vera
int_to_float(@Int.0) -- returns Float64 (int to float)
float_to_int(@Float64.0) -- returns Int (truncation toward zero)
nat_to_int(@Nat.0) -- returns Int (the identity: every Nat is an Int)
int_to_nat(@Int.0) -- returns Option<Nat> (None if negative)
byte_to_int(@Byte.0) -- returns Int (zero-extension)
int_to_byte(@Int.0) -- returns Option<Byte> (None if out of 0..255)
```
Vera has no implicit numeric conversions — use these functions to convert between numeric types. `int_to_float` and `byte_to_int` are widening conversions that always succeed (a `@Byte` is `0..255`, always in i64 range). `nat_to_int` widens `@Nat → @Int` as the identity, the same no-op as the implicit `@Nat → @Int` coercion, so it is never needed for widening. `float_to_int` truncates toward zero and traps on NaN/Infinity. `int_to_nat` and `int_to_byte` are checked narrowing conversions that return `Option` — pattern match on the result to handle the failure case. `byte_to_int` is SMT-verifiable (Tier 1); the rest are Tier 3 (runtime).
`Byte` is excluded from arithmetic operators (`+`, `-`, `*`, `/`, `%`, unary `-`) at type-check time — `@Byte.0 + @Byte.1` produces `E140`. For byte-level math, convert to `Int` via `byte_to_int`, do the arithmetic in `@Int`, and convert back via `int_to_byte` if needed. Direct `@Byte` arithmetic (with verified underflow + overflow guards) is an open design question, [#564](https://github.com/aallan/vera/issues/564); the convention keeps the verifier's range-checking story focused on `@Nat` (where only underflow can occur).
### Float64 predicates
```vera
float_is_nan(@Float64.0) -- returns Bool (true if NaN)
float_is_infinite(@Float64.0) -- returns Bool (true if ±infinity)
nan() -- returns Float64 (quiet NaN)
infinity() -- returns Float64 (positive infinity)
```
`float_is_nan` and `float_is_infinite` test for IEEE 754 special values. `nan()` and `infinity()` construct them — use `0.0 - infinity()` for negative infinity. All four are Tier 3 (runtime-tested, not SMT-verifiable).
**Float postconditions are near the solver's ceiling.** Contract predicates over `@Float64` are discharged against Z3's IEEE-754 sort, which costs roughly an order of magnitude more solver time than the integer equivalent of the same shape — a two-branch absolute difference runs to several seconds where the `@Int` version takes a fraction of one. Shapes that land near the default per-query budget (10 s) are therefore host-sensitive: the same program can report Tier 1 on a fast machine and Tier 3 on a slow or busy one. When a float contract falls to Tier 3, re-run it with a larger budget — `vera verify --timeout-ms 60000 file.vera`, or `VERA_Z3_TIMEOUT_MS` for a whole session — before concluding anything: a claim that proves with more time needed time, while one that stays Tier 3 at any budget is standing behind something the solver cannot see through at all, such as `sqrt` or `asin`. Only the second kind is a reason to restate the contract.
**Redeclaring a built-in effect is an error (E152)**: an `effect IO { ... }` block — or `State<T>`, `Exn<E>`, `Http`, `Random`, `Inference`, `DB`, `Diverge`, `Async`, `HttpServer` — is rejected at `vera check`, whether or not its operation signatures match the built-in. The operations come with the effect row: write `effects(<IO>)` on the function and call `IO.print(...)`. Beyond one canonical form, the block cannot be honoured — code generation routes a qualified `IO.op(...)` to the fixed host import by qualifier name and never reads the declaration, so a divergent signature would compile to invalid WebAssembly that traps at `run`. Give a genuinely different effect a distinct name (e.g. `Logger`).
**Redefining a built-in is an error (E151)**: a function whose name matches a built-in (e.g. `abs`, `array_length`, `clamp`, `to_string`) is rejected at `vera check`. Built-ins are always in scope as the single canonical definition, so a second one is both redundant (one canonical form) and — for the verifier-modelled built-ins — silently unsound: the verifier would reason with the built-in's model while codegen runs your body. Call the built-in directly (no import needed), or give your function a distinct name (e.g. `magnitude`) for genuinely different behaviour. The one exception is the prelude's Option/Result/Json/Html *combinators* (`option_map`, `option_and_then`, `option_unwrap_or`, `result_map`, `result_unwrap_or`, `json_*`, `html_attr`): these are ordinary Vera functions the prelude injects, so a same-named user definition replaces them, including where the prelude's own bodies call them.
**Declaring a data type with a built-in type's name is an error (E158)**: `data Array { ... }`, `data Map { ... }`, `data Set { ... }`, `data Decimal { ... }`, `data Future { ... }` and `data Tuple { ... }` are rejected at `vera check`, with any number of type parameters, at the entry file and inside a module alike. The compiler recognises `Future` and `Tuple` *by name* throughout code generation — how a value is rendered, compared and laid out — so a declaration of one could not be told apart from the built-in: under a `data Tuple`, `show(MkShadow(7))` would print `(7)`, dropping the constructor name. A declaration of `Array`, `Map`, `Set` or `Decimal` with the built-in's number of type parameters is the same type as the built-in to the type checker, so a built-in value would be accepted where the declaration's is expected and read through the wrong layout: `show(decimal_from_int(5))` beside a `data Decimal { MkShadow(Int) }` would print the declaration's constructor. It is the same rule that reserves built-in function names (E151) and built-in effect names (E152). For `Future` and `Tuple` it also covers a **constructor** name inside any ADT (`data Box { Tuple(Bool) }` is also E158, because code generation flattens constructor layouts by name and the user's would displace the built-in carrier's); a constructor may still be called `Array`, `Map`, `Set` or `Decimal`. The prelude's data types (`Option`, `Result`, `Ordering`, `UrlParts`, `Json`, `HtmlNode`, `MdBlock`, `MdInline`, `Request`, `Response`) are not reserved: they are ordinary declarations a program may shadow — `examples/vera/collections.vera` ships a `public data Option<T>`. A `type Future = ...` / `type Tuple = ...` alias is unaffected: an alias names a binding, not a layout. Rename the declaration (`data Money`, not `data Decimal`), or use the built-in directly.
**Two declarations may not share a constructor name (E159)**: within one file, two `data` declarations may not both declare a constructor of the same name — `private data A1 { Pair(Int, Int) }` beside `private data A2 { Pair(Bool, Bool) }` is rejected at `vera check`, located at the second declaration and naming the first. Constructor names are resolved by name alone, so one namespace cannot hold two, and accepting the pair produced diagnostics describing whichever declaration registered last rather than the collision. It is the single-file sibling of E610 (two modules) and E157 (two imports). Shadowing a *prelude* constructor is a different shape and stays legal — a program may restate `Option`, `Result` or `Ordering` — as is shadowing an *imported* constructor (§8.5.2), though see §11.16 for the compilation caveat on that pair.
**Reserved function names (E153)**: four groups of identifier cannot be a function name. `old` and `new` are contract state forms, so `old(...)` / `new(...)` always parses as a reference to an effect's before/after state (Chapter 7, Section 7.9.2) and never as a call. `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true` and `false` are keywords the lexer admits as a name after `fn` but reads as the keyword everywhere else, so `match(3)` in a body does not parse as a call either. `resume` is not a keyword and a declaration does parse, but inside every handler clause body `resume` is the resumption operator, so a function of that name would give one spelling two meanings by position; writing `resume(...)` inside a handler clause is unaffected. The 21 contextual keywords — `ability`, `data`, `decreases`, `effect`, `effects`, `else`, `ensures`, `import`, `in`, `invariant`, `module`, `op`, `private`, `public`, `pure`, `requires`, `result`, `then`, `type`, `where` and `with` — would parse and run as function names, but spec §1.4 reserves them, so they are refused too. A function under any of these names — top-level, `where`-helper, or in an imported module — is rejected at `vera check`; rename it (the diagnostic suggests a name, such as `combined_with` for `with`). Only the exact identifiers are reserved: `older`, `renew`, `matched`, `resumed` and the like are ordinary function names. `handle` is the one keyword still available, because `public fn handle(@Request -> @Response)` is the entry point `vera serve` invokes from the host (Chapter 9, Section 9.5.6).
Example:
```vera
private fn greet(@String -> @String)
requires(true)
ensures(true)
effects(pure)
{
string_concat("Hello, ", @String.0)
}
```
## Contracts
### requires (preconditions)
Conditions that must hold when the function is called:
```vera
private fn safe_divide(@Int, @Int -> @Int)
requires(@Int.1 != 0)
```
### ensures (postconditions)
Conditions guaranteed when the function returns. Use `@T.result` to refer to the return value:
```vera
ensures(@Int.result == @Int.0 / @Int.1)
```
### decreases (termination)
Required on **every** recursive function whose effect row does not name `Diverge`, pure or effectful: the expression must strictly decrease on each recursive call so Z3 can discharge termination. A function is recursive when it lies on a cycle of calls, whether it calls itself directly, through a `where` helper, through a closure or handler clause in its own body, or through other top-level functions. Every function on the cycle that does not name `Diverge` needs its own `decreases`, and the measure must decrease on every call from one member of the cycle to another. A recursive function with neither a `decreases` clause nor `Diverge` is rejected at check time (`E137`). An `<IO>` loop that counts up to a bound takes the distance left as its measure — see the FizzBuzz loop in the [Iteration](#iteration) section. A contract cannot call back into its own function, directly or through other calls (`E138`).
```vera
private fn factorial(@Nat -> @Nat)
requires(true)
ensures(@Nat.result >= 1)
decreases(@Nat.0)
effects(pure)
{
if @Nat.0 == 0 then {
1
} else {
@Nat.0 * factorial(@Nat.0 - 1)
}
}
```
For nested recursion, use lexicographic ordering: `decreases(@Nat.0, @Nat.1)`.
**A precondition no argument can satisfy is not a proof.** `requires(@Int.0 > 5 && @Int.0 < 3)` has no model, so every obligation in the function would discharge from a contradiction — the body is never checked against a reachable state. `vera verify` reports **E538**, an ERROR, and refuses the program at the definition; the function's *proved* obligations are demoted to `tier3_unguarded` (counted in no tier). An obligation that came back anything else — `violated`, `tier3`, `tier3_unguarded` — keeps its status and its own code, because a contradiction can only manufacture a proof and that verdict was reached for some other reason. A call to such a function reports the ordinary `E501` when the callee is monomorphic; through a `forall` generic it is only disclosed. A top-level `assume` is a premise here too, because it is taken on trust rather than discharged: `assume(@Int.0 < 3); assume(@Int.0 > 5);` is the same contradiction, and the diagnostic points at the `assume` rather than at a `requires` that may be blameless. A branch or `match` arm whose guard cannot hold is *unreachable* rather than contradictory, and is not reported. The same demotion under **E539** means the premises contradict a fact derived from the program — a callee's postcondition, a refined return, a declared-type fact. Usually that is the program disagreeing with itself (an `assume` or a `requires` no callee's contract permits) and the fix is to weaken one of them; only when no such premise is at fault is the derived fact the compiler's, and worth reporting. E539 stays a warning where E538 is an error: the premise at fault there can be one you do not control, so the run declines to certify rather than refusing your program. A third code, **E540**, is neither: it means the premises could not be SHOWN satisfiable and they use arithmetic outside the decidable fragment (a product or a division of two slot references), so Tier 1 is withheld rather than claimed — raise `--timeout-ms` or replace the nonlinear premise with a linear bound. E539 also covers the case where the solver could not decide which layer is at fault — E538 refuses only on a REFUTATION of your own premises, so a budget too small to attribute the contradiction never refuses your program.
The measure must have a well-founded ordering — `Nat`, `Int`, a data type (ordered by structural size), or a lexicographic tuple of these; a `Float64`/`String`/`Bool` measure is rejected at check time (`E127`). A measure Z3 cannot prove is checked at run time: a recursive re-entry whose measure fails to strictly decrease (or goes negative) traps with a message naming the function, instead of looping forever. Self-recursive tail calls keep tail-call optimization (the hop is checked at the call site, so guarded iteration still runs at constant stack depth); only *mutually*-recursive tail calls between guarded functions fall back to plain calls. An ADT measure of a *parameterized* type (`List<Int>`) is not runtime-ranked, and a function declaring `Exn` gets no runtime guard (a throw would unwind past the state restores). In both cases `vera verify` still reports an unproved measure as a Tier 3 runtime check (`E525`) that nothing performs, so prove those measures statically.
### Workflow: writing contracts incrementally
**Start with scaffolding, then strengthen.** A function with placeholder contracts type-checks
and compiles:
```vera
requires(true) ensures(true)
```
Fill in real contracts *after* the body type-checks cleanly. Strengthen in this order:
1. Write `requires(true) ensures(true)` and run `vera check` — confirm the body is correct first.
2. Add a `requires` condition for each invariant the caller must satisfy.
3. Add an `ensures` condition describing what the function guarantees. Use `@T.result` for the
return value.
4. Run `vera verify` — **not just `vera check`** — to confirm contracts are statically provable.
`vera check` only type-checks; `vera verify` runs Z3.
5. If `vera verify` reports a contract will be checked at runtime (Tier 3), the Z3 solver could
not prove it. Re-run with a larger budget first (`vera verify --timeout-ms 60000 file.vera`);
if it stays Tier 3, simplify the contract expression.
6. Run `vera test` to find counterexamples. If `vera test` reports a failure, the contract is
reachable and the function body is wrong.
### Quantified expressions
```vera
-- For all indices in [0, bound):
forall(@Nat, array_length(@Array<Int>.0), fn(@Nat -> @Bool) effects(pure) {
@Array<Int>.0[@Nat.0] > 0
})
-- There exists an index in [0, bound):
exists(@Nat, array_length(@Array<Int>.0), fn(@Nat -> @Bool) effects(pure) {
@Array<Int>.0[@Nat.0] == 0
})
```
The predicate takes exactly one parameter, the index, typed `@Nat` or `@Int` (or an alias of either), and returns `@Bool`. The index runs over every value from 0 up to the bound, so a refined parameter such as `fn(@{ @Nat | @Nat.0 < 10 } -> @Bool)` is refused (`E179`). Put the condition on the index type instead, `forall(@{ @Nat | @Nat.0 < 10 }, n, ...)`, which ranges over the values that satisfy it, or test it in the body: `P ==> Q` for `forall`, and `P && Q` for `exists`. The index type itself must be `@Nat` or `@Int`, or a refinement of one (`E186`). In a generic, a type parameter is accepted as the index type but not as the predicate's parameter or result (`E179`) or as the bound's type (`E128`), whatever the generic is instantiated at: write `@Nat`, `@Int` or `@Bool` there.
## Effects
Vera is pure by default. All side effects must be declared.
### Declaring effects on functions
```vera
effects(pure) -- no effects
effects(<IO>) -- performs IO
effects(<Http>) -- network access
effects(<State<Int>>) -- uses integer state
effects(<State<Int>, IO>) -- multiple effects
effects(<Http, IO>) -- network + IO
effects(<Async>) -- async computation
effects(<HttpServer>) -- HTTP request handler (vera serve)
effects(<Random>) -- non-deterministic (random number generation)
effects(<DB>) -- SQL database access
effects(<Diverge>) -- may not terminate
effects(<Diverge, IO>) -- divergent with IO
```
`Diverge` is a built-in marker effect with no operations. Its presence in the
effect row signals that the function may not terminate. Functions without
`Diverge` must be proven total (via `decreases` clauses on recursion). Use it
for a loop with no bound, such as a server or read-eval loop: a function that
declares it needs no `decreases`, and compiles like any other; it has a
termination guard only if it also declares `decreases`. Like any effect, it
propagates: every function that calls a `Diverge` function must declare
`Diverge` too (`E125`), up to `main`.
Every entry of a row names a built-in effect. An effect variable may stand in
a function type's row, a parameter typed `fn(A -> B) effects(<E>)`, and never
in a function's own row: `forall<E> fn f(...) effects(<E>)` is refused at check
(`E340`), since code generation compiles each instantiation's types and never
its row. A user-declared effect (`effect Logger { op log(String -> Unit); }`)
checks as a declaration, and no row may name it: nothing implements its
operations, and a handler for it is refused too, so a row naming it, a
function's, a closure's or a function type's, is refused at check (`E340`),
and so is a call of one of its operations under a row that does not name it.
`State` and `Exn` take their type argument in a row: `effects(<State<Int>>)`,
never `effects(<State>)` (`E340`).
An operation is held to the row in force where it is performed, as a call to a
function is: `Random.random_int(1, 6)` in a function declared `effects(<IO>)`
is refused at the call (`E125`), and under `effects(pure)` the function is
refused (`E122`). A row variable names no effect, so `effects(<IO, E>)`
permits `IO`'s operations and no others. A handler's body is checked under the
row around it with the handled effect added. A closure's body is checked under
the closure's own row, which a handler around the closure does not extend, so
a closure that performs a `State` or `Exn` operation writes the handler inside
its own body (`E340` otherwise).
### Effect declarations
The IO effect is built-in — no declaration is needed. It provides these operations:
| Operation | Signature | Description |
|-----------|-----------|-------------|
| `IO.print` | `String -> Unit` | Print a string to stdout (no implicit newline; flushes per call) |
| `IO.read_line` | `Unit -> String` | Read a line from stdin |
| `IO.read_char` | `Unit -> Result<String, String>` | Read one character from stdin — cbreak mode on a Unix TTY, where Ctrl-D gives `Err("EOF")`; redirected input reads one character from the stdin stream and gives `Err("EOF")` at end of input. Browser target not supported — depends on JSPI for suspend/resume. |
| `IO.read_file` | `String -> Result<String, String>` | Read file contents |
| `IO.write_file` | `String, String -> Result<Unit, String>` | Write string to file |
| `IO.read_bytes` | `String -> Result<Array<Byte>, String>` | Read a file's bytes, unchanged (no UTF-8 decoding, no newline translation) |
| `IO.write_bytes` | `String, Array<Byte> -> Result<Unit, String>` | Write bytes to a file, unchanged |
| `IO.args` | `Unit -> Array<String>` | Get command-line arguments |
| `IO.exit` | `Int -> Never` | Exit with status code |
| `IO.get_env` | `String -> Option<String>` | Read environment variable |
| `IO.sleep` | `Nat -> Unit` | Pause execution for N milliseconds |
| `IO.time` | `Unit -> Nat` | Current Unix time in milliseconds |
| `IO.stderr` | `String -> Unit` | Print a string to stderr |
Do **not** write an `effect IO { ... }` block: redeclaring a built-in effect is a compile error (`E152`), whether or not the signatures match the built-in. The same holds for `State<T>`, `Exn<E>`, `Http`, `Random`, `Inference`, `DB`, `Diverge`, `Async`, and `HttpServer`. Declaring `effects(<IO>)` on the function is all that is needed — the operations follow from the effect row, so there is exactly one way to write the program.
**Output buffering and live writes.** Under `vera run` text mode, every `IO.print` call writes to `sys.stdout` and flushes immediately — animations, progress bars, REPLs, and any output using ANSI escape sequences (cursor home, clear screen) render in real time. The captured transcript is *also* preserved in memory so that if the program traps, every byte printed before the trap reaches `WasmTrapError.stdout` and the JSON envelope's `stdout` field. Under `vera run --json`, live mirroring is suppressed — the transcript lives only in the JSON envelope, because writing live to stdout would corrupt the envelope for downstream consumers parsing it. Programs do not need to call any "flush" operation; per-call flushing is the contract.
### Performing effects
Call the effect operations directly:
```vera
private fn greet(@String -> @Unit)
requires(true)
ensures(true)
effects(<IO>)
{
IO.print(@String.0);
()
}
public fn main(@Unit -> @Unit)
requires(true)
ensures(true)
effects(<IO>)
{
match IO.read_file("data.txt") {
Ok(@String) -> IO.print(@String.0),
Err(@String) -> IO.print(@String.0)
};
()
}
```
### State effects
```vera
private fn increment(@Unit -> @Unit)
requires(true)
ensures(new(State<Int>) == old(State<Int>) + 1)
effects(<State<Int>>)
{
let @Int = get(());
put(@Int.0 + 1);
()
}
```
In `ensures` clauses, `old(State<T>)` is the state before the call and `new(State<T>)` is the state after.
### Exception effects
The `Exn<E>` effect models exceptions with error type `E`. It is built-in — no
declaration is needed, and writing one is `E152`. Its single operation is
`throw : E -> Never`, which never resumes.
Throw exceptions using the qualified call syntax:
```vera
private fn safe_div(@Int, @Int -> @Int)
requires(true)
ensures(true)
effects(<Exn<String>>)
{
if @Int.1 == 0 then {
Exn.throw("division by zero")
} else {
@Int.0 / @Int.1
}
}
```
Handle exceptions with `handle[Exn<E>]`:
```vera
private fn try_div(@Int, @Int -> @Option<Int>)
requires(true)
ensures(true)
effects(pure)
{
handle[Exn<String>] {
throw(@String) -> None
} in {
Some(safe_div(@Int.0, @Int.1))
}
}
```
The handler catches the exception and returns a fallback value. The `throw` handler clause receives the error value and must return the same type as the overall `handle` expression. Exception handlers do not use `resume` — throwing is non-resumable.
### Async effect
The `Async` effect enables asynchronous computation with `Future<T>`:
```vera
effects(<Async>) -- async computation
effects(<IO, Async>) -- async with IO
```
`async` and `await` are built-in generic functions:
```vera
private fn compute(@Int, @Int -> @Int)
requires(true)
ensures(true)
effects(<Async>)
{
let @Future<Int> = async(@Int.1 * 2);
let @Future<Int> = async(@Int.0 * 3);
await(@Future<Int>.0) + await(@Future<Int>.1)
}
```
`async(expr)` evaluates `expr` and wraps the result in `Future<T>`. `await(@Future<T>.n)` unwraps it.
**Concurrency (#841):** `async(Http.get(url))` and `async(Http.post(url, body))` — with call-free argument expressions — run **concurrently** in the native runtime: the request is issued on a worker thread at the `async(...)` point, and `await` blocks for the response. Fire several, then await them in any order to overlap network latency:
```vera
public fn fan_out(@String, @String -> @Bool)
requires(true) ensures(true) effects(<Http, Async>)
{
let @Future<Result<String, String>> = async(Http.get(@String.1));
let @Future<Result<String, String>> = async(Http.get(@String.0));
let @Result<String, String> = await(@Future<Result<String, String>>.1);
let @Result<String, String> = await(@Future<Result<String, String>>.0);
true
}
```
Every other `async` shape evaluates eagerly (sequential) — `Future<T>` is then just `T`'s representation with no overhead. The checker warns (`W002`) when the argument's effect row falls outside the commutative whitelist `{Http, Async}` (e.g. an `IO`-effectful call), marking where eager evaluation is semantically required. The browser runtime is always eager (identical values, request fires at the `async` point).
### HttpServer effect
`HttpServer` is a marker effect (no operations) for **verified HTTP request handling** (#305). Define a total handler and serve it with `vera serve prog.vera [--port N]` — the accept loop lives in the host, so no `Diverge` is involved and every contract on the handler is an ordinary obligation. `Request` / `Response` are built-in prelude ADTs:
```vera
public fn handle(@Request -> @Response)
requires(true) ensures(true) effects(<HttpServer>)
{
match @Request.0 {
Request(@String, @String, @Map<String, String>, @String) ->
Response(200, map_new(), @String.0)
}
}
```
Request fields: method, path, headers (`Map<String, String>`), body — in the match arm above the String bindings are method (`@String.2`, oldest), path (`@String.1`), body (`@String.0`, most recent). Response fields: status (`Int`), headers, body. Each request runs on a fresh instance (State cannot leak between requests); a runtime contract violation answers 500 with the trap diagnostic. Native-only (no browser serving).
### Http effect
The `Http` effect enables network I/O. It is built-in — no `effect Http { ... }` declaration is needed.
| Operation | Signature | Description |
|-----------|-----------|-------------|
| `Http.get` | `String -> Result<String, String>` | HTTP GET request |
| `Http.post` | `String, String -> Result<String, String>` | HTTP POST request (body as JSON; sends `Content-Type: application/json`) |
```vera
effects(<Http>) -- network access
effects(<Http, IO>) -- network + IO
```
Both operations return `Result<String, String>` — `Ok` with the response body on success, `Err` with the error message on failure. Compose with `json_parse` for typed API responses:
```vera
public fn fetch_json(@String -> @Result<Json, String>)
requires(string_length(@String.0) > 0)
ensures(true)
effects(<Http>)
{
let @Result<String, String> = Http.get(@String.0);
match @Result<String, String>.0 {
Ok(@String) -> json_parse(@String.0),
Err(@String) -> Err(@String.0)
}
}
```
Like IO, `Http` is a built-in effect. Unlike IO, it has a fixed set of two operations — there is no need to restrict operations via an explicit declaration.
### Inference effect
The `Inference` effect makes LLM calls explicit in the type system. It is built-in — no `effect Inference { ... }` declaration is needed.
| Operation | Signature | Description |
|-----------|-----------|-------------|
| `Inference.complete` | `String -> Result<String, String>` | Send a prompt, return `Ok(completion)` or `Err(message)` |
```vera
effects(<Inference>) -- LLM access
effects(<Inference, IO>) -- LLM + console output
effects(<Http, Inference>) -- fetch + LLM
```
Returns `Result<String, String>` — `Ok` with the completion text on success, `Err` with the error message on failure. Provider is selected from environment variables: `VERA_ANTHROPIC_API_KEY`, `VERA_OPENAI_API_KEY`, `VERA_MOONSHOT_API_KEY` (Kimi), `VERA_MISTRAL_API_KEY`, `VERA_XAI_API_KEY` (Grok), or `VERA_DEEPSEEK_API_KEY`. Auto-detection walks the provider registry in insertion order — `anthropic`, `openai`, `moonshot`, `mistral`, `xai`, `deepseek` — and takes the first whose key is set to a non-empty value — an empty string is skipped, as if unset — so when several are set the earliest in that order wins. Setting `VERA_INFERENCE_PROVIDER` (valid values: `anthropic`, `openai`, `moonshot`, `mistral`, `xai`, `deepseek`) skips detection entirely and forces that provider; `VERA_INFERENCE_MODEL` overrides its default model. See [`ENVIRONMENT.md`](https://github.com/aallan/vera/blob/main/ENVIRONMENT.md) for the full env-var reference.
```vera
private fn classify(@String -> @Result<String, String>)
requires(string_length(@String.0) > 0)
ensures(true)
effects(<Inference>)
{
let @String = string_concat("Classify the sentiment as Positive, Negative, or Neutral: ", @String.0);
Inference.complete(@String.0)
}
```
Compose with `match` to handle the `Result`:
```vera
public fn safe_classify(@String -> @String)
requires(string_length(@String.0) > 0)
ensures(true)
effects(<Inference>)
{
let @Result<String, String> = classify(@String.0);
match @Result<String, String>.0 {
Ok(@String) -> @String.0,
Err(@String) -> "unknown"
}
}
```
Like `Http`, `Inference` is host-backed. The browser runtime returns a detailed `Err` explaining that API keys cannot be safely embedded in client-side JavaScript; use a server-side proxy with `Http` instead.
### Random effect
The `Random` effect provides non-deterministic number generation. Like `IO` and `Http`, it is built-in — no `effect Random { ... }` declaration is needed. Functions that draw random values must declare `effects(<Random>)`, making the non-determinism visible in the type signature.
| Operation | Signature | Description |
|-----------|-----------|-------------|
| `Random.random_int` | `Int, Int -> Int` | Random integer in inclusive range `[low, high]` (caller ensures `low <= high`) |
| `Random.random_float` | `Unit -> Float64` | Uniform random in `[0.0, 1.0)` |
| `Random.random_bool` | `Unit -> Bool` | Coin flip |
```vera
private fn pick_card(@Unit -> @Int)
requires(true)
ensures(@Int.result >= 1 && @Int.result <= 52)
effects(<Random>)
{
Random.random_int(1, 52)
}
```
The Python runtime backs Random onto the `random` module (`random.randint`, `random.random()`). The browser runtime backs all three onto `Math.random()` — fast, non-cryptographic, adequate for games and simulations. There is no seeding API (deterministic testing via `handle[Random]` is not supported).
Functions that mix randomness with other effects compose normally:
```vera
public fn print_random_card(-> @Unit)
requires(true)
ensures(true)
effects(<IO, Random>)
{
IO.print(int_to_string(pick_card(())))
}
```
### DB effect
The `DB` effect executes SQL against a relational database. Like `IO` and `Http`, it is built-in — no `effect DB { ... }` declaration is needed. Functions that read or write the database must declare `effects(<DB>)`.
| Operation | Signature | Description |
|-----------|-----------|-------------|
| `DB.execute` | `String, Array<Option<String>> -> Result<Int, String>` | Runs a write (`CREATE`/`INSERT`/`UPDATE`/`DELETE`); `Ok` carries the affected-row count |
| `DB.query` | `String, Array<Option<String>> -> Result<Array<Array<Option<String>>>, String>` | Runs a `SELECT`; `Ok` is a grid of rows, each cell an `Option<String>` (SQL `NULL` is `None`) |
The second argument is the positional parameter list bound to the `?` placeholders: `Some(v)` binds a value, `None` binds SQL `NULL`. Bind data as parameters rather than splicing it into the SQL text — a bound value can never be parsed as SQL, the standard defence against injection.
```vera
public fn insert_and_count(-> @Int)
requires(true)
ensures(true)
effects(<DB>)
{
match DB.execute("CREATE TABLE users (name TEXT, nickname TEXT)", []) {
Err(@String) -> -1,
Ok(@Int) -> match DB.execute("INSERT INTO users (name, nickname) VALUES (?, ?)", [Some("Ada"), None]) {
Err(@String) -> -1,
Ok(@Int) -> match DB.query("SELECT name, nickname FROM users", []) {
Err(@String) -> -1,
Ok(@Array<Array<Option<String>>>) -> array_length(@Array<Array<Option<String>>>.0)
}
}
}
}
```
A query result is `Array<Array<Option<String>>>` — rows of cells, each cell `Some(text)` or `None` for SQL `NULL`. `NULL` and `""` stay distinct; read a `NOT NULL` column with `option_unwrap_or(cell, "")`. Both operations return `Result`, so a failed statement is the `Err(String)` arm, never a trap.
**Keep the SQL literal.** The query string must be a literal (or a `string_concat` / `let` chain of literals). A SQL string built from a runtime value — a call result, a parameter, or a `\(expr)` interpolation of one — is a **compile-time error** (`E207`): that is the injection vector. (An interpolation or concatenation whose parts are all literals stays literal, so it is accepted.) Pass every runtime value through a `?` placeholder and the params array — `DB.query("SELECT * FROM users WHERE id = ?", [Some(@String.0)])`, never `DB.query(string_concat("... id = ", @String.0), [])`. A `?`-placeholder/parameter count mismatch is `E208` when both are statically known.
The connection is chosen by `VERA_DB_URL` (default `sqlite::memory:`, or `sqlite:///path/to/file.db`). The effect is SQLite-only, single-connection, and un-mockable (`handle[DB]` is refused at check, `E340`). The browser runtime returns `Err` for every `DB` operation, and `vera compile --target wasi-p2` rejects `<DB>`.
### Effect handlers
Handlers eliminate an effect, converting effectful code to pure code. Only `State<T>` and `Exn<E>` handlers compile, and a handler for any other effect, built-in (`IO`, `Inference`) or user-declared, is refused at check (`E340`). A `State<T>` cell holds one word, so a `State<String>` or `State<Array<T>>` cell is refused too: wrap the value in a one-constructor `data` type (`private data Text { T(String) }`) and use `State<Text>`. A `State` clause ends in exactly one `resume(...)`, with any branch inside its argument (`resume(if c then { a } else { b })`).
```vera
private fn run_counter(@Unit -> @Int)
requires(true)
ensures(true)
effects(pure)
{
handle[State<Int>](@Int = 0) {
get(@Unit) -> { resume(@Int.0) },
put(@Int) -> { resume(()) }
} in {
put(42);
get(())
}
}
```
Handler syntax:
```vera
handle[EffectName<TypeArgs>](@StateType = initial_value) {
operation(@ParamType) -> { handler_body },
operation(@ParamType) -> { handler_body } with @StateType = new_value,
...
} in {
handled_body
}
```
Use `resume(value)` in a handler clause to continue the handled computation with the given return value.
For `State<T>`, `put(x)` stores `x` as the new state **intrinsically** — the canonical clause `put(@T) -> { resume(()) }` needs no `with` (see `run_counter` above). A `with @T = expr` clause **overrides** that intrinsic store, letting a clause *transform* what gets written. Inside a `put` clause the state slot `@T.0` is the state **before** the store and `@T.1` is the argument being stored (operation parameters bind first, state last — most-recent wins):
```vera
put(@Int) -> { resume(()) } with @Int = @Int.1 * 2 -- store double the argument
```
Because `@T.0` is the pre-store state, `with @T = @T.0` keeps the *old* state — it silently undoes the `put`. For an ordinary "store the argument" `put`, omit `with` entirely; reach for it only to transform the stored value. The `with` expression's type must match the handler's state type.
For the builtin `State` effect the state declaration **is** the `State<T>` cell: its declared type must structurally equal the effect's `T` after alias resolution (for refined types, predicate included), or the handle is a checker error (E336) — declare `handle[State<Nat>](@Nat = ...)`, never `(@Int = ...)`. An alias that resolves to `T`, like `type Count = Nat` with `(@Count = ...)`, is fine, and scalar aliases work as the cell type: `handle[State<Count>]`. A refined cell must use a **named** refinement alias on both sides — `type Small = { @Nat | @Nat.0 < 10 }; handle[State<Small>](@Small = 0)` — never an inline refinement literal in the `State<T>` argument (not compilable) or a refinement on the declaration alone (E336: nothing would enforce it). A handler **without** a state declaration binds no state slot in its clauses — in a stateless `put` clause, `@T.0` is the operation's argument. A user-declared effect's handler state is the handler's own accumulator and may take any type.
### Qualified operation calls
When two effects have operations with the same name, qualify the call:
```vera
State.put(42);
Logger.put("message");
```
### State handler with a loop helper
The most common State pattern uses a `where` block to define a loop helper with `effects(<State<Int>>)`. The handler wraps the entire computation; the helper calls `get` and `put` directly.
```vera
-- Sum 1..n using State<Int>
private fn add_value(@Int, @Int -> @Int)
requires(true)
ensures(@Int.result == @Int.1 + @Int.0)
effects(pure)
{
@Int.1 + @Int.0
}
public fn sum_with_state(@Nat -> @Int)
requires(true)
ensures(true)
effects(pure)
{
handle[State<Int>](@Int = 0) {
get(@Unit) -> { resume(@Int.0) },
put(@Int) -> { resume(()) }
} in {
sum_loop(@Nat.0, 1)
}
}
where {
fn sum_loop(@Nat, @Nat -> @Int)
requires(@Nat.0 <= @Nat.1 + 1)
ensures(true)
decreases(@Nat.1 + 1 - @Nat.0)
effects(<State<Int>>)
{
if @Nat.0 > @Nat.1 then {
get(())
} else {
put(add_value(get(()), @Nat.0));
sum_loop(@Nat.1, @Nat.0 + 1)
}
}
}
```
`vera run file.vera --fn sum_with_state -- 5` prints `15`, and `-- 0` prints `0`.
Key points:
- The outer function `sum_with_state` is **pure** — the handler discharges the State effect
- The `where` block helper `sum_loop` has `effects(<State<Int>>)` — it uses `get`/`put` directly
- Functions inside `where` blocks do NOT take `public`/`private` visibility
- The `put` clause stores its argument as the new state intrinsically — no `with` clause is needed for the common "store the value" case (a `with` clause is only for *transforming* the stored value; see the handler-syntax notes above)
- Pure helper functions (like `add_value`) can be called from the `where` block helper (`sum_loop`)
- The `decreases` clause on the loop helper ensures termination. The runtime guard evaluates a measure on every call, so a `@Nat` subtraction inside it needs the same bound a body would. Here the bound is `requires(@Nat.0 <= @Nat.1 + 1)`: it holds on the last call too, where the counter has passed the limit, and the measure adds before it subtracts. `decreases(@Nat.1 - @Nat.0 + 1)` computes `n - (n + 1)` on that last call and traps. A count-down loop, `decreases(@Nat.0)`, has no subtraction to bound
## Where Blocks (Mutual Recursion)
```vera
private fn is_even(@Nat -> @Bool)
requires(true)
ensures(true)
decreases(@Nat.0)
effects(pure)
{
if @Nat.0 == 0 then {
true
} else {
is_odd(@Nat.0 - 1)
}
}
where {
fn is_odd(@Nat -> @Bool)
requires(true)
ensures(true)
decreases(@Nat.0)
effects(pure)
{
if @Nat.0 == 0 then {
false
} else {
is_even(@Nat.0 - 1)
}
}
}
```
## Generic Functions
```vera
private forall<T> fn identity(@T -> @T)
requires(true)
ensures(true)
effects(pure)
{
@T.0
}
```
## Abilities (Type Constraints)
Abilities constrain type variables in generic functions. An ability declares operations that a type must support. `Eq` is one of the four built-in abilities, so the block below only shows its interface: a program never declares it, and declaring a built-in ability is an error (E185).
```vera
ability Eq<T> {
op eq(T, T -> Bool);
}
```
Use `where` in the `forall` clause to constrain type parameters:
```vera
private forall<T where Eq<T>> fn are_equal(@T, @T -> @Bool)
requires(true)
ensures(true)
effects(pure)
{
eq(@T.1, @T.0)
}
```
Four built-in abilities are available — no declarations needed:
- **`Eq<T>`** — `eq(x, y)` returns `@Bool`. Satisfied by: Int, Nat, Bool, Float64, String, Byte, Unit, and ADTs (including `Option` / `Result`, recursive, nested-generic, and mutually-recursive) whose fields are themselves `Eq` (structural derivation). Unlike `Hash`/`Show`, `Tuple`, `Array`, `Map`, and `Set` are **not** Eq-derivable — a non-Eq `==` / `eq` is rejected at check with E243.
- **`Ord<T>`** — `compare(x, y)` returns `@Ordering` (`Less`, `Equal`, `Greater`). Satisfied by: Int, Nat, Float64, Byte, String — exactly the orderable types (the `<`/`>`/`<=`/`>=` domain). A user ADT is **not** Ord-derivable, and neither is `Bool`; `compare` on a non-orderable operand is rejected with E242 (mirroring E143 on a direct `<`).
- **`Hash<T>`** — `hash(x)` returns `@Int`. Satisfied by: Int, Nat, Bool, Float64, String, Byte, Unit, and composite types (ADT, Tuple, Option, Result, Array) whose fields/elements are themselves `Hash` (structural derivation).
- **`Show<T>`** — `show(x)` returns `@String`. Satisfied by: Int, Nat, Bool, Float64, String, Byte, Unit, and composite types (ADT, Tuple, Option, Result, Array) whose fields/elements are themselves `Show`; renders `Ctor(f0, f1, …)` / `(a, b)` / `Some(x)` / `Ok(x)` / `[e0, e1, …]`.
The `Ordering` type is a built-in ADT with three constructors: `Less`, `Equal`, `Greater`. Use it with pattern matching:
```vera
public fn signum(@Int, @Int -> @Int)
requires(true)
ensures(true)
effects(pure)
{
match compare(@Int.1, @Int.0) {
Less -> 0 - 1,
Equal -> 0,
Greater -> 1
}
}
```
Key rules:
- Abilities are first-order only: `Eq<T>`, not `Mappable<F>` where `F` is a type constructor
- Constraint syntax: `forall<T where Eq<T>>` — constraints go inside the angle brackets
- Multiple constraints: `forall<T where Eq<T>, Ord<T>>`
- Ability declarations mirror effect declarations (both use `op`)
- User-defined abilities are declared with the same syntax, but nothing implements one for a type, so a call to one of their operations and a `where` constraint naming one are refused at check (`E340`); use the four built-in abilities, or pass an explicit function value. An ability's operation is called bare: `Eq.eq(1, 1)` is refused (`E340`), `eq(1, 1)` is the call
- ADT auto-derivation: `Eq` is derived **structurally** — a simple enum, or an ADT every field of which is itself `Eq` (an `Eq` primitive including `String` (compared by content), or a nested `Eq` ADT, recursively). A field with no `Eq` semantics (`Array`, `Map`, a host handle) makes the ADT non-derivable.
- Unsatisfied constraints produce error E613
## Modules
```vera
module vera.math;
import vera.collections;
import vera.collections(List, Option);
public fn exported(@Int -> @Int)
requires(true)
ensures(true)
effects(pure)
{
@Int.0
}
```
Every top-level `fn` and `data` must have explicit `public` or `private` visibility. Use `public` for functions that other modules should be able to import.
Import paths resolve to files on disk: `import vera.math;` looks for `vera/math.vera` relative to the importing file's directory (or the project root). Imported files are parsed and cached automatically. Circular imports are detected and reported as errors.
Imported functions can be called by name (bare calls): `import vera.math(magnitude); magnitude(-5)` resolves `magnitude` from the imported module. Selective imports restrict available names; wildcard imports (`import m;`) make all declarations available. Local definitions shadow imported names. Imported ADT constructors are also available: `import col(List); Cons(1, Nil)`.
Imported function contracts are verified at call sites by the SMT solver. Preconditions of imported functions are checked at each call site; postconditions are assumed. This means `magnitude(x)` with `ensures(@Int.result >= 0)` lets the caller rely on the result being non-negative.
Cross-module compilation uses a flattening strategy: imported function bodies are compiled into the same WASM module as the importing program. The result is a single self-contained `.wasm` binary. Imported functions are internal (not exported); only the importing program's `public` functions are WASM exports.
If two of a namespace's imports supply the same bare name, `vera check` refuses it — E155 (function), E156 (data type), E157 (constructor) — reported at the second supplying import, in whichever file holds the clash. For a **function** name, resolve it either by narrowing one import (`import m(other_name);`) so a single supplier remains, or by declaring the name locally and reaching the imports with the module-qualified form (`m::name(...)`) — the local declaration shadows every module's version, so each is compiled under its own internal name and each qualified call reaches its own module. For a **data type** or **constructor** name, the same two remedies work, provided they leave the two declarations unable to *meet* — see below. The compile-time rails E608/E609/E610 remain as the backstop and read declarations rather than any namespace's imports: E608 fires when two modules declare the same **function** name that would share the flattened `$name` — unless neither declaration owns that bare name (both private, out-of-filter, transitive-only, or shadowed by a local declaration), or exactly one owns it and both are top-level generics whose clones live in different module-qualified namespaces; E609 and E610 fire when two modules' same-named `data` declarations describe DIFFERENT layouts AND some namespace can *meet* them, and admit a restatement (the same constructors, in the same order, with the same field types; type parameters compared by position) with their shared constructor names. E608 does not honour its ownership exemption in every shape: two modules' private helpers of one name, a selective import whose other module calls its own same-named function, and a module declaring a function over one it imports fail with E608, so rename one of them. A local definition shadows an imported **function** name without error — that is checker resolution, and the bare call becomes the local one — and it extends to data: where the two module declarations differ, each is compiled under its own owner-qualified symbol with its own layout, so narrowing the import, declaring the name locally, or making one declaration private each clears the clash. What they must not leave behind is a namespace that can meet both declarations: one that imports the bare name from both, or that imports a signature carrying a value of the type from one while it can reach the other. Two same-named cross-module data types unify, so `bone(aone(6))` composes them even under filters that exclude the type; that pair is still E609/E610, and the remedy is to rename one in its source module. The prelude's own `data` names are never qualified away; whether a module declaring one contends is then E621's shape test, below — a module that restates the prelude's type shares the one layout and compiles.
A module's data type may also collide with one the prelude provides (`Option`, `Result`, `Ordering`, `UrlParts`, `Json`, `HtmlNode`, `Request`, `Response`). One name carries one layout in the compiled program, so the two contend when their shapes differ — different constructors, a different constructor order, different field types, or a different number of type parameters (their names are free, since they are matched by position). The compiler then reports **E621** at the module's declaration; rename it there, or give it the prelude's shape. A module declaring `data Json` is legal only while no file uses the prelude's `Json`. The prelude injects `Json` when the entry file, or any module it imports, uses it: a `json_*` call, a prelude `Json` constructor (`JNull` … `JObject`), or the type name where it means the prelude's. A module's mentions of its own `Json`, or of one it imports, do not count. Once any file uses the prelude's `Json`, a differently-shaped module `Json` contends with it (E621), even when the entry file never mentions `Json`. `HtmlNode`, `Request` and `Response` are injected on the same demand. `Option`, `Result`, `Ordering` and `UrlParts` are in every program, so a differently-shaped module declaration of one of those always contends. Declaring the type in the **entry** file instead suppresses the prelude's own, so it never contends with the prelude, but a built-in that produces or consumes the prelude's type still builds the prelude's shape: a differently-shaped entry `data Ordering` passes check and verify, and then a function calling `compare` is dropped at compile. It can still meet a **module**'s declaration of the same name, and the entry is an owner like any other: a module declaration the entry cannot reach — not importable under that name, and not carried to it by an imported signature — is compiled under its own owner-qualified symbol, so only a pair that really meets is decided by shape. Matching shapes share the one layout; differing ones that meet are **E623**, reported at the entry declaration with the module's file and line. A prelude name is never qualified away, so an entry and a module declaring one always meet. Rename it in the entry file, import the module's type instead of redeclaring it, or give the entry declaration the module's shape.
Type aliases and effect declarations are module-local and cannot be imported. If another module needs the same alias or effect, it must declare its own copy.
Module-qualified calls use `::` between the module path and the function name: `vera.math::magnitude(42)`. The dot-separated path identifies the module and `::` separates it from the function name. This syntax can be used anywhere a function call is valid, and it is not affected by local shadowing. A path that names an imported module resolves against that module's public declarations. Inside a module, its own path names the module itself: in `module ma;`, `ma::two(3)` calls the file's own top-level `two`, a private one too, and a `where` helper named `two` does not shadow it. Qualification names a call site, not an import list, so writing a clashing call as `m::name(42)` does not by itself lift E155 — the ambiguity is in the namespace. It is how you reach both suppliers once a local declaration or a narrowed import has settled which one owns the bare name.
There is no import aliasing (`import m(abs as math_abs)`) and no wildcard exclusion (`import m hiding(x)`). These are intentional design decisions, not limitations. When a function name clashes across two imports, narrow one import or declare the name locally and qualify the rest; when a data type or constructor name clashes, do the same — and rename it in one of the source modules where no import-side change can keep the two declarations from meeting. Two declarations describing the same layout (the same constructors, in the same order, with the same field types, type parameters compared by position) share the one compiled layout, so they pass the COMPILE-phase rails E609/E610 — but if both imports actually supply the bare name, `vera check` still refuses it as ambiguous (E156/E157) whatever the layouts are, because scope is decided before layout is. The exception is what lets a diamond compile where the importer names the type through at most one of them. This preserves the one-canonical-form principle — every declaration has exactly one name.
There are no raw strings (`r"..."`) or multi-line string literals. Use escape sequences for special characters; this is by design — alternative string syntaxes would create two representations for the same value.
The full set of escape sequences Vera's lexer accepts:
| Escape | Produces | Notes |
|---|---|---|
| `\n` | LF (0x0A) | |
| `\t` | TAB (0x09) | |
| `\r` | CR (0x0D) | |
| `\0` | NUL (0x00) | |
| `\\` | backslash | |
| `\"` | double-quote | |
| `\u{XXXX}` | Unicode code point | 1–6 hex digits, up to U+10FFFF |
`\v` / `\f` / `\x..` / `\a` / `\b` are **not** recognised — Vera's rule is "one canonical form per value". For ASCII control bytes outside the simple-escape set (e.g. ESC 0x1B, VT 0x0B, FF 0x0C), either use the unicode escape (`"\u{1B}"`, `"\u{0B}"`, `"\u{0C}"`) or call `string_from_char_code(N)` at runtime:
```vera
-- ANSI cursor-home sequence (ESC [ H):
let @String = string_concat(string_from_char_code(27), "[H");
-- or equivalently using the unicode escape:
let @String = "\u{1B}[H";
```
Raw UTF-8 bytes in string literals are supported — the lexer reads the source as UTF-8 and stores the bytes unchanged. `"██ hello ██"` compiles and prints the six UTF-8 bytes of each block character. `string_length`, indexing, and the classifiers operate on bytes, not grapheme clusters.
See: spec Chapter 8 for the full module system specification.
## Comments
```vera
-- line comment
{- block comment -}
{- block comments {- can nest -} -}
```
## Operators (by precedence, loosest to tightest)
| Precedence | Operators | Associativity |
|------------|-----------|---------------|
| 1 | `\|>` (pipe) | left |
| 2 | `==>` (implies, contracts only) | right |
| 3 | `\|\|` | left |
| 4 | `&&` | left |
| 5 | `==` `!=` | none |
| 6 | `<` `>` `<=` `>=` | none |
| 7 | `+` `-` | left |
| 8 | `*` `/` `%` | left |
| 9 | `!` `-` (unary) | prefix |
| 10 | `[]` (index) `()` (call) | postfix |
`&&`, `||` and `==>` evaluate their right operand only where the left one does not decide the result, so the left operand guards the right one: `@Int.0 != 0 && 10 / @Int.0 > 0` is `false` on `0` without dividing, and `vera verify` proves the division safe under `@Int.0 != 0`. The same holds for an index (`@Nat.0 < array_length(@Array<Int>.0) && @Array<Int>.0[@Nat.0] > 0`), a call whose `requires` the left operand establishes, and an effect, which runs only where the right operand is evaluated.
## Best Practices
### Keep functions small
Vera's De Bruijn slot references (`@T.n`) are clear when functions have 2–3 parameters of different types. They become harder to track with 4+ parameters of the same type or long let-chains where indices shift with each binding.
**Guidelines:**
- Keep functions under ~5 parameters total
- When multiple parameters share a type, prefer breaking into smaller helper functions or where-functions
- Break long let-chains (4+ bindings of the same type) into where-functions — they create fresh scopes with reset slot indices
- Commutative operations (`+`, `*`) mask index errors; be especially careful with non-commutative operations (`-`, `/`, `<`, `>`) and recursive calls
### Use typed holes to build incrementally
When writing a new function, start with `?` placeholders and check the skeleton first. The `W001` warning tells you the expected type and lists every available binding — it is the cheapest way to confirm the return type is correct before writing the body:
```vera
public fn gcd(@Int, @Int -> @Int)
requires(@Int.1 > 0 && @Int.0 > 0)
ensures(@Int.result > 0)
effects(pure)
{
? -- W001: expected Int. Available bindings: @Int.0: Int; @Int.1: Int
}
```
Read the hint, then fill in the expression. This is especially useful when De Bruijn indices are non-obvious — the hint always shows the correct `@T.n` form for every binding in scope.
### Use where-functions for complex logic
Where-functions are private helpers scoped to their parent function. They reset the slot index namespace, making code easier to reason about:
```vera
public fn process(@Int, @Int, @String -> @Int)
requires(@Int.1 > 0)
ensures(true)
effects(pure)
{
compute(@Int.1, @Int.0, string_length(@String.0))
}
where {
fn compute(@Int, @Int, @Int -> @Int)
requires(true)
ensures(true)
effects(pure)
{
(@Int.2 + @Int.1) * @Int.0
}
}
```
## Common Mistakes
### Missing contract block
WRONG:
```vera
private fn add(@Int, @Int -> @Int) {
@Int.0 + @Int.1
}
```
CORRECT:
```vera
private fn add(@Int, @Int -> @Int)
requires(true)
ensures(@Int.result == @Int.0 + @Int.1)
effects(pure)
{
@Int.0 + @Int.1
}
```
### Missing effects clause
WRONG:
```vera
private fn add(@Int, @Int -> @Int)
requires(true)
ensures(true)
{
@Int.0 + @Int.1
}
```
CORRECT — add `effects(pure)` (or the appropriate effect row):
```vera
private fn add(@Int, @Int -> @Int)
requires(true)
ensures(true)
effects(pure)
{
@Int.0 + @Int.1
}
```
### Wrong slot index
WRONG — both `@Int.0` refer to the same binding (the second parameter):
```vera
private fn add(@Int, @Int -> @Int)
requires(true)
ensures(true)
effects(pure)
{
@Int.0 + @Int.0
}
```
CORRECT — `@Int.1` is the first parameter, `@Int.0` is the second:
```vera
private fn add(@Int, @Int -> @Int)
requires(true)
ensures(true)
effects(pure)
{
@Int.0 + @Int.1
}
```
### Missing index on slot reference
WRONG:
```vera
@Int + @Int
```
CORRECT:
```vera
@Int.0 + @Int.1
```
### Missing decreases on recursive function
WRONG:
```vera
private fn factorial(@Nat -> @Nat)
requires(true)
ensures(true)
effects(pure)
{
if @Nat.0 == 0 then {
1
} else {
@Nat.0 * factorial(@Nat.0 - 1)
}
}
```
CORRECT:
```vera
private fn factorial(@Nat -> @Nat)
requires(true)
ensures(true)
decreases(@Nat.0)
effects(pure)
{
if @Nat.0 == 0 then {
1
} else {
@Nat.0 * factorial(@Nat.0 - 1)
}
}
```
### Undeclared effects
WRONG — `IO.print` performs IO but function declares `pure`:
```vera
private fn greet(@String -> @Unit)
requires(true)
ensures(true)
effects(pure)
{
IO.print(@String.0);
()
}
```
CORRECT:
```vera
private fn greet(@String -> @Unit)
requires(true)
ensures(true)
effects(<IO>)
{
IO.print(@String.0);
()
}
```
### Using `@T.result` outside ensures
WRONG:
```vera
private fn f(@Int -> @Int)
requires(@Int.result > 0)
ensures(true)
effects(pure)
{
@Int.0
}
```
CORRECT — `@T.result` is only valid in `ensures`, and the input bound that makes it hold goes in `requires`:
```vera
private fn f(@Int -> @Int)
requires(@Int.0 > 0)
ensures(@Int.result > 0)
effects(pure)
{
@Int.0
}
```
### Non-exhaustive match
WRONG:
```vera
match @Option<Int>.0 {
Some(@Int) -> @Int.0
}
```
CORRECT:
```vera
match @Option<Int>.0 {
Some(@Int) -> @Int.0,
None -> 0
}
```
### Missing braces on if/else branches
WRONG:
```vera
if @Bool.0 then 1 else 0
```
CORRECT:
```vera
if @Bool.0 then {
1
} else {
0
}
```
### Trying to use import aliasing
WRONG — Vera does not support renaming imports:
```vera
import vera.math(magnitude as math_magnitude);
```
CORRECT — use selective import and qualified calls for readability:
```vera
import vera.math(magnitude);
vera.math::magnitude(-5)
```
If two of a namespace's imports supply the same bare name, `vera check` refuses it (E155 function / E156 data type / E157 constructor). Narrow one import or declare a function name locally; rename a clashing data type or constructor in one of the source modules.
### Trying to use wildcard exclusion
WRONG — Vera does not support `hiding` syntax:
```vera
import vera.math hiding(larger);
```
CORRECT — use selective import to list the names you need:
```vera
import vera.math(magnitude, larger);
```
### Trying to use raw or multi-line strings
WRONG — Vera does not support raw strings or multi-line literals:
```
r"path\to\file"
"""multi-line
string"""
```
CORRECT — use escape sequences:
```vera
"path\\to\\file"
"line one\nline two"
```
### Standalone `map_new()` / `set_new()` without type context
WRONG — type inference cannot resolve the key/value or element types:
```vera
let @Map = map_new();
let @Set = set_new();
```
CORRECT — nest inside an operation so types can be inferred, or provide explicit type annotation:
```vera
let @Map<String, Int> = map_new();
map_insert(map_new(), "key", 42)
let @Set<Int> = set_new();
set_add(set_new(), 1)
```
### Declaring a data type with a built-in type's name
WRONG — `Array`, `Map`, `Set`, `Decimal`, `Future` and `Tuple` are reserved built-in type names:
```vera
private data Decimal {
Cents(Int)
}
```
CORRECT — give the type a name of its own:
```vera
private data Money {
Cents(Int)
}
```
## Complete Program Examples
### Pure function with postconditions
```vera
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
}
}
```
### Recursive function with termination proof
```vera
public fn factorial(@Nat -> @Nat)
requires(true)
ensures(@Nat.result >= 1)
decreases(@Nat.0)
effects(pure)
{
if @Nat.0 == 0 then {
1
} else {
@Nat.0 * factorial(@Nat.0 - 1)
}
}
```
### Stateful effects with old/new
```vera
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);
()
}
```
### ADT with pattern matching
```vera
private data List<T> {
Nil,
Cons(T, List<T>)
}
public fn length(@List<Int> -> @Nat)
requires(true)
ensures(@Nat.result >= 0)
decreases(@List<Int>.0)
effects(pure)
{
match @List<Int>.0 {
Nil -> 0,
Cons(@Int, @List<Int>) -> 1 + length(@List<Int>.0)
}
}
```
### Iteration with IO
FizzBuzz with a recursive loop and IO effects. `fizzbuzz` is pure; `loop` and `main` have `effects(<IO>)`. Run with `vera run examples/fizzbuzz.vera`.
```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)"
}
}
}
}
private fn loop(@Nat, @Nat -> @Unit)
requires(@Nat.0 <= @Nat.1)
ensures(true)
decreases(@Nat.1 - @Nat.0)
effects(<IO>)
{
IO.print(string_concat(fizzbuzz(@Nat.0), "\n"));
if @Nat.0 < @Nat.1 then {
loop(@Nat.1, @Nat.0 + 1)
} else {
()
}
}
public fn main(@Unit -> @Unit)
requires(true)
ensures(true)
effects(<IO>)
{
loop(100, 1)
}
```
## Conformance Suite
The `tests/conformance/` directory contains small programs — most self-contained, with the Chapter 8 module-system programs and a few cross-module Chapter 7 and 9 programs importing companion `_lib.vera` / `_mid.vera` modules — that validate the language against the spec, named by spec chapter and feature; some features (slot references, match, contracts) span several programs. These are the best minimal working examples of Vera syntax and semantics.
Each program is organized by spec chapter (`ch01_int_literals.vera`, `ch04_match_basic.vera`, `ch07_state_handler.vera`, etc.) and the `manifest.json` file maps features to programs. When you need to see how a specific construct works, check the conformance program before reading the spec.
Key conformance programs by feature:
| Feature | Program |
|---------|---------|
| Slot references (`@T.n`) | `ch03_slot_basic.vera`, `ch03_slot_indexing.vera` |
| Typed holes (`?`) | `ch03_typed_holes.vera` |
| Match expressions | `ch04_match_basic.vera`, `ch04_match_nested.vera` |
| Contracts (requires/ensures) | `ch06_requires.vera`, `ch06_ensures.vera` |
| Effect handlers | `ch07_state_handler.vera`, `ch07_exn_handler.vera` |
| Closures | `ch05_closures.vera` |
| Generics | `ch02_generics.vera` |
| Recursive ADTs | `ch02_adt_recursive.vera` |
## Known Limitations
These are known limitations in the reference implementation. Most are tracked as open issues; those without an issue link are noted as such.
| Limitation | Details | Issue |
|-----------|---------|-------|
| Effect row variable unification | A function's own row may not name a type variable (`effects(<E>)` is `E340`), and one in a parameter's function type is not unified with concrete effect rows at call sites. Functions that abstract over effects require explicit row declarations. | [#294](https://github.com/aallan/vera/issues/294) |
| `map_new()` / `set_new()` require type context | The empty-collection constructors `map_new()` and `set_new()` cannot infer their key/value types without a surrounding type annotation. Assign the result to a typed `let` binding: `let @Map<String, Int> = map_new();` | — |
| `Inference.complete` has no `max_tokens` or temperature controls; `Inference` effect has no user-defined handlers | The host sends a `max_tokens` of 1024 to Anthropic and nothing else; OpenAI-style requests take the provider's defaults, and `temperature`, top-p and a system prompt cannot be set from Vera. `Inference` is always host-backed (dispatches to a real API). User-defined handlers for mocking, local models, or replay are not supported, and a user-declared effect is a declaration only: no row may name it and no handler handles it (`E340`). | [#370](https://github.com/aallan/vera/issues/370) |
| `DB` effect has no user-defined handlers | `DB` is always host-backed; `handle[DB]` for mocking or replay is not supported (shared with the other host effects). Test against `sqlite::memory:` for a hermetic real database. | [#370](https://github.com/aallan/vera/issues/370) |
| `DB` effect is SQLite-only with positional string rows | `DB` supports SQLite only, a single connection per run, and stringly-typed positional rows (`Array<Array<Option<String>>>`). Named columns, typed cells, other backends, and transactions are not supported. | [#1143](https://github.com/aallan/vera/issues/1143) |
| Nested handlers over the SAME cell type, with an operation in a clause body | A bare `get`/`put` in a clause body is the ENCLOSING context's operation (spec §7.5.2), but the host state intrinsics address only the innermost cell of a family — so when the enclosing handler (or the function's declared row) is the *same* `State<T>`, the outer cell cannot be reached. That shape is refused at check time (`E339`), where the operation is written, rather than silently writing the wrong cell; a cell named by a type parameter counts as any family it can become at an instantiation, so a generic `State<T>` inside a `State<Int>` is refused whatever `T` is instantiated at. Nest handlers over *different* cell types, or refine the inner cell with `with @T = expr`, which is the clause's own state override. Handler nesting is also capped at 8 levels of outward clause re-entry (the expansion is exponential in the nesting depth); past it the operation is refused at check time (`E339`). | [#1233](https://github.com/aallan/vera/issues/1233) |
| Browser target: `IO.sleep` freezes the tab; Browser target: ANSI escapes render as literal text | `IO.sleep` busy-waits the browser's main thread, so animations and paced simulations don't run meaningfully under `--target browser`. Write browser-target programs as a pure simulation core with a JS driver, or stick to terminal output. ANSI escape sequences (cursor control, screen clear) appear as literal control characters in the DOM rather than being interpreted. Terminal-style rendering needs an ANSI-subset interpreter in `runtime.mjs`; no language change is required. | [#603](https://github.com/aallan/vera/issues/603) |
## Known Bugs and Workarounds
`requires` and `ensures` clauses are also compiled as runtime checks, so where one of these bugs lets `vera verify` prove a false contract, the run traps with `contract_violation` rather than returning a wrong value; a contract code generation cannot express, such as a quantified `ensures`, is not compiled into one. The full list of open bugs is in [KNOWN_ISSUES.md](https://github.com/aallan/vera/blob/main/KNOWN_ISSUES.md).
| Bug | Workaround | Issue |
|-----|-----------|-------|
| `==` between two generic-data values returned by calls compares heap addresses, so equal values compare unequal and a proved `ensures` fails at run time. `map_get` on a `Map` read straight from a `State` cell returns a wrong value. | Bind each call's result with `let` before comparing; bind the cell's value with `let` before `map_get`. | [#1525](https://github.com/aallan/vera/issues/1525) |
| A callee's `ensures` can be assumed on a branch whose condition the verifier cannot translate (an `apply_fn` call in an `if` condition), so a postcondition can be proved from a call that never happens on that path. | Bind the condition with `let` first, or keep `apply_fn` out of `if` conditions whose branches carry contracted calls. | [#1696](https://github.com/aallan/vera/issues/1696) |
| `array_find` over an array of `Bool`, `Byte`, `String` or a record returns a `Some` holding the wrong value; over `Int`, `Nat` and `Float64` it is right. | Use `array_filter` with the same predicate and take element 0 when its `array_length` is positive. | [#1525](https://github.com/aallan/vera/issues/1525) |
| A `--world server` component whose handler holds a closure (a lambda passed to `array_map`, say) is refused by the default `wasmtime serve`, which exits at load with `defined tables count of 2 exceeds the per-instance limit of 1`. | Serve it with `wasmtime serve -O pooling-allocator=n`. | [#1739](https://github.com/aallan/vera/issues/1739) |
When a Vera program type-checks cleanly, compiles without errors, and then produces a runtime trap you can't explain, runtime trap diagnostics are Vera-native end-to-end: each trap carries a `kind` label naming its cause — `contract_violation`, `overflow`, `nat_guard`, `nat_underflow`, `assertion_failed`, `index_out_of_bounds`, `string_index_out_of_bounds`, `float_conversion`, `heap_exhausted`, `uncaught_exception` (an `Exn<T>` no `handle[Exn<T>]` caught before it left the entry point), `divide_by_zero`, `out_of_bounds`, `stack_exhausted`, `host_error`, or `unreachable` for the runtime's own internal limits (shadow-stack overflow and the like), and `unknown` — a message describing the failure, which names the failing site wherever the check carries one (the assertion's text, the index and its bound, the subtraction and the `requires` that discharges it), a per-kind `Fix:` paragraph naming the canonical remediation (omitted for `contract_violation` and `host_error`, whose descriptions already carry the specific instruction, and for `unknown`, where there is nothing general to suggest), and, under the default `vera run` host, a source backtrace pointing at the offending Vera function and line — not just `wasm trap: <reason>` (a `--target wasi-p2` trap keeps its kind, message and `Fix:`, but its `frames` list is empty, because frames do not cross the component boundary, spec §13.6). Tail-recursive iteration runs in constant WASM stack space for both non-allocating ([#517](https://github.com/aallan/vera/issues/517)) and allocating ([#549](https://github.com/aallan/vera/issues/549)) tail calls — the latter prepends a `$gc_sp` restore before each `return_call` to keep the shadow stack bounded across iterations.
## Specification Reference
The full language specification is in the [`spec/`](https://github.com/aallan/vera/tree/main/spec) directory of the repository:
| Chapter | Spec | Topic |
|---------|------|-------|
| 0 | [Introduction](https://github.com/aallan/vera/blob/main/spec/00-introduction.md) | Design goals, diagnostics philosophy |
| 1 | [Lexical Structure](https://github.com/aallan/vera/blob/main/spec/01-lexical-structure.md) | Tokens, operators, formatting |
| 2 | [Types](https://github.com/aallan/vera/blob/main/spec/02-types.md) | Type system, refinement types |
| 3 | [Slot References](https://github.com/aallan/vera/blob/main/spec/03-slot-references.md) | The `@T.n` reference system |
| 4 | [Expressions](https://github.com/aallan/vera/blob/main/spec/04-expressions.md) | Expressions and statements |
| 5 | [Functions](https://github.com/aallan/vera/blob/main/spec/05-functions.md) | Functions and contracts |
| 6 | [Contracts](https://github.com/aallan/vera/blob/main/spec/06-contracts.md) | Verification system |
| 7 | [Effects](https://github.com/aallan/vera/blob/main/spec/07-effects.md) | Algebraic effect system |
| 8 | [Modules](https://github.com/aallan/vera/blob/main/spec/08-modules.md) | Module system, imports, visibility, qualified calls |
| 9 | [Standard Library](https://github.com/aallan/vera/blob/main/spec/09-standard-library.md) | Built-in types, effects, functions |
| 10 | [Grammar](https://github.com/aallan/vera/blob/main/spec/10-grammar.md) | Formal EBNF grammar |
| 11 | [Compilation](https://github.com/aallan/vera/blob/main/spec/11-compilation.md) | Compilation model and WASM target |
| 12 | [Runtime](https://github.com/aallan/vera/blob/main/spec/12-runtime.md) | Runtime execution, host bindings, memory model |
| 13 | [WASI Preview 2 Target](https://github.com/aallan/vera/blob/main/spec/13-wasi.md) | The wasi-p2 component target and server world |
========================================================================
# Agent Instructions (AGENTS.md)
========================================================================
# AGENTS.md — Instructions for AI agents
This document is for AI agents working with the Vera codebase. There are two audiences: agents writing Vera code, and agents working on the compiler.
## For agents writing Vera code
Read `SKILL.md` for the full language reference. It covers syntax, slot references, contracts, effects, common mistakes, and working examples that all parse correctly.
### Conformance programs as reference
The conformance suite in `tests/conformance/` contains small, self-contained programs — named by spec chapter and feature (`chNN_feature.vera`) — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion `_lib`/module fixtures). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the negative fixtures (the entries with `expected_error` in `tests/conformance/manifest.json`) instead must *fail* with the E-code in their `expected_error` field, at the stage their `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.
### Workflow
```text
write .vera file -> vera check -> fix errors -> vera verify -> fix errors -> done
```
Use **typed holes** (`?`) to build programs incrementally. A `?` in any expression position is valid — `vera check` reports a `W001` warning with the expected type and all available slot bindings:
```text
warning: [W001] Warning at file.vera, line 6, column 3:
?
^
Typed hole: expected Int.
? is a placeholder for an incomplete expression. The compiler reports the expected type and available bindings so the hole can be filled in.
Fix:
Replace ? with an expression of type Int. Available bindings: @Int.0: Int; @Int.1: Int.
See: Chapter 4, Section 4.17 "Typed Holes"
```
Programs with holes type-check (`ok: true`) but cannot compile (`E614`). Iterative workflow:
```text
write skeleton with ? -> vera check (get W001 hints) -> fill holes -> vera check -> vera verify
```
### Commands
```bash
vera check file.vera # Parse and type-check
vera check --json file.vera # Type-check with JSON output (for parsing)
vera verify file.vera # Type-check + verify contracts via Z3
vera verify --json file.vera # Verify with JSON output (for parsing)
vera verify --timeout-ms 60000 file.vera # Per-query Z3 budget in ms (default
# 10000; env VERA_Z3_TIMEOUT_MS)
vera verify --reconcile file.vera # Also compile, and check each Tier 3 claim has
# its check (E541) and each check a record (W004)
vera compile file.vera # Compile to .wasm binary
vera compile --wat file.vera # Print WAT text (human-readable WASM)
vera compile --target browser file.vera # Compile + emit browser bundle
vera run file.vera # Compile and execute (calls main)
vera run file.vera --fn f -- 42 # Call function f with argument 42
vera serve file.vera # Serve handle(Request -> Response) over HTTP (default :8000)
vera test file.vera # Contract-driven testing via Z3 + WASM
vera test --json file.vera # Test with JSON output
vera test --trials 50 file.vera # Limit trials per function (default 100)
vera test --distrust file.vera # Also execute proved functions; a failed proved check refutes the proof (E703)
vera fmt file.vera # Format to canonical form (stdout)
vera fmt --write file.vera # Format in place
vera fmt --check file.vera # Check if already canonical
vera version # Print the installed version (also --version, -V)
vera lsp # Serve LSP over stdio (needs the [lsp] extra; see LSP_SERVER.md)
vera builtins [--json] # List the built-in function registry (no file needed)
vera effects [--json] # List the effect and ability registry (no file needed)
vera errors [--json] # List the diagnostic-code registry (no file needed)
```
See [TOOLCHAIN.md](https://github.com/aallan/vera/blob/main/TOOLCHAIN.md) for the CLI cookbook — driving the toolchain to write, verify, test, run, and debug Vera, including the `builtins`/`effects`/`errors` introspection commands.
### The language server: proof deltas without re-running the CLI
For long editing sessions, `vera lsp` (install: `pip install -e ".[lsp]"`) keeps a warm incremental Z3 session alive, so verification feedback arrives at editor latency instead of cold-start latency. Any LSP client gets diagnostics (same error codes as `--json`), per-function verification-tier hints, hover types, slot go-to-definition, and typed-hole completion.
Four custom methods exist specifically for agents — full request/response shapes in [LSP_SERVER.md](https://github.com/aallan/vera/blob/main/LSP_SERVER.md):
| Method | Question it answers |
|---|---|
| `vera/speculativeEdit` | "Would this edit keep, break, or strengthen the proofs?" — in-memory verify, returns a proof delta, touches nothing |
| `vera/proposeEdit` | "Apply this edit *iff* it verifies" — the gate cannot be skipped; `force: true` overrides loudly |
| `vera/strengthenContract` | "Tighten this contract — do all call sites still satisfy it?" — refusals point at the breaking call sites |
| `vera/addEffect` | "Thread this effect through every transitive caller" — one verified multi-site rewrite, all-or-nothing |
The intended loop: draft → `speculativeEdit` → inspect the delta → `proposeEdit`. Prefer the two structured refactors over hand-editing contracts/effect rows — the server constructs the candidate and audits the blast radius for you.
### Error handling
Error messages are natural language instructions explaining what went wrong and how to fix it. They include the offending source line, a rationale, a concrete code fix, a spec reference, and a stable error code. Feed the full error back into your context to correct the code.
For machine-parseable errors, use the `--json` flag:
```json
{
"ok": false,
"file": "example.vera",
"diagnostics": [
{
"severity": "error",
"description": "Function is missing its contract block...",
"location": {"file": "example.vera", "line": 12, "column": 1},
"source_line": "private fn add(@Int, @Int -> @Int)",
"rationale": "Vera requires all functions to have explicit contracts...",
"fix": "Add a contract block after the signature:\n\n private fn example(@Int -> @Int)\n requires(true)\n ensures(@Int.result >= 0)\n effects(pure)\n {\n ...\n }",
"spec_ref": "Chapter 5, Section 5.2 \"Function Declaration Syntax\"",
"error_code": "E001"
}
],
"warnings": []
}
```
### Error codes
Diagnostics carry stable codes, which `vera errors` lists; a few diagnostics carry none. Common codes:
| Code | Meaning |
|------|---------|
| W001 | Typed hole (`?`) — expected type and available bindings reported |
| E001 | Missing contract block (requires/ensures/effects) |
| E020 | Unterminated block comment — `{-` with no matching `-}` (they nest, so each needs its own closer) |
| E121 | Function body type doesn't match return type |
| E130 | Unresolved slot reference (`@T.n` has no matching binding) |
| E140 | Arithmetic requires numeric operands |
| E170 | Let binding type mismatch |
| E200 | Unresolved function call |
| E300 | If condition is not Bool |
| E311 | Non-exhaustive match |
| E614 | Program contains typed holes — compile rejected until holes are filled |
Full code ranges: W0xx (warnings), E0xx (parse), E1xx (type/expressions), E2xx (calls), E3xx (control flow), E5xx (verification), E6xx (codegen), E7xx (testing). See `vera/errors.py` `ERROR_CODES` for the complete registry.
The `verify --json` output includes a verification summary:
```json
{
"ok": true,
"file": "example.vera",
"diagnostics": [],
"warnings": [],
"verification": {
"tier1_verified": 2,
"tier3_runtime": 0,
"assumptions": 0,
"total": 2
}
}
```
Alongside it, an `obligations` array carries one entry per reified proof obligation (`kind`, `status`, `description`, `location`). The summary is derived from that array by `status` — `verified` counts as `tier1_verified`, `tier3`/`timeout` as `tier3_runtime`, and `total` is their sum. Reproduce the counts by *filtering on `status`*, not by taking the array's length: a `violated` or `tier3_unguarded` obligation discharged to no tier, so it is counted nowhere and is surfaced as an error or warning diagnostic instead. On a program with one refuted contract, `total: 2` beside a three-entry array is the expected partition.
`assumptions` sits beside those counts and is NOT part of that identity: it counts the `assume` statements this run took on trust (one W003 warning each, spec §6.2.6), which are not obligations and discharge to no tier. It is derived from the assembled diagnostics, so a consumer reproduces it by counting W003 rather than by reading any obligation's status. A non-zero value is the honest measure of how much of a "verified" result rests on something nobody proved.
### Essential rules
1. Every function needs `requires()`, `ensures()`, and `effects()` between the signature and body
2. Use `@Type.index` to reference bindings (`@Int.0` = most recent Int, `@Int.1` = one before)
3. Declare all effects: `effects(pure)` for pure functions, `effects(<IO>)` for IO, `effects(<Http>)` for network, `effects(<Inference>)` for LLM calls
4. `Http.get(@String.0)` and `Http.post(@String.0, @String.1)` return `Result<String, String>`; match the result
5. `Inference.complete(@String.0)` returns `Result<String, String>`; requires `VERA_ANTHROPIC_API_KEY`, `VERA_OPENAI_API_KEY`, `VERA_MOONSHOT_API_KEY` (Kimi), `VERA_MISTRAL_API_KEY`, `VERA_XAI_API_KEY` (Grok), or `VERA_DEEPSEEK_API_KEY` to run; provider auto-detected from whichever key is set to a non-empty value. See [`ENVIRONMENT.md`](https://github.com/aallan/vera/blob/main/ENVIRONMENT.md) for the full env-var reference, including `VERA_INFERENCE_PROVIDER` / `VERA_INFERENCE_MODEL` overrides
6. Recursive functions need a `decreases()` clause
7. Match expressions must be exhaustive
8. `DB.query` / `DB.execute` (effect `<DB>`) take a **literal** SQL string — a query assembled from a runtime value is a compile-time error (`E207`). Every runtime value goes through a `?` placeholder and the `Array<Option<String>>` params array (`DB.query("SELECT ... WHERE id = ?", [Some(@String.0)])`); a placeholder/params count mismatch with a literal params array is `E208`. The connection comes from `VERA_DB_URL` (default: in-memory SQLite) — see [`ENVIRONMENT.md`](https://github.com/aallan/vera/blob/main/ENVIRONMENT.md)
## For agents working on the compiler
Read `vera/README.md` for architecture docs, module map, and design patterns.
### Pipeline
```
source -> parse (parser.py) -> transform (transform.py) -> resolve (resolver.py) -> typecheck (checker/) -> verify (verifier.py) -> compile (codegen/ + wasm/) -> execute (wasmtime or browser/runtime.mjs)
```
Each stage is a module with a single public API function (`parse_file`, `transform`, `resolve_imports`, `typecheck`, `verify`, `compile`, `execute`, `test`) and is independently testable.
### Key modules
| Module | Purpose |
|--------|---------|
| `vera/grammar.lark` | Lark LALR(1) grammar |
| `vera/parser.py` | Parser: source text to Lark parse tree |
| `vera/transform.py` | Lark tree to typed AST |
| `vera/ast.py` | AST node definitions |
| `vera/types.py` | Internal type representation |
| `vera/environment.py` | Type environment and slot resolution |
| `vera/checker/` | Type checker (mixin package) |
| `vera/smt.py` | Z3 SMT translation layer |
| `vera/verifier.py` | Contract verifier |
| `vera/registration.py` | Shared function registration for checker and verifier |
| `vera/errors.py` | LLM-oriented diagnostics |
| `vera/wasm/` | WASM translation layer (mixin package) |
| `vera/codegen/` | Code generation orchestrator (mixin package) |
| `vera/tester.py` | Contract-driven testing engine |
| `vera/cli.py` | Command-line interface |
| `vera/markdown.py` | Markdown parser (host-side implementation) |
| `vera/browser/` | Browser runtime: JS host bindings, Node.js harness, bundle emission |
### Testing
```bash
pytest tests/ -v # Run all tests (see TESTING.md)
pytest tests/test_conformance.py -v # Conformance suite only
mypy vera/ # Type-check the compiler
python scripts/check_conformance.py # Every conformance program holds (positives pass; negatives fail with their E-code)
python scripts/check_examples.py # Every example must pass
python scripts/check_corpus_canonical.py # Every corpus program in canonical form
```
Test helpers follow a pattern: `_check_ok(source)` / `_check_err(source, match)` / `_verify_ok(source)` / `_verify_err(source, match)`. See existing tests for examples.
When implementing a new language feature, write the conformance program *first* — add a `.vera` file and manifest entry in `tests/conformance/`, then implement the feature until the conformance test passes. A `run`-level entry pins its run: `expected_stdout`, exactly what the program must print, and `expected_exit`, or a `nondeterministic_stdout` reason in place of `expected_stdout` (TESTING.md § Manifest).
When one mechanism bounds a bug's class, the fix closes the **class** the report belongs to, not the reported instance, in the same pull request and bounded to that mechanism: name the class boundary in the PR body and ship a class instrument — an exhaustive matrix over the space the class spans, or a generator — rather than hand-picked cases. A class whose boundary is architectural, two phases re-deriving the same fact, is not fixed per site: its issue carries the milestone of the release that removes the mechanism, and closes there. A class instrument is a burndown tool: its file carries the `matrix` marker, naming the modules that decide its class; the nightly lane and any pull request that changes the file or one of those modules run it in full, and every other pull request runs a stratified sample of its cells, pinned for a week. Review is capped at three rounds; a fourth needs a written answer to "which mechanism produces these members, and does this PR remove it?". One issue per class, with its instances as a checklist. See `CONTRIBUTING.md` § Bugs: the class, not the instance, and `TESTING.md` § Class Instruments.
### Invariants
- Every conformance program in `tests/conformance/` must hold at its declared level — positive entries pass, and the negative fixtures (the entries with `expected_error` in `tests/conformance/manifest.json`) must *fail* with their `expected_error` E-code, at the stage `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses, which also asserts the program type-checks cleanly first
- Every example in `examples/` must pass `vera check` and `vera verify`
- `mypy vera/` must be clean
- `pytest tests/ -v` must pass
- The version is written in `pyproject.toml` alone: `vera.__version__` reads the installed metadata, and `uv lock --check` holds `uv.lock`'s own entry to it; a release also needs a matching `## [X.Y.Z]` section in CHANGELOG.md, which `scripts/release.py` requires
### Releases and install docs
**Releases are automated after merge.** A version bump on `main` (`[project].version` in `pyproject.toml`, with a matching non-empty `CHANGELOG.md` section) triggers `.github/workflows/release.yml`: it builds, waits for the maintainer to approve the protected `pypi` environment, publishes to PyPI via Trusted Publishing, then creates the tag and GitHub Release at the merge SHA. Do NOT create tags, run `twine`, or `gh release create` — the maintainer and the workflow own that. See `CONTRIBUTING.md` §Releases and `RELEASING.md`.
**Install docs are circumstance-dependent — match `README.md`, `SKILL.md`, and `PYPI_README.md`; don't invent "the install route".** The GitHub source checkout (`pip install -e .`, plus `[lsp]` or `[dev]`) is the full environment — the toolchain alongside `examples/`, `tests/conformance/`, and `spec/` — and is the recommended route for agents; `pip install veralang` installs the toolchain only; the `[lsp]` extra adds the language server; never write `pip install vera` (an unrelated PyPI project). Only document a channel as an available install route once the artifact is live there **and** the install flow works end to end — check the registry, don't rely on what you remember. The VS Code extension meets that bar: [`veralang.vera-language`](https://marketplace.visualstudio.com/items?itemName=veralang.vera-language) installs from the Marketplace, in the Extensions view or via `code --install-extension veralang.vera-language`. The same gate applies to any future distribution channel.
### Contributing
See `CONTRIBUTING.md` for guidelines. Pre-commit hooks run the fast gates on every commit — ruff, mypy, trailing whitespace checks, the doc gates, and the test files the commit stages; CI runs the full test suite, the conformance suite and every example on every pull request.
========================================================================
# Language Server (LSP_SERVER.md)
========================================================================
# The Vera language server (`vera lsp`)
Vera ships a language server: a long-running process that an editor (or
an agent) talks to over the [Language Server
Protocol](https://microsoft.github.io/language-server-protocol/), the
standard JSON-RPC protocol editors use to get language intelligence —
diagnostics, hover, go-to-definition, completion — without each editor
reimplementing the compiler. One server, any LSP-capable client: VS
Code, Neovim, Emacs, Helix, Zed, or a coding agent speaking the
protocol directly.
What makes Vera's server different from a typical language server is
*what* it serves. Most language servers answer "does this parse, what
type is this?". Vera's also answers "**does this still prove?**" — it
keeps a warm, incremental Z3 verification session alive between
keystrokes, so contract proofs re-check at editor latency rather than
batch-compile latency, and it exposes that capability to agents through
four custom methods that no generic language server has.
This guide covers the editor/agent surface — the long-running server.
For the command-line surface (`vera check`/`verify`/`test`/`run` and
the introspection commands), see the CLI cookbook,
[TOOLCHAIN.md](https://github.com/aallan/vera/blob/main/TOOLCHAIN.md).
## Install and run
The server lives behind the optional `[lsp]` extra (pure-Python
dependencies: `pygls`, `lsprotocol`):
```bash
python -m venv .venv && source .venv/bin/activate # Windows: .venv\Scripts\activate
python -m pip install "veralang[lsp]"
```
To install the current GitHub source instead:
```bash
git clone https://github.com/aallan/vera.git
cd vera
python -m venv .venv && source .venv/bin/activate # Windows: .venv\Scripts\activate
python -m pip install -e ".[lsp]" # or ".[dev]", which includes it
```
Then:
```bash
vera lsp
```
speaks LSP over stdio. There is nothing to configure server-side: the
client launches the process and the handshake does the rest. Without
the extra installed, `vera lsp` prints an actionable install message
and exits; every other `vera` command works without it.
### Wiring up an editor
- **VS Code** — install [Vera Language from the VS Code
Marketplace](https://marketplace.visualstudio.com/items?itemName=veralang.vera-language)
(or see the [extension source](https://github.com/aallan/vera/tree/main/editors/vscode)).
It starts the server automatically for `.vera` files, finding the binary via the
`vera.lsp.path` setting, then a workspace-local venv
(`.venv/bin/vera`, or `.venv\Scripts\vera.exe` on Windows — so a
from-source clone needs no configuration on either platform), then
`PATH`. See its [README](https://github.com/aallan/vera/blob/main/editors/vscode/README.md) for setup.
- **Anything else** — point your editor's generic LSP client at the
command `vera lsp` for language `vera` / file pattern `*.vera`,
using stdio transport and full-document sync. That is the whole
contract for diagnostics, hover, navigation and completion. The three
custom methods that edit the document also need the client to
advertise `workspace.applyEdit` and
`workspace.workspaceEdit.documentChanges`: the server sends only
version-guarded edits, and `documentChanges` is the only form that
can carry a version.
## Standard features
On `didOpen`/`didChange` the server runs the full pipeline — parse,
type-check, **verify** — on the in-memory buffer (unsaved changes
included) and publishes:
- **Diagnostics** with the same stable error codes, rationale, and
spec references as `vera check --json` / `vera verify --json`, plus
a `tier` annotation on verification diagnostics (Tier 3 fallbacks
carry `tier: 3` in their data).
- **Per-function verification-tier hints** — a Hint-severity
diagnostic per function summarising its proof state: "Tier 1 — all
contracts proven by Z3" or "Tier 3 — N of M obligations fall back
to runtime checks". The verifier itself stays silent about
successes; the hint is how the editor shows you which functions are
*proven* rather than merely checked.
- **Hover** — the inferred type of the smallest expression under the
cursor.
- **Go-to-definition on slot references** — `@T.n` under the cursor
jumps to the parameter it names under De Bruijn resolution
(most-recent-first), which is exactly the lookup humans find
hardest to do in their head. Both sides of the lookup — the
parameter's name and the reference's — are rendered by the same
function the checker keys its binding table with, so a
parameterised reference (`@Option<Int>.0`) resolves, an
alias-spelled parameter (`@Option<Cnt>` under `type Cnt = Int`) is
reachable from its canonical spelling, and a reference inside a
`where` helper resolves against that helper's own scope, including
any `forall` variables it inherits from its parent.
- **Typed-hole completion** — with the cursor at a `?` hole,
completion lists the in-scope bindings that fit, innermost first,
each with its type.
If the pipeline itself fails on a text (an internal compiler error,
which is a bug), the server publishes whatever diagnostics the failing
step had already recorded, then one `E699` naming the failure, in place
of that text's diagnostics, and keeps no analysis of it: hover,
go-to-definition and completion answer nothing, and the proof delta and
the edit methods refuse, until a change the server can analyse. None of
them answers from the previous text's analysis, because the buffer no
longer holds that text.
## What no generic language server can do
### The warm verification core
Verification state persists between edits. Each function's discharged
proof obligations are cached against a structural hash, and the
invalidation rule follows the proof dependencies: editing a function's
*body* re-verifies only that function; editing its *contract* also
re-verifies every caller (callers assume postconditions and must
re-prove preconditions at call sites). Timeouts are never cached. The
result: after the first full pass, re-verification cost is
proportional to what your edit could actually have broken.
### Custom methods: the agent surface
Four methods extend LSP 3.17, designed for coding agents rather than
humans-with-cursors. All take plain JSON params; malformed requests
(missing/non-string fields, unknown functions) refuse with standard
JSON-RPC `InvalidParams` rather than opaque errors.
#### `vera/speculativeEdit` — "would this edit break my proofs?"
```json
{"uri": "file:///main.vera", "text": "<full proposed source>", "version": 7}
```
Verifies the proposed text *in memory* — the canonical document, its
published diagnostics, and the editor's view are untouched — and
returns a **proof delta** against the document's current obligation
set. A delta is only as good as its baseline, so the request is
refused with `InvalidParams`, as `vera/proposeEdit` is, when there is
no baseline to measure against — the document is not open, or the
server has no analysis of its current text — or when the optional
`"version"` names a version the document is no longer at:
```json
{
"ok": true,
"proof_delta": {
"newly_discharged": [],
"newly_undischarged": [{"fn": "f", "kind": "nat_sub",
"expr": "@Nat.0 - 1", "line": 6, "column": 3,
"status_before": "verified",
"status_after": "violated"}],
"timed_out": [], "removed": [], "unchanged": 11,
"proof_regressions": [{"fn": "f", "kind": "nat_sub",
"expr": "@Nat.0 - 1", "line": 6, "column": 3,
"line_before": 6, "column_before": 3,
"status_before": "verified",
"status_after": "violated"}]
},
"diagnostics": 1
}
```
An agent learns whether an edit **keeps** the program's proofs
(everything still discharges), **breaks** them (obligations become
violated or fall to runtime checks), or **strengthens** them
(previously-runtime obligations now prove) — before committing
anything.
Three of the lists — `newly_discharged`, `newly_undischarged` and
`timed_out` — **sort the speculative obligations by their status AFTER
the edit**, and together with `unchanged`, which is a count rather
than a list, they account for every obligation in the speculative
stream exactly once. `removed` is the old side: baseline-only
obligations, each carrying `status_after: null`. So the set is a
presentation of the delta rather than an answer to "did this edit take
a proof away?". That question has its own list: `proof_regressions`
holds every obligation that was `verified` before and is anything else
after — `timeout`, `tier3`, `tier3_unguarded` or `violated` — so an
obligation appears in it **as well as** in whichever status list its
new status puts it in (`verified → timeout` is in both `timed_out` and
`proof_regressions`). Read `proof_regressions` to ask
about lost proofs; read the lists to display what happened.
The two views also differ on **identity**, and deliberately. An
obligation is keyed by its span, so one inserted line above it gives it
a new key: the categories report that as a removal plus a rediscovery,
which is what a display of positions should say. The gate cannot
reason that way — an edit that shifts a line and costs a proof further
down the file would walk straight past it — so before judging anything
it pairs the leftovers on a span-insensitive key (file, owning
function, function, kind, predicate text; equal keys pair positionally
in source order). A pair is one obligation that **moved**. Pairing
changes what an entry is reported *against*, not which list it is in: the three status lists
still account for every speculative obligation exactly once, and a
relocated obligation is still an entry in `removed` at its old span
plus an entry in a status list at its new one — it simply carries the
`status_before` it paired with, where an
obligation the edit really did introduce carries `null`. The gate
reads that: a `newly_undischarged` entry whose `status_before` equals
its `status_after` only moved, so it introduced nothing and took
nothing away. Relocation is invisible to the gate; the presentation
keeps its span view.
Each `proof_regressions` entry carries both ends: `line` / `column` are
where the obligation is now, `line_before` / `column_before` where it
was. They differ exactly when the obligation moved — in the same-span
example above they are equal — and the pair is what points an agent at
the proof it broke rather than at the line it happens to sit on now.
An old obligation with no counterpart on the new side is a **deletion**,
not a regression, and does not need `force`: the gate protects proofs,
not contracts — the removal is visible in the edit itself, and no
unproved code is left behind. It is reported under `removed` with the
status it had. Replacing a proved contract with a differently-worded
one is a deletion plus an addition, so the replacement is judged as an
addition: refused if it is `violated`, `tier3` or `tier3_unguarded` —
every after-status other than `verified` and `timeout` reaches
`newly_undischarged`, and with no `before` to match, a `status_before`
of `null` differs from any `status_after` — and applied if it merely
times out, which is the same boundary any newly introduced timeout
already sits on. What the pairing key does not cover, by construction:
renaming the function, changing the obligation's kind, rewriting the
predicate text, or moving the code to another file all make it a new
obligation to the gate.
#### `vera/proposeEdit` — the enforced edit workflow
```json
{"uri": "file:///main.vera", "text": "<full proposed source>", "force": false,
"version": 7}
```
The whole edit → verify → apply sequence as one method, so the
verification gate cannot be skipped or reordered: the proposed text is
speculatively verified, and **applies only if** the proof delta has no
`proof_regressions` (no obligation lost a proof — whatever it lost it
to, and wherever in the file it now sits), no `newly_undischarged`
entry whose `status_before` differs from its `status_after`, and no
error diagnostics in the proposed state. Neither list subsumes the
other: `newly_undischarged` is the only one that can see an obligation
the edit INTRODUCES, which has no `before` to regress from and so
arrives with `status_before: null`. The `status_before` qualifier is
what lets a **relocated** obligation through: one that is undischarged
at both ends of its pair is listed here — the status lists account for
every speculative obligation, so it has to be — but it introduced
nothing and took nothing away, so the gate passes it. A pair that
worsened is refused exactly as the identical unmoved edit is.
On a pass the server asks the client to apply the edit, and changes
nothing of its own. The client owns the buffer: the server's copy of
the text, its version and the published diagnostics describe what the
client has, and they move only when the client's own `didOpen`,
`didChange` or `didClose` says the buffer moved. So the edit goes out
as one `workspace/applyEdit` — a whole-document replacement guarded by
the version of the text it was verified against, which a client whose
buffer has moved on since (the user typed, or another edit landed
first) must refuse rather than let it overwrite the newer text. The
server waits for the answer without holding up anything else, and an
applied edit reaches it as the client's `didChange`: at the client's
own version, analysed and published like any other change, and
replayed from the warm cache. On refuse, nothing is sent and nothing
changes, and the response says why:
```json
{"applied": false, "ok": true, "proof_delta": {...}, "diagnostics": 0,
"client": null, "client_reason": null}
```
`applied` is `true` when the client applied the edit, `false` when it
did not or the edit was never sent, and `null` when the server cannot
tell — it states only what it knows. `client` says what became of the
edit, and `client_reason` says why when there is a why — the client's
`failureReason`, the error it answered with, or what arrived in place
of an answer:
| `client` | What happened | What to do |
|----------|---------------|------------|
| `null` | The gate refused; nothing was sent. | Read the proof delta and the diagnostics count. |
| `"applied"` | The client applied the edit. | Nothing: its `didChange` brings the server's state along. |
| `"declined"` | The client answered `applied: false` — most often because its buffer is no longer at the version the edit was verified against. | Re-read the document and propose again. |
| `"failed"` | The client answered with an error, or the request could not be sent (`applied: false`); or the client answered with something other than a boolean `applied` (`applied: null`). | Propose again; after `applied: null`, re-read the document first. |
| `"timeout"` | No answer arrived within 60 seconds, the bound on the wait, so the proposal answers rather than wait for ever (`applied: null`). The edit request is still open: the client may still apply it, and its `didChange` then updates the server as any change does. | Re-read the document before proposing again. |
| `"cancelled"` | The request was cancelled before the client answered (`applied: null`). | Re-read the document before proposing again. |
| `"unsupported"` | The client does not advertise `workspace.applyEdit` and `workspace.workspaceEdit.documentChanges`, so no version-guarded edit could be sent, and none was. | Advertise both capabilities. |
If the client cancels the `vera/proposeEdit` request itself while the
edit is pending, that request ends with a `RequestCancelled` error —
never `applied` — and the edit request stays open for the client to
answer.
The version guard protects the newer text only if the edit was made
from, and judged against, the text at that version, so all three edit
methods refuse with `InvalidParams`, and say why, rather than act on a
text the client no longer has:
- **The document is not open.** An edit is sent only for a document
the client has open, because only then is there a version to guard it
with — the protocol's `null` version means "the file on disk is the
master", which a client applies to whatever its buffer holds when the
edit lands — and an analysis to judge it against. Open the document
first.
- **The server has no analysis of the open text** — the change it last
received could not be analysed (see [Standard
features](#standard-features)). `force` does not waive this: it
overrides the gate's verdict, not the question of which text the edit
is about. The next change the server can analyse clears it.
- **The request was made from an older version.** The optional
`"version"` names the document version the request was made from —
for `vera/proposeEdit`, the version the proposed text was written
against. When the open document is at any other version, the server
has seen changes the request did not, and refuses. Without
`"version"` the server cannot tell: a proposal written against an
older text replaces whatever the buffer holds, including typing the
server had already seen. A client that cannot send it accepts that
risk.
`"force": true` (strictly boolean — anything else fails closed)
overrides the gate for the cases where breaking a proof is the point,
but it must be said out loud. This is the same philosophy as Vera's
mandatory contracts, applied to tooling: the right thing is the only
easy thing.
#### `vera/strengthenContract` — contract change with a call-site audit
```json
{"uri": "file:///main.vera", "fn": "callee",
"kind": "requires", "expr": "@Nat.0 >= 1", "version": 7}
```
Splices the new expression over the first `requires`/`ensures` clause
of the named top-level function and runs it through the proposeEdit
gate. The call-site audit *is* the proof delta: a tightened
precondition some caller no longer satisfies surfaces as
`newly_undischarged` items of kind `call_pre` located **at the call
sites**, and the gate refuses. There is no `force` here — an agent
that wants to push through a breaking contract change must construct
the full text and call `vera/proposeEdit` with `force` explicitly.
The splice is made from the server's current text, so the optional
`"version"` here guards the agent's choice of function and clause
rather than a text it wrote; it is refused on the same terms as
`vera/proposeEdit`'s, and so is `vera/addEffect`'s.
#### `vera/addEffect` — effect propagation through the call graph
```json
{"uri": "file:///main.vera", "fn": "target", "effect": "Async", "version": 7}
```
The genuinely multi-site one. Adding an effect to a function
invalidates the effect row of every **transitive caller**, so the
server computes that closure over the call graph, rewrites each
affected `effects(...)` clause (`pure` → `<Async>`; `<IO>` →
`<IO, Async>`; functions already naming the effect are skipped —
identity is the base name before type arguments), and verifies the
whole rewrite as **one** candidate through the proposeEdit gate:
all-or-nothing, never a half-propagated document. The response adds
`"rewritten"`: the affected functions in declaration order. If every
row already carries the effect, nothing runs and the no-op shape comes
back (`"applied": false, "ok": true, "proof_delta": null,
"client": null, "rewritten": []`).
The closure is **bounded at handlers**: a call site inside a
`handle[E]` body contributes no edge, because the handler discharges
the effect there, so a caller that wraps every one of its call sites
is left unrewritten and nothing propagates past it. A caller that also
reaches the callee on an unhandled path is still rewritten — the
effect genuinely escapes along that path — and a call in a handler
*clause* propagates, since a clause body runs outside its own handler,
as does one in the handler's *state initialiser*, which is evaluated
in the enclosing scope before the handler is installed.
The bound compares the `handle[...]` head's **spelling** to the
requested effect, type arguments included and as written rather than
as resolved. So `handle[State<Nat>]` does not bound a `State<Int>`
propagation and a caller around it still gets the row — which it
needs, since the checker discharges against effect *instance*
equality. An alias spelling of the same instance
(`handle[State<MyAlias>]` with `type MyAlias = Int`) does not bound it
either, though the checker does discharge that one: there the
comparison under-prunes, leaving a row the program does not need,
which still type-checks.
[#1292](https://github.com/aallan/vera/issues/1292) tracks keying the
bound on the resolved instance. Propagation stops at the file boundary, by
design: module-qualified calls are not followed.
Rows are rewritten for top-level functions only. A call inside a
`where` block attributes to the top-level function containing it —
that is what the closure reports, and the handler bound applies inside
a helper body the same way — but the helper's own `effects(...)` row is
never rewritten, so a helper that itself needs the new effect leaves
the candidate refused at the gate rather than half-applied.
Declared-but-unused effects are legal in Vera, so the agent ordering
"propagate rows first, then write the effectful code" type-checks at
every step.
### A typical agent loop
1. `didOpen` the file; read the published diagnostics and tier hints.
2. Draft an edit; `vera/speculativeEdit` it; inspect the proof delta.
3. If the delta looks right, `vera/proposeEdit` the same text — the
server re-verifies (cheaply, from the warm cache) and has the client
apply it; `applied: true` means the client did.
4. For the two structured refactors — tightening a contract,
threading an effect — call the dedicated method instead and let
the server construct the candidate.
## Current limitations
A row without an issue link is deliberate behaviour rather than
tracked work.
| Limitation | Issue |
|-----------|-------|
| Single-file model: module imports resolve from disk, relative to the analysed document's own path, not from open editor buffers — so unsaved edits to an imported module are invisible until saved. A document that names no local path resolves no imports and is analysed alone: an `untitled:` buffer or other non-`file:` URI, and a `file://host/…` URI naming another machine (carried opaquely). | [#724](https://github.com/aallan/vera/issues/724) |
| Slot go-to-definition covers parameters only — references binding through `let`/`match` have no definition site to jump to. | [#181](https://github.com/aallan/vera/issues/181) |
| `vera/addEffect` propagation stops at the file boundary, by design: the closure runs over unqualified call names, so a module-qualified call is not followed and a caller in another file is never rewritten. | — |
## Under the hood
The server is a thin transport and feature layer over the reusable
obligation core in `vera/obligations/` (reified `ProofObligation`
records, the warm incremental `VerificationSession`). Architecture
notes live in the [compiler README](https://github.com/aallan/vera/blob/main/vera/README.md) module map; the
design history —
including why the obligation core was built before any wire format —
is the comment trail on
[#222](https://github.com/aallan/vera/issues/222).
========================================================================
# Frequently Asked Questions (FAQ.md)
========================================================================
# Frequently Asked Questions
## Why no variable names?
Variable names are one of the things that confuse LLMs rather than help them. Unlike with humans, names undermine a model's efforts to keep track of state over larger scales. Models confuse similarly named variables in different parts of the codebase easily. Names help us; they don't help them.
Wang et al. ("How Does Naming Affect LLMs on Code Analysis Tasks?", [arXiv:2307.12488](https://arxiv.org/abs/2307.12488)) systematically replaced variable and function names with nonsense or shuffled strings and measured the impact on CodeBERT across code analysis tasks. Good names do help LLM performance — but shuffled names (where a variable named `count` gets swapped with one named `result`) perform *worse* than random gibberish. The model actively gets misled by plausible-but-wrong names. Python, being dynamically typed, is hit harder than Java, because models compensate for lost names using type declarations in statically typed languages.
That last point is the Vera thesis in miniature. In a language with strong types, explicit contracts, and no variable names, the model can't fall back on the naming crutch, but it also can't be misled by it. It has to use the structural information.
Le et al. ("When Names Disappear", [arXiv:2510.03178](https://arxiv.org/abs/2510.03178)) make this sharper still: LLMs exploit statistical correlations between identifiers and functionality even on execution prediction tasks that should depend only on program structure. They call this "identifier leakage." The model *appears* to understand code when it's actually pattern-matching on familiar tokens.
So the problem isn't that variable names are useless to LLMs. It's that they're a crutch that lets the model appear to understand code when it's actually not reasoning about the code. Vera's bet is that if you remove the crutch and give the model verified structural information instead — contracts, types, effect declarations — you force it onto firmer ground.
See [`DE_BRUIJN.md`](https://github.com/aallan/vera/blob/main/DE_BRUIJN.md) for a deeper treatment: where the indexing idea comes from academically, how Vera's typed variant differs from classic De Bruijn indices, worked examples of the common traps (particularly the commutative-operations pitfall), and further reading.
## Why not keep variable names and strip them with tooling?
You could absolutely build a bidirectional transform: names in, indices out for the model, indices back to names for humans. The tooling for that would be straightforward.
The reason Vera doesn't do this is that the canonical form *is* the language. If names exist in the source, they're part of the program, which means they can diverge from intent, be inconsistent, or be misleading — and now you have two representations to keep in sync. Vera sidesteps that by having one representation that's unambiguous by construction. The model writes exactly what the compiler sees. No translation layer, no sync problem.
That said, a visualiser that infers human-readable names from types and usage for display purposes is interesting tooling *on top* of Vera. The canonical form stays clean for the model, but humans get an annotated view when they need one.
## But don't variable names help the LLM relate implementation to requirements?
This is a fair point. The contracts can say what the output *cannot* be, but if the constraints fully determine the output then the function body is superfluous. So the implementation matters, and shouldn't the implementation be tied to the human's requirements?
Vera's answer is that the contracts *are* the link between implementation and requirements. The human writes (or reviews) the contracts — preconditions, postconditions, effect declarations — and those are small, declarative, and human-readable. The compiler then proves the implementation satisfies them. The human audits the specification, not the code.
The bet is that contracts are a better surface for capturing intent than variable names scattered through an implementation. A function signature with `requires(@Int.1 != 0)` and `ensures(@Int.result == @Int.0 / @Int.1)` communicates what the function does more precisely than any variable name could.
## How do type aliases interact with `@T.n` references?
A slot reference names a type, so `type` declarations are how a program shapes its own slot namespaces. Three rules apply, and they differ deliberately.
At the **head** of a slot name an alias is opaque. `type Cnt = Int;` does not make `@Cnt` and `@Int` interchangeable — a parameter declared `@Cnt` is reached only by `@Cnt.0`. That opacity is what stops a library adding an alias and silently splitting a caller's `Int` stack.
Inside a type **argument** an alias resolves. Under the same declaration, a parameter written `@Option<Cnt>` binds `Option<Int>` and is referenced `@Option<Int>.0` — because `Option<Cnt>` and `Option<Int>` are one type, and one type must not become two namespaces.
A `State<T>` or `Exn<E>` **cell** resolves through the head as well: identity is the *resolved* type, so a helper declaring `State<Option<Int>>` and a handler spelling `State<MaybeInt>` share their state. That holds wherever the resolved type has a mangle-safe family name — see [`DE_BRUIJN.md`](https://github.com/aallan/vera/blob/main/DE_BRUIJN.md) §6.5 for the one case where the compiler falls back to the spelling instead.
The practical consequence is that an alias is how you give a parameter a name without reintroducing names. Two parameters of one underlying type become two stacks, so every reference is `.0` and there is no ordering to get wrong:
```vera
type Meters = Int;
type Feet = Int;
private fn excess(@Meters, @Feet -> @Int)
requires(true)
ensures(true)
effects(pure)
{
@Meters.0 - @Feet.0 / 3
}
```
`vera check --explain-slots` prints what each parameter actually bound, and spec [§3.8 and §3.8.1](https://github.com/aallan/vera/blob/main/spec/03-slot-references.md) are the formal statement.
## What actually gets verified?
There are three layers, and they cover different things.
**Layer 1: Type system (mechanical).** Every binding uses typed De Bruijn indices (`@Int.0`, `@String.1`, etc.), so the type checker can verify that every reference resolves to a binding of the correct type, every function call matches its signature, every pattern match is exhaustive, and generics monomorphise correctly. This is the "components slot together" layer. Nothing novel here beyond the index scheme; the known gaps in it, such as a case missing inside a nested constructor pattern, are listed in [KNOWN_ISSUES.md](https://github.com/aallan/vera/blob/main/KNOWN_ISSUES.md).
**Layer 2: Z3 contract verification (mechanical, bounded).** Every function has mandatory preconditions, postconditions, and effect declarations. The compiler translates these into a decidable SMT fragment and hands them to Z3. That fragment covers linear arithmetic over integers and booleans, array lengths, ADT constructor discrimination and field access (via Z3 datatype sorts), and termination measures for structural recursion. Across the example programs, the vast majority of contracts verify statically — the compiler can prove the implementation satisfies the spec without running the code. The remainder are contracts outside that fragment — nonlinear arithmetic, floating-point functions, a generic function with no concrete instantiation to verify (generic functions are verified per instantiation) — or symbolic effect state modelling across handlers. These fall back to runtime contract checking: those assertions still execute, they just aren't proven at compile time. A check code generation cannot express, such as a quantified `ensures`, is reported as a runtime check but not compiled into one.
This layer does cover actual correctness properties, not just interface compatibility. If you write `ensures(@Nat.result >= 0)` on an absolute value function, `vera verify` will prove it holds for all inputs, give you a counterexample, or — where it can do neither — compile it as a runtime check and say so.
**Layer 3: Agent documentation and human intent (expressive, unverified).** The contracts themselves are unverified with respect to user intent. Nothing in the pipeline checks whether `ensures(@Int.result >= 0)` is actually what you wanted the function to do. The contract could be a perfectly verified implementation of the wrong specification. This is where SKILL.md lives — it steers the model toward writing contracts that capture reasonable intent, but "reasonable" has no formal backing.
So: provably correct relative to stated requirements, yes, where Tier 1 proves them — the open soundness bugs in [KNOWN_ISSUES.md](https://github.com/aallan/vera/blob/main/KNOWN_ISSUES.md) are the known exceptions, and the compiled program checks its contracts at run time, so a wrong proof traps rather than returning a wrong answer (a contract code generation cannot express, such as a quantified `ensures`, is not compiled into a check). Provably correct relative to unstated intent, no — but the auditable surface is deliberately as small as possible. The human reviews contracts, not implementations.
## Is SQL injection really a compile-time error?
Yes. 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 argument of `DB.query` / `DB.execute` must have **literal provenance**. It can be a string literal, or a `string_concat`, an interpolation, or a `let` chain — but every part of that chain has to trace back to a literal. A query built from a parameter, a call result, or a `\(expr)` interpolation of one is rejected at compile time with `E207`. Data from outside the program reaches the database only through the `?` placeholders and the params array:
```vera
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)])
}
```
Swap the placeholder for `string_concat("SELECT ... WHERE name = '", @String.0)` and the program does not compile.
It is not a lint, so there is no configuration to get right and no suppression comment to add. It is not a scanner run over a build, so it cannot be skipped or fall behind the code. And it is not a solver result, so it does not weaken where the solver does: Vera's contract verification has tiers and can fall back to runtime checks, but this check has neither. It asks one question about where a string came from, answers it in the type checker, and gives the same answer inside handled code and generic code as anywhere else.
Two smaller errors sit alongside it. A `?`-placeholder/parameter count mismatch is `E208` when the params array's length is statically known — written out at the call site, or reached through a `let` — while anything else defers that arity check to the driver — and numbered or named placeholder styles are rejected in favour of the single positional form (`E209`).
The guarantee is exactly as wide as the query path, and no wider. Every string that reaches the database goes through `DB.query` / `DB.execute`, and the language has no other string-to-SQL route, so there is no back door to leave open. What it does not catch is a fixed query that is simply wrong: a literal `DELETE FROM users` compiles happily, because nothing in it came from outside. And the effect is SQLite-only, and a `handle[DB]` is refused at check (`E340`), so a test cannot mock it.
## Does the compiler prove division-by-zero, out-of-bounds indexing, etc. can't happen?
Where the solver can decide the operation, yes; where it cannot, a runtime guard catches it. The verifier auto-synthesises a proof obligation at every primitive operation whose well-definedness depends on operand values, and discharges it from the surrounding preconditions and path conditions. **Integer** division and modulo by zero carry a `b != 0` obligation (E526) — float division is exempt, since `f64.div` by zero yields inf or NaN rather than trapping; array indexing carries a `0 <= i < array_length(arr)` obligation (E527); `@Nat` subtraction underflow and `@Int` → `@Nat` narrowing carry `>=` / `>= 0` obligations (E502 / E503). A function that declares `requires(@Int.1 != 0)` and performs `@Int.0 / @Int.1` is statically proven free of a zero divisor (`INT_MIN / -1` has no obligation and traps at run time); a function that declares `requires(true)` and performs `@Int.1 / @Int.0` is refused by `vera verify` (E526), not left to a runtime trap. (An operation inside a closure body, quantifier predicate, or handler clause is walked under a fresh slot scope: a slot-dependent obligation is reported as a Tier-3 entry — runtime-guarded at the codegen-guarded sites, while the few unguarded sites carry no codegen guard and say so in the stream as `tier3_unguarded` warnings (`E504`, `E506`) — while a manifest violation like `5 / 0` is the same loud compile error as direct position. A quantifier domain and a handler's state-init and body are enclosing-scope positions and prove at full precision.)
You discharge an obligation by encoding the constraint in a precondition (`requires(...)`), a guarding `if` (whose path condition holds in the relevant branch), or a refinement type (`{ @Int | @Int.0 != 0 }`) — the verifier then proves it at every call site. Integer division and modulo are decidable, so an unguarded divisor the solver can show may be zero is a compile error (E526); a divisor the solver can't translate — opaque, like a value behind an uninterpreted call — falls to a Tier-3 runtime guard instead, the same way array bounds do. Array bounds depend on `array_length`, which the solver treats as opaque, so they are proven at Tier 1 only where a literal length, refinement, precondition, or path condition pins it — and a provably out-of-range index (e.g. `[1, 2, 3][5]`) is a compile error (E527).
Where a bound can't be proved at Tier 1 — a dynamic array index whose length the solver can't pin, or an index inside a closure body — it falls to a runtime-guarded **Tier 3** rather than a static proof, and that fallback is honest, not silent: `vera verify --json` counts it. Those traps are Vera-native — each carries a kind label (`divide_by_zero`, `index_out_of_bounds`), a per-kind `Fix:` paragraph naming the precondition that would lift it to a static proof, and a source backtrace.
Lifting dynamic or closure-captured array bounds from a runtime-guarded Tier 3 to a Tier-1 proof is part of the Tier 2 verification work ([#427](https://github.com/aallan/vera/issues/427)).
## How can we verify if the written code is safe and follows compliance?
Every function in Vera must declare what it requires, what it guarantees, and what side effects it performs. The compiler proves the implementation satisfies those contracts via Z3 — it verifies statically, gives you a counterexample, or (where it can do neither) compiles a runtime check and says so. So a compliance reviewer can audit the contracts (which are small and declarative) without reading the implementation, and the compiler proves the code matches them.
The effect system adds another dimension: a function that declares `effects(pure)` is proven to have no side effects. A function that declares `effects(<IO>)` can only perform IO operations. A caller that only permits `<Http>` cannot invoke a function that also performs `<IO>`. This makes it possible to enforce security boundaries at the type level — a sandboxed module literally cannot perform operations outside its declared effect set.
## What are abilities?
Abilities are Vera's mechanism for constrained generics — type constraints that restrict what types a generic function can accept. They're inspired by Roc's ability system and serve a similar role to Haskell's type classes or Rust's traits, but with a fixed set of built-in abilities rather than user-defined ones.
Vera has four built-in abilities:
- **`Eq<T>`** — equality comparison via `eq(a, b)`, satisfied by all primitive types and ADTs whose fields are themselves `Eq`
- **`Ord<T>`** — ordering via `compare(a, b)`, which returns the built-in `Ordering` ADT (`Less`, `Equal`, `Greater`), satisfied by `Int`, `Nat`, `Bool`, `Float64`, `String`, and `Byte`
- **`Hash<T>`** — hashing via `hash(x)`, which returns an `Int`, satisfied by `Int`, `Nat`, `Bool`, `Float64`, `String`, and `Byte`
- **`Show<T>`** — string conversion via `show(x)`, satisfied by `Int`, `Nat`, `Bool`, `Float64`, `String`, and `Byte`
You use them in generic signatures with `where` clauses:
```vera
public forall<T where Eq<T>> fn contains(@Array<T>, @T -> @Bool)
requires(true)
ensures(true)
effects(pure)
{
...
}
```
The compiler checks at every call site that the concrete type satisfies the required ability. ADTs can auto-derive `Eq` if all their constructor fields are themselves `Eq`-satisfying types — simple enums satisfy `Eq` automatically.
The design choice to fix the ability set (rather than allowing user-defined abilities) is deliberate: it keeps the language simpler for models and avoids the coherence problems that plague open type class systems. The grammar still parses an `ability` declaration, and a program that calls a user-declared ability's operation passes `vera check` but does not compile.
## How does HTTP work in Vera?
HTTP is modelled as a built-in algebraic effect. `Http.get(url)` and `Http.post(url, body)` are effect operations that return `Result<String, String>`. Functions that use them must declare `effects(<Http>)` in their signature, making network access explicit and trackable in the type system.
The effect system means a caller that only permits `<IO>` cannot invoke a function that performs `<Http>` — network access is a separate capability. User handlers for `Http` are not compiled: a `handle[Http]` is refused at check (`E340`), so a test cannot mock the network. The pattern for fetching and parsing JSON from an API is: call `Http.get`, then `json_parse` the response body.
HTTP supports GET and POST. Custom headers, additional HTTP methods, response status codes, timeouts, and streaming are not supported.
## Can I run Vera programs in the browser?
Yes. `vera compile --target browser` produces a self-contained directory with a `.wasm` binary, a JavaScript runtime (`runtime.mjs`), and an `index.html`:
```bash
vera compile --target browser examples/hello_world.vera
# produces examples/hello_world_browser/
# module.wasm
# runtime.mjs
# index.html
```
Serve it with any HTTP server and open `index.html` — no build step, no bundler, no dependencies. The JavaScript runtime provides browser-appropriate implementations of the host bindings the browser target supports — the ones a page can host, which leaves a filesystem, an accept loop, a database and a model provider outside it by construction (spec §12.9.3 lists each and why): `IO.print` writes to the page, `IO.read_line` uses `prompt()`, and State, contracts, JSON serialization and Markdown rendering work identically to the wasmtime runtime. `json_stringify` and `md_render` reach that identity by emitting a canonical form the specification states — §9.7.1 and §9.7.3 — rather than by the two hosts happening to agree, which is what the parity suite checks them against. `json_parse` reaches it from the other side, by accepted domain rather than by output form: §9.7.1 states what it takes — RFC 8259-valid text that decodes to finite numbers and strings of Unicode scalar values — so the JavaScript constants (`NaN`, `Infinity`, `-Infinity`) and a lone-surrogate escape are `Err` at the parse on both hosts, with one message, and every text inside the domain parses identically. `md_parse` reaches it a third way again, by grammar: §9.7.3 states the character classes the patterns are written in, the order the block constructs claim a line, the fixed width a list continuation loses and the maximal-run rule for inline text, and both runtimes read one shared table of those patterns rather than each carrying its own spelling. `IO.read_char` is not supported in the browser target, and unlike the boundaries above it is an implementation gap: a page could host it, but it needs the JSPI suspend/resume primitive, so the stub returns an explanatory `Err` reading `IO.read_char not yet supported in browser target`.
Two effects are refused outright rather than merely differing. `Inference` and `DB` return an explanatory `Err` from every operation in the browser, because the API key or database credential they would need is readable from page source and network traffic in client-side JavaScript. Reach them through a server-side endpoint and call it with `Http`, which does run in the browser — it is backed by `XMLHttpRequest`, not a stub. That refusal is a deliberate platform boundary; spec §9.5.5 states it for `Inference`.
The runtime also works in Node.js:
```bash
node --experimental-wasm-exnref vera/browser/harness.mjs module.wasm
```
Mandatory parity tests enforce that on every PR. For the two operations that carry a canonical form, each case asserts the expected string as well as cross-host equality, since two hosts agreeing on a wrong answer would satisfy equality on its own; for the two parsers it compares what they produce — `json_parse` by accepted domain and message, `md_parse` by parsing a generated Markdown corpus on both hosts and comparing the resulting ADTs byte for byte, which is the only comparison that can see how a paragraph's plain-text runs are grouped.
## How does contract-driven testing work?
`vera test` is Vera's built-in testing command. It generates test inputs automatically from function contracts — you don't write test cases manually.
The process works in three steps:
1. **Input generation**: The compiler reads each function's `requires()` clause and uses Z3 to generate concrete values that satisfy the precondition. For example, if a function requires `@Int.1 != 0`, Z3 produces pairs of integers where the first is non-zero — `@Int.1` is the leftmost parameter, since De Bruijn indices count back from the most recent binding. It generates up to 100 trials per function by default (configurable with `--trials`). Whether a parameter can be generated for is decided on its *resolved* type, not its spelling, so an alias of a generatable type (`type Cnt = Int;`) is trialled rather than skipped, and an alias-spelled precondition still constrains the inputs. "Satisfy the precondition" is exact rather than best-effort, for the functions that reach trials at all: among the Tier-3 targets, if any conjunct — or any refined parameter's predicate — falls outside the SMT layer's decidable fragment, Z3 cannot constrain the inputs by it, so the function is *skipped* with the blocking conjunct named instead of being exercised on inputs its own guard would reject. A function the verifier proved at Tier 1 is reported `VERIFIED` and never trialled, so the question does not arise for it — unless `vera test --distrust` runs it too, and then a proved function whose precondition the generator cannot honour is reported `VERIFIED` and not exercised, never run on inputs its precondition does not admit.
2. **Execution**: Each generated input is compiled to WASM and executed via wasmtime. The function runs with real values, not symbolic ones.
3. **Contract checking**: The `ensures()` postcondition is checked against the actual output. If any trial produces a result that violates the postcondition, the test fails with the concrete input that triggered it.
```bash
vera test examples/safe_divide.vera # test all functions
vera test --trials 50 examples/safe_divide.vera # limit trials
vera test --json examples/safe_divide.vera # JSON output for agents
vera test --distrust examples/safe_divide.vera # run the proved functions too
```
`--distrust` runs the proved functions too. Code generation emits a contract's runtime check whatever its tier, wherever it can express one, so a proved function's checks are in the module the trials run. A failing trial is a **refuted** proof when every check of its trap's kind, in the function the trap fired in, stands for an obligation the verifier proved. It is reported as an `E703` error naming the obligation and the arguments, and any `assume` the proof rests on. When those checks mix proved and unproved obligations, or one has no obligation on record, the trial is reported `unattributed` instead. On the trial's own call, the function's `requires` checks and refined-parameter guards are left out, because the arguments were generated to satisfy them; a trap with nothing else to blame is `unattributed`.
This combines the best of property-based testing (generated inputs, no manual cases) with the best of formal verification (inputs derived from specifications, not random). The contracts serve double duty: they're both the specification the compiler proves and the test oracle that validates runtime behaviour.
## What are the intended applications? Who are the end users?
The reference compiler targets WebAssembly, so the initial applications are web-based. The `.wasm` binary runs at the command line via wasmtime or in any browser with the self-contained JavaScript runtime.
But the deeper answer is that the end users aren't humans directly — they're AI coding agents. The intended workflow is: a human (or an orchestrating agent) describes what they want; a model generates Vera code; the compiler verifies it; the WASM binary runs. The human's job is to review contracts, not implementations.
HTTP, JSON, and Markdown are built-in, which supports the primary agent workloads: API integration, data processing, and structured document generation. A Vera program can make an HTTP request, parse the JSON response, and return typed, contract-checked data — all with the network I/O declared as an algebraic effect (`effects(<Http>)`). A research function that fetches data from the web, processes results via LLM inference, and returns typed, contract-checked Markdown output is the kind of program Vera is designed for.
## Is there evidence this actually works?
Vera-specific benchmark data is available across multiple models. **[VeraBench](https://github.com/aallan/vera-bench)** — a 60-problem benchmark across 5 difficulty tiers — covers 9 models across 3 providers (VeraBench v0.0.18, measured on Vera v0.1.8). The headline result: six of the nine write 100% correct Vera, a language none of them was trained on. Vera has the highest score, or level with it, for six of the nine models. The metric is **% solved** (pass@1): a refusal, a compile failure, a crash and a wrong answer all count alike as not solved, so a model cannot score higher by answering less.
The sharpest evidence that the design choices are doing the work is Vera against [Aver](https://averlang.dev), a second language that is also absent from every training set and also learned from a single document in the prompt — so familiarity cannot explain a difference between them. What separates them is that Aver has ordinary variable names where Vera has typed slot references. Vera scores higher on all five models that ran both. The two languages differ in more than one respect, so this isolates the variable better than the Python comparison without isolating it completely.
These caveats matter: single run per model, no pass@k. v0.0.18 is the first sweep in which all 60 problems are graded, so one problem is worth 1.7 percentage points — which narrows the increment but does not remove the caveat, since most of the gaps are still one or two problems wide. Stable rates will require pass@k evaluation with multiple trials — see the [full report](https://github.com/aallan/vera-bench) for details.
The broader literature is also encouraging. The type-constrained decoding paper (Mündler, He, Wang et al., "Type-Constrained Code Generation with Language Models", PLDI 2025, [ACM DL](https://dl.acm.org/doi/10.1145/3729274)) found that enforcing type constraints during LLM code generation cut compilation errors by more than half and improved functional correctness by 3.5–4.5%. Syntax constraints alone provided limited improvement — it was the *type* constraints that made the difference. The same paper found that 94% of LLM-generated compilation errors are type-check failures — exactly the class of error that a strong static type system catches at compile time.
The Vericoding benchmark (Sun et al., "A Benchmark for Vericoding", [arXiv:2509.22908](https://arxiv.org/abs/2509.22908)) shows LLMs achieving 82% verification success on Dafny versus 27% on Lean, which suggests SMT-automated verification (Vera's approach) is significantly more LLM-tractable than explicit proof construction.
Blinn et al. ("Statically Contextualizing Large Language Models with Typed Holes", OOPSLA 2024, [ACM DL](https://doi.org/10.1145/3689728)) demonstrated that providing type context at incomplete program locations significantly improves LLM completion quality — a result that directly motivates Vera's typed holes: a `?` in any expression position type-checks with a `W001` warning naming the expected type and the bindings in scope.
None of this is Vera-specific, but it validates the design choices. The thesis is plausible, the tooling exists, and initial Vera-specific results are consistent with the broader literature. What's needed is expanded and replicated evaluations — more models, more tiers, and longitudinal tracking across releases — to confirm these findings across languages and settings.
## What about the training data problem? LLMs have never seen Vera code.
This is a real concern. LLMs are trained on trillions of tokens of Python, TypeScript, and JavaScript. A MojoBench study (NAACL 2025) found that even fine-tuned models achieved only 30–35% improvement over base models on Mojo code generation, illustrating the cold-start problem for new languages.
Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) goes into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular (fewer constructs, each with one preferred surface spelling `vera fmt` produces deterministically), which reduces the surface area a model needs to learn. Third, the conformance test suite (programs named by spec chapter and feature) gives models concrete examples to learn from and conform to. Simon Willison's December 2025 JustHTML write-up illustrates the same point in practice: an LLM-assisted implementation, guided by the html5lib conformance suite, conformed to the HTML parsing spec by running against its tests, and a comprehensive test suite is a strong scaffold for a model implementing to a specification.
## How does Vera compare to Dafny / Lean / Koka / F*?
**Dafny** shares Vera's Z3/SMT verification approach and is used in production at AWS (Cedar authorisation). But it's imperative, lacks algebraic effects, and has optional (not mandatory) annotations. The 2025 paper proposing Dafny as a verification intermediate language for LLM-generated code validates Vera's core thesis — but Dafny wasn't purpose-built for it.
**Lean 4** has the richest LLM integration ecosystem (LeanDojo, Lean Copilot) and significant investment. But it's primarily a theorem prover with monadic effects. LLMs achieve only 27% success rate on Lean versus 82% on Dafny, suggesting explicit proof construction is harder for models than SMT-automated verification.
**Koka** pioneered the row-polymorphic algebraic effect type system that Vera draws from. But it has no verification, no contracts, and isn't production-ready.
**F*** combines refinement types, algebraic effects, and SMT-based verification. It's the closest to Vera's feature set, but targets human programmers, not models. It also has a steep learning curve.
No production language today combines mandatory contracts, algebraic effects, refinement types, constrained generics with built-in abilities, De Bruijn indices, Z3 verification, and WebAssembly compilation into a single design optimised for LLM code generation.
## Why WebAssembly?
Three reasons. First, portability — the same `.wasm` module runs at the command line and in the browser, which is what the browser-parity suite asserts by running identical module bytes under both hosts; `--target wasi-p2` emits a WASI 0.2 component from that same source. Second, sandboxing — WebAssembly has no ambient capabilities, so a Vera program cannot do anything its effect declarations don't permit. Third, the WASM Component Model (W3C, production-ready in Wasmtime) will enable Vera components to interoperate with Rust, Go, and Python components via WIT interfaces, providing ecosystem access without requiring a massive native package system.
## Why Python for the compiler?
Correctness over performance. The reference compiler is a specification-faithful implementation, not a production compiler. Python makes the compiler readable, testable, and easy to modify during rapid language evolution. The seven-stage pipeline (parse → transform → resolve → typecheck → verify → compile → execute) is independently testable at each stage.
If Vera reaches the point where compiler performance matters, a production compiler in Rust or OCaml would be a separate project. The Python reference compiler would remain as the specification oracle.
## Why are contracts mandatory?
Because the whole point is that code should be checkable. If contracts are optional, models won't write them — and then you're back to unverifiable code. Making contracts mandatory means every function is a specification that the compiler can verify against its implementation. The model doesn't need to be right; it needs to be checkable.
This is a deliberate trade-off. Mandatory contracts add friction. But the friction is the feature — it forces the model (and any human) to state what the function requires, what it guarantees, and what effects it performs. That statement is the auditable surface.
## What does the project status look like?
The reference compiler is under active development. The current release includes:
- A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute
- A formal specification, a chapter per part of the language ([`spec/`](https://github.com/aallan/vera/blob/main/spec/))
- A test suite with conformance programs named by spec chapter and feature, counted in [TESTING.md](https://github.com/aallan/vera/blob/main/TESTING.md#overview)
- Working example programs ([`examples/`](https://github.com/aallan/vera/blob/main/examples/))
- Built-in functions covering strings, arrays, math, parsing, and data types, as `vera builtins` lists them
- Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation
- Full IO operations (print, read_line, read_char, read_file, write_file, read_bytes, write_bytes, args, exit, get_env, sleep, time, stderr)
- Algebraic data types, pattern matching, closures, generics with monomorphisation
- Algebraic effect handlers with resume and state (compiled for `State` and `Exn` only)
- Built-in `<Http>`, `<HttpServer>`, `<Inference>`, `<DB>`, `<State>`, `<IO>`, `<Async>`, `<Random>`, `<Diverge>`, and `Exn<T>` (typed exception) effects
- `<Inference>` dispatches to Anthropic, OpenAI, Kimi (Moonshot), Mistral, Grok (xAI), or DeepSeek via env vars
- Collection types: `Map<K,V>`, `Set<T>`, `Array<T>`, `Decimal`, `Json`, `HtmlNode`, `Markdown`
- String interpolation with auto-conversion for primitive types
- Cross-module imports with contract verification at call sites
- Contract-driven testing via Z3 and WASM
- A canonical code formatter
- WebAssembly compilation and execution via wasmtime
- Browser runtime with mandatory parity tests
The language is under active development. See the [Roadmap](https://github.com/aallan/vera/blob/main/ROADMAP.md) and [Changelog](https://github.com/aallan/vera/blob/main/CHANGELOG.md) for current status and planned features.
## How do I try it?
Clone the repository — the checkout carries the bundled examples this command runs, plus the conformance suite and specification (a PyPI install ships the toolchain only):
```bash
git clone https://github.com/aallan/vera.git && cd vera
python -m venv .venv && source .venv/bin/activate
python -m pip install -e .
vera run examples/hello_world.vera
```
If you only need the `vera` command — no examples, spec, or conformance programs — install the released distribution from PyPI:
```bash
python -m venv .venv && source .venv/bin/activate
python -m pip install veralang
vera version
```
For agents, point your model at [SKILL.md](https://raw.githubusercontent.com/aallan/vera/main/SKILL.md). It's the complete language reference, written for a model's context window. For driving the command-line toolchain itself — checking, verifying, testing, running, and debugging Vera, plus the `builtins`/`effects`/`errors` introspection commands — see the CLI cookbook, [TOOLCHAIN.md](https://github.com/aallan/vera/blob/main/TOOLCHAIN.md).
## References
- Wang et al., "How Does Naming Affect LLMs on Code Analysis Tasks?", [arXiv:2307.12488](https://arxiv.org/abs/2307.12488)
- Le et al., "When Names Disappear: Revealing What LLMs Actually Understand About Code", [arXiv:2510.03178](https://arxiv.org/abs/2510.03178)
- Mündler, He, Wang et al., "Type-Constrained Code Generation with Language Models", PLDI 2025, [ACM DL](https://dl.acm.org/doi/10.1145/3729274)
- Blinn et al., "Statically Contextualizing Large Language Models with Typed Holes", OOPSLA 2024, [ACM DL](https://doi.org/10.1145/3689728)
- Sun et al., "A Benchmark for Vericoding: Formally Verified Program Synthesis", [arXiv:2509.22908](https://arxiv.org/abs/2509.22908)
- Allan, "VeraBench: a benchmark for LLM code generation in Vera", [github.com/aallan/vera-bench](https://github.com/aallan/vera-bench)
========================================================================
# Error Codes (vera/errors.py)
========================================================================
## Error Code Reference
Diagnostics carry stable codes, grouped by compiler phase; the list after the table is the registry itself, read from vera/errors.py:
| Range | Phase |
|-------|-------|
| E001-E009 | Parse errors |
| E010 | Transform errors |
| E011-E013 | Import resolution |
| E020-E023 | Parse: malformed comments (lexical) |
| E030-E032 | Parse: contract clauses |
| E040 | Transform: pipe operand |
| E1xx | Type check: core + expressions |
| E2xx | Type check: calls |
| E3xx | Type check: control flow |
| E5xx | Verification |
| E6xx | Code generation |
| E7xx | Testing |
| W0xx | Warnings |
- **W001**: Typed hole
- **W003**: Unverified assumption (assume statement)
- **W002**: Async argument evaluates eagerly
- **W004**: Emitted runtime check not matched by an obligation record
- **E001**: Missing contract block
- **E002**: Missing effect clause
- **E003**: Malformed slot reference
- **E004**: Missing closing brace
- **E005**: Unexpected token
- **E006**: Unexpected character
- **E007**: Internal parser error
- **E008**: Module-qualified call uses dot instead of ::
- **E009**: Invalid string escape sequence
- **E010**: Unhandled grammar rule
- **E011**: Circular import detected
- **E012**: Cannot resolve import (no file found)
- **E013**: Error parsing imported module
- **E020**: Unterminated block comment
- **E021**: Unterminated annotation comment
- **E023**: Annotation comments do not nest
- **E030**: old() argument is not an effect reference
- **E031**: new() argument is not an effect reference
- **E032**: Contract clause after the effects clause
- **E040**: Pipe's right operand is not a call
- **E120**: Data invariant not Bool
- **E121**: Function body type mismatch
- **E122**: Pure function performs effects
- **E123**: Precondition predicate not Bool
- **E124**: Postcondition predicate not Bool
- **E125**: Call-site effect mismatch
- **E126**: Refinement predicate not Bool
- **E127**: Decreases measure not well-founded
- **E128**: Quantifier bound not an integer
- **E129**: Non-regular recursion in a data declaration
- **E130**: Unresolved slot reference
- **E131**: Result ref outside ensures
- **E132**: Cyclic type alias
- **E133**: Type alias arity mismatch
- **E134**: Type does not take type arguments
- **E135**: Array/Map/Set with a zero-size element, key, or value type
- **E136**: Unknown type name
- **E137**: Recursive function declares neither decreases nor Diverge
- **E138**: Contract calls back into its own function
- **E140**: Arithmetic requires numeric operands
- **E141**: Arithmetic requires matching numeric types
- **E142**: Cannot compare incompatible types
- **E143**: Ordering requires orderable operands
- **E144**: Logical operand not Bool (left)
- **E145**: Logical operand not Bool (right)
- **E146**: Unary not requires Bool
- **E147**: Unary negate requires numeric
- **E148**: Non-convertible type in string interpolation
- **E149**: Integer literal out of range for its target type
- **E150**: Cannot import private declaration
- **E151**: Function redefines a built-in
- **E152**: Effect redeclares a built-in effect
- **E153**: Function name is reserved
- **E154**: Name is reserved for the prelude
- **E155**: Bare function name supplied by two imports
- **E156**: Bare data type name supplied by two imports
- **E157**: Bare constructor name supplied by two imports
- **E158**: Declaration takes a reserved built-in type name
- **E159**: Two data declarations share a constructor name
- **E160**: Array index must be Int or Nat
- **E161**: Cannot index non-array type
- **E162**: Array literal element type mismatch
- **E163**: Result reference does not name the return type
- **E170**: Let binding type mismatch
- **E171**: Anonymous function body type mismatch
- **E172**: Assert requires Bool
- **E173**: Assume requires Bool
- **E174**: old() outside ensures
- **E175**: new() outside ensures
- **E176**: Unknown expression type
- **E177**: old()/new() names an effect the row does not declare
- **E178**: Bare call to a where-helper from outside its parent
- **E179**: Quantifier predicate is not a function of the index to Bool
- **E180**: Unknown ability in constraint
- **E181**: Constraint references undeclared type variable
- **E182**: Slot reference to a zero-size type
- **E183**: Let binding of a zero-size type
- **E184**: Name declared twice in one namespace
- **E185**: Declaration takes a built-in ability's name or operation
- **E186**: Quantifier index type is not Int or Nat
- **E200**: Unresolved function
- **E201**: Wrong argument count
- **E202**: Argument type mismatch
- **E203**: Effect operation wrong argument count
- **E204**: Effect operation argument type mismatch
- **E205**: Conflicting type argument inference
- **E206**: Generic type parameter instantiated at Unit
- **E207**: Non-literal SQL argument
- **E208**: SQL placeholder count mismatch
- **E209**: Unsupported SQL placeholder syntax
- **E210**: Unknown constructor
- **E211**: Constructor is nullary
- **E212**: Constructor wrong field count
- **E213**: Constructor field type mismatch
- **E214**: Unknown nullary constructor
- **E215**: Constructor requires arguments
- **E216**: Empty tuple type
- **E217**: Bare effect operation must be qualified or handled
- **E220**: Unresolved qualified call
- **E230**: Module not found
- **E231**: Function not imported from module
- **E232**: Function is private in module
- **E233**: Function not found in module
- **E240**: Ability operation wrong argument count
- **E241**: Ability operation argument type mismatch
- **E242**: Ord ability operation on non-orderable type
- **E243**: Eq ability operation on non-Eq-derivable type
- **E300**: If condition not Bool
- **E301**: If branches incompatible types
- **E302**: Match arm type mismatch
- **E310**: Unreachable match arm
- **E311**: Non-exhaustive match (ADT)
- **E312**: Non-exhaustive match (Bool)
- **E313**: Non-exhaustive match (infinite type)
- **E314**: Pattern cannot match the scrutinee's type
- **E320**: Unknown constructor in pattern
- **E321**: Pattern constructor wrong arity
- **E322**: Unknown nullary constructor in pattern
- **E323**: Empty tuple pattern
- **E330**: Unknown effect in handler
- **E331**: Handler state type mismatch
- **E332**: Effect has no such operation
- **E333**: Handler with-state but no state declaration
- **E334**: State update type name mismatch
- **E335**: State update expression type mismatch
- **E336**: Handler state diverges from the State<T> cell type
- **E337**: Builtin effect handler type-argument arity
- **E338**: Unknown effect in an effect row
- **E339**: Handler-clause State operation code generation cannot lower
- **E340**: Code generation cannot lower this construct
- **E500**: Postcondition verified false
- **E501**: Call-site precondition violation
- **E502**: @Nat subtraction underflow obligation not discharged
- **E503**: @Nat binding-site narrowing may be negative
- **E504**: @Nat narrowing unverified and not runtime-guarded
- **E505**: Refinement predicate may be violated at narrowing site
- **E506**: Refinement narrowing not statically verified (Tier-3)
- **E507**: Assertion verified false
- **E520**: Cannot verify contract (generic function with no concrete instantiation)
- **E521**: Cannot verify precondition (undecidable)
- **E522**: Cannot verify postcondition (body undecidable)
- **E523**: Cannot verify postcondition (expression undecidable)
- **E524**: Cannot verify postcondition (timeout)
- **E525**: Cannot verify termination metric
- **E526**: Division or modulo by zero
- **E527**: Array index out of bounds
- **E528**: Arithmetic overflow
- **E529**: Float-to-integer truncation domain (NaN, infinity, or out of i64 range)
- **E532**: Cannot verify call-site precondition (undecidable)
- **E535**: Cannot statically verify assertion (runtime-checked)
- **E534**: Contract holds only from a disclosed fact
- **E533**: Instantiated handler state diverges from the State<T> cell type
- **E538**: Premise set unsatisfiable (no call can reach the body)
- **E539**: Premise set contradictory beyond the author's premises
- **E540**: Premise satisfiability not established (Tier 1 withheld)
- **E541**: Runtime-check claim not matched by an emitted check
- **E600**: Unsupported parameter type
- **E601**: Unsupported return type
- **E602**: Unsupported body expression type
- **E604**: Unsupported state effect type
- **E605**: Unsupported state type parameter
- **E607**: State with unsupported operations
- **E608**: Name collision: function
- **E609**: Name collision: ADT type
- **E610**: Name collision: constructor
- **E612**: Exn with unsupported type
- **E613**: Type does not satisfy ability constraint
- **E614**: Program contains typed holes
- **E615**: Cannot interpolate value of unknown type
- **E616**: Cannot infer closure return type for call_indirect
- **E617**: Refinement predicate not compilable to runtime guard
- **E618**: Nested refinement base unsupported
- **E619**: Cannot infer type argument for ability-constrained parameter
- **E620**: Function dropped: skipped callee or no function table
- **E621**: Name collision: module ADT contends with a prelude data type
- **E622**: Cannot infer a generic call's type argument
- **E623**: Name collision: entry-file ADT contends with a module data type
- **E699**: Internal compiler error
- **E700**: Contract violation during testing
- **E701**: Cannot generate test inputs
- **E702**: Test execution error
- **E703**: Tier 1 proof refuted by a test run
========================================================================
# Grammar (vera/grammar.lark)
========================================================================
## Formal Grammar (Lark LALR(1))
```lark
// Vera Language Grammar
// Lark LALR(1) parser — translated from spec/10-grammar.md
//
// Conventions:
// - String literals ("fn", "let", etc.) for keywords and operators
// - Named terminals (UPPER_CASE) for identifiers and literals
// - ?rule prefix = inline single-child nodes (cleaner parse trees)
// =====================================================================
// Program Structure
// =====================================================================
start: module_decl? import_decl* top_level_decl*
module_decl: "module" module_path ";"
module_path: LOWER_IDENT ("." LOWER_IDENT)*
import_decl: "import" module_path import_list? ";"
import_list: "(" import_name ("," import_name)* ")"
import_name: LOWER_IDENT | UPPER_IDENT
top_level_decl: visibility? fn_decl -> fn_top_level
| visibility? data_decl -> data_top_level
| type_alias_decl
| effect_decl
| ability_decl
visibility: "public" | "private"
// =====================================================================
// Function Declarations
// =====================================================================
fn_decl: forall_clause? "fn" LOWER_IDENT fn_signature contract_block effect_clause fn_body where_block?
forall_clause: "forall" "<" type_var_list ">"
| "forall" "<" type_var_list "where" ability_constraint_list ">"
type_var_list: UPPER_IDENT ("," UPPER_IDENT)*
// Function signatures use @Type for params and return (binding sites)
fn_signature: "(" fn_params? "->" "@" type_expr ")"
fn_params: "@" type_expr ("," "@" type_expr)*
// Plain type lists (no @) for type-level signatures: fn_type, op_decl
param_types: type_expr ("," type_expr)*
contract_block: contract_clause+
?contract_clause: requires_clause
| ensures_clause
| decreases_clause
requires_clause: "requires" "(" expr ")"
ensures_clause: "ensures" "(" expr ")"
decreases_clause: "decreases" "(" expr ("," expr)* ")"
effect_clause: "effects" "(" effect_row ")"
?effect_row: pure_effect
| effect_set
pure_effect: "pure"
effect_set: "<" effect_list ">"
effect_list: effect_ref ("," effect_ref)*
effect_ref: UPPER_IDENT type_args?
| UPPER_IDENT "." UPPER_IDENT type_args? -> qualified_effect_ref
fn_body: "{" block_contents "}"
where_block: "where" "{" fn_decl+ "}"
// =====================================================================
// Data Type Declarations
// =====================================================================
data_decl: "data" UPPER_IDENT type_params? invariant_clause? "{" constructor_list "}"
type_params: "<" type_var_list ">"
invariant_clause: "invariant" "(" expr ")"
constructor_list: constructor ("," constructor)*
constructor: UPPER_IDENT "(" type_expr ("," type_expr)* ")" -> fields_constructor
| UPPER_IDENT -> nullary_constructor
// =====================================================================
// Type Aliases
// =====================================================================
type_alias_decl: "type" UPPER_IDENT type_params? "=" type_expr ";"
// =====================================================================
// Effect Declarations
// =====================================================================
effect_decl: "effect" UPPER_IDENT type_params? "{" op_decl+ "}"
op_decl: "op" LOWER_IDENT "(" param_types? "->" type_expr ")" ";"
// =====================================================================
// Ability Declarations
// =====================================================================
ability_decl: "ability" UPPER_IDENT type_params? "{" op_decl+ "}"
ability_constraint_list: ability_constraint ("," ability_constraint)*
ability_constraint: UPPER_IDENT "<" UPPER_IDENT ">"
// =====================================================================
// Type Expressions
// =====================================================================
type_expr: UPPER_IDENT type_args? -> named_type
| fn_type
| refinement_type
type_args: "<" type_expr ("," type_expr)* ">"
fn_type: "fn" "(" param_types? "->" type_expr ")" effect_clause
refinement_type: "{" "@" type_expr "|" expr "}"
// =====================================================================
// Expressions — precedence climbing, loosest to tightest
//
// 1 |> left pipe_expr
// 1.5 ==> right implies_expr
// 2 || left or_expr
// 3 && left and_expr
// 4 == != none eq_expr
// 5 comparisons cmp_expr
// 6 + - left add_expr
// 7 * / % left mul_expr
// 9 ! - prefix unary_expr
// 10 [] call postfix_expr
// =====================================================================
?expr: pipe_expr
?pipe_expr: implies_expr
| pipe_expr "|>" implies_expr -> pipe
// right-associative: a ==> b ==> c parses as a ==> (b ==> c)
?implies_expr: or_expr
| or_expr "==>" implies_expr -> implies
?or_expr: and_expr
| or_expr "||" and_expr -> or_op
?and_expr: eq_expr
| and_expr "&&" eq_expr -> and_op
// non-associative: a == b == c is a parse error
?eq_expr: cmp_expr
| cmp_expr "==" cmp_expr -> eq_op
| cmp_expr "!=" cmp_expr -> neq_op
// non-associative
?cmp_expr: add_expr
| add_expr "<" add_expr -> lt_op
| add_expr ">" add_expr -> gt_op
| add_expr "<=" add_expr -> le_op
| add_expr ">=" add_expr -> ge_op
?add_expr: mul_expr
| add_expr "+" mul_expr -> add_op
| add_expr "-" mul_expr -> sub_op
?mul_expr: unary_expr
| mul_expr "*" unary_expr -> mul_op
| mul_expr "/" unary_expr -> div_op
| mul_expr "%" unary_expr -> mod_op
?unary_expr: "!" unary_expr -> not_op
| "-" unary_expr -> neg_op
| postfix_expr
?postfix_expr: primary_expr
| postfix_expr "[" expr "]" -> index_op
?primary_expr: INT_LIT -> int_lit
| FLOAT_LIT -> float_lit
| STRING_LIT -> string_lit
| "true" -> true_lit
| "false" -> false_lit
| "(" ")" -> unit_lit
| "?" -> hole_expr
| slot_ref
| result_ref
| fn_call
| anonymous_fn
| if_expr
| match_expr
| block_expr
| handle_expr
| array_literal
| old_expr
| new_expr
| assert_expr
| assume_expr
| forall_expr
| exists_expr
| "(" expr ")" -> paren_expr
// =====================================================================
// Slot References
// =====================================================================
slot_ref: "@" UPPER_IDENT type_args? "." INT_LIT
result_ref: "@" UPPER_IDENT type_args? "." "result"
// =====================================================================
// Function Calls and Constructors
// =====================================================================
fn_call: LOWER_IDENT "(" arg_list? ")" -> func_call
| UPPER_IDENT "(" arg_list? ")" -> constructor_call
| UPPER_IDENT -> nullary_constructor_expr
| UPPER_IDENT "." LOWER_IDENT "(" arg_list? ")" -> qualified_call
| module_path "::" LOWER_IDENT "(" arg_list? ")" -> module_call
arg_list: expr ("," expr)*
// =====================================================================
// Anonymous Functions
// =====================================================================
anonymous_fn: "fn" "(" fn_params? "->" "@" type_expr ")" effect_clause fn_body
// =====================================================================
// Conditional Expressions
// =====================================================================
if_expr: "if" expr "then" block_expr "else" block_expr
// =====================================================================
// Match Expressions
// =====================================================================
match_expr: "match" expr "{" match_arm ("," match_arm)* "}"
match_arm: pattern "->" expr
?pattern: UPPER_IDENT "(" pattern ("," pattern)* ")" -> constructor_pattern
| UPPER_IDENT -> nullary_pattern
| "_" -> wildcard_pattern
| INT_LIT -> int_pattern
| STRING_LIT -> string_pattern
| "true" -> true_pattern
| "false" -> false_pattern
| "@" type_expr -> binding_pattern
// =====================================================================
// Block Expressions
// =====================================================================
block_expr: "{" block_contents "}"
block_contents: statement* expr
statement: let_stmt
| expr ";" -> expr_stmt
let_stmt: "let" "@" type_expr "=" expr ";"
| "let" tuple_destruct "=" expr ";" -> let_destruct
tuple_destruct: UPPER_IDENT "<" "@" type_expr ("," "@" type_expr)* ">"
// =====================================================================
// Effect Handlers
// =====================================================================
handle_expr: "handle" "[" effect_ref "]" handler_state? "{" handler_clause ("," handler_clause)* "}" "in" block_expr
handler_state: "(" "@" type_expr "=" expr ")"
handler_clause: LOWER_IDENT "(" handler_params? ")" "->" handler_body with_clause?
handler_params: "@" type_expr ("," "@" type_expr)*
// handler_body is just an expr — block_expr is already reachable via expr
?handler_body: expr
with_clause: "with" "@" type_expr "=" expr
// =====================================================================
// Array Literals
// =====================================================================
array_literal: "[" arg_list? "]"
// =====================================================================
// Contract-Only Expressions
// =====================================================================
old_expr: "old" "(" effect_ref ")"
new_expr: "new" "(" effect_ref ")"
assert_expr: "assert" "(" expr ")"
assume_expr: "assume" "(" expr ")"
forall_expr: "forall" "(" "@" type_expr "," expr "," anonymous_fn ")"
exists_expr: "exists" "(" "@" type_expr "," expr "," anonymous_fn ")"
// =====================================================================
// Terminals
// =====================================================================
// Identifiers — lower priority than keywords (Lark string literals win)
UPPER_IDENT: /[A-Z][A-Za-z0-9_]*/
LOWER_IDENT: /[a-z][A-Za-z0-9_]*/
// Numeric literals
FLOAT_LIT: /[0-9]+\.[0-9]+/
INT_LIT: /0|[1-9][0-9]*/
// String literals
STRING_LIT: /\"([^\"\\]|\\.)*\"/
// =====================================================================
// Whitespace and Comments (ignored)
// =====================================================================
%ignore /\s+/
%ignore /--[^\n]*/
// Block comments are nestable (spec 1.3) and are resolved by
// vera/lexical.py before parsing -- a regex cannot count depth.
%ignore /\/\*[^*]*\*+([^\/*][^*]*\*+)*\//
```