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/:

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. Verify the install end to end with the bundled example:

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:

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:

python -m pip install -e ".[dev]"

Platform support: README §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 for the CLI cookbook — driving the toolchain to write, verify, test, run, and debug Vera, plus the builtins/effects/errors introspection commands.

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_lengthover a non-literal is the usual trigger — Vera counts UTF-8 bytes and Z3's string theory has no byte-length operator — so compare astring_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:

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:

• 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). 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. --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:

node --experimental-wasm-exnref vera/browser/harness.mjs module.wasm

JSON diagnostics

Use --json on check or verify for machine-readable output:

{"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.

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:

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:

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:

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.

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:

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):

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 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:

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:

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

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:

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.

vera check --explain-slots your_file.vera

Output:

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:

  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) — and at the State write boundaries (#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). 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

@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:

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:

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

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)

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):

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:

type Positive = { @Int | @Int.0 > 0 };

Pattern Matching

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:

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

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:

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

public fn double(@Int -> @Int)
  requires(true) ensures(true) effects(pure)
{
  ?
}

vera check reports a W001 warning (not an error):

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:

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:

  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:

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

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.

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

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

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:

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:

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

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.

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.

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.

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.

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:

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:

-- 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:

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

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

"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

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

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

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

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

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.

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

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

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.

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

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

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

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; the convention keeps the verifier's range-checking story focused on @Nat (where only underflow can occur).

Float64 predicates

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:

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:

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:

  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 section. A contract cannot call back into its own function, directly or through other calls (E138).

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:

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

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

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:

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:

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

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:

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>]:

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>:

effects(<Async>)                 -- async computation
effects(<IO, Async>)             -- async with IO

async and await are built-in generic functions:

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:

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:

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.

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:

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.

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 for the full env-var reference.

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:

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.

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:

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

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.

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 })).

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:

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):

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:

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.

-- 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)

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

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

ability Eq<T> {
  op eq(T, T -> Bool);
}

Use where in the forall clause to constrain type parameters:

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:

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

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:

\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:

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

-- line comment

{- block comment -}

{- block comments {- can nest -} -}

Operators (by precedence, loosest to tightest)

&&, || 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:

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:

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:

private fn add(@Int, @Int -> @Int) {
  @Int.0 + @Int.1
}

CORRECT:

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:

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

CORRECT — add effects(pure) (or the appropriate effect row):

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):

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:

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

Missing index on slot reference

WRONG:

@Int + @Int

CORRECT:

@Int.0 + @Int.1

Missing decreases on recursive function

WRONG:

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:

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:

private fn greet(@String -> @Unit)
  requires(true)
  ensures(true)
  effects(pure)
{
  IO.print(@String.0);
  ()
}

CORRECT:

private fn greet(@String -> @Unit)
  requires(true)
  ensures(true)
  effects(<IO>)
{
  IO.print(@String.0);
  ()
}

Using @T.result outside ensures

WRONG:

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:

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

Non-exhaustive match

WRONG:

match @Option<Int>.0 {
  Some(@Int) -> @Int.0
}

CORRECT:

match @Option<Int>.0 {
  Some(@Int) -> @Int.0,
  None -> 0
}

Missing braces on if/else branches

WRONG:

if @Bool.0 then 1 else 0

CORRECT:

if @Bool.0 then {
  1
} else {
  0
}

Trying to use import aliasing

WRONG — Vera does not support renaming imports:

import vera.math(magnitude as math_magnitude);

CORRECT — use selective import and qualified calls for readability:

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:

import vera.math hiding(larger);

CORRECT — use selective import to list the names you need:

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:

"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:

let @Map = map_new();
let @Set = set_new();

CORRECT — nest inside an operation so types can be inferred, or provide explicit type annotation:

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:

private data Decimal {
  Cents(Int)
}

CORRECT — give the type a name of its own:

private data Money {
  Cents(Int)
}

Complete Program Examples

Pure function with postconditions

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

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

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

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.

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:

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.

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.

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) and allocating (#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/ directory of the repository: