Metadata-Version: 2.4
Name: qiskit-transpile-verify
Version: 0.1.0
Summary: Formal and statistical equivalence checking for Qiskit transpiler output on the Clifford fragment, with optional Lean 4 certificate generation.
Author: Rex Rowan
License: Apache-2.0
Project-URL: Homepage, https://github.com/RexRowan/qiskit-transpile-verify
Project-URL: Repository, https://github.com/RexRowan/qiskit-transpile-verify
Project-URL: Issues, https://github.com/RexRowan/qiskit-transpile-verify/issues
Keywords: qiskit,transpiler,formal-verification,clifford,stabilizer,lean4
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering :: Physics
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: qiskit<3,>=2.0
Requires-Dist: numpy>=1.23
Provides-Extra: dev
Requires-Dist: pytest>=7.0; extra == "dev"
Requires-Dist: pytest-cov; extra == "dev"
Provides-Extra: cli
Requires-Dist: qiskit-qasm3-import>=0.4.0; extra == "cli"
Dynamic: license-file

# 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`](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

```bash
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

```python
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`:

```python
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:

```bash
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`](https://github.com/RexRowan/qiskit-zx-verified) —
which formally proves (Lean 4, zero `sorry`s) 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`](lean/README.md) for the honest current
status (not implemented in v0.1) and the reasoning behind the scoping.

## License

Apache-2.0
