Aver.

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 provocative move appears against 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”)

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.