Quantum computing, without the guesswork.
We're a team in Seoul building the tools we wanted ourselves: a quantum language you can actually read, a runtime that runs on your hardware, and proofs that a circuit does what you meant. Then we use them on real problems in optimization and finance.
Here's what we work on.
Aria Language
A small, readable language for quantum circuits. One source runs, trains and exports to OpenQASM 2.0 or machine-checked Lean 4.
Explore Aria →OptimizationAria-Opt
Write a MILP / QUBO model once in Aria and route it to HiGHS, CBC, SCIP, CP-SAT or our simulated-bifurcation machine. In development; it keeps the parameter names and model semantics you already know from the big commercial solvers.
See Aria-Opt →LicensedQuantum Toolkit (Sqetch)
Our licensed toolkit on the Aria runtime: optimizer passes, QML, error correction, Lean 4 and Rocq export, and a finance lab.
See the toolkit →AppliedFinance & Trading
Synthetic OHLC data, regime classification with GBDT, DNN or QNN, and walk-forward backtests on synthetic series.
See finance →You write the circuit once. Aria takes it from there.
- Pure-Rust runtime, no libtorch required
- Export to OpenQASM or Lean 4
- Opt-in Python bindings and editor support
Next releaseFaster simulation, and multi-QPU emulation: several QPUs linked by a quantum optical network, emulated from one Aria program.
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.000000iWe built an image generator that a quantum circuit can steer.
An image generator steered by sixteen numbers. Today a small classical network picks them; the plan is for a quantum circuit to do it instead.
See the generator →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.
→