Things we've written about how it works.
How the pieces work: proofs, compilers, runtimes and the languages on top.
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.
→