Quantum program verification made as simple as classical array checks
Connecting Quantum Proof Systems and Hoare Logic
Logic in Computer ScienceProgramming Languages
Summary
Verifying that quantum programs work correctly is very hard and usually needs special tools. The authors found a way to turn the problem of checking quantum programs into a problem of checking classical programs that handle arrays, which is much easier and better supported by existing tools. This means developers can use classical verification tools to ensure quantum programs are correct. Their approach makes quantum program verification more accessible and less costly.
What this means in practice
- •For quantum software developers: Use classical program verifiers to check quantum code correctness without specialized quantum proof tools.
- •For classical verification tool builders: Expand existing verification tools to support quantum programs by leveraging the embedding of quantum proofs into classical logic.
Authors
Liyi Li, Zoukarneini Difaizi Tagba, Alex Potanin
Abstract
Verifying quantum programs today requires specialized proof systems built on interactive theorem provers such as Rocq, Lean, Isabelle, or Why3, and even modest quantum algorithms cost substantial human effort to verify. Because quantum programs cannot be effectively checked by runtime testing, formal verification is the only viable path to correctness, making the cost of these bespoke systems the chief barrier to scalable quantum software assurance. We show that verifying a quantum program should be no harder than verifying a classical array program, a paradigm commonly used in parallel programming: the Qafny quantum proof system translates into Hoare logic with array theory completely (every Qafny proof becomes a valid Hoare triple) and soundly (a valid translated triple certifies only true quantum specifications), and we mechanize the completeness direction in Rocq. The embedding determinizes quantum proof obligations and exposes the full machinery of classical automated verifiers (e.g. Dafny and SMT-based separation logic) to quantum code, removing the need for dedicated quantum proof system infrastructure. In particular, the embedding supplies the correctness argument that the existing compilation of Qafny into Dafny lacks.