cli.md

Aver CLI

Full toolchain reference for the aver binary. README points here for the per-command surface; deeper topics: bench, transpilation, Lean, Dafny, effects, WASI 0.2, and Rust.

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 wasip2 -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. 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+, Cloudflare Workers).
• --target wasip2: WASI 0.2 / Component Model output for wasmtime and other component hosts. It wraps the wasm-gc core with wit-component; see docs/wasip2.md for the supported effect surface.
• --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, escape, build_symbols, name_resolve, refinement_lower, contract_lower, law_lower }. 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.

Artifact certificates

aver compile app.av --target wasm-gc --certify -o out/
aver-cert verify out/app.wasm out/cert
aver-cert check out/app.wasm out/cert
aver-cert explain out/app.wasm out/cert
aver cert verify out/app.wasm out/cert
aver cert check out/app.wasm out/cert
aver cert explain out/app.wasm out/cert

--certify emits a version-1 artifact certificate for admitted exports of the exact wasm-gc module. Install aver-cert separately; it is an independently versioned verifier using Lean 4.32. A crates.io compiler install needs the backend enabled: cargo install aver-lang --features wasm. Verification also requires a standard Elan installation for the pinned toolchain.

check is the faster development preflight. It trusts the freshly built or explicitly cached .olean closure, skips the final leanchecker --fresh replay, and prints CHECKED, never CERTIFIED. Use strict verify for release or admission gates.

aver cert ... is only a subprocess shortcut. It forwards the original arguments, standard streams, and exit status to a sibling aver-cert binary or one on PATH; aver contains no linked verification fallback. explain performs the same full check as verify before printing the report, and inspect is an alias of explain.

This command is different from aver verify: source verify runs examples, whereas aver cert verify kernel-checks a behavioral certificate for compiled WebAssembly. See the certificate guide and architecture for the admitted families and trust boundary.

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-gc         # embedded wasmtime, requires --features wasm
aver bench bench/scenarios/fib.toml --target=wasm-gc-v8      # the same bytes under Node/V8
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).
• Four targets: vm (default, in-process), wasm-gc (wasmtime in-process), wasm-gc-v8 (Node/V8 subprocess), and 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 the benchmark guide for the full reference.

Proof

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

Lean export modes:

• auto
• sorry
• theorem-skeleton

--check builds the export with lake and gates on the result (--check-json for a machine-readable summary); --gate <baseline> / --write-baseline are the proof ratchet; --minimize (Lean, implies --check) collapses each auto-proof to the single tactic that actually closed it. See docs/lean.md for the proof workflow, the --check summary fields, and --minimize.

Replay

aver replay recordings/ --test --diff

Use replay for effectful debugging and regression capture.

Recommended workflows

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.