# Aver

A statically typed programming language designed for AI models to write and humans to review, with a Lean-checked certificate of proof obligations attached to compiled code.

Aver is a programming language built around the idea that AI-generated code arrives faster than anyone can read it, so a checkable certificate matters more over time than a one-time human review. Aver source makes effects part of a function's signature, keeps decisions next to the code they explain, and separates pure logic in colocated verify blocks so behavior can be checked rather than only read.

It has a bytecode virtual machine, a Rust backend for deployment, a WebAssembly backend for browsers and embedded targets, and exports proofs to the Lean theorem prover for pure logic and classified effectful behavior; a compiled WebAssembly module can ship with a sidecar certificate bound to its exact bytes and signed off by the Lean kernel. Its toolchain covers running, verifying, checking, auditing, compiling, benchmarking and replaying a program, and a command can wire an AI coding assistant to write Aver by installing skill files describing the language and toolchain.

Website: https://averlang.dev