We open-sourced Aria, the small readable language our quantum models are written in, under Apache-2.0 at github.com/Anzaetek/aria-quantum-language-oss-public. It is a standalone repository now — its own CLI, its own pure-Rust runtime, 32 worked examples, and Lean 4 correctness proofs — not a tutorial bundled inside something else.
The pitch is one source, many targets. An Aria circuit parses to a backend-agnostic IR and then runs, trains its symbolic angles, and exports — to OPENQASM 2.0, JSON, or machine-checked Lean 4 — all from the same readable text.
circuit Bell() {
qreg q[2]
creg c[2]
apply H on q[0]
apply CX on q[0], q[1]
measure q[0] -> c[0]
measure q[1] -> c[1]
}
$ aria run examples/aria/bell.aria --circuit Bell --statevector
|00> +0.707107+0.000000i
|11> +0.707107+0.000000i
$ aria run examples/aria/bell.aria --circuit Bell --expectation "Z0 Z1"
<Z0 Z1> = 1.000000000000
No libtorch required
The default backend is a pure-Rust CPU statevector simulator — exact, no Python, no libtorch. symbolic[k] declares a trainable angle, and aria train optimizes it with parameter-shift gradients on that same pure-Rust simulator. The canonical demo recovers the H₂ ground-state energy (exact minimum −1.851199) by VQE, with nothing on the host but Rust.
Performance and scale are backend choices behind a single trait (omega_core::executor::Backend):
| --backend | What | Status | |-------------|------|--------| | sim (default) | pure-Rust CPU statevector, exact | ✅ | | mps | pure-Rust MPS, scales with bounded entanglement | ✅ | | gpu | Metal / CUDA / OpenCL (feature-gated; auto-falls back to sim) | ✅ | | remote | delegate to a running omega-server over HTTP | ✅ | | tch | libtorch tensor statevector, if you want it | ✅ (opt-in) |
libtorch is the opt-in, not the dependency.
Verified, not "looks right"
Every .aria file is held to a numeric standard. 31 of 32 examples are numerically verified against an independent oracle — a closed-form classical algorithm where one exists (DFT for QFT, Jacobi SVD for QSVD, brute-force max-cut for QAOA, hidden-string recovery for Bernstein–Vazirani, decoded bits for teleport…), or a differential check against a separate pure-Rust statevector for the parametrized templates. CI asserts on the PASS/FAIL. The one exception is shor_ecdlp.aria, which is labelled a showcase because cross-register oracle inlining is not implemented — and we say so in LIMITATIONS.md rather than quietly counting it as passing.
The repository ships an honest scope document precisely because the verified parts are strong: HHL and QSVT are present as structural .aria templates, while their faithful, proven forms live in Lean (HHL.lean, QSVT.lean) and the pure-Rust solver kernels. We would rather draw that line in writing than blur it.
Proven in Lean 4
The recognized circuits — Bell, GHZ, QFT, QPE, Grover — export to sorry-free Lean 4 correctness theorems through a structural recognizer, and the proof root (38 Lean files, including the QSP forward/converse theorems we wrote about separately) is machine-checked. The general arbitrary-circuit correspondence is explicitly deferred, and labelled as such. aria export --gate-model is the bridge from a circuit you can read to a theorem a machine has checked.
Learn it in one sitting
TUTORIAL.md is a hands-on tour — Bell → GHZ → QFT → when conditionals → trainable ansätze → backends → QASM/Lean export — with every command real and its numeric output shown. GRAMMAR.md is the complete reference with an EBNF grammar, and editor support (tree-sitter · Neovim · VS Code) lives in editors/.
$ cargo build -p aria-cli
$ aria run examples/aria/qft.aria --circuit QFT --int n=3 --statevector
Clone it, build the CLI, run an example, and read the proof it exports. That is the whole point of putting it in the open.