Efficiently Verifying Quantum Programs with Few T Gates

Abstract

We mechanize a lightweight quantum logic in the Rocq proof assistant to verify Clifford+T quantum programs, particularly those with low T counts. Our tool is lightweight and automation-centric: Hoare triple validation composes simple rules, reduces all obligations to syntactic well-formedness side-conditions, and efficiently discharges those conditions. We demonstrate our tool using several case studies: a standard low-T Toffoli decomposition, graph-state generators, and the 7-qubit Steane encoder. A small empirical study on graph-state families shows near-linear growth in the number of Clifford gates and a slightly super-quadratic trend in the number of qubits, consistent with implementation overheads from list-based tensor representations, while repeated T gates on a single qubit exhibit an exponential blow-up due to additive branching. The results indicate that a rule-driven, syntax-directed approach suffices to verify low-T quantum circuits while keeping the trusted core and user-facing proofs simple.