Description

In this paper, we introduce the idea of the hierarchical formal verification for quantum circuits, where we use a powerful language, higher-order logic, to reason about quantum circuits formally. The analysis and verification is conducted within a mechanized theorem prover. We propose a formal modeling and verification approach that captures quantum models built hierarchically from primitive optical quantum gates. The analysis and verification of composed circuits is done seamlessly based on dedicated mathematical foundations formalized in the theorem prover. In order to demonstrate the effectiveness of the proposed infrastructure, we present the formal analysis of the controlled-phase gate and Shor's factoring circuits. Consequently, we design and verify a new design for quantum flip gate.