Aver

Website | Source

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 + wasip2 (Lean 4 / Dafny via proof export)
Licence: MIT
First seen: February 2026
Maturity: working compiler

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.

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 (additionally lowered to wasip2 / WASI 0.2 Component Model for server-side deployment) — 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 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 (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 (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 (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+.

Tags: language ai verification rust web assembly vm

Last modified 15 June 2026