Structural Verification of Quantum Circuits: A Haskell Implementation via Hoare Logic

As quantum hardware remains limited by qubit count and noise, the efficiency and correctness of quantum programs cannot yet be efficiently checked by execution or classical simulation alone. This thesis develops a Hoare logic for reasoning about the structural properties of quantum circuits produced by Proto-Qiskit, a Qiskit inspired programming language. We define derivation rules that treat commands that modify circuits as assignments, allowing properties such as gate count, circuit width, and depth to be specified and verified. These results are implemented in a Haskell tool that parses annotated Proto-Qiskit programs and proves their validity by generating verification conditions using weakest precondition calculus, with the support of an SMT solver. The tool is demonstrated on parametric example programs, including a quantum Fourier transform circuit, highlighting both its capabilities and its current limitations. Furthermore, we informally discuss the implementation of an optimization-aware extension of the logic based on a quantum state assertion language. This allows triviality conditions to be checked during verification so that redundant gates can be identified and removed while proving the correctness of the resulting optimized circuit. We discuss the issues this extension introduces for automated verification.