​While quantum computers are still a while away, one day they will exponentially increase computing capacities in several key fields. And researchers are getting ready now, making sure they will be prepared to verify the performance of the programs that will ultimately be implemented on quantum computers—a task that presents a number of challenges. While there are methods for testing conventional programs, they are not really suitable for quantum computers, either because they would be too costly or, in some cases, simply impossible to implement.

To fill this gap, List researchers drew on their broad, deep knowledge of computer security to develop a reliable analysis tool. They used state-of-the-art formal methods (techniques to verify that conventional programs do not contain any bugs), but made them compatible with quantum code. First, they made the necessary changes to each logic component (specifications for the behaviors expected of the system, mathematical characterization of the system's actual behavior, and the algorithm to verify that the behavior aligns with specifications). Next, they created QBrick, a specification, programming, and formal verification environment for quantum programs based on the best practices in formal methods for conventional software verification, but modified for quantum computing. They validation-tested this significant advance on a complex use case:  the Quantum Phase Estimation (QPE), the core component of Shor's algorithm, which can be used to hack financial transaction encryption keys, a world first!