We are publishing a snapshot of the Anzaetek Quantum stack as it stands today. This post is deliberately narrow: it lists what is shipping, not what is coming. If you want a feature, check here before asking — if it is not on this page, it is not in the build.
Two layers
The stack is two layers: an open-source runtime (omega-functions) and a closed-source toolkit (Quantum) built on top.
Runtime — open source, Apache-2.0 at github.com/Anzaetek/omega-functions-public. Announced today. It is the execution layer — four simulation backends, PQC-authenticated server, C FFI, WASM sandbox, CLI.
Quantum toolkit — closed source. It is the circuit layer — an IR with symbolic parameters and annotations, optimizer passes, format exporters, a QML stack, error-correction codes, and a spec-extraction pipeline to Lean 4 and Rocq. It compiles down to the open runtime.
Circuit language
The Quantum toolkit's AST covers 30+ gate types across Pauli, Clifford, T, rotation, controlled, and photonic families. Parameters can be symbolic (ParamExpr: symbols, Pi, binary operations, function calls), which is what makes variational algorithms work without special-casing. Annotations — Assert, Prove, Ensures, Requires, Invariant, ResourceBound — attach correctness claims to circuit points so that the Lean/Rocq exporters know what to prove.
There is a circuit! proc-macro for inline Rust construction:
circuit!(bell, 2, 2 => { h 0; cx 0,1; measure_all; })
And a pipe/tensor-product composition algebra (>>, |, repeat, inverse) for building larger circuits from parts.
Optimizer — 13 passes
Identity removal, adjacent gate cancellation, adjoint-pair cancellation (collapses QFT >> IQFT to zero gates), rotation merging, commutation reorder, gate decomposition, T-merge, FastTMerge on a Clifford tableau, PhasePolyDedup with an F₂ Gaussian-elimination kernel search (per arXiv:2407.08695), BBMerge, InternalHOpt, the Clifford+T pipeline, and optional Tket2 integration. These are not speculative; they ship in quantum-core and each has unit tests.
Format exporters — 8 formats
OpenQASM 2.0, OPTICQASM 1.0, JSON, .qc, omega-IR (for direct handoff to the runtime), C ABI FFI, Lean 4, and Rocq/Coq. The Lean 4 and Rocq exports turn a circuit plus its annotations into theorem statements that the prover checks.
QML
quantum-qml is a statevector simulator with mid-circuit projective measurement and reset, a QuantumLayer type that integrates with PyTorch through tch-rs, parameter-shift gradients that flow through tch's autograd, a pure-Rust CMA-ES optimizer for the gradient-free cases, and a surrogate trainer implementing arXiv:2505.05249.
The circuit builders that ship today cover standards (Bell, GHZ, QFT, QPE), Trotter steps (1st and 2nd order, H₂, Ising, Heisenberg), photonic meshes (Clements, MZI), QSVT and LCU block encoding, and QML encoding layers (angle, IQP, hardware-efficient).
Error correction
Repetition code [[n,1,n]], Steane [[7,1,3]], and surface code [[d²,1,d]] with an add_error_correction transform that lifts a logical circuit into an encoded one. There is an MWPM decoder for surface-code syndromes.
Algorithmic examples
These compile, run, and are part of the examples directory and test matrix:
- Shor — factors 15, 21, 35; a semiclassical 1-counting-qubit variant; Shor-DLP (discrete logarithm); Shor-ECDLP with structural EC-point-addition circuits at p = 97 and surface-code physical-resource estimates at secp256k1-sized primes (256–521 bits).
- QFT / QPE — both standard and iterative (Kitaev's 1-ancilla variant), with robust-phase-estimation examples.
- HHL — full linear-system solver example, not a stub.
- Grover — 2- and 3-qubit search with statevector verification.
- Block encoding and LCU — diagonal block encoding and linear-combination-of-unitaries demos.
- Quantum walk, Deutsch–Jozsa, Bernstein–Vazirani, Simon, swap test, teleportation, superdense coding — small but real.
- QAOA — MaxCut example with parameter-shift gradient descent and a CMA-ES variant; lives as a WASM guest that the open runtime can execute in its sandbox.
- VQE — H₂ ground-state example at the reference energy, also shipped as a WASM guest.
Aria DSL and resource estimation
Aria is the surface DSL we use to describe circuit templates that can be instantiated with different parameters. The parser in quantum_core::ast::aria produces an AriaProgram of templates; AriaProgram::instantiate(name, ¶ms) lowers a template to a concrete Circuit — loops unrolled, oracles inlined, symbolic parameter arrays resolved. Five example .aria files all round-trip through parse and instantiate.
The quantum_core::resource module provides logical ResourceEstimate counts and surface-code PhysicalEstimate extrapolations, plus an oracle-sketching layer for comparing algorithm variants that differ only in their oracle implementation.
Spec extraction to Lean 4
quantum spec extract --aria turns Aria annotations into Lean 4 theorem obligations. There is also a #[quantum_core::spec] attribute macro that decorates a fn -> Circuit and emits build.rs recipe for compile-time emission.
Proofs that actually close
Lean 4 standalone (23 theorems, 0 sorry). Gate identities (H² = I, HXH = Z, HZH = X, Clifford self-inverse pairs), Grover probability bounds, DFT unitarity up to packaging, QPE accuracy bounds.
Lean 4 mathlib-backed (6 files, partial closure). ECC is fully closed — rep3_encode is defined as denote [CX(0,1); CX(0,2)] and the syndrome/decode theorems are proved. BlockEncoding is fully closed. CircuitSemantics has one open sorry on denote_embed_subcircuit. QFT has two open sorries on the dft_unitary and qft_correct step cases (mathlib's Kronecker packaging). QPE has two open sorries on the orthogonality / Dirichlet-kernel packaging. Grover has four open sorries on the 2D-subspace argument. The statements are all load-bearing types over real unitary / matrix predicates, not placeholder Prop := sorry stubs.
Rocq. Four files (Gates, QFT, Grover, QLibCompat shim). Covers σ-self-inverse, S² = Z, XZ anti-commute, QFT 1-qubit structural lemmas, Grover probability bounds.
Server and clients
quantum-server speaks length-prefixed JSON over a Unix socket with 0600 permissions or a TCP socket with bearer-token auth. Methods: ping, info, parse, optimize, compile. Reference client implementations ship in Rust (standalone Cargo, serde_json only), Python (stdlib only, ≥ 3.8, tested on 3.13.5 and 3.9.6), and shell (bash + python3 for framing + optional jq).
Omega-functions integration
Eleven of eleven integration requirements with omega-functions are done. The open runtime's omega-server exposes /v1/quantum/execute accepting the Quantum toolkit's OmegaCircuitIR JSON with a backend selector that dispatches to Statevector / MPS / Pauli / Photonics. The Observable builder and gradient methods are wired end-to-end. The photonics backend has a parameter-shift-based adjoint gradient.
Distribution
Binary-only tarballs via scripts/release/: build-host-cpu.sh for the current machine, build-host-gpu.sh for Metal (macOS) or CUDA (Linux) with libtorch bundling, build-all-cpu.sh for darwin-arm64, linux-amd64, linux-arm64 cross-builds, and build-all-gpu.sh for the GPU variants. Each tarball carries bin/, examples/ (Aria, e2e, client-rust/python/shell, Rust, WASM guests), and docs/. A compile-time expiry check runs when QUANTUM_EXPIRY_DAYS is set.
What this post is not
This is a state-of-the-build. It is not a roadmap. Items that are on the TODO list — closing the remaining Lean 4 sorries, GPU backends, full executable Shor-ECDLP at large primes, TOHPE kernel-search equivalence proofs — are left out on purpose. When they ship, they will be announced the same way.
For access to the closed-source toolkit or a custom integration, contact@anzaetek.com. The open runtime is at github.com/Anzaetek/omega-functions-public and needs no contact — clone, build, ship.