# Aver > Every function carries intent, declared effects, and a colocated verify block. Pure verify blocks export to Lean 4 theorems and Dafny lemmas; effectful ones lift through the Oracle proof export. **Camp:** Verification **Author:** jasisz **Implementation language:** Rust **Compilation target:** bytecode VM, Rust, WebAssembly GC (Lean 4 / Dafny via proof export) **Licence:** MIT **First seen:** March 2026 **Maturity:** working compiler **Site:** https://averlang.dev **Repo:** https://github.com/jasisz/aver **Agent tooling:** - CLAUDE.md - llms.txt ## Key idea Co-locate intent, effects, and verification with the function body. Every function carries a prose intent (?), an effect declaration (!), and a colocated verify block. Pure verify blocks export as Lean 4 theorems and Dafny lemmas; effectful ones lift through Oracle, which quantifies over bounded effect parameters in the exported theorem. ## The thesis. Aver is a verification-camp project that names its target audience explicitly: the reviewer, not the generator. Every function carries a prose intent (`? "..."`), an effect declaration (`! [Console.print]`), and a colocated `verify` block of `expression => expected` cases. Pure verify blocks export as Lean 4 theorems or Dafny lemmas through `aver proof --backend lean|dafny`; effectful functions get the same treatment via Oracle, which lifts classified effects (`Random`, `Http`, `Disk`, `Time`, `Console.readLine`, ...) into proof artefacts as explicit function parameters typed with bounded subtypes (`RandomFloatInUnit`). The exported theorem quantifies over every possible such function, not just the one the test stub provided. Architectural choices are first-class syntax: `decision UseResultNotExceptions { chosen = "Result", rejected = ["Exceptions"], ... }`.

Code is cheap to generate. Expensive to trust.

The distinctive move shows up in the comparison with Vera. The two share design DNA — mandatory verification artefacts, explicit effects, no `if`/`else`, no closures, no exceptions, no nulls, no loops — but disagree on what to drop. Vera drops names entirely via De Bruijn slot references (`@Int.0`). Aver keeps names and makes the surrounding metadata mandatory. Vera's bet is that names are the failure mode; Aver's is that absence of intent is. ## What it looks like. 
fn safeDivide(a: Int, b: Int) -> Result<Int, String>
    ? "Safe integer division. Returns Err on zero."
    match b
        0 -> Result.Err("Division by zero")
        _ -> Result.Ok(a / b)

verify safeDivide
    safeDivide(10, 2) => Result.Ok(5)
    safeDivide(7, 0)  => Result.Err("Division by zero")

Prose intent (?), no if/else, and a colocated verify block. The function ships its specification.

## Distinctive moves. - **Mandatory intent.** Every function carries a `?` prose description directly after the signature. Functions with effects but no description warn. - **Effects as type signatures.** `! [Http.get]` declares a specific capability; `! [Http]` covers the namespace. Violations are type errors, with `aver.toml` constraining which hosts and paths are reachable. - **Verify, then prove.** The same `verify` block runs as sampled cases (`aver verify`), adversarial-profile checks (`aver verify --hostile`), or as a Lean 4 / Dafny export (`aver proof`). The four readings can disagree on identical source — the Oracle page walks one through. - **Oracle for effectful code.** Classified effects are lifted into proof artefacts via `BranchPath` and per-branch counters; the theorem quantifies over them universally. - **`aver context` for agents.** Token-budgeted export of types, effects, and intents (`--budget 10kb`), designed to fit an LLM window. - **Decisions as syntax.** `decision` blocks make ADRs queryable from the codebase, not from a wiki. ## Maturity. v0.21 on crates.io (`cargo install aver-lang`), MIT-licensed, written in Rust, primary author `jasisz`. Three backends: a bytecode VM, native Rust codegen, and a standalone WASM-GC target — the site demonstrates the latter with seven games compiled directly to WebAssembly GC, including Snake at 4.3 KiB and a roguelike at 25.6 KiB on Chrome 119+/Firefox 120+/Safari 18.2+. Proof export targets Lean 4 (via `lake build`) and Dafny. The GitHub repository is small (6 commits visible at time of cataloguing) but the toolchain surface is wide and functional. The bet is that the same source can serve as implementation and reviewable specification, with proof export as the upper-bound check. ## Agent tooling. The site publishes `llms.txt` at averlang.dev/llms.txt — a long-form crib sheet covering syntax, the `=>` separator (vs `=`), constructor qualification (`Result.Ok`, never bare `Ok`), and a numbered list of the most common LLM mistakes. `CLAUDE.md` and a `.claude/skills/` directory ship in the repo. The `aver context` command exports a token-budgeted slice of the codebase. Diagnostics ship with structured hints (`Hint: add ! [Console.print]`); the playground renders the same diagnostics live. ## Design DNA - **[Vera](https://agentlanguages.dev/languages/vera.md)** *(Verification)* — Closest design relative. Both ship mandatory verification artefacts, explicit effects, no if/else, no exceptions. Vera drops variable names entirely (@Int.0); Aver keeps names and makes the surrounding metadata mandatory. Aver became the first non-Python/TS baseline integrated into VeraBench, described in the bench README as ‘a Haskell-inspired language with zero LLM training data.’ - **[Prove](https://agentlanguages.dev/languages/prove.md)** *(Verification)* — Same camp, opposite politics. Both ship contracts and explicit effects; Aver ships an llms.txt and welcomes AI authoring, Prove ships an anti-training licence that prohibits training use of source. - **[Pact](https://agentlanguages.dev/languages/pact.md)** *(Verification)* — Adjacent design DNA. Both treat intent and effects as declarations on every function (Aver's ? and ![Effect]; Pact's intent and needs db). Aver pushes proof export; Pact pushes built-in SQLite and HTTP. ## Timeline - **Apr 2026** — First external language integrated into VeraBench as a baseline alongside Python and TypeScript — described in the bench README as ‘a Haskell-inspired language with zero LLM training data, providing a second data point alongside Vera for the zero-training-data thesis.’ - **May 2026** — v0.21 published on crates.io. Oracle proof export to Lean 4 and Dafny stabilises. Seven games shipped to WASM-GC (Snake at 4.3 KiB, Doom at 20.4 KiB, roguelike at 25.6 KiB) on Chrome 119+/Firefox 120+/Safari 18.2+. --- HTML version: https://agentlanguages.dev/languages/aver/ Catalogue index: https://agentlanguages.dev/llms.txt Catalogue homepage: https://agentlanguages.dev/index.md