aallan/vera/docs

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_length over a non-literal is the usual trigger — Vera counts UTF-8 bytes and Z3's string theory has no byte-length operator — so compare a string_length` against a literal where you want the function trialled. Float64 uses Z3's mathematical reals (NaN, ±∞, and subnormals are not generated). Strings are capped at 50 characters.

Browser compilation

vera compile --target browser produces a ready-to-serve browser bundle:

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