# Aver — Deep Documentation Index > Start with [`llms.txt`](https://averlang.dev/llms.txt). This file goes deeper. It documents the full toolchain and points to the language docs, examples and implementation notes. ## Recommended read order 1. [`llms.txt`](https://averlang.dev/llms.txt) for syntax guardrails and the minimal working shape of an Aver file 2. [Language Guide](https://github.com/jasisz/aver/blob/main/docs/language.md) for the full surface-language contract 3. [Services (stdlib)](https://github.com/jasisz/aver/blob/main/docs/services.md) for stdlib and effect namespaces 4. one or two raw `.av` examples close to your task 5. [`AGENTS.md`](https://github.com/jasisz/aver/blob/main/AGENTS.md) only if you need repository internals or implementation details ## Primary docs - [Language Guide](https://github.com/jasisz/aver/blob/main/docs/language.md): complete surface-language reference - [Services (stdlib)](https://github.com/jasisz/aver/blob/main/docs/services.md): every namespace and its API - [Common Pushback](https://github.com/jasisz/aver/blob/main/docs/pushback.md): questions, objections and answers ## Advanced topics - [Independence (`?!`)](https://github.com/jasisz/aver/blob/main/docs/independence.md): parallel products - [Constructors](https://github.com/jasisz/aver/blob/main/docs/constructors.md): constructor routing rules - [Oracle](https://github.com/jasisz/aver/blob/main/docs/oracle.md): proof export for classified effectful functions via `verify fn trace` and `given` stubs, plus `--hostile` - [Lean proof export](https://github.com/jasisz/aver/blob/main/docs/lean.md): verify blocks to Lean 4 - [Effect and wasm-gc support](https://github.com/jasisz/aver/blob/main/docs/effects.md): browser and host surface - [WASI 0.2 target](https://github.com/jasisz/aver/blob/main/docs/wasip2.md): Component Model deployment ## Canonical examples - [Hello](https://github.com/jasisz/aver/blob/main/examples/core/hello.av): minimal pure file - [Calculator](https://github.com/jasisz/aver/blob/main/examples/core/calculator.av): verify on basic arithmetic - [Independent Fan-out](https://github.com/jasisz/aver/blob/main/examples/core/independent_fanout.av): `!` / `?!` independent products - [Quicksort](https://github.com/jasisz/aver/blob/main/examples/data/quicksort.av): recursion and verify on a recursive algorithm - [Oracle Trace](https://github.com/jasisz/aver/blob/main/examples/formal/oracle_trace.av): `verify fn trace` with `given` stubs for classified effects ## Toolchain ## Main commands ### Run ```bash aver run file.av aver run file.av --module-root . aver run file.av -- arg1 arg2 arg3 aver run file.av --module-root . --wasip2 ``` - Aver program args are available through `Args.get()` - `--record ` records effect traces for replay - `AVER_YIELD_DUMP=1` (env var, read by any door that type-checks a program) prints the generated Aver for every lowered process to stderr. Use it to debug the state types, request/outcome sums and answer functions it built. - A file names a program: the entry module, everything it reaches through `depends [...]`, and the `[providers]` bindings of the project's `aver.toml`. When the program reaches a capability that `aver.toml` binds to a Rust package, `run` builds that provider host once and reuses it from the cache afterwards. The first build says which packages it links and where they come from. With `--wasip2` it adapts the WIT-lowerable bindings to Component Model imports, while `--wasm-gc` adapts the complete provider value vocabulary through the contract-derived raw ABI. `--self-host` has no provider host and refuses such a program with `error[capability-provider-unhosted]`. A project without `[providers]` never invokes Cargo ### Check ```bash aver check file-or-dir --module-root . ``` `check` reports every module of the program (the entry plus everything it reaches through `depends [...]`), leaves first, with one `Check:` section per module. A directory is the union of the programs rooted at each file, and each module is reported once. Embedded standard modules are typed but not reported. Any module with an error fails the command. `check` handles static contract diagnostics: - missing `intent =` - missing `?` descriptions on relevant functions - missing `verify` on pure, non-trivial, non-`main` functions (`error[missing-verify]`; answer functions and seam functions count as such functions). A function is exempt when a parameter has no value a verify case can write: a capability resource such as `Tcp.Connection` or `Work.Job`, or a tuple, record or sum of the same module that always carries one - coverage-style warnings for thin `verify` examples - file size warnings - exposed names that nothing in the checked program imports (`unused-expose`). A directory input judges exposes over every program in it, and a single file only over its own program, so a name used only by a sibling program outside the input is reported. What only the generated loop reaches (an answer module's functions, a job kind's `begin` and `take`, the seam) is not an import, so leave those out of `exposes` Warnings do not make `check` fail. `missing-verify` is an error and does. Below each module's summary line, `check` lists the module's processes, one line each with what made it a process: `process loop: requests Pool.claim, answered by Pooled`, `process walk: calls process fetch`, `process ticking: requests Run.turn`. Nothing in the source marks a process, so this is where to read which functions the compiler lowers. With `--json` the same list is the `processes` field of each module's report. ### Capabilities ```bash aver capabilities file.av --module-root . aver capabilities file.av --module-root . --json ``` `capabilities` prints the target-total binding manifest for every capability in the loaded dependency closure. Each contract has exactly one row for each of `vm`, `rust`, `wasm-gc` and `wasip2`: `provided`, `host-bound` or `unsupported(reason)`. Declared and actually required operation sets are shown separately, so you can audit an unused contract without it blocking a target. Use `--json` for the deterministic `schemaVersion = 1` envelope that tooling and future adapter planners consume. `capability-provider-missing` means a target can accept a binding but none was installed. `capability-target-unsupported` means that target has no adapter mechanism for the contract; it carries a stable reason code. ### Effects ```bash aver effects file-or-dir --module-root . aver effects file-or-dir --module-root . --json aver effects file-or-dir --module-root . --write aver effects file-or-dir --module-root . --since ``` `effects` compares every declared `! [...]` against the minimum the checker computes for that function, and every module `effects [...]` against the union of its functions. The minimum is the same set the `unused-effect` warning already computes, taken over the whole module graph: a function's set is what its own body performs plus the set of everything it calls. It is iterated upward from the empty set, so a recursion group settles on the least set. Starting from the written lists would leave a cycle as its own answer, because two functions that call each other keep each other's surplus entries alive. A module with nothing to report gets one summary line. The others list each function with what is missing and what is unused, then the same for the boundary. The report never fails the command, and it works on a program that does not type-check, which is the state a primitive swap leaves behind. `--write` rewrites exactly the lists the report names, on functions and on module boundaries, to that minimum. It renders them through the formatter's own layout, so `aver format --check` stays clean afterwards. It is idempotent, and a tree whose lists the report calls minimal is left byte-identical. You read the report to decide whether to run the rewrite at all, so the rewrite never touches a list the report said nothing about. Four rules keep it mechanical: - The callback-forwarding marker `_` is copied through verbatim: it is not a computed effect, so the rewrite never invents it and never removes it. `Run.turn` is an effect like any other: a function whose body calls `Run.turn()` gets it written, which makes it a process. A process's list only grows: what it reaches through another process is lowered out of the signatures the rewrite reads, so dropping it would drop what makes it a process. - A namespace entry you wrote, such as `Disk`, stays as written while it covers the computed set, including when you wrote a method beside it. Narrowing it to `Disk.readText` is a decision about the contract, so `effect-granularity` raises that as a warning instead. - A module that declares no boundary does not get one. `check` already nudges for that, and declaring the boundary is the author's call. - A `//` comment written on a list's own lines is put back on the rewritten list. The formatter leaves a line carrying a comment alone, and the rewrite does the same. An out-of-date effect list does not stop `aver effects`. Any other error does, in every mode. A callee whose name does not resolve contributes no effects, so the computed minimum would come out short: the report would understate every list above it, and the rewrite would delete entries the program needs. The command names those errors and refuses. Run `aver check` and fix them first. A rewrite applies to the whole tree, but the walk reads one program. When `--write` rewrites a module the input did not name, it names that module and says it was reached as a dependency. Another program can import that module, this run did not read that program, and the module's lists moved anyway. Run `aver check` over the module root afterwards, not over the input you rewrote from. `--since ` is the reviewer's view. It reads each module at that git revision through `git show` and, per module, separates two groups: functions whose declared list changed while their body stayed byte-identical, and functions whose own body changed. The first group needs no decision. Their lists moved because something further down the call chain moved, and a reviewer can skip them. A function the revision did not have is named as added, and one it had that the working tree does not is named as removed. That is how a rename shows up. An unknown revision fails with the revision named. A module that revision did not carry is reported as new. Granularity stays `Namespace.method` everywhere. The command writes the lists for you. It adds no way to omit a list, to name a set of effects, or to abbreviate one. ### Verify ```bash aver verify file-or-dir --module-root . aver verify file-or-dir -j 8 aver verify file-or-dir --wasm-gc ``` `verify` runs the declared `left => right` examples and laws of every module of the program (the entry plus everything it reaches through `depends [...]`), leaves first, with one `Verify:` section per module and a `Summary: N modules | …` line. A directory is the union of the programs rooted at each file, and each module is verified once. Embedded standard modules are not sampled; their blocks are verified per release. A failing case in any module fails the command. Pointing at a single module is still the fast way to iterate on it. VM verification resolves one project graph, prepares each project module once, then runs independent files and declared cases in a bounded worker pool. `-j N` / `--jobs N` sets the pool's maximum size and defaults to the machine's available parallelism. `-j 1` turns off concurrency but keeps graph reuse, so it is the mode to use for comparison and debugging. Reports are always collected in input, module, block and case order, so sequential and parallel runs emit identical text/JSON and failure coordinates. `--hostile` keeps the base/profile cases of a block sequential, and `--wasm-gc` keeps cases within a module sequential. Independent input files may still share the bounded pool. It fails on: - mismatched examples - parse/type errors - execution errors - cases it could not answer within their step budget It is not a coverage tool. Every case runs under a per-case budget of VM opcodes, 1,000,000 by default. A case that exceeds it is **declined**. That is a third outcome: it is counted separately from passes and failures, reported as `fail[verify-declined]: case not answered`, and it fails the command. A decline is not a counter-example. It says the case was not checked, so it can never be read as a pass. A project whose corpus legitimately contains expensive cases raises the budget for the function it knows about, in `aver.toml`, with a written reason (see `[verify]` below). The report then names the cases the raise bought: ``` ✓ checkScript 1119/1119 checkScript case 41: 8.2M steps (limit 50M, aver.toml [[verify.costly]] fn = "checkScript") ``` `--wasm-gc` runs the same cases on the same budget, converted to wasmtime fuel by one documented factor, so a case is runnable on both lanes or on neither. A second budget, per turn, is off by default. `[verify] turn-budget = N` makes each case count VM steps since its last wait (`Tcp.poll` or `Wait.poll`) or since the case began. A turn that runs past N is reported once per case as `warning[turn-budget]: case : one turn ran N steps without waiting; deepest function on the stack at the limit: `, where `` is the case's 1-based position in the block, so two cases with the same expression stay distinguishable. It is a warning and never a failure: the case was answered, but it did not wait often enough on the way. Only VM steps count. Time spent inside a provider, live or stubbed, is not measured, and with the budget off nothing is counted at all. The count is checked on the same 256-opcode cadence as the step limit, so a turn shorter than that cadence cannot be measured, and a reported length is the length at the check that caught it. The wasm-gc verify lane (`--wasm-gc`) does not measure turns: it runs on fuel instead of opcodes and has no `Tcp.poll` seam to reset on. `aver check` reports the static shape behind most of these as `warning[serve-path]`. A file whose program `verify` could not run (a type error anywhere in it, a backend or provider failure, a refusal by verify itself) is **not checked**, and the report says so instead of leaving it out. Such files are listed under a heading naming the reason, each with the number of verify blocks that went unchecked. The module named is the one that carries the fault, not the entry that depends on it. The summary line gains a `| N file(s) not checked` member and is never green while N is above zero, and `--json` carries `files_skipped` and `blocks_unchecked` in its summary record. Modules that did verify before the walk stopped still report their cases. A stop before the first module runs (a project file that does not parse, for instance) counts every module of that program, not just the entry. Only the buckets verify itself is known to own say that `aver check` will not help: a `--wasm-gc` backend refusal, a provider composition failure, and verify's own refusals. Anything else is treated as a source error and points at `aver check`. Declined cases and unchecked files are independent counts, and one run can carry both. The summary states each of them separately. `--json` carries `cases_declined` (only when something was declined) alongside `files_skipped` and `blocks_unchecked`. Either count above zero keeps the run out of green and out of exit code 0. When the project's `aver.toml` binds providers and a module reaches one of those capabilities, the cases run inside the cached provider host, so a configured pure provider executes in ordinary VM cases. An exact operation `given` is still a case-local override. Project bindings unrelated to a module are ignored for that module; they do not cause a skip or a fake type error. `verify --wasm-gc` has no configured-provider adapter yet and refuses such a program. Ordinary `run --wasm-gc` and `replay --wasm-gc` do use the cached provider host. `--wasm-gc` (0.17.3+) executes the same cases on the wasm-gc backend instead of the VM. This cross-target check 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/String). Trace projections (`.trace.*`), classified-effect Oracle stubs (`given X: Time = stub`) and case bodies that mention `BranchPath` are rejected upfront with a pointer back to VM verify. Those features depend on namespace-value dispatch and runtime override, which the wasm-gc backend does not have yet. ### Format ```bash aver format . aver format examples aver format examples --check ``` `format` accepts files or directories and walks `.av` files recursively. ### Audit ```bash aver audit file-or-dir --module-root . ``` `audit` is the single-shot CI gate. It runs all three axes at once: 1. static checks (same diagnostics as `check`) 2. `verify` execution (same as `verify`) 3. `format --check` (structural compliance) Like `check` and `verify`, `audit` walks the whole program: the entry plus everything it reaches through `depends [...]`, leaves first, one `Audit:` section per module. A directory is the union of the programs rooted at its files, and each module is audited once, so a dependency outside the directory is audited too. Embedded standard modules are typed but not audited. When the project's `aver.toml` binds providers, the verify axis runs through the same cached provider host as `aver verify`. Static checks and formatting stay provider-neutral. A project without `[providers]` never invokes Cargo. Output is a flat list of `error[slug]:` / `warning[slug]:` lines plus a summary footer: `N modules | X check errors | Y verify failures | Z format`. Any non-zero count fails the command. - warnings (e.g. `independence-hazard`, `non-tail-recursion`) are advisory and do not fail the audit - 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 bare `aver run` can miss when the VM short-circuits on the first failure. `--hostile` (0.13+) layers adversarial worlds on top of every `verify law` block: typed `given`s get type-boundary values, and classified effects get hostile profiles. Failures use a separate slug, `verify-hostile-mismatch`, so CI can route declared-world and adversarial-world regressions to different channels. ### Context ```bash 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: ```bash 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 ```bash 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: ```toml # 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" ``` `aver shape` is a static module-shape analyzer: an *architectural smell radar*. It does not classify truth. The histogram is the fact, and Kind and Layer are interpretation. Output is auditable: every interpretation comes with the metric that drove it (confidence, margin and 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`). A fn can carry several labels. The 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 have the Oracle one-shot req/resp shape) or `ShellEffectful` (contains a shell/lifecycle effect like `Tcp.listen`; Oracle skips those by design, not because the classifier fails to recognize them). 3. **Architectural Layer**: `Domain | Parse | Command | AiStrategy | RenderUi | Infra`, picked 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 the runner-up). Low confidence or low margin marks the verdict `uncertain`, with explicit "best: X" wording so the user does not read it as a hard label. Runners-up (the 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 a separate, orthogonal section: which verify blocks the source carries (`Cases`, `Laws`, `Trace`, `Mixed`), how many blocks, and per-fn coverage. It is a static read of the source and does not run the VM. Use cases: - "What is this module structurally?": a first look before reading it - "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 and ModuleShape are stable per-module facts worth attaching to AI prompts about that file Notes: - `--summary` collapses the per-fn listing to the header + histogram; the content is otherwise the same - `--json` emits an audit-friendly structure with `facts` + `vector` + `kind` + `histogram` + `layer` + `fns` side by side, so consumers can pick any layer ### Compile ```bash 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 --target wasm-gc --pack wasmtime -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. A self-contained binary; the engine handles GC and recursion, and per-instantiation helpers are DCE'd down to what each program calls. 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`: derive `.optimized.wasm` from the canonical `.wasm` with binaryen `-Oz` (size) or `-O3` (speed). It drops the name section, so a wasm trap reports `` instead of the name of the function that trapped. `aver compile` says so on stderr for a program whose named helpers it is about to strip. On wasm-gc it can accompany `--certify`: the certificate binds only the unchanged canonical file. - `--pack wasmtime`: native self-contained wasm-gc directory pack. It emits the canonical `.wasm`, optional `.optimized.wasm`, a matching AOT-compiled `.cwasm`, `manifest.json`, and a stripped `aver-wasmtime-host` carrying Wasmtime plus the exact custom providers selected by `aver.toml`. The destination needs no Aver, Cargo, Wasmtime installation, provider source, project tree, or first-start Cranelift compilation. With `--certify --optimize`, proof, optimization and native execution stay three explicit artifacts. The host defaults to zero-JIT AOT. `--artifact canonical|optimized -- ` explicitly JITs either portable stage for differential diagnosis; it never falls back automatically. The host is built for the current OS/architecture and runs `main`; see `docs/wasmtime-pack.md`. - `--preset cloudflare --handler `: Cloudflare Workers pack. It means `--target wasm-gc --pack cloudflare` and drops `worker.js` + `wrangler.toml` next to the wasm. `` must have signature `Fn(HttpRequest) -> Http.Response`. - `--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. Use it for CI checks that fail when an invariant breaks ("fail if buffer_build no longer fires on the canonical shape", "fail if hot fn loses no-alloc status"). Pair it with `--json` for a 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`. Query it with `jq '.passes[] | select(.stage=="buffer_build") | .data.rewrites'` instead of regex-parsing summary strings. **`Map` size on wasm-gc.** A `Map` compiled to `wasm-gc` (and therefore to `wasip2`, which wraps it) is an open-addressing table that starts at 16 buckets and doubles whenever an insert would take it past three quarters full, rehashing its entries into the wider table. `Map.set` therefore takes keys until memory runs out, the same as on the VM and the Rust target, and no size is a cliff. The table used to be fixed at 16384 buckets, so the 16385th distinct key had nowhere to go. That ceiling is gone. ### Artifact certificates ```bash aver compile app.av --target wasm-gc --certify -o out/ aver compile app.av --target wasip2 --certify -o out/ aver-cert verify out/app.wasm out/cert aver-cert verify out/app.component.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 verify out/app.component.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 an exact wasm-gc module or wasip2 component. A wasip2 package hashes the delivered `.component.wasm`. Its declared prefix/core/suffix envelope binds the exact embedded core bytes that the existing Wasm wall consumes. Install `aver-cert` separately; it is an independently versioned verifier using Lean 4.33. A crates.io compiler install needs `--features wasm` for wasm-gc, plus `wasip2` for component output. Verification also requires a standard Elan installation for the pinned toolchain. `--certify` bridges only the law cone by default: the functions a law-claim of the package mentions, and the functions their plans call. Every other certified export keeps `model: plan` and is listed in `sourceBridgesDeclined` with the reason `no law-claim reaches it (only verify examples or nothing do); pass --examples to bridge it`. `--examples` bridges every certified export. The byte certificate and the bridges each law-claim cites are the same in both modes. `--examples` is refused without `--certify`. `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`. `aver cert verify` is a different command from `aver verify`. Source `verify` runs examples; `aver cert verify` kernel-checks a behavioral certificate for compiled WebAssembly. See the [certificate guide](https://github.com/jasisz/aver/blob/main/docs/certification.md) and [architecture](https://github.com/jasisz/aver/blob/main/docs/certification-architecture.md) for the admitted families and trust boundary. ### Bench ```bash 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/--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 runs on different machines can be told apart. - `--save-baseline` works in both single-scenario (pretty JSON) and directory (NDJSON) mode. `--compare` is single-scenario only. - `--baseline-dir DIR` auto-picks `--.json` from `DIR`. It skips silently when no matching baseline exists, so one workflow gates wherever a baseline is pinned. CI uses this. - See the [benchmark guide](https://github.com/jasisz/aver/blob/main/docs/bench.md) for the full reference. ### Proof ```bash aver proof file.av -o /tmp/proof --module-root . --verify-mode auto ``` Lean export modes: - `auto` - `sorry` - `theorem-skeleton` `aver proof` exports the laws (`verify ... law`) with their samples, `because` and `using`, and what the laws reach. `--examples` also exports the `verify` examples and what only they reach, such as an effectful function no law calls. The flag means the same on `aver compile --certify`, where it bridges every certified export instead of only the law cone. Without `--examples`, an example is not exported, so it is neither a sorry nor a declined claim. `--backend` picks the judge. With `lean` (the default) the Lean kernel checks the exported model: a law's proof written as steps by the compiler goes first and its tactics stay behind it. With `aver` the proof kernel written in Aver (`tools/proof-kernel`, built into `aver`) checks those step proofs in process against its closed list of rules, without Lean; a law the compiler writes no steps for is reported as not closed by this backend. What a step may do, and how the compiler refuses when it cannot write one, is in [proof steps](lean.md#proof-steps). `aver cert` always uses Lean. `--check` builds the export with `lake` and gates on the result (`--check-json` gives a machine-readable summary). `--gate ` / `--write-baseline` are the proof ratchet. `--gate` fails when a law of the baseline is gone, drops to a lower tier, changes backend, newly depends on an axiom other than Lean's standard three (`propext`, `Classical.choice`, `Quot.sound`), or newly depends on one of the standard three while staying at the same tier. A law that moves to a higher tier, such as failed to universal, is reported as `promoted` and passes, even when its universal proof uses the standard axioms. A guarded (`when`) law is stated for every input only; one whose speculative proof Lean does not close is declined (charged against `--declined-budget`), not counted as a sorry. A baseline from 0.30 that still holds `bounded` laws fails the gate with a message saying so. `--compare-manifest ` (Lean, check mode) says, for each law that did not close, whether its own script changed and which definitions it opens changed since that manifest. `--minimize` (Lean, implies `--check`) collapses each auto-proof to the single tactic that actually closed it. See [docs/lean.md](lean.md) for the proof workflow, the `--check` summary fields, `--compare-manifest` and `--minimize`. ### Builtin facts ```bash aver facts # every builtin fact, with its statement as an Aver law aver facts List.reverse # only the facts whose name starts with this aver facts --json ``` A law cites a builtin fact in `using` like one of its own program's laws (`using [List.len.ofConcat]`). Facts hold for lists of any element type and maps of any key and value type (some have a `when`, such as `Map.get.afterSetOther`); their step proofs travel with the citation and are checked before use. When `aver proof` leaves a law open, or closes it only by tactics, it prints a `hint:` line naming each fact whose left side matches a part of where the steps stopped. Add the fact to `using` yourself; nothing is cited for you. When steps refuse because the claim passes the law's own function different givens where it recurses (`append(append(xs, ys), zs) => append(xs, append(ys, zs))`), the refusal lists them; add an `induction xs` line, just before the claim, naming the one to follow. ### Replay ```bash aver replay recordings/ --test --diff ``` Use replay for effectful debugging and regression capture. ### Agent connect ```bash aver agent-connect # this project: skills + a marked AGENTS.md section aver agent-connect --global # ~/.claude/skills/ instead, AGENTS.md untouched aver agent-connect --print # the language guide on stdout, nothing written ``` The language guide and this toolchain guide ship inside the `aver` binary, so an install carries them and nothing has to be fetched. `aver agent-connect` writes them out as `.claude/skills/aver/SKILL.md` and `.claude/skills/aver-tooling/SKILL.md`, then creates or refreshes a short pointer section in `AGENTS.md` between `` and ``. Aver prescribes no agent workflow. Take the files and keep whatever prompt, harness or command you already use. `--print` exists so that an agent that wants one file instead of a skill directory can have it. Safety: - bytes outside the `AGENTS.md` markers are never touched, and a file with no markers is appended to, never rewritten - a marker bounds the section only when it is alone on its own line, so a sentence that names one (like the paragraph above) is prose and is left where it stands - an `AGENTS.md` carrying half a marker pair, an inverted pair, or a second pair is refused by name instead of being rewritten on a guess - a `SKILL.md` that exists without the `aver agent-connect: managed file` marker is refused by name, never overwritten - re-running produces no diff; every line of the summary says `created`, `updated` or `unchanged` - exit is nonzero only on a refusal or an IO error ## 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` ### Effect list propagation 1. change the call at the leaf 2. `aver effects . --module-root . --write` 3. `aver check .` over the whole module root, because a rewritten module can be imported by a program the walk did not read 4. `aver effects . --module-root . --since ` before asking for review ### Project discovery 1. `aver agent-connect` once, so the language and toolchain guides are in the project 2. `aver context --budget 10kb` 3. if needed, raise budget or target a specific module 4. only then open raw source files ## aver.toml Project-level config (deployment guardrails + check tweaks): ```toml [effects.Http] hosts = ["api.example.com", "*.internal.corp"] [effects.Disk] paths = ["./data/**"] [effects.Env] keys = ["APP_*", "TOKEN"] [effects.Tcp] connect_timeout_secs = 5 request_idle_timeout_secs = 30 max_connections = 256 [[check.suppress]] slug = "verify-coverage" files = ["domain/checks.av"] fn = "eachInBranch" # optional exact function scope reason = "Its Result error arm is uninhabited by constructible inputs." [verify] step-limit = 1_000_000 # per-case opcode budget (default) max-cases = 10_000 # ceiling on `given`-domain expansion (default) turn-budget = 50_000 # steps one turn may run between two Tcp.poll waits (default: off) [[verify.costly]] fn = "checkScript" files = ["domain/scriptcases*.av"] step-limit = 50_000_000 # raise the per-case budget for this fn max-cases = 40_000 # raise the case ceiling for this fn reason = "Bitcoin Core corpus includes consensus-max 10,000-byte scripts" [work] max-jobs = 4 # jobs running at once (default: host parallelism) ``` Effect-host / path / key allowlists narrow which hosts, files and env keys the runtime will admit. Tcp's positive-integer settings configure connection establishment, one-shot request idle timeouts, and one shared limit for established/accepted connections plus in-flight dials. They never impose a deadline on persistent session I/O. Unknown or misplaced keys inside an effect section are errors. `[[check.suppress]]` lets a project waive specific lint slugs in specific paths, optionally for one exact function, with a reason. Disk path patterns are deliberately small and explicit: | Pattern | Meaning | |---|---| | `path` or `path/**` | That path and its entire subtree | | `.`, `./`, or `./**` | The project-relative subtree | | `/` or `/**` | Every absolute path from the filesystem root | | `**` | Invalid; use `./**` or `/**` to state the intended boundary | An empty pattern, unsupported `*` placement, or a `..`-rooted pattern is also a config-load error. An absent `paths` key or `paths = []` keeps the existing allow-all behavior. Matching is string-only: Aver normalizes `.` and `..` in the caller-supplied path without resolving it against the working directory or touching the filesystem. A project-relative pattern therefore does not admit an absolute spelling of the same in-project file. `[work] max-jobs` bounds how many jobs a program runs at once. It must be a positive integer. Without it a program gets the host's own available parallelism. At the limit, a job kind's `begin` queues the job and answers its handle at once, never a refusal, and the job starts when a running one stops; so the limit decides how much of the host a program uses and nothing it can observe, and a recording replays under any limit. The wasm-gc runner and Wasmtime packs honour it the same way; the JavaScript adapter takes its limit from its own `maxJobs` option. On `wasip2`, a job currently runs inline at `begin` and is over before the next expression. A manifest that sets the key for that target gets `warning[work-max-jobs-ignored]` at the program door, naming the key and the target, and the program runs. ### Processes, answer modules and jobs in `aver.toml` A program that serves several processes writes no loop and no loop configuration. An answer module says what it answers in its own header (`answers [Clock]`), a keyed process is declared in the entry with `process member seated by Hub.members`, and the entry's optional `stop` and `admit` are found by name. The manifest keeps only deployment: which function a job kind runs, how many jobs run at once, and host packages. This is the whole manifest of the smallest such program (one answer module, one job kind, one process), and it checks and runs as written: ```toml [providers] schema = 1 [[providers.bindings]] capability = "Scoring" work = "Clocked.points" [work] max-jobs = 2 ``` - `work = "Module.function"`: the pure `(T) -> R` a job kind runs off the turn, for a capability of Work shape (`begin(task: T) -> Result`, `take(job: Work.Job) -> Result, String>`). Every job kind requires it. The function belongs to a module the program depends on, never to the entry module. An answer module begins the job itself and parks the request on it. - `[work] max-jobs`: jobs running at once, shared by every job kind. A positive integer; the default is the host's parallelism. - `answer`, `task`, `started`, `landed` and `[run]` are gone, and a manifest that still has one is refused with the repair: `answer` became the `answers [...]` header, the job seam became the job as a request, and `[run]` became nothing at all. The program this manifest belongs to is `tests/fixtures/run_guide_example/`; the language guide shows its modules. The diagnostics an agent meets on the way, each with its recipe (`docs/diagnostics-slugs.md` has the full rows): | Slug | What it says | Recipe | |---|---|---| | `process-direct-call` | `main`, an unsupported verify form, or a function value calls a process as written. The message names what made it a process. | Call it from another process, seat it as a process the generated loop runs (`Run.all()`), or test it with a cases-form `verify` that stubs every request. | | `process-non-tail-call` | A process calls itself outside tail position. | Pass what comes next as data, or make it a tail call. | | `process-unsupported` | Mutual nesting between processes, a request or a helper call inside `(a, b)!`, a function value live across a request, or a process with no stop. | Break the cycle, perform them one after another, pass data instead of a callback, or drop the request it never makes from its effect list. | | `request-outside-process` | A function that is not a process requests an operation of an answered capability: its module does not depend on the answer module, or it is `main`. | List the answer module in that module's `depends`, or call the answer module's own function directly. | | `answer-shape` | Error: an answer function is a process. Warning: an answer function declares effects that can block, which stalls every process while it runs. | Drop the request from the answer and make the process the caller; for the warning, accept the stall or move the work into a job. | | `answer-binding` | An `answers [...]` header names a capability that module cannot answer: a standard capability, a capability module, a missing operation, a wrong signature, two states in one module. | Declare a capability of your own; write `op(state: S, args) -> Tuple>` for every operation with one state. | | `run-binding` | Something the generated loop is built from is off: a process with parameters and no `process ... seated by ...` line, a process answering something other than `Unit`, a seating function that is not `(S) -> List` of an answer module, an answer module without `fresh`, a `stop` or `admit` of the wrong shape, `Run.all()` with no process to seat, or a `[run]` table. | Declare a keyed process with `process seated by `, give every answer module a pure `fresh`, write `stop(view: Run.View) -> Bool` and `admit(view: Run.View, id: Int) -> Bool`, and remove `[run]`. | | `work-shape` | A capability names `Work.Job` but is not exactly `begin`/`take` with the Work result shapes. | Declare exactly those two operations; keep capability resources out of `T` and `R`. | | `work-binding` | A job kind with no `work` binding, a binding naming a missing, effectful, entry-module or wrongly typed function, or a `task`, `started` or `landed` key. | Bind `work = "Module.function"` with `(T) -> R`; begin the job in the answer module instead of a seam. | | `work-max-jobs-ignored` | Warning: `[work] max-jobs` is set and the target is wasip2, where a job currently runs inline at `begin`. | Leave the key for the VM, Rust and wasm-gc hosts, or remove it. | | `serve-path` | Warning: a function that waits reaches a loop with input effects that runs to completion inside one turn. | Do one step per turn, run it as its own command, or suppress with `[[check.suppress]]` and a reason. | | `turn-budget` | Warning: with `[verify] turn-budget = N`, one turn of a case ran past N VM steps without waiting. | Wait more often: one step of the named loop per turn. | `[verify]` budgets in detail: - `step-limit` is the per-case opcode budget `aver verify` installs before every case. The default, 1,000,000, is what stops a tail-recursive function that has no base case: Aver's tail-call optimization turns it into a goto-loop with no stack growth, so nothing else would stop it. Raising it globally gives up that bail-out for every case in the project. `[[verify.costly]]` gives it up for one function, which is almost always what you mean. - `[[verify.costly]]` raises the budgets for the verify blocks of one function. `fn` is required. `reason` is required and must be non-empty, the same rule `[[check.suppress]]` has and for the same reason: nobody can retire a budget that nobody explained. `files` is optional and uses the same anchored globs, matched against the file's path relative to the module root. - An entry carries both dials and must set at least one: `step-limit` for a fn whose cases are slow, `max-cases` for a fn whose `given` domain is wide, both for a fn that is both. An entry that sets neither is a config error. So is a dial that is not above the number already in force: `[[verify.costly]]` says "this case is expensive, give it room", and a lower number says the opposite. An entry therefore only ever raises, and where several entries match one block the most permissive value wins, for both dials. First-match-wins would make the order of the entries part of what the file means. An entry added near the top would silently change which one governs a block elsewhere, and a reader would have to scan the whole list to know what applies. With the most permissive value winning, each entry is an independent statement about one function, and adding one can only loosen, never re-point. - The report names every case that needed more than the project default, with its step count and the entry that raised it, so no raise goes unreported. - An entry that matched no verify block during a run is reported on stderr, separately for "matched no verified file" and "matched files but no block of that fn", and never changes the exit code. An entry that another entry out-granted is not reported. It matched a live block, and losing a tie-break says nothing about whether the declaration is still true of the project. - `max-cases` is the ceiling on how many cases one verify block may expand into, on both sides: the `given` domain the parser expands and the `--hostile` cartesian the runner expands on top of it. Both fail loudly with the count instead of truncating, because a truncated case list is a claim you did not make. Each expanded case clones an expression pair, so raising this costs parse-time memory in proportion to the new ceiling. `[verify] max-cases` moves it for the whole project. A `[[verify.costly]]` entry moves it for the blocks of the one function it names, which is usually what a wide corpus actually means. - The ceiling applies to the file at every command. Every command that reads your `.av` files parses them under it (`check`, `run`, `compile`, `proof`, `audit`, `format`, `shape`, `context`, `why`, `capabilities`, `replay`, `bench`), and so does the dependency walk each of them performs. A `given` domain your project declared legal is legal at every door, a domain over the ceiling is refused at every door, and the message names the number that actually applied instead of the built-in one. - `turn-budget` is a second counter, per turn instead of per case, and off unless set. A turn is the run of VM steps since the case's last wait (`Tcp.poll` or `Wait.poll`) or since the case began. A turn past the budget earns the case one `warning[turn-budget]` naming the case by its index and the innermost function at the limit. It never fails the run. Only VM steps are counted, so time inside a provider is invisible to it. The count is tested every 256 opcodes, so a turn shorter than that cannot be measured. With the budget off the VM does no extra counting. The wasm-gc lane does not measure turns at all. `[[verify.costly]]` does not raise it, because a slow case and a turn that never waits are different facts. - None of these settings changes what a program means. The same source verifies the same way under any budget; it only gets more or less room to finish. `[[check.suppress]]` rules in detail: - `files` globs match the file's path **relative to the module root**, so a leading `./` is insignificant on either side and every spelling of the same file (`aver check domain/version.av`, `aver check ./domain/version.av`, `aver check .`, an absolute path, or a dependency module of the program) honours the same rule. A rule with no `files` key applies everywhere. - `fn` is optional. When present, the rule matches only diagnostics carrying that exact function name, and a file-level diagnostic cannot match it by accident. This is the narrow form for an unavoidable leftover such as one `verify-coverage` Result arm. Without `fn`, the rule keeps its existing file-wide meaning. - `aver check` and `aver audit` apply the same rules. Both print how many warnings a file's waivers removed. - Suppression applies to warnings only. It can never hide an `error[...]`, a verify failure, or the `needs-format` result, so a waiver can never change a command's exit code. - A rule that removes nothing during a whole-directory run (`aver check .`, `aver audit .`) is reported on stderr, telling you whether its globs matched no checked file at all or matched files whose warning no longer fires. Single-file runs stay quiet, since they legitimately never exercise rules scoped to other paths.