aver

A programming language for code written with AI.

Source language · Bytecode VM · Rust · WebAssembly GC · Lean 4.34

Function descriptions, effect sets, verify blocks, architecture decisions and certificate obligations are part of the language. The wasm-gc backend can emit behavioral certificates, which a standalone verifier checks.

Agent referencellms.txt ↗

Try in browser ↗ Read the source example ↓
LANGUAGE SURFACE
  • ? intent
  • ! effects
  • verify
  • artifact cert

01 / SOURCE

Cart totals.

A complete pure module with a public API, function descriptions, concrete cases and one law checked over nine input pairs.

cart.av 26 lines / complete module
01module Cart
02intent =
03"Cart operations and the total they preserve."
04exposes [cartTotal, combine]
05effects []
06 
07fn cartTotal(items: List<Int>) -> Int
08? "Sum the prices in a cart."
09match items
10[] -> 0
11[price, ..rest] -> price + cartTotal(rest)
12 
13fn combine(a: List<Int>, b: List<Int>) -> List<Int>
14? "Put cart b's items after cart a."
15match a
16[] -> b
17[x, ..rest] -> List.prepend(x, combine(rest, b))
18 
19verify combine
20combine([], [1, 2]) => [1, 2]
21combine([3, 4], [1, 2]) => [3, 4, 1, 2]
22 
23verify cartTotal law combinePreservesTotal
24given a: List<Int> = [[], [5], [3, 4]]
25given b: List<Int> = [[], [10], [1, 2]]
26cartTotal(combine(a, b)) => cartTotal(a) + cartTotal(b)
  1. 01—05

    Module contract

    intent says what the module is for. exposes lists the public API. effects [] means the module is pure.

  2. 07—17

    Descriptions + patterns

    Both functions have a ? description and cover every list shape with explicit patterns.

  3. 19—21

    Concrete cases

    A plain verify block pins what combine does with an empty and a non-empty list.

  4. 23—26

    Named law

    Three values per input give nine pairs, and combinePreservesTotal is checked on each.

Read the source Open cart.av ↗

Give it to an agent Read llms.txt ↗

02 / DESIGN POSITION

Deliberate omissions.

Aver leaves these constructs out. Each one has an explicit replacement.

Ref. Absent Replacement
D.01 No null

Option<T> with explicit Some and None.

D.02 No exceptions

Result<T, E>. Errors show up in signatures and values.

D.03 No if / else

Exhaustive match. The compiler reports a missing case.

D.04 No mutable bindings

A value never changes behind the reader’s back.

D.05 No closures

Top-level functions. Every input is passed in where you can see it.

D.06 No async runtime

Parallel work is written as independent products. There is no hidden scheduling syntax.

D.07 No loops

Recursion and pattern matching, with tail-call optimization.

D.08 No runtime magic

No decorators, no reflection, no implicit behavior.

03 / TOOLCHAIN

Check, verify, prove, compile.

The main commands for analysing and building source, in the order you run them.

01

aver check

Static checks

Types, descriptions, module intent, effect propagation and diagnostics.

02

aver verify

Source verification

Examples and laws written next to the code run as regression checks.

03

aver proof

Proof export

The Lean backend takes selected laws past example checking.

04

aver compile

Artifact compilation

Deploy through Rust or WebAssembly. Supported wasm-gc artifacts can also be certified.

$ aver check payment.av

effect-violation ‘charge’ calls ‘Http.post’ but does not declare it.

hint / add ! [Http.post] to the function contract Open example ↗

Case study The randomness paradox: verify, hostile mode, and Lean ↗

04 / ABC

Artifact Behavioral Certificates.

A certificate states what selected exports of one WebAssembly module compute. Verification ties each accepted claim to the supplied bytes and to a statement schema that the checker owns.

BEHAVIORAL PROOF / FAIL CLOSED

Verifier independence.

  • Identity

    aver-cert validates the .wasm file it is given, hashes it and encodes it for Lean.

  • Authority

    The statement schema, soundness wall, toolchain and fresh witness all belong to the checker.

  • Scope

    Unsupported exports are declined explicitly. The certificate makes no claim about them.

AVER / ABC RECORD FORMAT 1 · SCHEMA 2
Subject
out/app.wasm
Byte binding
SHA-256 / checker recovered
Verifier
aver-cert / independent process
Kernel
Lean 4.34 / pinned wall
Accepted scope
selected admitted exports
STRICT VERDICT CERTIFIED
INPUT / 01 actual app.wasm validated + hashed
INPUT / 02 cert/ package Plans.lean / authoritative plan data
CHECKER aver-cert + Lean 4.34 checker-owned statement and wall
OUTPUT CERTIFIED or decline
01aver compile app.av --target wasm-gc --certify -o out/
02aver-cert verify out/app.wasm out/cert

Precise limit: this is a behavioral proof. It is not a signature and not a reproducible-build attestation.

Read the ABC record ↗ Source guide ↗ Architecture source ↗

05 / BUILD LEDGER

WebAssembly GC examples.

Eight browser programs, compiled straight from Aver source.

Program Artifact size Open
Wumpus9.2 KiBRun ↗ Snake9.3 KiBRun ↗ Game of Life14.0 KiBRun ↗ Tetris14.7 KiBRun ↗ Egg Catch16.5 KiBRun ↗ Doom31.5 KiBRun ↗ Checkers32.4 KiBRun ↗ Roguelike37.4 KiBRun ↗

Size bars are relative to the largest artifact in this set. You need a recent browser with WebAssembly GC.

06 / PROJECT NOTE

“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.”

— Aver README

Documents and discussion.

ABCArtifact Behavioral Certificate ↗ The randomness paradoxVerify, hostile mode, and proof ↗ Finding Aver’s grandfatherACL2 and an executable paper bug ↗ Aver ManifestoLong-form position ↗ Common PushbackObjections and limits ↗ Happy Path Programming #120Conversation ↗ Language GuideSurface reference ↗

07 / INSTALL

Install Aver.

Install the released compiler from crates.io, then run and verify the example that ships with it.

--features wasm turns on WebAssembly GC output and ABC production. To check an ABC independently you need aver-cert, plus Elan for its pinned Lean 4.34 toolchain.

01cargo install aver-lang --features wasm
02cargo install aver-cert
03aver run examples/core/hello.av
04aver verify examples/core/hello.av
aver-lang on crates.io ↗ aver-cert on crates.io ↗ Build from source ↗