Aria, open-sourced: one language, every modality
Aria is open source under Apache-2.0 at github.com/Anzaetek/aria-quantum-language-oss-public: its own CLI, its own pure-Rust runtime, 43 verified example circuits and Lean 4 correctness proofs.
The idea is one source, many targets. A circuit parses to a backend-agnostic IR, then runs, trains its symbolic[k] angles, and exports to OpenQASM 2.0, JSON or Lean 4.
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.000000iOne runtime, five modalities
Every engine implements the same trait, omega_core::executor::Backend, so the choice of physics is a flag, not a rewrite. Each modality has its own language surface and is checked against an independent implementation, never only against our own.
| Modality | Written as | Engines | Checked against |
|---|---|---|---|
| Qubits | .aria, OpenQASM 2 | dense statevector (CPU · CUDA · Metal · OpenCL · libtorch) · MPS tensor network (GPU SVD) · Pauli propagation with a certified truncation bound | Qiskit Aer, quimb, ppvm |
| Qudits | DITQASM (mixed radix) | exact mixed-radix statevector · MPS | mqt.qudits, QuickQudits |
| Fermions (Majorana) | FermionicQASM 1.0, OpenFermion ladder text | Majorana propagation with a dropped-mass certificate · fixed particle-number sector · Jordan–Wigner lowering to any qubit engine | ffsim, OpenFermion-FQE |
| Photons (DV, CV) | .opticqasm, CV programs | Fock-space photonics with a one-way cluster-state executor · continuous-variable on a truncated Fock space | Perceval, piquasso |
| Stabilizer | OpenQASM 2 | Clifford tableau · stabilizer rank (exact-phase CH form) | Stim |
On top of the modalities, aria-qec runs surface and Steane codes, transversal gates, magic-state distillation and decoders on any of those engines.
Backends from the command line
$ aria run qft.aria --circuit QFT --int n=3 --backend sim # pure-Rust statevector (default)
$ aria run bell.aria --circuit Bell --shots 4096 --backend mps # tensor network
$ aria run bell.aria --circuit Bell --expectation "Z0 Z1" --backend pauliprop
$ aria run qft.aria --circuit QFT --int n=3 --backend gpu # Metal / CUDA / OpenCL
$ aria run qft.aria --circuit QFT --int n=3 --backend remote --url http://host:8080
$ omega-run --backend {stabilizer,sr,qudit,sector,mp,photonics,cv} …GPU backends are feature-gated and fall back to the CPU engine when no device is present. libtorch is an opt-in backend (tch), not a dependency.
Train, verify, prove
aria train optimizes symbolic[k] angles with parameter-shift or exact adjoint gradients on the pure-Rust simulator; the canonical demo recovers the H₂ ground-state energy by VQE. aria tune searches meta-parameters with TPE and pruning.
Every example carries a numeric check against an outside oracle: a closed-form algorithm where one exists, a differential statevector otherwise. CI asserts on the result, and the gate set is mutation-tested (797 gate and 286 angle mutants).
The recognized circuits (Bell, GHZ, QFT, QPE, Grover) export to sorry-free Lean 4 theorems; the proof root includes the QSP forward and converse theorems we wrote about separately. What is not yet proven, such as the general arbitrary-circuit correspondence, is listed as deferred in LIMITATIONS.md rather than blurred.
Try it
$ cargo build -p aria-cli
$ aria run examples/aria/qft.aria --circuit QFT --int n=3 --statevectorTUTORIAL.md walks from Bell to trainable ansätze and Lean export with every command shown; GRAMMAR.md is the full reference. Editor support for VS Code, Neovim and tree-sitter is in editors/.