Aria Language
A small, readable language for quantum circuits. One source parses to a backend-agnostic IR, then runs, trains its parameters, and exports to OpenQASM 2.0, JSON or machine-checked Lean 4.
Here's a Bell pair, run from the command line.
Circuits are plain text. The aria binary lists, parses, runs, trains, exports and tunes them.
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 bell.aria --circuit Bell --statevector
|00> +0.707107+0.000000i
|11> +0.707107+0.000000i
$ aria run bell.aria --circuit Bell --expectation "Z0 Z1"
<Z0 Z1> = 1.000000000000What you get from writing circuits in Aria.
Export to whatever you need
The same circuit runs directly or exports to OpenQASM 2.0, JSON or Lean 4 correctness theorems.
Train it where it is
symbolic[k] declares trainable angles. aria train optimizes them with parameter-shift gradients in pure Rust, without libtorch. aria tune searches meta-parameters.
Pick your simulator
Every backend implements one trait: CPU statevector by default, plus MPS, GPU (Metal, CUDA, OpenCL), libtorch and a remote omega-server.
Every example is checked
All 43 examples are numerically verified against independent classical oracles. The Lean 4 proofs are sorry-free.
What it can simulate, and how.
Every modality has its own engines, and each is checked against an outside reference such as Qiskit, Stim, ffsim or Perceval.
- QubitsDense statevector on CPU, CUDA, Metal, OpenCL or libtorch; MPS tensor network with GPU-accelerated SVD; Pauli propagation in the Heisenberg picture with a certified truncation bound.
- QuditsExact mixed-radix statevector for DITQASM circuits, with MPS as a second engine.
- Fermions (Majorana)Majorana propagation with a dropped-mass certificate; an exact fixed-particle-number sector engine; Jordan–Wigner lowering to any qubit engine. Written in FermionicQASM 1.0 or OpenFermion ladder text.
- Photons (CV and DV)Discrete-variable: Fock-space photonics for OPTICQASM circuits, with a one-way cluster-state executor. Continuous-variable: programs on a truncated Fock space.
- StabilizerClifford tableau for fast expectation values; stabilizer rank in exact-phase CH form for amplitudes, inner products and Pauli matrix elements.
The ways it computes.
Pick the method that fits the circuit. Exact where exact is affordable, certified approximations where it is not.
- Dense statevectorExact amplitudes for every basis state, on CPU, CUDA, Metal, OpenCL or libtorch.
- Tensor network (MPS)Matrix-product states with a bounded bond dimension, so width scales with entanglement rather than qubit count. Includes a noisy-MPS lane.
- Heisenberg propagationObservables pushed back through the circuit as Pauli or Majorana sums. Exact on Clifford circuits; truncated elsewhere, with a certified bound on the dropped weight.
- Stabilizer methodsClifford tableau for fast expectation values; stabilizer rank in CH form for exact amplitudes and inner products.
- Fock-space simulationPhoton-number states for discrete and continuous-variable optics, with permanent-based amplitudes.
- Particle-number sectorFermionic circuits simulated exactly inside a fixed-particle-number subspace.
- Measurement-based (one-way)A reference executor for cluster-state measurement patterns alongside the gate model.
- Training and searchParameter-shift and exact adjoint gradients for variational circuits; aria tune for meta-parameters (TPE with pruning); QUBO and QAOA formulations.
What we're working on next.
- PerformanceFaster simulation across the CPU and GPU backends.
- Multi-QPU emulationSeveral QPUs connected by a quantum optical network, emulated from a single Aria program.
What's in the repository.
- 43 example circuitsEach header cites the harness and the check it must pass.
- Error correction (aria-qec)Surface and Steane codes with transversal gates, magic-state distillation and decoders, on any of the backends.
- Lean 4 proof rootCorrectness theorems for the recognized circuits: Bell, GHZ, QFT, QPE and Grover.
- Editor supportSyntax for VS Code, Neovim and tree-sitter, plus opt-in Python bindings.
- Documented limitsLIMITATIONS.md, GATE-EXACTNESS.md and measured CPU-to-GPU crossover sizes ship with the code.
Things we've written about how it works.
Quantum Signal Processing, formally: the converse theorem in Lean 4
The converse fundamental theorem of Quantum Signal Processing — every admissible polynomial pair is realized by a phase sequence — is machine-checked, sorry-free, in the Lean 4 proof tree that ships with Aria.
→Aria LanguageFrom a circuit you can read to a theorem a machine has checked
aria export --lean turns a circuit and its annotations into Lean 4 theorems. Here is what gets exported, how we closed the proofs that were still open, and where the proof tree lives.
→Aria LanguageA circuit optimizer you can trust
Aria ships its own runtime. Its circuit optimizer rewrites gates in three small passes, each unit-tested, with the self-inverse identities it relies on proved in Lean 4.
→Aria LanguageAria, open-sourced: one language, every modality
Aria, our readable quantum-circuit language, is Apache-2.0 at github.com/Anzaetek/aria-quantum-language-oss-public. One source runs on qubit, qudit, fermion, photon and stabilizer engines, trains in pure Rust, and exports to OpenQASM 2.0 or machine-checked Lean 4.
→