<p align="center"> <picture> <source media="(prefers-color-scheme: dark)" srcset="docs/logo-dark.svg"> <source media="(prefers-color-scheme: light)" srcset="docs/logo-light.svg"> <img alt="aver" src="docs/logo-dark.svg" width="360"> </picture> </p>

Aver

Aver is a statically typed language designed for AI to write in and humans to review, with a fast interpreter for iteration, a bytecode VM for runtime execution, a Rust backend for deployment, Lean proof export for pure core logic, and Dafny verification for automated law checking via Z3.

It is built around one idea: the risky part of AI-written code is usually not syntax, it is missing intent. 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
• effectful behavior can be recorded and replayed deterministically
• aver why scores every function's justification coverage: description, verify, decisions
• aver context exports the contract-level view of a module graph for humans or LLMs
• aver compile turns an Aver module graph into a Rust/Cargo project
• aver proof exports the pure subset of an Aver module graph to a Lean 4 proof project (default) or Dafny verification file (--backend dafny)

This is not a language optimized for humans to type by hand all day. It is optimized for AI to generate code that humans can inspect, constrain, test, and ship.

Read the Aver Manifesto for the longer argument, or Common Pushback for questions, objections, and honest answers.

---

Quickstart

Install from crates.io

cargo install aver-lang

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 --vm
aver run      hello.av --self-host
aver verify   hello.av
aver verify   hello.av --vm
aver verify   hello.av --json
aver check    hello.av
aver check    hello.av --json
aver why      hello.av
aver context  hello.av
aver compile  hello.av -o out/
(cd out && cargo run)

Unit is Aver's "no meaningful value" type, roughly like void and rendered as () in diagnostics. main often returns Unit, but it can also return Result<Unit, String>; 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 . --force

aver run      examples/core/calculator.av
aver run      examples/core/calculator.av --vm
aver run      examples/core/calculator.av --self-host
aver verify   examples/core/calculator.av
aver verify   examples/core/calculator.av --vm
aver check    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 replay   recordings/ --test --diff
aver replay   recordings/ --test --check-args
aver replay   recordings/ --test --json

Requires: Rust stable toolchain.

Editor support

For editor integration:

cargo install aver-lsp

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

---

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 intentionally opinionated. These omissions are part of the design, not missing features:

• no if/else — branching goes through match
• 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; the runtime handles the rest. See docs/independence.md

The point is to remove classes of implicit behavior that are easy for AI to generate and annoying for humans to audit.

For the fuller language rationale, see docs/language.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 is explicit: AI writes Aver, humans review contracts and intent, and execution happens through the interpreter or bytecode VM during development, with deployment also available through Rust code generation.

Bytecode VM

aver run hello.av --vm
aver verify hello.av --vm
aver replay recordings/ --vm

--vm executes the same Aver program, verify cases, or replay session through the bytecode virtual machine instead of the tree-walking interpreter. This is useful when you want a runtime path that is closer to the eventual compiled model, while keeping the same source language and effect checks.

For the VM internals and design rationale, see docs/vm.md.

Self-hosted interpreter

aver run hello.av --self-host
aver replay recordings/ --self-host

--self-host executes the program through the Aver interpreter written in Aver itself, compiled to Rust and cached on demand. There is no separate "aver-self" install step: cargo install aver-lang already ships the self_hosted/ sources inside the crate, and the first aver run ... --self-host builds a cached helper binary automatically. That helper cache is shared across guest projects for the same installed Aver build, so changing --module-root does not force a rebuild. On the first cold run Aver prints short progress messages while it generates and builds the helper.

For generated Rust projects, aver compile now exposes policy mode explicitly:

aver compile app.av --policy embed
aver compile app.av --policy runtime

embed bakes the current aver.toml into the artifact. runtime loads aver.toml from the active module root when the binary runs.

Most users should never run self_hosted/main.av directly. That entry exists mainly for hacking on the self-host inside this repository; the normal installed interface is still just:

aver run hello.av --self-host
aver replay recordings/ --self-host

For --record and aver replay --self-host, replay and aver.toml policy are scoped to the guest program boundary only: the self-host's own bootstrap reads and module loading stay outside the recording. aver.toml is loaded from the guest --module-root at runtime, so changing guest policy does not invalidate the cached helper.

If you generate self-host-like Rust binaries directly, see docs/rust.md for the explicit --with-self-host-support / --guest-entry contract used by SelfHostRuntime.*.

---

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<HttpResponse, 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. Missing declarations are type errors. The runtime enforces the same boundary as a backstop.

Effects are exact:

• ! [Http.get] allows only Http.get
• ! [Http] does not cover Http.get

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

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

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

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

Think of this as two separate controls:

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

Generated Rust can use the same scoped runtime machinery when you compile with --with-replay; see docs/rust.md.

Decisions

decision UseResultNotExceptions
    date = "2024-01-15"
    reason =
        "Invisibl