qiskit-transpile-verify

Translation validation for the Qiskit transpiler: verify that a PassManager's output implements the same operation as its input, pass by pass, on the Clifford fragment.

A transpiler pass that silently produces a non-equivalent circuit is a correctness bug that's easy to miss in review and hard to catch with unit tests alone, since the bug only shows up on specific gate sequences. This tool checks every pass in a run against stabilizer tableau equivalence, so a miscompilation is caught at the pass that introduced it — not discovered downstream as a wrong measurement distribution.

Scope: this is a Clifford-fragment tool, stated up front

qiskit-transpile-verify v0.1 verifies circuits made up of Clifford gates (h, s, sdg, sx, x, y, z, cx, cy, cz, swap, ecr, and rz/rx/ry/p at Clifford angles). It does not verify circuits containing t, arbitrary rotation angles, or other non-Clifford gates — those are reported as out-of-scope, not silently skipped or falsely passed. See docs/LIMITATIONS.md for exactly what this does and doesn't prove, and why universal (Clifford+T) verification is a substantially different — and harder — problem, not just a bigger gate list.

Install

pip install qiskit-transpile-verify
# CLI (QASM3 file support) needs one extra dependency:
pip install "qiskit-transpile-verify[cli]"

Quick start: verify a custom pass

from qiskit.circuit import QuantumCircuit
from qiskit.transpiler import PassManager
from qiskit.transpiler.passes import CommutativeCancellation
from qiskit_transpile_verify import verify_transpile

qc = QuantumCircuit(3)
qc.h(0)
qc.cx(0, 1)
qc.cx(0, 1)   # redundant pair
qc.cx(1, 2)
qc.s(2)

report = verify_transpile(PassManager([CommutativeCancellation()]), qc)
print(report.summary())
assert report.all_verified

1 pass(es) run:
  [0] CommutativeCancellation: VERIFIED

What it actually catches

This isn't a hypothetical. Here's a deliberately broken cancellation pass that cancels cx(a, b) against cx(b, a) as if they were inverses of each other — they aren't, since swapping control and target changes the operation — run through verify_transpile:

class BuggyCXCancellation(TransformationPass):
    """Cancels any two adjacent CX gates on the same qubit pair,
    regardless of control/target order. This is wrong."""
    ...

qc = QuantumCircuit(2)
qc.h(0)
qc.cx(0, 1)
qc.cx(1, 0)   # NOT the inverse of cx(0, 1)

report = verify_transpile(PassManager([BuggyCXCancellation()]), qc)
print(report.summary())

1 pass(es) run:
  [0] BuggyCXCancellation: MISMATCH — possible miscompilation

FIRST FAILURE at pass [0] BuggyCXCancellation: no qubit permutation
reproduces a matching tableau

The full runnable version of this example is in tests/test_verify.py::test_buggy_pass_is_caught.

Verifying a full preset pass manager run

The CLI runs a QASM3 circuit through one of Qiskit's built-in preset pass managers and verifies every pass:

qtv circuit.qasm3 --optimization-level 3

37 pass(es) run:
  [0] ContainsInstruction: VERIFIED
  [1] UnitarySynthesis: VERIFIED
  [2] HighLevelSynthesis: VERIFIED
  ...
  [36] ContainsInstruction: VERIFIED

(Tested against Qiskit 2.5.2's generate_preset_pass_manager at optimization levels 0–3 on Clifford-fragment input; every individual pass verified across all levels tried so far. This is not a formal proof that the preset pass managers are bug-free in general — see Limitations.)

API surface

• verify_transpile(pass_manager, circuit) — run and verify a whole PassManager, pass by pass. Returns a VerificationReport with .all_verified, .first_failure, .out_of_scope_passes, .summary().
• check_equivalence(circuit_a, circuit_b, allow_permutation=True) — check two circuits directly, with optional qubit-permutation search (useful since layout/routing passes legitimately relabel qubits).
• check_equivalence_with_layout(circuit_a, circuit_b, layout) — same, but with a known layout instead of brute-force search (use this above ~8 qubits, since permutation search is O(n!)).
• check_scope(circuit) — check whether a circuit is in the Clifford fragment before attempting verification.

Relationship to qiskit-zx-verified

This package extends the translation-validation idea from qiskit-zx-verified — which formally proves (Lean 4, zero sorrys) that one specific Clifford phase-fusion pass is correct — into a general-purpose checker that works on any PassManager, at the cost of a weaker guarantee: a fast runtime equivalence check rather than an independently checkable proof term. Generating Lean certificates for arbitrary passes is the planned v0.2 direction; see lean/README.md for the honest current status (not implemented in v0.1) and the reasoning behind the scoping.

License

Apache-2.0