Aven documentation

Aven is a relational language: you state equations that must hold, give it the values you know, and it settles the rest. This page takes you from installation to compiled code. Every example here runs as written with avenc v0.9.0.

Install

Aven builds from source with a standard Rust toolchain (install one from rustup.rs). The compiler has no external crate dependencies.

cargo install --git https://github.com/Thrainkrilleve/aven.git avenc

Or clone the repository, which also gives you the examples used throughout this guide:

git clone https://github.com/Thrainkrilleve/aven.git
cd aven
cargo install --path .

The one-line installers at avenc.dev/install.sh and avenc.dev/install.ps1 run the same cargo install. Prebuilt binaries are not published yet.

avenc --version
avenc check examples/server_capacity.aven

Your first model

A relation holds equations. A solve block supplies the values you observed. Save this as dynamics.aven:

relation Dynamics {
    force = mass * acceleration
}

solve Dynamics with {
    mass = 1200.0
    acceleration = 3.5
}

avenc run dynamics.aven

Solver Trace:
  [force = mass * acceleration] force <- forward eval

Settled Environment:
  acceleration     = 3.5000
  force            = 4200.0000
  mass             = 1200.0000

Fact Ledger: 3 facts settled.

Solving in any direction

The equation does not fix which side is the input. Change the solve block to give the force and acceleration instead, and Aven solves for mass with Newton–Raphson:

solve Dynamics with {
    force = 4200.0
    acceleration = 5.0
}

Solver Trace:
  [force = mass * acceleration] mass <- backward Newton

Settled Environment:
  acceleration     = 5.0000
  force            = 4200.0000
  mass             = 840.0000

Relations, solves and forward blocks

• relation declares equations and inequalities that must all hold. Any variable can be the unknown.
• solve … with binds observed values, and may add bounds or an objective.
• forward pins the direction: each equation computes its left-hand side from values already known. Forward blocks run without a solver and are what emit-c and emit-wasm compile.

forward ProductionProfile {
    raw_workers       = (reqs_per_second * avg_latency_ms) / 1000
    allocated_workers = ceil(raw_workers / target_utilization)
    total_ram_needed  = (allocated_workers * (ram_per_worker + socket_buffer_mb)) + os_kernel_ram_mb
    payload_gbps      = (reqs_per_second * avg_payload_kb * 8) / 1000000
    wire_rate_gbps    = payload_gbps * framing_overhead_ratio
}

Operators, from highest to lowest precedence: ^ (right-associative), * /, + -, then the comparisons < <= > >=. Comments start with //.

Units and dimensions

Declare a signal's unit with signal name : unit, or attach a unit to a value in a solve block. avenc check infers the dimension of every variable and rejects equations that mix incompatible dimensions:

signal speed : km/h
signal t : s

relation Mixed {
    bad = speed + t
}

✗ Type Error at line 5, col 5: dimensional mismatch in expression '(speed + t)'
  — cannot perform '+/-' between [m·s^-1] and [s]

The checker tracks ten base dimensions: length, time, mass, electric current, temperature and amount of substance from SI, plus angle, money, data and transactions. Values are converted to base units before solving and shown back in each variable's declared unit, so velocity = 250 km/h is solved as 69.44 m/s and printed as 250 km/h.

Compound units use /, * and integer ^: km/h, kg/m^3. Symbols are case-sensitive where it matters (MW megawatt, mW milliwatt); ambiguous spellings such as Mb (megabit or megabyte?) are rejected with the valid choices.

Optimization

Declare integer variables with int, constrain with inequalities, and add minimize(…) or maximize(…) to the solve block:

relation ServerProvisioning {
    int nodes
    total_cores = nodes * cores_per_node
    total_ram_gb = nodes * ram_per_node_gb
    total_cost_monthly = nodes * node_monthly_cost

    total_cores >= required_cores
    total_ram_gb >= required_ram_gb
}

solve ServerProvisioning with {
    cores_per_node = 16.0
    ram_per_node_gb = 64.0
    node_monthly_cost = 145.0
    required_cores = 100.0
    required_ram_gb = 350.0
    minimize(nodes)
}

Solver Trace:
  [optimize] simplex branch-and-bound (1 nodes) — objective = 7.000000 (proven optimal)
             [bound = 7.000000, duality_gap = 0.00e0, cuts = 1, dual_norm = 3.00e0]

Settled Environment:
  nodes            = 7 (int)
  total_cores      = 112.0000
  total_cost_monthly = 1015.0000
  total_ram_gb     = 448.0000

Without an objective, bounds only check values: every variable a bound mentions must be given or derived, or the model is reported as under-determined.

A result is reported as proven optimal only when the bound and duality gap certify it. To explore a trade-off instead of a single optimum, sweep one variable with avenc pareto <file> <var> <min> <max>.

Functions and constants

Constants: pi, e and tau (upper-case spellings also work). There is no log10; use ln(x) / 2.302585092994046.

External data

A relation can take its facts from a live source with a using clause. Each fact from an adapter records the SHA-256 of the adapter's raw output in the ledger.

// A subprocess that prints JSON facts
relation Flame using external("python", "evaluations/tests/flame_eval.py") {
}

// A persistent local daemon over TCP
relation FlightAtmosphericDynamics using ipc("127.0.0.1:9090") {
    speed_of_sound_ms = sqrt(1.4 * 287.058 * ambient_temp_k)
    mach_number = velocity_ms / speed_of_sound_ms
}

Two more backends exist for low-latency use: shm("name") reads a shared-memory ring buffer, and native("lib.so") calls a C or Rust dynamic library in process.

Supervising a live feed

avenc stream reads one JSON object per line from stdin and solves each as a cycle. examples/stream/openplc_supervisor.aven checks PLC readings against limits; feed it the OpenPLC Modbus poller:

python evaluations/tests/PLC-test/openplc_poller.py --host <plc-address> \
  | avenc stream examples/stream/openplc_supervisor.aven

#1      | a7c77c66d26612c6 | SETTLED
        power_margin_w = 39.0000, quality_margin = 3.7000, scan_margin_ms = 8.8000, thermal_margin_c = 11.9000
#2      | c553b51e377de931 | ALARM: Constraint violation in 'thermal_margin_c >= 0': thermal_margin_c = -6.0000 violates bound 0.0000
#3      | 429fb659cb5aa557 | UNSOLVED: System is under-determined (3 degree(s) of freedom):

A reading that leaves the model under-determined, such as one missing a field, is reported as UNSOLVED; it is never filled in. The limits in the example are placeholders to set for your own line.

Facts can carry a time-to-live. If a decision depends on a fact older than its TTL, avenc run prints DECISION BLOCKED and exits with code 3 unless you pass --allow-stale.

Command reference

Exit codes

C and WebAssembly

Both targets compile a model's forward block. Equations are topologically ordered, so the output is straight-line code with no solver, and the C output includes a main that runs the example's solve-block values.

avenc emit-c examples/server_capacity.aven -o capacity.c
cc -O2 capacity.c -lm -o capacity && ./capacity

avenc emit-wasm examples/server_capacity.aven -o capacity.wasm
avenc emit-wasm examples/server_capacity.aven --wat

The WebAssembly module exports memory, a function named after the block that takes each input as a parameter, and aven_solve(in_ptr, out_ptr), which reads inputs as consecutive f64 values in alphabetical order of name and writes outputs in evaluation order:

const { instance } = await WebAssembly.instantiate(bytes);  // no imports: server_capacity uses none
const mem = new Float64Array(instance.exports.memory.buffer);
mem.set([20, 64, 1.04, 4096, 16, 50000, 4, 0.7], 0);  // inputs, sorted by name
instance.exports.aven_solve(0, 1024);
console.log(mem.slice(128, 133));  // raw_workers, allocated_workers, ...

floor, ceil, round and sign compile into the module and match avenc run exactly. WebAssembly has no exponential, logarithm, trigonometric or general power instruction, so a model that uses exp, ln, sin, cos, tan or a ^ other than an integer constant or 0.5 imports them from the host as module "math"; supply those functions in the import object. Those results come from the host's math library and agree with avenc run to within a few units in the last place.

Audit ledger

Every settled fact extends a SHA-256 hash chain. Write it with --ledger; sign it by setting AVEN_LEDGER_KEY or passing --key.

avenc run examples/server_capacity.aven --ledger audit.jsonl
avenc verify-ledger audit.jsonl

Ledger OK: 13 fact(s), chain intact (signatures not checked: pass --key <code>
or set AVEN_LEDGER_KEY), head 1e61a9c5de48af4c628242f5088dba27a5051ed1a3270057c5b4579d90987bf8

Editing, deleting, reordering or truncating any entry makes verify-ledger fail with exit code 1 and name the first bad line.

Explaining results

avenc why prints how a value was derived, down to the bindings it came from:

avenc why examples/server_capacity.aven allocated_workers

avenc debug replays a run. With --what-if it branches the timeline and shows the effect of a change on every output:

avenc debug examples/thermostat.aven --what-if "current_temp_c=35.0"

Counterfactual What-If Result (mutating 'current_temp_c' = 35.0000 at t0):
  Output Variable                 Nominal         Branch          Delta
  --------------------------------------------------------------------
  compressor_amps                  3.7500         6.5000        +2.7500
  cooling_power_w                900.0000      1560.0000      +660.0000
  temp_delta_c                     7.5000        13.0000        +5.5000

In the interactive debugger: step, prev, goto <n>, why <var>, what-if <var>=<val>, diff, vars, help, quit.

Packages

A package is a directory with an Aven.toml manifest and a lib.aven entry file, sealed into an .avenpkg archive with a SHA-256 digest.

mkdir my_physics && cd my_physics
avenc pkg init my_physics              # writes Aven.toml and lib.aven here
avenc pkg pack                         # → my_physics-0.1.0.avenpkg
avenc pkg install my_physics-0.1.0.avenpkg
avenc pkg list

Packages install into .aven/packages in the current project. Installing by name from a remote registry is not implemented yet; avenc reads and preserves the [dependencies] and [[units]] manifest sections but does not fetch, resolve or register them.

Further reading

The full guides ship with the source tree, under docs/:

• docs/GETTING_STARTED.md — the fifteen-minute walkthrough, including SMT export.
• docs/TUTORIAL.md — Aven by example, ten progressive recipes.
• docs/CHEAT_SHEET.md — syntax, functions and commands on one page.
• STANDARDS.md — numerical, cryptographic and code-generation rules.
• docs/AVEN_AI_MODEL_GUIDE.md — writing Aven with a language model.