v0.9.0 Pure-std Rust compiler · C · WebAssembly · SMT-LIB2

Write the physics once. Solve for any unknown.

Aven is a relational language for physical and operational systems. Equations are invariants, not assignments: give Aven any sufficient set of knowns and it settles the rest, checks the units, records every derived fact in a hash-chained ledger, and compiles pinned models to solver-free C or WebAssembly.

Try the solver in the browser Read the guide

dynamics.aven

// One equation. No input or output is fixed.
relation Dynamics {
    force = mass * acceleration
}

// Knowns go in a solve block; Aven settles the rest.
solve Dynamics with {
    force        = 4200.0
    acceleration = 5.0
}

$ avenc run dynamics.aven
Solver Trace:
  [force = mass * acceleration] mass <- backward Newton

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

Fact Ledger: 3 facts settled.

External crates

Compiler, solver and SHA-256 are Rust std only

1414.9µs

Median solve, including IPC

avenc bench evaluations/flight_mesh/flight_mesh_ipc.aven --iterations 2000. Log: evaluations/flight_mesh/runs/2026-10-27-linux/avenc_bench.txt. 4-vCPU Linux container, 2026-10-27.

664.3/s

Solves per second, one client

Same command and log.

Execution targets

Native solver, C99, WebAssembly, SMT-LIB2

Live demo

The real solver, running in your browser

This is the actual Aven omnidirectional solver compiled to WebAssembly — not a one-way calculator. Change the inputs to solve forward, or switch to reverse to fix a target and let it solve backward for an input. The model is examples/server_capacity.aven, a Little's Law sizing relation. Nothing is sent to a server.

Inputs

Solved values

Loading solver…

Model solved this tick

The solver (symbolic forward evaluation plus guarded Newton–Raphson) is compiled from the same Rust that powers avenc run — 348 KB of WebAssembly, instantiated with no imports. Both directions run entirely in your browser.

What it does

One model, checked, solved, explained and compiled

Solve in any direction

Relations have no fixed inputs. Aven evaluates forward where it can, and solves backward with symbolic derivatives and guarded Newton–Raphson where it must.

avenc run

Units checked and converted

Dimensions are inferred across every equation; adding m/s to s is a compile error. Values given in km/h, hPa or MB are converted before solving and shown back in their own units.

avenc check

Tamper-evident audit log

Every settled fact extends a SHA-256 hash chain, optionally HMAC-signed. Edits, deletions, reordering and truncation are all detected. Stale inputs block the decision (exit code 3).

avenc verify-ledger

Optimization with certificates

minimize and maximize over real and integer variables. Results are labelled proven optimal only when a bound certifies them. Pareto frontiers with knee detection.

avenc pareto

Solver-free C and WebAssembly

forward blocks compile to branchless C99 or WebAssembly 1.0 with no runtime. Generated C is checked to match avenc run exactly.

avenc emit-c · avenc emit-wasm

Explain every number

Print the derivation tree of any value, replay a run in the time-travel debugger, branch a what-if, or export the model to SMT-LIB2 for Z3 or CVC5.

avenc why · avenc debug · avenc emit-smt

Workflow

From model to deployment

Real output from examples/server_capacity.aven, a Little's Law sizing model.

avenc check

$ avenc check examples/server_capacity.aven
Checking module 'examples/server_capacity.aven'...
  Blocks:   2
  Solves:   1

✓ Dimensional Analysis PASSED:
  Verified 10 equation(s) across SI/Systems unit registry.

✓ System Determinacy PASSED: All relation blocks have
  0 degrees of freedom.

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

Settled Environment:
  allocated_workers  = 1429.0000
  avg_latency_ms     = 20.0000
  payload_gbps       = 25.6000
  raw_workers        = 1000.0000
  reqs_per_second    = 50000.0000
  target_utilization = 0.7000
  total_ram_needed   = 32676.0000
  wire_rate_gbps     = 26.6240

Fact Ledger: 13 facts settled.

$ avenc why examples/server_capacity.aven total_ram_needed
Causal Derivation Tree for 'total_ram_needed':
#11 total_ram_needed = 32676.0000  ; forward ProductionProfile: = allocated_workers * (ram_per_worker + socket_buffer_mb) + os_kernel_ram_mb
  #10 allocated_workers = 1429.0000  ; forward ProductionProfile: = ceil(raw_workers / target_utilization)
    #9 raw_workers = 1000.0000  ; forward ProductionProfile: = reqs_per_second * avg_latency_ms / 1000
      #2 avg_latency_ms = 20.0000  ; user binding
      #1 reqs_per_second = 50000.0000  ; user binding
    #7 target_utilization = 0.7000  ; user binding
  #6 os_kernel_ram_mb = 4096.0000  ; user binding
  #4 ram_per_worker = 16.0000  ; user binding
  #5 socket_buffer_mb = 4.0000  ; user binding

$ avenc emit-c examples/server_capacity.aven -o capacity.c
/* Generated by avenc -- direction-pinned, solver-free */
static void aven_ProductionProfile(double avg_latency_ms, ...,
                                   double* out_raw_workers, ...) {
    const double raw_workers = ((reqs_per_second * avg_latency_ms) / 1000.0);
    const double allocated_workers = aven_ceil((raw_workers / target_utilization));
    const double total_ram_needed = ((allocated_workers *
        (ram_per_worker + socket_buffer_mb)) + os_kernel_ram_mb);
    const double payload_gbps = (((reqs_per_second * avg_payload_kb) * 8.0) / 1000000.0);
    const double wire_rate_gbps = (payload_gbps * framing_overhead_ratio);
    ...
}

$ avenc verify-ledger audit.jsonl
Ledger OK: 13 fact(s), chain intact (signatures not checked: pass
  --key <code> or set AVEN_LEDGER_KEY), head 1e61a9c5de48af4c628242f5…

# change one recorded value by hand, then verify again
$ avenc verify-ledger audit.jsonl
Ledger TAMPERED or invalid: line 1: fact #1: displayed value
  differs from its hashed value_bits
exit code 1

Verification

Claims are checked against independent references

The verify/ harnesses in the repository compare Aven with established tools, and tests/claims.rs turns each documented claim into a test.

Harness	What it checks
`verify/oracle.py`	Answers match HiGHS and SciPy on random integer, linear, infeasible, unbounded, nonconvex-integer and smooth models.
`verify/c_diff.py`	Emitted C compiles warning-free, is branchless, and matches `avenc run` exactly.
`verify/fuzz.py`	Malformed and adversarial input never crashes, panics or hangs the compiler.
`verify/ledger_tamper.py`	Every tampering technique tried on an audit log is detected.
`verify/live_atmosphere.py`	The flight model matches an independent ISA computation on 150 live aircraft.

Build your first model in fifteen minutes

The guide walks from installation to solving, unit checking, optimization and code generation, with every example runnable as written.

Start the guide Try the live demo