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.34 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 shared bound covering established connections, accepted connections and in-flight dials.

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 =
        "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 part of the language syntax and sit next to the code they explain.

Query only the decision history for a module graph:

aver context decisions/architecture.av --decisions-only

impacts, chosen, and rejected accept either validated symbols or quoted semantic labels.

Context export

aver context examples/core/calculator.av

Aver walks the dependency graph and emits a compact context summary: module intent, public signatures, effect declarations, verify samples and decisions. It exports the contract-level view that another human or LLM needs first, instead of dumping the whole source tree.

By default, aver context uses --depth auto --budget 10kb with priority scoring: elements with more verify coverage, spec references and decisions are included first. --depth N and --depth unlimited bypass that budget. Long verify examples are skipped so they do not bloat the artifact.

Use --focus <symbol> to build context around one function. Its callees, types, verify blocks and decisions get priority within the budget:

aver context examples/data/json.av --focus fromString

The token budget becomes a way to navigate. Another human or model can start with a small architecture map, zoom into the modules that matter, or focus on one function's dependency cone.

If you want a larger export for a medium project, raise the budget explicitly:

aver context projects/workflow_engine/main.av \
  --module-root projects/workflow_engine \
  --json \
  --budget 24kb \
  --output projects/workflow_engine/CONTEXT.json

When --output is used, Aver also prints a short selection summary to stdout, for example:

mode auto, included depth 2, used 22622b, budget 24kb, truncated, next depth 3 would use 40739b

JSON output embeds the same selection metadata, so you can see whether the export stopped because of the budget.

Example shape:

## Module: Calculator
> Safe calculator demonstrating Result types, match expressions, and co-located verification.

### `safeDivide(a: Int, b: Int) -> Result<Int, String>`
> Safe integer division. Returns Err when divisor is zero.
verify: `safeDivide(10, 2)` → `Result.Ok(5)`

## Decisions
### NoExceptions (2024-01-15)
**Chosen:** Result — **Rejected:** Exceptions, Nullable

Verify

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 stay next to the function they cover. aver check treats a missing verify block on a pure, non-trivial, non-main function as a contract error.

Regular verify:

verify add
    add(1, 2) => 3
    add(0, 0) => 0

Law verify:

verify add law commutative
    given a: Int = -2..2
    given b: Int = [-1, 0, 1]
    add(a, b) => add(b, a)

verify ... law ... is deterministic and does no random sampling. Its cases are the cartesian product of explicit domains, capped at 10_000.

For the proof-oriented style where a law relates an implementation to a pure spec function, see docs/language.md and docs/lean.md.

Oracle laws for classified effects:

fn fairDie(path: BranchPath, n: Int, min: Int, max: Int) -> Result<Int, String>
    ? "Deterministic Random.int stub."
    Result.Ok(4)

fn pickOne() -> Int
    ? "Rolls once."
    ! [Random.int]
    Random.int(1, 6)

verify pickOne law usesOracle
    given rnd: Random.int = [fairDie]
    Result.Ok(pickOne()) => rnd(BranchPath.Root, 0, 1, 6)

verify <fn> law <name> is the proof-oriented Oracle form. aver proof lifts the effectful function to a pure function with explicit oracle parameters and can emit a universal theorem over that oracle. For runtime assertions over .result and .trace.*, such as trace.contains(Random.int(1, 6)), use the cases form verify <fn> trace. See docs/oracle.md for the full model.

Replay

Use deterministic replay for stateful, interactive, or external effectful code:

1. run once against real services and record the effect trace
2. replay offline with no real network, disk, or TCP calls
3. use --diff and --test to turn recordings into a regression suite

aver run    examples/services/console_demo.av --record recordings/
aver replay recordings/rec-123.json --diff
aver replay recordings/ --test --diff

# Same flow under wasm-gc — recordings are interchangeable across the
# VM, self-host, and wasm-gc backends.
aver run    examples/services/console_demo.av --wasm-gc --record recordings/
aver replay recordings/rec-123.json --wasm-gc

Use Oracle laws when classified effects should become proof obligations over explicit stubs. Use verify <fn> trace when you need runtime assertions over .result or .trace.*. Use replay when the flow depends on ambient state, persistent TCP sessions, terminal modes, or server callbacks.

---

Common commands

aver check   file.av
aver run     file.av
aver verify  file.av
aver context file.av
aver compile file.av -o out/
aver compile file.av --target wasm-gc --certify -o out/
aver compile file.av --target wasip2 --certify -o out/
aver cert check out/file.wasm out/cert
aver cert verify out/file.wasm out/cert
aver cert verify out/file.component.wasm out/cert
aver cert explain out/file.wasm out/cert

The full per-command reference, including flags, replay, formatting, the REPL and the audit / why / proof / bench commands, is in docs/cli.md. check, verify and audit walk the whole program (the entry plus every module it reaches through depends [...]) and report per module. aver verify --wasm-gc runs the same cases through the wasm-gc backend as a cross-target check.

Command	What it checks	Use as a gate?
aver check	Source contracts and static diagnostics	Source-quality gate
aver verify	Declared source examples	Regression gate
aver cert check	Fast certificate preflight using the built or trusted-cache .olean closure	Development only (CHECKED)
aver cert verify	Exact artifact certificate with final fresh replay	Release/admission gate (CERTIFIED)

aver-cert runs as an independent process. aver cert ... forwards to that binary, so no verifier is linked into the compiler. docs/certification.md describes the certificate package format and schema version 1.

---

Language and runtime

Aver is small on purpose. The core model:

• immutable bindings only
• match instead of if/else
• Result and Option instead of exceptions and null
• top-level functions only, with no closures
• explicit method-level effects
• module-based structure via module, depends, and exposes
• automatic tail-call optimization for eligible code

For the surface-language guide, see docs/language.md.

For constructor rules and edge cases, see docs/constructors.md.

For namespaces, effectful services, and the standard library, see docs/services.md.

Execution and proof backends

Aver has three backend paths:

• VM-based workflow for run, check, verify, replay, and context
• Rust compilation for generating a native Cargo project with aver compile
• Lean proof export for pure core logic, Oracle-lifted classified effectful laws, and verify / verify law obligations with aver proof. Supported law shapes become real universal theorems. The rest stay as executable samples or checked-domain theorems and are never presented as proofs.

The VM and generated Rust share runtime behavior through aver-rt. List teardown, deep append -> match paths and string helpers such as String.slice live there on purpose, so one runtime fix improves both execution paths.

Typical Rust flow:

aver compile examples/core/calculator.av -o out/
cd out
cargo run

Typical Lean flow:

aver proof examples/formal/law_auto.av --verify-mode auto -o out/
cd out
lake build

Rust is the deployment backend. Lean is the proof backend: it handles verify cases via native_decide and supported verify law shapes via tactic strategies that the Lean kernel checks.

For backend-specific details, see:

• docs/rust.md for Cargo generation and deployment flow
• docs/lean.md for proof export, formal-verification path, and current Lean examples
• docs/oracle.md for Oracle laws, classified-effect stubs, and trace assertions

---

Examples

Shared examples under examples/ resolve from --module-root examples. They are grouped by role:

• core/ for language and syntax tours
• data/ for pure data structures and parsers
• formal/ for Lean-oriented proof examples
• modules/ for import and module-root examples
• services/ for effectful adapter demos
• apps/ for small multi-file applications under the shared examples root
• games/ for interactive terminal games (Snake, Tetris, Braille Doom)

Standalone multi-file showcase projects live under projects/ and use their own local module roots.

Repository layout rule:

• files under examples/ share one root: --module-root examples
• each folder under projects/ is its own root, for example --module-root projects/workflow_engine

Typical commands:

aver check examples/modules/app.av --module-root examples
aver check projects/workflow_engine/main.av --module-root projects/workflow_engine
aver check projects/payment_ops/main.av --module-root projects/payment_ops

Curated shared examples:

File	Demonstrates
core/hello.av	Functions, string interpolation, verify
core/calculator.av	Result types, match, decision blocks
core/shapes.av	Sum types, qualified constructors (Shape.Circle), match on variants
data/fibonacci.av	Tail recursion, records, decision blocks
formal/law_auto.av	Lean proof export, verify law, conservative universal auto-proofs plus sampled/domain fallback
formal/spec_laws.av	Implementation-vs-spec laws (verify foo law fooSpec) and Lean spec theorems for supported shapes
formal/oracle_trace.av	Oracle laws and trace assertions for classified effects with explicit stubs
apps/mission_control.av	Command parser, pure state machine, effectful shell
games/wumpus.av	Hunt the Wumpus: cave exploration, match-driven control flow
modules/app.av	Module imports via depends [Data.Fibonacci]
services/console_demo.av	Console service and replay-friendly effectful flow
services/http_demo.av	HTTP service with sub-effects: Http.get, Http.post
services/weather.av	End-to-end service: HttpServer + Http + Tcp
apps/notepad/app.av	Multi-file HTTP app under the shared examples module root
games/snake.av	Terminal Snake: immutable state, TCO game loop, Terminal service
games/tetris/main.av	Modular Tetris: sum types, 2D grid, collision, line clearing (4 modules, 66 verify cases)
games/checkers/main.av	Checkers with alpha-beta AI: cursor UI, forced capture, decision trace (5 modules, 144 verify cases)
games/doom/main.av	Braille Doom: raycasting FPS with Unicode Braille rendering, procedural levels, 3 enemy types with AI, shooting, wall textures (7 modules)
core/test_errors.av	Intentional aver check failures: type errors + verify/decision/effect diagnostics

Standalone projects:

File	Demonstrates
projects/workflow_engine/main.av	Explicit app/domain/infra flow, event replay, derived events, verify-driven orchestration
projects/payment_ops/main.av	Dirty payment backoffice flow: provider normalization, replay, settlement reconcile, manual-review cases, audit trail
self_hosted/main.av	Full self-hosted interpreter: lexer, parser, resolver, evaluator. All 55 examples pass. Compiles to native via aver compile and powers aver run --self-host.

See examples/ and projects/ for the full set. For repository self-documentation via decision exports, see decisions/architecture.av.

---

Documentation

Document	Contents
docs/language.md	Surface-language guide: syntax, semantics, modules, and deliberate omissions
docs/formatting.md	Formatter behavior and guarantees
docs/constructors.md	Constructor rules and parsing contract
editors/README.md	VS Code + LSP setup and Sublime Text support
docs/services.md	Full API reference for all namespaces (signatures, effects, notes)
docs/oracle.md	Oracle: effectful laws, trace assertions, and proof export for classified effects
docs/vm.md	Bytecode VM design note: execution model, NanValue, opcodes, effects
docs/types.md	Key data types (compiler, AST, runtime)
docs/extending.md	How to add keywords, namespace functions, expression types
docs/transpilation.md	Overview of aver compile and aver proof
docs/rust.md	Rust backend: deployment-oriented Cargo generation
docs/effects.md	Effect support across the VM, wasm-gc, and wasip2 targets
docs/wasip2.md	WASI 0.2 / Component Model target and host compatibility
docs/lean.md	Lean backend: proof export and formal-verification path
docs/certification.md	Artifact behavioral certificates: commands, guarantees, admitted families, and limits
docs/certification-architecture.md	Certificate data flow, checker ownership, and trust boundary
docs/certificate-format.md	Normative certificate format reference for independent verifier reimplementors, with the trust inventory and the versioning and freeze policy
docs/independence.md	Independent products: the semantic model behind ?! and !
docs/research.md	Narrow related work for effects, Oracle, independent products, and proof targets
docs/pushback.md	Common pushback: questions, objections and answers
docs/decisions.md	Decision export generated via aver context --decisions-only