A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm

TL;DR

This paper demonstrates the first formally certified end-to-end implementation of Shor's quantum factoring algorithm, showcasing how formal methods can enhance correctness and reduce human errors in quantum programming.

Contribution

It introduces a novel framework for applying formal methods to quantum programming, enabling certified correctness proofs for complex quantum algorithms like Shor's.

Findings

First certified implementation of Shor's algorithm

Framework reduces human programming errors in quantum software

High-assurance quantum applications become feasible with formal verification

Abstract

Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but these are only useful if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors -- "bugs". Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. With such methods, a programmer writes a mathematical specification alongside their program, and semi-automatically proves the program correct with respect to it. The proof's validity is automatically confirmed -- certified -- by a "proof assistant". Formal methods have successfully yielded high-assurance classical software artifacts, and the underlying technology has produced certified proofs of major mathematical theorems. As a demonstration of the feasibility of applying formal methods to quantum programming, we present the first formally certified end-to-end implementation of Shor's prime factorization algorithm, developed as part of a novel framework for applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain a high-assurance implementation of large-scale quantum applications in a principled way.