Vera：LLM编程语言

Prerequisites

• Python 3.11+
• Git
• Node.js 22+ (optional, for browser runtime and parity tests)

Contracts the compiler proves

A precondition like requires(@Int.1 != 0) becomes a static obligation: the SMT solver proves it holds at every call site, or refuses to compile. A program that calls safe_divide with a divisor the verifier can't prove non-zero is a compile error, not a runtime error.

public fn safe_divide(@Int, @Int -> @Int)
  requires(@Int.1 != 0)
  ensures(@Int.result == @Int.0 / @Int.1)
  effects(pure)
{
  @Int.0 / @Int.1
}

The verifier checks the contracts the programmer wrote. A function that performs @Int.1 / @Int.0 without a guarding precondition will type-check, verify, and trap at runtime if called with a zero divisor — with a Vera-native diagnostic explaining how to add the missing precondition. Automatically synthesising obligations for primitive operations is the principled long-term move and tracked in #680.

Getting started

Installation

git clone https://github.com/aallan/vera.git
cd vera
python -m venv .venv
source .venv/bin/activate
pip install -e ".[dev]"

Supported platforms

Tested in CI on every commit:

• macOS 15 (Sequoia) and macOS 26 (Tahoe) on Apple Silicon, against Python 3.11, 3.12, 3.13
• Ubuntu 24.04 LTS on x86_64, against Python 3.11, 3.12, 3.13
• Windows Server 2022 on x86_64, against Python 3.11, 3.12, 3.13

Untested but expected to work (wheels available for all dependencies):

• Linux x86_64 with glibc 2.27+ (Ubuntu 18.04+ / Debian 10+ / RHEL 8+)
• Linux aarch64 with glibc 2.38+ (Ubuntu 23.10+ / Ubuntu 24.04 LTS / Debian 12+)
• macOS 15+ on Intel (x86_64)

Out of scope — pip install -e . will fail at dependency resolution (clear "no matching distribution" error rather than a cryptic source-build failure):

• macOS 14 (Sonoma) and earlier — see #691 for the documented decision and workarounds
• Linux aarch64 with glibc < 2.38 (e.g. Ubuntu 22.04 LTS aarch64) — see #701

The macOS 15+ baseline reflects TelemetryDeck's macOS version distribution data: macOS 26 (~75%) and macOS 15 (~24%) account for ~99% of the macOS install base; macOS 14 is ~1.4% and falling. The cost of supporting older macOS versions does not earn its keep at that share.

The workflow

$ vera check examples/absolute_value.vera
OK: examples/absolute_value.vera

$ vera verify examples/safe_divide.vera
OK: examples/safe_divide.vera
Verification: 4 verified (Tier 1)

$ vera run examples/hello_world.vera
Hello, World!

vera check parses and type-checks. vera verify adds contract verification via Z3 — Tier 1 contracts (decidable arithmetic, comparisons, Boolean logic, ADTs, termination) are proved automatically; contracts Z3 cannot decide become Tier 3 runtime checks. vera run compiles to WebAssembly and executes.

vera run file.vera --fn f -- 42           # call function f with argument 42
vera compile --target browser file.vera   # emit browser bundle
vera test file.vera                       # contract-driven testing via Z3 + WASM
vera fmt file.vera                        # format to canonical form
vera verify --json file.vera              # JSON diagnostics for agent feedback loops
vera check --explain-slots file.vera     # show slot resolution table (which @T.n maps to which param)
vera version                             # print the installed version

vera compile --target browser produces a self-contained bundle (wasm + JS runtime + HTML) that runs in any browser — no build step, no bundler. Mandatory parity tests ensure identical behaviour between the command-line and browser runtimes for the pure-language surface (arithmetic, ADTs, pattern matching, closures, contracts, effects-as-host-imports, etc.). The IO surface is the documented exception: terminal Vera programs that rely on IO.sleep for animation pacing or ANSI escape codes for cursor control compile cleanly to --target browser but render the escapes as literal text and freeze the tab while sleeping — the browser target expects Vera to be the pure simulation core and JavaScript to drive timing and rendering (SKILL.md §Browser compilation has the recommended pattern).