Omega Functions has been quietly getting more serious. Three months ago it was a multi-backend quantum runtime; today the circuit optimizer is backed by Lean 4 correctness proofs, the gradient stack handles mid-circuit measurement, and the optimization loop supports gradient-free CMA-ES for the cases where adjoint differentiation doesn't apply. This post covers what's changed and why it matters for anyone running quantum workloads in production.
Verified Optimizer Passes
Circuit optimization is high-leverage. A pass that turns a 10,000-gate VQE circuit into a 6,000-gate equivalent saves 40% of the shot budget, which on current hardware is the difference between a viable experiment and a wasted week. But optimizer bugs are silent killers — if a pass subtly changes the operator it implements, every downstream result is wrong in a way that unit tests rarely catch.
The new work adds Lean 4 + mathlib proofs of pass correctness. For each optimization pass, we state a denotational equivalence theorem: the circuit before and after the pass denote the same unitary matrix up to global phase. The proofs cover the stable passes:
- Identity gate removal
- Adjacent gate cancellation (X·X = I, H·H = I, CNOT·CNOT = I)
- Rotation merging (R_z(α)·R_z(β) = R_z(α+β))
- Commutation-based reordering (operators on disjoint qubits commute)
- T-gate merging
The T-merge proof was the tricky one — it depends on the Clifford tableau representation staying faithful across the merge, which is a structural claim about the stabilizer formalism rather than a straight matrix equality. The proof chain uses mathlib's group theory for the Pauli group and bounded-qubit-count induction for the tableau preservation.
CMA-ES for Non-Differentiable Loops
Not every quantum loss landscape is smooth. Hardware-efficient ansätze with measurement-based postselection have discontinuities at the postselection boundaries. Stochastic compilation pipelines introduce noise that defeats gradient-based optimizers. For those cases the runtime now includes CMA-ES, a gradient-free evolutionary strategy that adapts a covariance matrix over the search distribution.
CMA-ES is well-studied and the implementation is standard, but the integration is worth noting: it runs inside the WASM execution mode alongside gradient-based optimizers. A user can flip a single flag to move a QAOA loop from parameter-shift gradients to CMA-ES without rewriting the circuit. For noisy near-term hardware this turned out to be the right default for several workloads we ran — gradient-shift overhead swamps the signal when shot noise is large, and CMA-ES's population-based exploration is more tolerant.
Mid-Circuit Measurement, Conditional Gates, Reset
Classical control flow inside quantum circuits is no longer a special case. The runtime handles:
- Mid-circuit measurement with post-measurement amplitude propagation in statevector mode, stabilizer projection in Pauli mode, and transfer-matrix norm computation in MPS mode.
- Conditional gates —
when m[k] == vstyle branches that evaluate classically on measurement outcomes and dispatch the gate only on the matching branch. - Reset — post-measurement amplitude transfer to $|0\rangle$, implemented consistently across all four backends.
Together these lift Omega from "simulates the unitary evolution of a circuit" to "simulates a full quantum program, including measurement-based computation." Teleportation, iterative phase estimation, error-correction cycles, and dynamic-circuit QAOA now run end-to-end without host-side classical stitching.
Observable Builder and Operator Arithmetic
Constructing Pauli observables used to require manual tensor assembly. The new Observable builder supports natural operator arithmetic:
let H = 0.5 * Z(0) + 0.3 * (X(0) * X(1)) - 0.2 * Y(0) * Y(1);
let energy = backend.expectation(circuit, H)?;
Behind the scenes the builder flattens into a Pauli-string representation with fused-multiply-add accumulation. Resource estimation (gate counts, circuit depth, T-count, two-qubit count) runs on the CircuitIR directly without needing to execute.
Multi-Observable Evaluation
The WASM host functions now include a shots_multi_observable entry point that evaluates multiple observables against the same measurement batch. A typical VQE loop needs to estimate the energy by summing expectation values of many Pauli strings; this entry point does it in a single host call rather than N round-trips across the WASM boundary. The reduction in FFI overhead is measurable for circuits where the classical loop is the bottleneck.
Why This Matters
If you're running quantum workloads today, the value of a runtime isn't raw simulation speed — many runtimes are fast. The value is trust. A verified optimizer means you can rewrite your circuit without wondering whether the rewrite broke anything. A multi-backend runtime with consistent semantics means you can prototype on statevector, scale to MPS when entanglement allows, and drop to Pauli for Clifford-heavy error-correction work, without changing your source code.
That's what Omega Functions is trying to be: a runtime you can stake a result on. The OSS counterpart lives at github.com/Anzaetek/omega-functions-public under Apache-2.0; the internal build tracks the same core plus Anzaetek-specific backends and the managed Sqetch integration.