Aver CLI

May 29, 2026 · View on GitHub

Full toolchain reference for the aver binary. README points here for the per-command surface; deeper topics live in dedicated docs (docs/bench.md, docs/transpilation.md, docs/lean.md, docs/dafny.md, docs/wasm.md, docs/rust.md).

Main commands

Run

aver run file.av
aver run file.av --module-root .
aver run file.av -- arg1 arg2 arg3
  • Aver program args are available through Args.get()
  • --record <dir> records effect traces for replay

Check

aver check file-or-dir --module-root . --deps

check handles static contract diagnostics:

  • missing intent =
  • missing ? descriptions on relevant functions
  • missing verify on pure, non-trivial, non-main functions
  • coverage-style warnings for thin verify examples
  • file size warnings

Warnings do not make check fail.

Verify

aver verify file-or-dir --module-root . --deps
aver verify file-or-dir --wasm-gc

verify runs only declared left => right examples. It fails on:

  • mismatched examples
  • parse/type errors
  • execution errors

It is not a coverage tool.

--wasm-gc (0.17.3+) executes the same cases via the wasm-gc backend instead of the VM — cross-target check that catches divergence between VM and wasm-gc codegen on equality. The host decodes a single Bool per case (wasm-gc lowers == per-type via eq_helpers natively). Failure diagnostics show the actual runtime value for primitive return types (Int/Float/Bool/Str). Trace projections (.trace.*), classified-effect Oracle stubs (given X: Time = stub), and case bodies mentioning BranchPath are rejected upfront with a pointer back to VM verify — those features depend on namespace-value dispatch and runtime override that the wasm-gc backend doesn't have yet.

Format

aver format .
aver format examples
aver format examples --check

format accepts files or directories and walks .av files recursively.

Audit

aver audit file-or-dir --module-root . --deps

audit is the single-shot CI gate that runs all three axes at once:

  1. static checks (same diagnostics as check)
  2. verify execution (same as verify)
  3. format --check (structural compliance)

Output is a flat list of error[slug]: / warning[slug]: lines plus a summary footer: N files | X check errors | Y verify failures | Z format. Any non-zero count fails the command.

  • warnings (e.g. independence-hazard, non-tail-recursion) do not fail the audit — they are advisory
  • errors come from the same machinery as check / verify / format, so slugs are stable and match docs/diagnostics-slugs.md
  • prefer aver audit over chaining check && verify && format --check — it runs the pipeline once and reports everything in one place

Use it before showing a snippet to the user or committing docs examples; it catches illegal ?! usages, match-arm body-on-next-line parse errors, and effect-type mismatches that a naked aver run can miss when the VM short-circuits on the first failure.

--hostile (0.13+) layers adversarial worlds on top of every verify <fn> law block — typed givens get type-boundary values, classified effects get hostile profiles. Failures use the separate slug verify-hostile-mismatch so CI can route declared-world vs adversarial-world regressions to different channels.

Context

aver context file.av --module-root .

Default:

  • --depth auto
  • --budget 10kb

This is the preferred AI discovery workflow:

  1. start with a small budget
  2. inspect the architecture map
  3. look at selection metadata
  4. zoom in only where needed

Examples:

aver context examples/modules/app.av --budget 10kb
aver context projects/workflow_engine/main.av --module-root projects/workflow_engine --budget 24kb
aver context projects/workflow_engine/main.av --module-root projects/workflow_engine --json --budget 24kb --output projects/workflow_engine/CONTEXT.json

Notes:

  • --depth N and --depth unlimited bypass the auto-budget behavior
  • --decisions-only exports only decision blocks
  • selection metadata is printed to stdout and embedded in JSON output

Shape

aver shape file.av
aver shape file.av --summary
aver shape file.av --json
aver shape file.av --lint           # opt-in lint vs aver.toml expectations
aver shape file.av --module-root .

# Corpus mode: pass a directory and `aver shape` walks every .av
# underneath, prints a per-file table + aggregate Kind / Layer /
# archetype distributions, and runs the same --lint check against
# every file in one pass.
aver shape src/
aver shape src/ --summary           # aggregate only, no per-file table
aver shape src/ --json              # NDJSON, one object per file
aver shape src/ --lint              # exit 1 if any file mismatches its expected layer

aver.toml config:

# Per-project layer fingerprints — override the built-in v0 baseline.
[[shape.layer]]
name = "Domain"
match = 40
recursion = 25
pipeline = 0
orchestration = 5
helpers = 30

# Path → expected layer. `--lint` flags mismatches; without these
# entries, `--lint` is a silent no-op.
[[shape.expected]]
glob = "src/parse/**"
layer = "Parse"

Static module-shape analyzer — an architectural smell radar, not a classifier of truth. The histogram is the fact; Kind and Layer are interpretation. Output is auditable: every interpretation comes with the metric that drove it (confidence + margin + top-3 candidates for Layer; the rule that mapped the vector to Kind), so reviewers can decide whether to trust the label.

Three views in one run:

  1. Per-fn archetype — 14 labels (scc-mutual, structural-recursion, match-dispatcher, pipeline-result, manual-result-adapter, renderer-formatter, match-on-value, orchestration, effectful-leaf, let-pipeline, constructor-wrapper, data-as-function, trivial-helper, pure-expression). Multi-label per fn; output lists every label that fires plus a primary pick.
  2. ModuleShape vector + Kind — 5 dims (purity, entry, state_shape, type_surface, api_shape). Kind is a single label projected from the vector: ServiceClient, Orchestration, SmartConstructor, DataModule, PureHelpers, Library, EffectfulLibrary, EffectfulShell. purity is Pure / ClassifiedEffectful (all effects are Oracle one-shot req/resp shape) / ShellEffectful (contains shell/lifecycle effect like HttpServer.listen — Oracle skips by design, not because the classifier doesn't recognize it).
  3. Architectural Layer — Domain | Parse | Command | AiStrategy | RenderUi | Infra by Euclidean distance between the per-module archetype histogram and the fingerprint table. Two metrics: confidence (absolute fit to the best fingerprint) and margin (distance gap to runner-up). Low confidence OR low margin marks the verdict uncertain, with explicit "best: X" wording so the user doesn't read it as a hard label. Runners-up (top-3 closest layers with distances) are always printed so the user sees how decisive the call is. Confidence is penalized on tiny modules (<5 fns capped at 0.2, <10 fns softened by 0.7×).

Verification appears as an orthogonal section — what verify blocks the source carries (Cases, Laws, Trace, Mixed), how many blocks, and per-fn coverage. Static read of the source, doesn't run VM.

Use cases:

  • "What is this module structurally?" — first glance before reading
  • "Does the directory layer match what the histogram looks like?" — architectural lint (full --lint mode + [[shape.expected]] config is the next iteration)
  • LLM context enrichment — Kind + ModuleShape are stable per-module facts worth attaching to AI prompts about that file

Notes:

  • --summary collapses per-fn listing to the header + histogram; same content otherwise
  • --json emits an audit-friendly structure with facts + vector + kind + histogram + layer + fns all side by side, so consumers can pick any layer

Compile

aver compile file.av -o /tmp/out --module-root .
aver compile file.av --target wasm-gc -o /tmp/out
aver compile file.av --target wasm-gc --optimize size -o /tmp/out
aver compile file.av --preset cloudflare --handler handler -o /tmp/out
aver compile file.av --emit-ir-after=PASS
aver compile file.av --explain-passes
  • Default: Rust codegen, emits a modular Cargo project
  • --target wasm-gc: native WebAssembly GC + tail-call output (recommended). Self-contained binary, engine handles GC/recursion, per-instantiation helpers DCE'd to what each program calls. Modern host baseline (Chrome 119+, Firefox 120+, Safari 18.2+, wasmtime 25+, Node 22+).
  • --target wasm: legacy fallback for pre-2024 hosts. Bundles a custom NaN-boxed runtime via wasm-merge.
  • --optimize size|speed: post-process with binaryen -Oz (size) or -O3 (speed).
  • --preset cloudflare --handler <fn>: Cloudflare Workers pack — --target wasm-gc --pack cloudflare, drops worker.js + wrangler.toml next to the wasm. <fn> must have signature Fn(HttpRequest) -> HttpResponse.
  • --emit-ir-after=PASS: print the IR snapshot after the named pipeline stage and exit before codegen. PASS ∈ { parse, tco, typecheck, interp_lower, buffer_build, resolve, last_use, analyze }. diff -u between two stages shows exactly what each pass rewrote.
  • --explain-passes: run the full pipeline (no codegen) and print a per-pass diagnostic report — tail-call conversions, interpolations lowered, fusion sites rewritten + sinks synthesized, slots resolved, last-use markers annotated, alloc/recursion facts. Drives failable-invariant CI checks ("fail if buffer_build no longer fires on the canonical shape", "fail if hot fn loses no-alloc status"). Pair with --json for typed-per-stage shape: {schema_version: 1, passes: [{stage, data: {...stage-specific fields}}, ...]} — buffer_build's data exposes rewrites, synthesized, sinks, rewrites_by_sink; analyze's exposes total_fns, no_alloc_fns, recursive_fns, mutual_tco_members. jq '.passes[] | select(.stage=="buffer_build") | .data.rewrites' instead of regex-parsing summary strings.

Bench

aver bench foo.av                                            # ad-hoc, defaults (30 iter, 3 warmup)
aver bench foo.av --iterations=50 --warmup=5                 # ad-hoc with overrides
aver bench bench/scenarios/fib.toml                          # named manifest
aver bench bench/scenarios/fib.toml --json                   # structured report
aver bench bench/scenarios/                                  # directory mode (every *.toml)
aver bench bench/scenarios/ --json                           # NDJSON
aver bench bench/scenarios/fib.toml --target=wasm-local      # requires --features wasm
aver bench bench/scenarios/fib.toml --target=rust            # native binary, subprocess per iter
aver bench bench/scenarios/fib.toml --save-baseline base.json
aver bench bench/scenarios/fib.toml --compare base.json --fail-on-regression
aver bench bench/scenarios/ --save-baseline bench/baselines/<host>-<arch>-vm.json   # capture baseline (NDJSON)
aver bench bench/scenarios/ --baseline-dir bench/baselines/ --fail-on-regression   # CI gate
  • Three input shapes: .av (ad-hoc, defaults + --iterations / --warmup overrides), .toml (named manifest with per-scenario tolerance + expected shape), directory (globs *.toml).
  • Three targets: vm (default, in-process), wasm-local (wasmtime in-process), rust (native binary).
  • Reports include backend (aver version, build, wasmtime version) and host (os/arch/cpus) so cross-machine runs disambiguate.
  • --save-baseline works in both single-scenario (pretty JSON) and directory (NDJSON) mode. --compare is single-scenario only.
  • --baseline-dir DIR auto-picks <host.os>-<host.arch>-<backend.name>.json from DIR. Silent skip when no matching baseline exists — single workflow gates wherever a baseline is pinned. CI uses this.
  • See docs/bench.md for the full reference.

Proof

aver proof file.av -o /tmp/proof --module-root . --verify-mode auto

Lean export modes:

  • auto
  • sorry
  • theorem-skeleton

Replay

aver replay recordings/ --test --diff

Use replay for effectful debugging and regression capture.

Logic bug

  1. add or tighten a verify
  2. run aver verify ...
  3. fix code
  4. keep the example

Effect bug

  1. run with --record
  2. inspect replay artifact
  3. run aver replay ... --test --diff

Project discovery

  1. aver context <entry> --budget 10kb
  2. if needed, raise budget or target a specific module
  3. only then open raw source files

aver.toml

Project-level config (deployment guardrails + check tweaks):

[effects.Http]
hosts = ["api.example.com", "*.internal.corp"]

[effects.Disk]
paths = ["./data/**"]

[effects.Env]
keys = ["APP_*", "TOKEN"]

[[check.suppress]]
slug = "non-tail-recursion"
files = ["**/eval/**"]
reason = "Tree-walking interpreter — CPS would destroy correspondence."

Effect-host / path / key allowlists narrow which hosts, files, and env keys the runtime will admit. [[check.suppress]] lets a project waive specific lint slugs in specific paths with a reason.