Qiskit ZX Verified

formal-verification
compiler
lean4
A Clifford phase-gate fusion pass with a Lean 4 formal verification bridge
Published

August 13, 2026

STATUS · Qiskit Ecosystem Member · 34 passing tests

What it does

A ZX-calculus-based transpiler pass for Qiskit that fuses adjacent Clifford phase gates — the same class of local rewrite PyZX and similar tools perform — but pairs the rewrite rule with a Lean 4 proof obligation, using the same verification approach as Qiskit-LEAN-Bridge: the fusion identity is checked against an independent, machine-checkable semantics rather than trusted by construction.

This follows directly from the LEAN bridge work above. Once you have a pipeline for numerically verifying gate-identity conventions and staging them into real Lean lemma statements, applying the same discipline to an actual transpiler pass — one that changes circuits, not just documents equivalences — is the natural next step.

Why pair a compiler pass with a proof obligation

Circuit optimizers that rewrite gates are exactly the kind of code where a silent sign error or an off-by-one convention mismatch produces a circuit that looks right, runs, and returns a subtly wrong answer. ZX-calculus fusion rules are simple enough to state precisely and small enough to actually verify — which makes them a good first target for closing the loop between “this rewrite rule is intended to preserve the circuit’s unitary” and “this rewrite rule is proven to preserve the circuit’s unitary.”