| name | vera-language |
| description | Write programs in the Vera programming language. Use when asked to write, edit, debug, or review Vera code (.vera files). Vera is a statically typed, purely functional language with algebraic effects, mandatory contracts, and typed slot references (@T.n) instead of variable names. |
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). Install the released veralang distribution from PyPI:
python -m venv .venv && source .venv/bin/activate
python -m pip install veralang
This installs the vera command and all runtime dependencies (Lark parser, Z3 solver, wasmtime). For editor/agent integration via the Language Server Protocol, install python -m pip install "veralang[lsp]" — see LSP_SERVER.md.
The GitHub source route remains supported for unreleased changes and compiler development:
git clone https://github.com/aallan/vera.git && cd vera
python -m venv .venv && source .venv/bin/activate
python -m pip install -e .
For an editable source install with the language server, use python -m pip install -e ".[lsp]". Verify the installed CLI — works for either route, with no checkout required:
vera version
From a source checkout you can also run the bundled example end to end:
vera check examples/hello_world.vera
vera run examples/hello_world.vera
If you are working on the compiler itself, install development dependencies too:
python -m pip install -e ".[dev]"
Platform support: Vera is tested in CI on macOS 15+ (Apple Silicon), Ubuntu 24.04 LTS (x86_64), and Windows Server 2022, against Python 3.11–3.13. macOS 14 (Sonoma) and earlier, and Ubuntu 22.04 LTS aarch64, are out of scope — install will fail at dependency resolution. See README §Supported platforms for the full matrix, 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.
One caveat: 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
vera check --json file.vera
vera check --quiet file.vera
vera typecheck file.vera
vera verify file.vera
vera verify --json file.vera
vera verify --quiet file.vera
vera compile file.vera
vera compile --wat file.vera
vera compile --json file.vera
vera compile --target browser file.vera
vera compile --target wasi-p2 file.vera
vera compile --target wasi-p2 --world server file.vera
vera run file.vera
vera run file.vera --fn f -- 42
vera run file.vera --fn f -- 3.14
vera run file.vera --fn f -- true
vera run file.vera --fn f -- "hello"
vera run --json file.vera
vera serve file.vera
vera serve --port 8080 file.vera
vera test file.vera
vera test --json file.vera
vera test --trials 50 file.vera
vera test file.vera --fn f
vera parse file.vera
vera ast file.vera
vera ast --json file.vera
vera fmt file.vera
vera fmt --write file.vera
vera fmt --check file.vera
vera version
vera lsp
vera builtins [--json]
vera effects [--json]
vera errors [--json]
pytest tests/ -v
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. Functions with ADT or function-type parameters are skipped with a message naming the specific type. 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
vera compile --target browser file.vera -o dist/
This generates three files: module.wasm (the compiled binary), vera-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 pending JSPI suspend/resume support (#609 / #618). 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. Pulling on this thread, two runtime gaps make the recommended pattern less ergonomic than it should be — both are tracked and neither is closed today:
- #609 — implement
IO.sleep against the WebAssembly JavaScript Promise Integration (JSPI) proposal so the WASM call suspends on setTimeout instead of busy-waiting.
- #610 — interpret a minimal ANSI escape subset in the browser runtime so terminal-style programs (clear-screen, cursor-home, colour) render unchanged.
Until those land, 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 (experimental)
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 family (Http, Map, Set, Decimal, Json, Html, Md, Regex, Math, Inference, State, Async) is rejected with a diagnostic naming the family. 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; stdin/filesystem/env ops are rejected in that world (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 with tier1_verified, tier3_runtime, and total counts.
Error codes
Every diagnostic has a stable error code grouped by compiler phase:
- W001 — Typed hole (
?) — expected type and available bindings reported (warning, not error)
- E001–E007 — Parse errors (missing contracts, unexpected tokens)
- E010 — Transform errors (internal)
- E120–E176 — Type check: core + expressions (type mismatches, slot resolution, operators)
- E200–E233 — Type check: calls (unresolved functions, argument mismatches, module calls)
- E300–E335 — Type check: control flow (if/match, patterns, effect handlers)
- E500–E528 — Verification (contract violations, undecidable fallbacks, primitive-operation safety incl. arithmetic overflow)
- E600–E614 — Codegen (unsupported features, typed holes block compilation)
- E700–E702 — Testing (contract violations, input generation, execution errors)
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)
effects(effect_row)
{
body_expression
}
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) or when the program's entry point traditionally takes Unit. main works either way; all examples in this file use main(@Unit -> @Unit) for consistency with the broader spec.
Stored function values and apply_fn
Functions passed as arguments or stored in let bindings use the type form Fn(T -> U) effects(...). 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)
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:
- Write the function signature.
- Run
vera check --explain-slots to get the slot table.
- Use the table to write contracts and body expressions with correct
@T.n indices.
- If
vera check reports E130 (unresolved slot), re-read the table — you have the wrong index.
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, falseInt — signed integers (arbitrary precision)Nat — natural numbers (non-negative)Float64 — 64-bit IEEE 754 floating-pointByte — unsigned 8-bit integer (0–255)String — textUnit — singleton type, value is ()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. Both directions carry a value-level obligation, because @Nat is a u64 and @Int an i64: narrowing requires >= 0 (E503/E504), and widening requires <= i64.MAX (E530; or an E531 warning at the generic-instantiated @Int-field component site code generation cannot guard) — a @Nat above i64.MAX bit-reinterprets to a negative @Int. Runtime guards and verifier obligations mostly correspond, with documented residuals in both directions. Guarded-but-not-reported: a closure nested inside another closure's body is runtime-guarded but not obligated (#985), so a guard can fire there that vera verify did not report. Obligated-but-not-guarded: three narrowing sites are statically obligated yet carry no runtime guard — the effect-operation argument and the generic-instantiated constructor field (#754/#757), and the nat_to_int/nat_to_string conversion builtins — where an E504 warning discloses the unguarded residual rather than claiming a check the runtime never performs. Do not insert nat_to_int defensively; it's only needed when the value is genuinely allowed to be negative. 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> -- unordered unique elements (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.
Type aliases
type PosInt = { @Int | @Int.0 > 0 };
type Name = String;
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)
}
Note: 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 (NYI — see #686; 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 not currently working in the reference compiler — every documented form fails with [E130] no <DataName> bindings in scope. Until that's fixed, 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)
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 ().
Call with the limit first and counter second: loop(100, 1).
For pure recursive functions that need termination proofs, add a decreases clause (see Recursion). Effectful recursive functions like the loop above do not require decreases.
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 wrapper 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:
| Pattern | When | Examples |
|---|
domain_verb | Most functions | string_length, array_append, regex_match, md_parse |
source_to_target | Type conversions | int_to_float, float_to_int, nat_to_int |
domain_is_predicate | Boolean predicates | float_is_nan, float_is_infinite |
| Prefix-less | Math universals and float constants only | abs, min, max, floor, ceil, round, sqrt, pow, nan, infinity |
String operations always use string_ prefix — string_contains, string_starts_with, string_split, string_join, string_strip, string_upper, string_lower, string_replace, string_index_of, string_char_code, string_from_char_code, string_chars, string_lines, string_words, string_reverse, string_trim_start, string_trim_end, string_pad_start, string_pad_end. Character classifiers use is_ prefix — is_digit, is_alpha, is_alphanumeric, is_whitespace, is_upper, is_lower. First-character conversion uses char_ prefix — char_to_upper, char_to_lower. JSON typed accessors use json_as_ and json_get_ prefixes — json_as_string/number/bool/int/array/object for Layer-1 coercions; json_get_string/number/bool/int/array for Layer-2 compound field accessors. Float64 predicates use float_ prefix — float_is_nan, float_is_infinite. Type conversions use source_to_target — int_to_float (not to_float), float_to_int, int_to_nat. Math functions (abs, min, max, etc.) and float constants (nan, infinity) are the only exceptions — they need no prefix because they are universally understood mathematical names.
If vera check reports an unresolved function name, apply these patterns to derive the correct name before giving up. The convention is strict and consistent — the right name is always derivable. Do not invent names that don't follow the pattern; they will not exist.
Option and Result Combinators
The standard prelude provides Option<T> and Result<T, E> along with combinator functions that are always available:
-- 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.
Array operations
array_length(@Array<Int>.0) -- returns Nat (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 yet implemented — use array_sort_by with an explicit comparator, or array_any / array_find with an equality predicate, until that infrastructure lands.
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, Unit). Values can be any type. All operations are pure — insert and remove return new maps.
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 an unordered collection of unique elements. Elements must satisfy Eq and Hash abilities (primitive types: Int, Nat, Bool, Float64, String, Byte, Unit). 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.
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>
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; total: nan/inf/-inf for non-finite)
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. Programs must redefine UrlParts locally (like Result) to use it in match expressions.
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 textMdCode(String) — inline codeMdEmph(Array<MdInline>) — emphasis (italic)MdStrong(Array<MdInline>) — strong (bold)MdLink(Array<MdInline>, String) — link with text and URLMdImage(String, String) — image with alt text and source
MdBlock — block-level content:
MdParagraph(Array<MdInline>) — paragraphMdHeading(Nat, Array<MdInline>) — heading with level (1–6)MdCodeBlock(String, String) — fenced code block (language, code)MdBlockQuote(Array<MdBlock>) — block quoteMdList(Bool, Array<Array<MdBlock>>) — list (ordered?, items)MdThematicBreak — horizontal ruleMdTable(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 contentHtmlComment(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 on NaN or out-of-range values (WASM semantics). 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 (guarded: traps if @Nat > i64.MAX)
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, but a @Nat above i64.MAX bit-reinterprets to a negative @Int, so — like the implicit @Nat → @Int coercion — it carries a <= i64.MAX obligation (E530): Tier 1 when the value is provably bounded, otherwise a runtime trap (vera run traps rather than silently returning the reinterpreted value). 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. The forward-looking design question of allowing direct @Byte arithmetic (with verified underflow + overflow guards) is tracked speculatively as #564; the current 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).
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 soundly replaces them.
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 pure recursive functions: the expression must strictly decrease on each recursive call so Z3 can discharge termination. Effectful recursive functions (<IO>, <State>, <Http>, etc.) do not require decreases — see the FizzBuzz example in the Iteration section, which loops over <IO> recursively without one.
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).
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:
- Write
requires(true) ensures(true) and run vera check — confirm the body is correct first.
- Add a
requires condition for each invariant the caller must satisfy.
- Add an
ensures condition describing what the function guarantees. Use @T.result for the
return value.
- Run
vera verify — not just vera check — to confirm contracts are statically provable.
vera check only type-checks; vera verify runs Z3.
- If
vera verify reports a contract will be checked at runtime (Tier 3), the Z3 solver could
not prove it. Add a decreases clause for recursive functions, or simplify the contract
expression.
- 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
})
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(<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).
Effect declarations
The IO effect is built-in — no declaration is needed. It provides eleven operations:
| Operation | Signature | Description |
|---|
IO.print | String -> Unit | Print a string to stdout (no implicit newline; flushes per call) |
IO.read_line | Unit -> String | Read a line from stdin |
IO.read_char | Unit -> Result<String, String> | Read one character from stdin (raw mode on TTY). Returns Err("EOF") when stdin closes. Browser target not yet supported — depends on JSPI (#609) for suspend/resume. |
IO.read_file | String -> Result<String, String> | Read file contents |
IO.write_file | String, String -> Result<Unit, String> | Write string to file |
IO.args | Unit -> Array<String> | Get command-line arguments |
IO.exit | Int -> Never | Exit with status code |
IO.get_env | String -> Option<String> | Read environment variable |
IO.sleep | Nat -> Unit | Pause execution for N milliseconds |
IO.time | Unit -> Nat | Current Unix time in milliseconds |
IO.stderr | String -> Unit | Print a string to stderr |
If you declare effect IO { op print(String -> Unit); } explicitly, that overrides the built-in and only the declared operations are available. Most examples do this — declaring only print — because it follows the principle of least privilege: a program that only declares op print cannot accidentally perform file I/O or call exit.
Why IO works differently from State and Async: IO has 11 operations and programs choose which ones they need. State and Async have fixed, minimal operation sets (State: get/put; Async: no operations, it is a marker effect), so there is nothing to restrict.
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. Pre-v0.0.123 the whole transcript was buffered until program exit; that behaviour was correct for trap preservation and JSON consumers but made interactive output invisible.
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)
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:
effect Exn<E> {
op throw(E -> Never);
}
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.
| Operation | Signature | Description |
|---|
Http.get | String -> Result<String, String> | HTTP GET request |
Http.post | String, String -> Result<String, String> | HTTP POST request (body as JSON; sends Content-Type: application/json) |
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.
| Operation | Signature | Description |
|---|
Inference.complete | String -> Result<String, String> | Send a prompt, return Ok(completion) or Err(message) |
effects(<Inference>) -- LLM access
effects(<Inference, IO>) -- LLM + console output
