aver

A programming language for code written with AI.

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

Function descriptions, effect sets, verify blocks, architecture decisions, and certificate obligations are language constructs. The wasm-gc backend can emit behavioral certificates checked by the standalone verifier.

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: public API, function descriptions, concrete cases, and a 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 states the purpose, exposes names the public API, and effects [] keeps it pure.

  2. 07—17

    Descriptions + patterns

    Both typed functions carry a ? description and exhaust lists with explicit patterns.

  3. 19—21

    Concrete cases

    The ordinary verify block fixes empty and non-empty behavior for combine.

  4. 23—26

    Named law

    Three values for each input produce nine checked pairs for combinePreservesTotal.

Read the source Open cart.av ↗

Give it to an agent Read llms.txt ↗

02 / DESIGN POSITION

Deliberate omissions.

The language does not include the following constructs; each 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 stay in signatures and values.

D.03 No if / else

Exhaustive match; a missing case is a compiler concern.

D.04 No mutable bindings

Values do not change behind the reader’s back.

D.05 No closures

Top-level functions; inputs are visible rather than captured.

D.06 No async runtime

Independent products express parallel work without hidden scheduling syntax.

D.07 No loops

Recursion, pattern matching, and tail-call optimization.

D.08 No runtime magic

No decorators, reflection, or implicit behavior.

03 / TOOLCHAIN

Check, verify, prove, compile.

The main source-analysis and build commands, in order.

01

aver check

Static checks

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

02

aver verify

Source verification

Colocated examples and laws become executable regression evidence.

03

aver proof

Proof export

Lean and Dafny backends carry selected laws beyond example checking.

04

aver compile

Artifact compilation

Deploy through Rust or WebAssembly; certify supported wasm-gc artifacts.

$ 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, Lean, and Dafny ↗

04 / ABC

Artifact Behavioral Certificates.

A certificate states what selected exports of one WebAssembly module compute. Verification binds accepted claims to the supplied bytes and to a checker-owned statement schema.

BEHAVIORAL PROOF / FAIL CLOSED

Verifier independence.

  • Identity

    The .wasm file passed to aver-cert is validated, hashed, and encoded for Lean.

  • Authority

    The checker owns the statement schema, soundness wall, toolchain, and fresh witness.

  • Scope

    Unsupported exports are declined explicitly; no claim is made 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.32 / 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.32 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 behavioral proof, not a signature or reproducible-build attestation.

Read the ABC record ↗ Source guide ↗ Architecture source ↗

05 / BUILD LEDGER

WebAssembly GC examples.

Eight browser programs emitted directly from Aver source.

Program Artifact size Open
Wumpus7.9 KiBRun ↗ Snake8.2 KiBRun ↗ Game of Life12.3 KiBRun ↗ Tetris13.2 KiBRun ↗ Egg Catch15.7 KiBRun ↗ Doom28.2 KiBRun ↗ Checkers28.8 KiBRun ↗ Roguelike33.3 KiBRun ↗

Size bars are relative to the largest artifact in this set. Modern WebAssembly GC browser required.

06 / PROJECT NOTE

“This is not a language optimized for humans to type by hand all day. It is optimized for AI to generate code that humans can inspect, constrain, test, and ship.”

— 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 bundled example.

--features wasm enables WebAssembly GC and ABC production. Independent ABC verification uses aver-cert and requires Elan for its pinned Lean 4.32 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 ↗