Aver

Imagine AI writes 90% of your code. What do you need to trust it?

Aver is hard to write, clean to read — and in a world where AI does the writing, that's the only trade-off that matters.

Not better prompts. Not more reviews. You need a language that makes the AI's intent verifiable — statically, at the call site, before a single line runs.

Aver is that language. Read the Aver Manifesto for the full story.

---

The problem with AI-generated code

LLMs are good at writing functions. They're terrible at communicating:

• what a function is allowed to do (call the network? write files? read secrets?)
• why a particular approach was chosen over the alternatives
• whether a change still passes the invariants the original author had in mind
• what an AI needs to know to continue working on a 50-file codebase it's never seen

Traditional languages leave all of this as implicit knowledge in someone's head, in stale docs, or nowhere at all. That was fine when humans wrote all the code. It isn't now.

---

Aver's answer, feature by feature

"How do I know this function doesn't make HTTP calls?"

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]
    Http.get("https://api.ecb.europa.eu/rates/{currency}")

Effect declarations (! [Http], ! [Disk], ! [Console], ! [Tcp], ! [HttpServer]) are part of the signature. The type checker enforces them — a function that calls Http.get without declaring ! [Http] is a type error, not a warning. The runtime enforces the same boundary as a backstop.

You can read any function in Aver and know exactly what it's capable of — without running it, without reading its body.

"Why was this decision made?"

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, refund, settle]
    author = "team"

decision blocks are first-class syntax, co-located with the code they describe. Not a Confluence page that goes stale. Not a commit message no one reads. Queryable:

aver context payments.av --decisions-only

Three months later — human or AI — you know why the code looks the way it does.

"How does an AI understand this codebase without reading everything?"

aver context payments.av

Aver traverses the dependency graph and emits a compact summary — module intents, public signatures, effect declarations, verify cases, and all decision blocks — typically 1–3k tokens. Enough for an LLM to understand contracts, boundaries, and rationale without the full source.

## Module: Payments
> Processes transactions with an explicit audit trail.

### `charge(account: String, amount: Int) -> Result<String, String>` ! [Http, Ledger]
> Charges account. Returns txn ID or a human-readable error.
verify: `charge("alice", 100)` → `Result.Ok("txn-alice-100")`, `charge("bob", 0)` → `Result.Err("Cannot charge zero")`

## Decisions
### UseResultNotExceptions (2024-01-15)
**Chosen:** Result — **Rejected:** Exceptions, Nullable
> Invisible exceptions lose money at runtime...

This is what AI-assisted development actually needs: context that travels with the code, not context that lives in someone's memory.

"How do I know a refactor didn't break anything?"

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

verify blocks are intended to stay close to the function they cover (same module, usually right after the definition). aver check warns when a pure, non-trivial, non-main function has no verify block by name. It intentionally skips effectful functions (covered by replay) and trivial pass-through wrappers. Verify blocks run with aver verify (or aver run --verify) under the same type/effect checks as normal code.

"How do I test effectful code without flaky mocks?"

Use deterministic replay.

1. Run once against real services and record the effect trace.
2. Replay offline: same effect sequence, same outcomes, no real network/disk/TCP calls.
3. Use --diff/--test to turn recordings into a regression suite.

# Real execution + capture
aver run payments.av --record recordings/

# Deterministic replay (single file or whole directory)
aver replay recordings/rec-123.json --diff
aver replay recordings/ --test --diff

No mock framework. No mock code. No mock maintenance.

In Aver, effectful tests are just replay files:

1. capture once,
2. replay forever,
3. optionally tweak one recorded effect outcome to create a new edge-case test.

Pure logic stays in verify; effectful flows are covered by replay recordings. Testing stays embarrassingly simple.

---

Full example

module Payments
    intent =
        "Processes transactions with an explicit audit trail."
    depends [Ledger, Models.User]
    exposes [charge]

decision UseResultNotExceptions
    date = "2024-01-15"
    reason =
        "Invisible exceptions lose money at runtime."
        "Callers must handle failure — Result forces that at compile time."
    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."
    ! [Http, Ledger]
    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 magic.

---

CLI

aver run       file.av                   # type-check, then execute
aver run       file.av --verify          # execute + run verify blocks
aver run       file.av --record recs/    # execute + record effect trace
aver replay    recs/rec-123.json         # replay one recording offline
aver replay    recs/ --test --diff       # replay suite; fail on output mismatch
aver check     file.av                   # type errors + intent/desc warnings
aver verify    file.av                   # run all verify blocks
aver compile   file.av -o out/           # transpile to a Rust project
aver compile   file.av -t rust -o out/   # explicit target (rust is default)
aver compile   file.av -t lean -o out/   # transpile pure core to a Lean 4 project (WIP)
aver context   file.av                   # export project context (Markdown)
aver context   file.av --json            # export project context (JSON)
aver context   file.av --decisions-only        # decision blocks only (Markdown)
aver context   file.av --decisions-only --json # decision blocks only (JSON)
aver decisions                          # ADR-style decisions from decisions/architecture.av
aver decisions --docs                   # regenerate docs/decisions.md from decision blocks
aver repl                              # interactive REPL

run, check, verify, compile, and context also accept --module-root <path> to override import base (default: current working directory).

See docs/transpilation.md for full transpilation documentation.

Lean target (-t lean, WIP)

Lean transpilation emits a Lean 4 project (lakefile.lean, lean-toolchain, <Project>.lean) for pure core logic.

• Pure functions, types, and decisions are emitted.
• Effectful functions and main are intentionally skipped.
• verify blocks are exported as Lean example ... := by sorry obligations.
• Lean codegen now fails fast on unresolved internals:
  • Expr::Resolved in codegen input → hard error
  • Type::Unknown in codegen input → hard error
  • no silent fallback sorry for those cases

---

Language reference

Types

Primitive: Int, Float, String, Bool, Unit Compound: Result<T, E>, Option<T>, List<T>, Map<K, V>, (A, B, ...), Fn(A) -> B, Fn(A) -> B ! [Effect] User-defined sum types: type Shape → Shape.Circle(Float), Shape.Rect(Float, Float) User-defined product types: record User → User(name = "Alice", age = 30), u.name

Bindings

All bindings are immutable. No val/var keywords — they are parse errors.

name = "Alice"
age: Int = 30
xs: List<Int> = []

Optional type annotation provides a hint to the type checker; the annotation wins over inference when both are compatible. Binding to an empty list literal without a type annotation (x = []) is a type error.

Duplicate binding of the same name in the same scope is a type error.

Operators

Arithmetic: +, -, *, / — operands must match (Int+Int, Float+Float, String+String). No implicit promotion; use Int.toFloat / Float.fromInt to convert. Comparison: ==, !=, <, >, <=, >=. Pipe: value |> fn — passes the left-hand value as the sole argument to the right-hand function. Right-hand side must be a function reference (fn / Ns.fn), not a call (fn(...)). Error propagation: expr? — unwraps Result.Ok, propagates Result.Err as a RuntimeError.

String interpolation

Expressions inside {} are evaluated at runtime:

greeting = "Hello, {name}! You are {age} years old."

Constructors

UpperCamel callee = constructor, lowerCamel = function call. Records use named args (User(name = "A", age = 1)), variants use positional args (Shape.Circle(3.14)), zero-arg constructors are bare singletons (Option.None, Shape.Point).

All constructors are namespaced — no bare Ok/Err/Some/None:

Result.Ok(42)
Result.Err("not found")
Option.Some("hello")
Option.None

Match expressions

match is the only branching construct (no if/else). Patterns:

match value
    42 -> "exact"                          // literal
    _ -> "anything"                        // wildcard
    x -> "bound to {x}"                    // identifier binding
    [] -> "empty list"                     // empty list
    [h, ..t] -> "head {h}, tail {t}"       // list cons
    Result.Ok(v) -> "success: {v}"         // constructor
    Result.Err(e) -> "error: {e}"
    Shape.Circle(r) -> "circle r={r}"
    Shape.Point -> "point"
    User(name, age) -> "user {name}"       // record positional destructuring
    (a, b) -> "pair: {a}, {b}"             // tuple destructuring
    ((x, y), z) -> "nested: {x}"          // nested tuple

Nested match in match arms is supported. Arm body must follow -> on the same line — extract complex expressions into a named function.

Record update

Creates a new record with overridden fields, preserving all other fields:

updated = User.update(u, age = 31)

Map literals

m = {"key" => value, "other" => 42}

=> is required inside map literals; : stays type-only.

Effect aliases

Named effect sets reduce repetition:

effects AppIO = [Console, Disk]

fn main() -> Unit
    ! [AppIO]
    // ...

Functions

fn add(a: Int, b: Int) -> Int = a + b

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

• ? "..." — optional prose description (part of the signature)
• ! [Effect] — optional effect declaration (statically and runtime enforced)
• = expr — single-expression shorthand
• Block body with indentation for multi-statement functions

No closures

All user-defined functions are top-level. At call time, a function sees globals + its own parameters — no closure capture at definition time. There is no lambda syntax. Higher-order APIs (for example List.map, List.filter, List.any) take a top-level function name.

Common patterns (without closures)

fn double(n: Int) -> Int
    ? "Doubles a number."
    = n * 2

doubled = List.map([1, 2, 3, 4], double)

hasAlice = List.contains(["alice", "bob"], "alice")

ages = Map.fromList([("alice", 30), ("bob", 25)])
maybe_age = Map.get(ages, "alice")

Auto-memoization

Pure recursive functions with memo-safe arguments (scalars, records/variants of scalars) are automatically memoized at runtime. No keyword needed — the compiler detects eligibility via call-graph analysis (Tarjan SCC). Cache is capped at 4096 entries per function.

Tail-call optimization

Self and mutual tail recursion is optimized automatically. A transform pass after parsing rewrites tail-position calls into a trampoline — no stack growth for recursive functions. Tail position = last expression in function body, or each arm body in a match at tail position.

Modules

Module imports resolve from a module root (--module-root, default: current working directory).

module Payments
    intent = "Processes transactions."
    depends [Examples.Fibonacci]
    exposes [charge]

depends [Examples.Fibonacci] → examples/fibonacci.av, call as Examples.Fibonacci.fn(...). depends [Examples.Models.User] → examples/models/user.av, call as Examples.Models.User.fn(...).

Static type checking

Type errors block run, check, and verify. No partial execution. The checker covers function bodies, top-level statements, effect propagation, and duplicate binding detection.

---

What Aver deliberately omits

Absent	Reason
if/else	match is exhaustive — no silent missing cases
for/while	Use map, filter, fold — iteration is data transformation
null	Option<T> with Some/None only
Exceptions	Result<T, E> only — errors are values
Global mutable state	No shared mutable state by design
Closures	All functions are top-level — no captured variables, explicit is better than implicit
Magic	No decorators, no implicit behaviour, no runtime reflection

---

Built-in services

Aver ships built-in namespaces for I/O. All require explicit effect declarations — the typechecker and runtime both enforce this.

Namespace	Effect	Key functions
Console	! [Console]	print, error, warn, readLine
Http	! [Http]	get, post, put, patch, head, delete
HttpServer	! [HttpServer]	listen, listenWith
Disk	! [Disk]	readText, writeText, appendText, exists, delete, deleteDir, listDir, makeDir
Tcp	! [Tcp]	connect, writeLine, readLine, close, send, ping

Pure namespaces (no effects):

Namespace	Key functions
Int	fromString, fromFloat, toString, toFloat, abs, min, max, mod
Float	fromString, fromInt, toString, abs, floor, ceil, round, min, max
String	len, byteLength, charAt, startsWith, endsWith, contains, slice, trim, split, replace, join, chars, fromInt, fromFloat, fromBool, toLower, toUpper
List	len, map, filter, fold, get, push, head, tail, find, any, contains, zip, flatMap
Map	empty, fromList, set, get, has, remove, keys, values, entries, len
Char	toCode (String→Int), fromCode (Int→Option<String>) — not a type, operates on String/Int
Byte	toHex (Int→Result), fromHex (String→Result) — not a type, operates on Int/String

Full API reference: docs/services.md

---

Editor support

Aver ships with a VS Code extension and a Language Server Protocol (LSP) server.

Features

Feature	Description
Syntax highlighting	TextMate grammar — keywords, types, effects, string interpolation, ? descriptions
Diagnostics	Lex, parse, and type errors shown inline. check warnings (missing ?, missing verify) as yellow underlines
Completion	Built-in namespaces (List., Console.), user-defined types (Shape.), user functions, module members — all cross-module
Hover	Full function source (≤12 lines), type definitions, variable types, namespace member signatures
Go-to-definition	Jump to function, type, or binding — works cross-file for module dependencies
Signature help	Parameter hints inside function calls

All features work cross-module — depends [Examples.Redis] is resolved from the workspace root, matching aver run behaviour.

Install

# Build the LSP server
cargo install aver-lang   # installs `aver`
cargo build -p aver-lsp --release
ln -sf $(pwd)/target/release/aver-lsp /usr/local/bin/aver-lsp

# Install the VS Code extension
ln -sf $(pwd)/editors/vscode ~/.vscode/extensions/aver-lang-0.1.0

Open a .av file — the extension activates automatically.

To point at a different binary, set aver.lsp.path in VS Code settings.

---

Getting started

Install from crates.io

cargo install aver-lang

This installs the aver binary. Then:

aver run      examples/calculator.av
aver verify   examples/calculator.av
aver check    examples/calculator.av
aver repl

Build from source

git clone https://github.com/jasisz/aver
cd aver
cargo build --release

cargo run -- run      examples/calculator.av
cargo run -- verify   examples/calculator.av
cargo run -- check    examples/calculator.av
cargo run -- run      examples/services/console_demo.av --record recordings/
cargo run -- replay   recordings/ --test --diff
cargo run -- context  decisions/architecture.av --decisions-only
cargo run -- context  examples/calculator.av
cargo run -- repl

Requires: Rust stable toolchain.

---

Examples

File	Demonstrates
hello.av	Functions, string interpolation, pipe, verify
calculator.av	Result types, match, decision blocks
lists.av	List literals, map / filter / fold
map.av	Typed maps: Map.fromList, Map.set, Map.get, Map.entries
grok_s_language.av	S-expression parser + evaluator (add/sub/mul/div): recursive descent, custom ADT, parse + render + eval
mission_control.av	Space mission simulator: command parser, pure state machine, effectful shell (great with replay)
shapes.av	Sum types, qualified constructors (Shape.Circle), match on variants
user_record.av	Record types, field access, positional match
fibonacci.av	Tail recursion, records, decision blocks
app.av	Module imports via depends [Examples.Fibonacci]
app_dot.av	Dot-path imports (depends [Examples.Models.User])
services/http_demo.av	HTTP service: GET, POST, response handling
services/disk_demo.av	Disk service: full I/O walkthrough
services/console_demo.av	Console service: print, error, warn, readLine
services/tcp_demo.av	TCP persistent connections (Tcp.Connection)
services/weather.av	End-to-end service: HttpServer + Http + Tcp
decisions/architecture.av	The interpreter documents itself in Aver
type_errors.av	Intentional type errors — shows what the checker catches

---

Documentation

Document	Contents
docs/services.md	Full API reference for all namespaces (signatures, effects, notes)
docs/types.md	Key data types (compiler, AST, runtime)
docs/extending.md	How to add keywords, namespace functions, expression types
docs/transpilation.md	Transpilation (aver compile): targets, flags, supported features
docs/decisions.md	Partially generated ADR document from decision blocks

---

Project status

Implemented in Rust with extensive automated test coverage.

• Lexer with significant indentation (Python-style INDENT/DEDENT)
• Recursive-descent parser — hand-written, no libraries
• Static type checker — blocks execution on type errors
• Effect system — statically enforced + runtime call-edge gate
• verify block runner — co-located tests
• decision tooling — queryable ADRs via aver context --decisions-only and docs generation via aver decisions --docs
• List builtins: map, filter, fold, get, head, tail, push, find, any, contains, zip, flatMap
• User-defined sum types (type) and product types (record)
• List pattern matching ([], [h, ..t]), tuple patterns ((a, b), nested)
• Module imports (depends [Examples.Foo], depends [Examples.Models.User])
• AI context export — aver context emits Markdown or JSON
• Interactive REPL — persistent state, multi-line, type-checked
• Built-in services — Console, Http, HttpServer, Disk, Tcp — ! [Effect] enforced everywhere
• Deterministic replay — aver run --record + aver replay for effectful regression testing
• Record update — User.update(u, age = 31)
• Auto-memoization — pure recursive functions with scalar args
• Tail-call optimization — self and mutual recursion
• Effect aliases — effects AppIO = [Console, Disk]
• Map, Char, Byte pure namespaces
• Pipe operator — value |> fn
• Error propagation — expr? on Result values
• String interpolation — "Hello, {name}!"
• Transpilation — aver compile to Rust (all examples, modules, services)
• Compile-time variable resolution
• LSP server — diagnostics, completion, hover, go-to-definition, signature help (cross-module)
• VS Code extension — syntax highlighting + LSP client