Aver - это статически типизированный язык, предназначенный для написания ИИ и просмотра людьми. Он имеет байт-код VM для запуска кода, Rust backend для развертывания, WASM backend для браузера и встроенных целей и Lean proof export для чистой логики и классифицированных эффективных законов.

Мнение рецензента ИИ о генерируемом коде с каждым годом становится все дешевле. Сертификат, проверенный ядром Lean, сохраняет свою цену. Источник Aver несет обязательства доказательства, и скомпилированный артефакт Wasm-Gc может поставляться с сертификатом коляски, привязанным к его точным байтам. Ядро Lean подписывается на эти гарантии, поэтому они не опираются на кого-то, кто посмотрел код один раз. Сгенерированный код уже поступает быстрее, чем кто-либо может его прочитать, и сертификат остается полезным, когда спот-чеки больше не могут идти в ногу.

Читаемость занимает второе место, и это все еще имеет значение. Рискованная часть написанного ИИ кода обычно не имеет намерения, гораздо чаще, чем плохой синтаксис. Авер делает это намерение явным и машиночитаемым:

• эффекты являются частью подписи функции
• решения живут рядом с кодом, который они объясняют
• чистое поведение живет в смешанных блоках verify

Aver

Aver is a statically typed language designed for AI to write and humans to review. It has a bytecode VM for running code, a Rust backend for deployment, a WASM backend for browser and embedded targets, and Lean proof export for pure logic and classified effectful laws.

An AI reviewer’s opinion of generated code gets cheaper every year. A certificate checked by the Lean kernel keeps its price. Aver source carries proof obligations, and a compiled wasm-gc artifact can ship with a sidecar certificate bound to its exact bytes. The Lean kernel signs off on those guarantees, so they do not rest on someone having looked at the code once. Generated code already arrives faster than anyone can read it, and the certificate is what stays useful when spot-checks can no longer keep up.

Readability comes second, and it still matters. The risky part of AI-written code is usually missing intent, much more often than bad syntax. Aver makes that intent explicit and machine-readable:

• effects are part of the function signature
• decisions live next to the code they explain
• pure behavior lives in colocated verify blocks
• selected effectful behavior can be verified with explicit stubs and trace assertions
• effectful runs can be recorded and replayed deterministically

The toolchain (run / verify / check / audit / why / context / compile / bench / proof / replay) is documented in docs/cli.md. The backends have their own pages: docs/bench.md, docs/transpilation.md, docs/lean.md, docs/effects.md, docs/wasip2.md and docs/rust.md. Compiled wasm-gc modules and wasip2 components can carry a machine-checkable certificate of what their exports compute; see docs/certification.md.

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.