Quantum Circuit and Algorithm Validation With Prove-It

Validating algorithm implementations is increasingly important, especially to distinguish implementation mistakes from noise inherent to so-called Noisy Intermediate-Scale Quantum (NISQ) technologies. Debugging a quantum computation is problematic because intermediate states cannot be probed without interfering with the computation. We demonstrate formal quantum algorithm verification using our versatile Python software package called Prove-It [1]. Prove-It is designed to be accessible, convenient, and extensible. It supports unlimited expressivity using LaTeX (including quantum circuit expressions), freedom to add and conveniently track axioms, flexibility to prove theorems independently in any order, and extensible automation capabilities.
[1] www.pyproveit.org