diff --git a/README.md b/README.md
index 14cc005..f953349 100644
--- a/README.md
+++ b/README.md
@@ -73,6 +73,7 @@ This repo contains a list of languages that currently compile to or have their V
- [Wonkey](#wonkey)
- :egg: - Work in progress.
+ - [Aver](#aver)
- [Ballerina](#ballerina)
- [BASIC](#basic)
- [Co](#co)
@@ -133,6 +134,12 @@ This repo contains a list of languages that currently compile to or have their V
--------------------
+### Aver [top⇈](#contents)
+> Aver is a statically typed language designed for AI-assisted development. Every function carries optional prose intent, effects are tracked in the type system, and verify blocks act as executable specs.
+* [Aver](https://github.com/jasisz/aver) - compiles to standalone `.wasm` modules with typed ABI (Int→i64, Float→f64, Bool→i32, heap types→i32 ptr). Supports own `aver/*` import ABI for custom hosts, `--adapter wasi` for standalone wasmtime, and a built-in browser runner. Also compiles to native Rust and exports to Lean 4 proofs.
+
+--------------------
+
### Ballerina [top⇈](#contents)
> Ballerina is an open-source programming language for the cloud that makes it easier to use, combine, and create network services.
> The WebAssembly compiler is implemented for the native Ballerina compiler [nBallerina](https://github.com/ballerina-platform/nballerina).