Certified Quantum Computation in Isabelle/HOL

TL;DR

This paper details the formalization of quantum algorithms and theorems within Isabelle/HOL, aiming to enhance the safety and security of quantum computing through rigorous proof methods.

Contribution

It introduces a comprehensive library for quantum computing in Isabelle/HOL and formalizes key quantum theorems and algorithms, advancing formal verification in quantum information.

Findings

Successful formalization of the no-cloning theorem

Formal proofs of quantum teleportation and algorithms

Application to quantum game theory

Abstract

In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch's algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory.