​Although the perfect quantum computer hasn't been invented yet, algorithms have been developed and are ready to be implemented on tomorrow's quantum machines. The best-known example is probably Shor's algorithm, which can crack virtually any encryption key in a fraction of a second. CEA-List quantum software researchers are studying how to verify during development that quantum programs can be run on a machine and that they will operate as intended.

Verification methods do exist for classical software but are not applicable to quantum programs. CEA-List possesses strong expertise in formal verification methods for classical software, and the quantum verification tools developed here were adapted from these methods. The result is a software environment called QBrick that can be used to verify that a quantum program will run as intended, regardless of the inputs.

In this research, QBrick was used to verify the quantum part of a Shor's algorithm implementation—a world first. And the verification process was more than 95% automated: three times more automation than other verification methods on a program six times the size. The research, which marks a major step toward the development of efficient quantum programming methods and environments and positions the CEA as one of France's leaders in quantum, was presented at ESOP 2021.