Verification of quantum algorithms using quantum Hoare logic.


QHLProver is a tool for formally reasoning about correctness of quantum algorithms. It contains a formalization of quantum Hoare logic (QHL) in Isabelle/HOL. QHL is an extension of Floyd-Hoare logic to quantum programs. Our implementation of QHL in Isabelle/HOL is foundational: basic concepts in quantum computing are defined in terms of existing theories on complex numbers and matrices, and the soundness and completeness of QHL is proved within Isabelle, after specifying a denotational semantics for quantum programs. The tool is applied to verify the correctness of Grover’s algorithm.

QHLProver is developed at the State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences.


QHLProver requires Isabelle2018. Isabelle can be downloaded at: http://isabelle.in.tum.de/

Moreover, QHLProver depends on Isabelle’s AFP library. The AFP Library can be downloaded at: https://www.isa-afp.org/ (see “Using Entries” page for how to set up AFP on your computer).

Once Isabelle AFP is set up, the tool, download for QHLProver, can be opened directly in Isabelle/jEdit. See Grover.thy for an example.


A tutorial for QHLProver is available.