Formal methods for quantum research workflows

Quantum programs are unusually hard to debug empirically — you often cannot look at the state, and sampling error hides bugs. That makes them a natural target for formal methods, applied at three different altitudes.

Three altitudes of verification

1. Mathematics. Proof assistants (Lean, Coq, Isabelle/HOL) for the theorems a protocol rests on — unitarity, error bounds, the correctness of an amplitude estimate.
2. Circuits. SMT solvers (Z3) for circuit-equivalence and gate-level obligations, e.g. showing a compiled circuit implements the same unitary as its specification $U_{\text{spec}} = U_{\text{compiled}}$ up to global phase.
3. Systems. TLA+ for the classical orchestration coordinating classical and quantum execution — where the subtle concurrency bugs actually live.

These complement, rather than replace, Qiskit / PennyLane / Braket / QuTiP: the simulators tell you what a circuit does; the formal layer tells you what it is supposed to do, and where the two diverge.