Aver

Aver

Aver is a statically typed language designed for AI to write and humans to review. It has a bytecode VM for running code, a Rust backend for deployment, a WASM backend for browser and embedded targets, and Lean proof export for pure logic and classified effectful laws.

An AI reviewer's opinion of generated code gets cheaper every year. A certificate checked by the Lean kernel keeps its price. Aver source carries proof obligations, and a compiled wasm-gc artifact can ship with a sidecar certificate bound to its exact bytes. The Lean kernel signs off on those guarantees, so they do not rest on someone having looked at the code once. Generated code already arrives faster than anyone can read it, and the certificate is what stays useful when spot-checks can no longer keep up.

Readability comes second, and it still matters. The risky part of AI-written code is usually missing intent, much more often than bad syntax. Aver makes that intent explicit and machine-readable:

• effects are part of the function signature
• decisions live next to the code they explain
• pure behavior lives in colocated verify blocks
• selected effectful behavior can be verified with explicit stubs and trace assertions
• effectful runs can be recorded and replayed deterministically

The toolchain (run / verify / check / audit / why / context / compile / bench / proof / replay) is documented in docs/cli.md. The backends have their own pages: docs/bench.md, docs/transpilation.md, docs/lean.md, docs/effects.md, docs/wasip2.md and docs/rust.md. Compiled wasm-gc modules and wasip2 components can carry a machine-checkable certificate of what their exports compute; see docs/certification.md.

Aver is optimized for AI to generate code that humans can inspect, constrain, test and ship. Typing it by hand all day is not the goal.

Prompting an LLM to write Aver? Run aver agent-connect in your project. The language guide and the toolchain guide ship inside the binary, so every install already has them. The command writes them out as .claude/skills/aver/SKILL.md and .claude/skills/aver-tooling/SKILL.md and points a marked section of your AGENTS.md at them. It touches nothing else. aver agent-connect --global puts the same two skills in ~/.claude/skills/ instead, and aver agent-connect --print writes the language guide to stdout for an agent that wants a single file. There is no blessed workflow; keep whatever prompt or harness you already use. If you would rather link than install, the same curated guide is the repo-root llms.txt and averlang.dev/llms.txt. It covers the .av extension, single-line match arms, qualified constructors, classified effects, verify block shapes, and the other rules models tend to get wrong on the first try. A longer reference cut is llms-full.txt.

Website: averlang.dev
Browser playground: averlang.dev/playground

The Aver Manifesto makes the longer argument, and Common Pushback collects questions and objections. intent-trace is an empirical benchmark that compares Aver's legibility against Python variants across 108 AI-reviewed code changes.

Quickstart

Docker

docker build -t aver-one-command . && docker run --rm aver-one-command

This builds aver and aver-cert, runs examples/core/hello.av, checks one Lean law, and smoke-checks a small artifact certificate. See docs/quickstart.md.

Install from crates.io

cargo install aver-lang --features wasm
cargo install aver-cert

The wasm feature enables wasm-gc compilation and --certify. Leave it out only if you need nothing beyond the VM and the Rust backend. Install with --features wasm,wasip2 if you also want the WASI 0.2 target shown below. aver-lang installs the compiler as aver.

aver-cert installs the independent certificate verifier that aver cert uses. Keep both executables in the same directory or on PATH. The verifier has its own public version line, starting at 0.1.0 and separate from the aver-lang version, and it checks certificates with the pinned Lean 4.35 toolchain. Verification needs a standard Elan installation. The verifier resolves the canonical Elan executable directly and does not look up its trusted Lake, Lean or leanchecker processes through PATH.

Then try it with a tiny file:

cat > hello.av <<'EOF'
module Hello
    intent =
        "Tiny intro module."
    exposes [greet]

fn greet(name: String) -> String
    ? "Greets a user."
    "Hello, {name}"

fn runCli() -> Unit
    ? "Starts the CLI."
      "Prints one rendered response."
    ! [Args.get, Console.print]
    Console.print("todo")

verify greet
    greet("Aver") => "Hello, Aver"

fn main() -> Unit
    ! [Console.print]
    Console.print(greet("Aver"))
EOF

aver run      hello.av
aver run      hello.av --self-host
aver verify   hello.av
aver verify   hello.av --json
aver check    hello.av
aver check    hello.av --json
aver capabilities hello.av
aver capabilities hello.av --json
aver audit    hello.av
aver audit    hello.av --json
aver why      hello.av
aver context  hello.av
aver shape    hello.av
aver compile  hello.av -o out/
(cd out && cargo run)

aver run, verify, check and replay use the bytecode VM by default. The old --vm flag has been removed.

Unit is Aver's "no meaningful value" type. It is roughly void and shows up as () in diagnostics. main often returns Unit, but it can also return Result<Unit, String>, and aver run treats Result.Err(...) from main as a process failure.

Build from source

git clone https://github.com/jasisz/aver
cd aver
cargo install --path . --features wasm --force
cargo install --path aver-cert --force

aver run      examples/core/calculator.av
aver run      examples/core/calculator.av --self-host
aver verify   examples/core/calculator.av
aver check    examples/core/calculator.av
aver audit    examples/core/calculator.av
aver why      examples/core/calculator.av
aver context  examples/core/calculator.av
aver compile  examples/core/calculator.av -o out/
(cd out && cargo run)
aver proof    examples/formal/law_auto.av -o proof/
(cd proof && lake build)
aver run      examples/services/console_demo.av --record recordings/
aver run      examples/core/calculator.av -e 'safeDivide(10, 2)' --record recordings/
aver run      examples/services/console_demo.av --wasm-gc --record recordings/
aver replay   recordings/ --test --diff
aver replay   recordings/ --test --check-args
aver replay   recordings/ --test --json
aver replay   recordings/rec-…json --wasm-gc

Recordings are byte-compatible across the VM, self-host and wasm-gc backends. A trace written by any one of them replays cleanly under any of the three.

Requires: Rust stable toolchain.

Editor support

For editor integration:

cargo install aver-lsp

Then install the VS Code extension Aver.aver-lang, or have your editor start the aver-lsp binary directly. editors/README.md has setup notes for VS Code, Sublime Text and manual LSP configuration.

Small example

module Payments
    intent =
        "Processes transactions with an explicit audit trail."
    exposes [charge]

decision UseResultNotExceptions
    date = "2024-01-15"
    reason =
        "Invisible exceptions lose money at runtime."
        "Callers must handle failure — Result forces that at the call site."
    chosen = "Result"
    rejected = ["Exceptions", "Nullable"]
    impacts = [charge]

fn charge(account: String, amount: Int) -> Result<String, String>
    ? "Charges account. Returns txn ID or a human-readable error."
    match amount
        0 -> Result.Err("Cannot charge zero")
        _ -> Result.Ok("txn-{account}-{amount}")

verify charge
    charge("alice", 100) => Result.Ok("txn-alice-100")
    charge("bob",   0)   => Result.Err("Cannot charge zero")

No if/else. No loops. No exceptions. No nulls. No implicit side effects.

Deliberate constraints

Aver is opinionated on purpose. Each of these omissions is a design choice:

• no if/else: branching goes through match, which dispatches directly on literals ("verack" ->, 253 ->), constructors, lists and tuples as well as booleans
• no for/while: iteration is recursion or explicit list operations
• no exceptions: failure is Result
• no null: absence is Option
• no closures: functions are top-level and explicit
• no async/await, streams or channels: (a, b)?! declares independent computations and the runtime handles the rest. See docs/independence.md
• no hidden state behind effects: Disk.write does not affect a later Disk.read. If state matters, it lives in pure user data (see below)

Each omission removes a kind of implicit behavior that AI generates easily and humans find tedious to audit.

For the fuller language rationale, see docs/language.md.

Pure core, effect shell

Prove the model, not the world.

Aver splits programs into two layers:

• Pure core: explicit data, explicit state transitions, laws. Read-after-write consistency, ordering and accumulation are properties of your data structures (a FileStore, a PaymentLedger, a WorkflowState), proven by verify over pure functions.
• Effect shell: Disk.*, Time.*, Process.*, Tcp.*, Http.*, Env.*. These are one-shot calls to the world. Oracle stubs are explicit functions of branch and call index. An Env.set does not change a later Env.get, a first Time.now does not constrain the next, and a Disk.write does not seed a later Disk.read. Capability-owned laws may still relate observations. Process.stopRequested does this: it can only go from false to true.

This is deliberate. Real wall clocks are not monotonic (NTP, leap, suspend, VM clock skew). Filesystems are not transactional. Aver does not give external services nicer laws than the platform actually promises, because that would prove guarantees the OS never gave.

If a property depends on memory across effect calls, model the state in pure user code. The shell stays thin.

Runnable patterns: examples/formal/file_store_pure_core.av + examples/formal/file_store_shell.av, examples/formal/clock_as_data.av. Background: docs/oracle.md.

Why Aver exists

LLMs can produce function bodies quickly. They are much worse at preserving the information reviewers actually need:

• what a function is allowed to do
• why a design was chosen
• what behavior must keep holding after a refactor
• what a new human or model needs to understand the codebase without reading everything

Traditional languages usually push that into comments, external docs, stale tests, or team memory. Aver makes those concerns part of the language and tooling.

The intended workflow: AI writes Aver, humans review contracts and intent, the bytecode VM runs the code during development, and deployment goes through Rust code generation or WASM compilation.

Talks

I discussed Aver on Happy Path Programming #120 with Bruce Eckel and James Ward. We talked about why Aver optimizes for the reviewer and not the generator, why effects, intent, verify blocks and decisions belong in the language itself, and what "AI-native" should mean when a human still has to trust the generated code.

Watch / listen: https://www.youtube.com/watch?v=D_mPxGtSzbQ

Execution modes

Default (VM)

aver run hello.av

All commands use the bytecode VM. For VM internals, see docs/vm.md.

WASM

# Native WebAssembly GC + tail-call output for browsers / Workers
aver compile hello.av --target wasm-gc

# Run through embedded wasmtime (uses the same wasm-gc emit path)
aver run hello.av --wasm-gc

# Carry that Wasmtime host with the program; the destination needs no Aver
aver compile hello.av --target wasm-gc --pack wasmtime -o out/
./out/aver-wasmtime-host some-arg

# Diagnose a particular deployment stage (default remains zero-JIT AOT)
./out/aver-wasmtime-host --artifact canonical -- some-arg
./out/aver-wasmtime-host --artifact optimized -- some-arg

# WASI 0.2 / Component Model output (wasmtime, Spin, NGINX Unit, etc.)
aver compile hello.av --target wasip2

# Run a wasip2 component through embedded wasmtime + wasi
aver run hello.av --wasip2 -- some-arg

--target wasm-gc is the default modern target (Chrome 119+ / Firefox 120+ / Safari 18.2+ / wasmtime 25+ / Node 22+ / Workers). --target wasip2 is its counterpart for the Component Model. The pre-2024 NaN-boxed wasm32 backend (--target wasm + --bridge) was dropped in 0.18. See docs/effects.md and docs/wasip2.md for the supported deployment surfaces.

The Wasmtime pack is a native directory bundle. It contains the canonical wasm-gc module, an optional distinct Binaryen result, its matching precompiled Wasmtime image, a manifest, and a stripped aver-wasmtime-host executable with the engine and the project's configured providers linked in. Only the build machine needs Aver, Cargo and provider sources. The destination loads the AOT image without running Cranelift. --certify --optimize keeps three stages on purpose: the certificate binds <name>.wasm, deployment uses <name>.optimized.wasm, and Wasmtime executes <name>.cwasm. See docs/wasmtime-pack.md. The bundled host defaults to .cwasm. For differential diagnosis it can explicitly JIT either portable stage with --artifact canonical|optimized. It never falls back automatically.

Custom capabilities whose whole contract uses only Unit, Bool, Float and String compile to typed wasip2 component imports. They are host-bound. An external Component Model host may provide the generated interface directly, or aver run app.av --wasip2 can adapt the same Rust ProviderBinding that the project's aver.toml binds for the VM. Without such a binding, aver run --wasip2 reports the missing import before component linking.

Native Rust

aver compile hello.av              # generates Rust/Cargo project
aver compile hello.av --policy embed   # bake aver.toml into binary
aver compile hello.av --policy runtime # load aver.toml at runtime

See docs/rust.md for the generated code model.

Generated Rust can also be linked with native custom capability providers. The generated library accepts the same aver_rt::provider::ProviderBinding that an embedded VM uses. A versioned [providers] section in aver.toml can name an explicit Cargo package/path and a zero-argument binding factory. aver compile then emits the dependency and the stock-binary bootstrap, and Cargo resolves the package during the generated build.

The same manifest is part of what a program means on every backend. When a program reaches a bound capability, aver run, aver verify and aver audit build a thin cached Rust host once (the first build names the packages it links) and run the ordinary bytecode VM inside it with those bindings in-process. Project-wide verify/audit installs only the bindings each module needs, so independent modules still run and are not mislabeled as type errors. For a WIT-lowerable contract, aver run app.av --wasip2 uses the same host package and binding behind the generated Component Model import. aver run app.av --wasm-gc uses the same binding behind the contract-derived raw wasm-gc ABI, including compound values, packed Bytes and opaque provider resources. --self-host still has no provider host and refuses such a program. A project without [providers] never invokes Cargo. Its generated artifacts stay host-bound, and embedders can install bindings through the library API.

Self-hosted

aver run hello.av --self-host

This runs the program through the Aver interpreter written in Aver, which is compiled to Rust and cached on demand. See self_hosted/README.md.

What Aver makes explicit

Effects

fn processPayment(amount: Int) -> Result<String, String>
    ? "Validates and records the charge. Pure — no network, no disk."
    match amount
        0 -> Result.Err("Cannot charge zero")
        _ -> Result.Ok("txn-{amount}")

fn fetchExchangeRate(currency: String) -> Result<Http.Response, String>
    ? "Fetches live rate from the ECB feed."
    ! [Http.get]
    Http.get("https://api.ecb.europa.eu/rates/{currency}")

Effects such as Http.get, Disk.readText, and Console.print are part of the signature. A missing declaration is a type error. The runtime also enforces the same boundary as a backstop.

Effects can be granular or namespace-wide:

• ! [Http.get] allows only Http.get
• ! [Http] covers all Http.* effects

aver check suggests narrowing a broad namespace effect when a function only needs a smaller subset.

Runtime policy in aver.toml can narrow the allowed destinations further:

[effects.Http]
hosts = ["api.example.com", "*.internal.corp"]

[effects.Disk]
paths = ["./data/**"]

[effects.Env]
keys = ["APP_*", "PUBLIC_*"]

[effects.Tcp]
connect_timeout_secs = 5
request_idle_timeout_secs = 30
max_connections = 256

Disk paths accept concrete subtrees, ./** for the project-relative subtree, and /** for the filesystem root. Loading aver.toml rejects bare **, empty entries, unsupported glob spellings and ..-rooted entries. The CLI reference has the full grammar and explains the limitation that matching is string-only.

These are two separate controls:

• code answers: what kind of I/O is allowed?
• policy answers: which concrete destinations are allowed?

The three Tcp values configure the standard capability provider. They do not grant additional effects. The two deadlines apply to connection establishment and to one-shot request calls. Reads and writes on persistent sessions have no deadline, by design. max_connections is a single sha