Abstract While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor’s integer factoring, quantum phase estimation (QPE) and Grover’s search.
Abstract While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor’s integer factoring, quantum phase estimation (QPE) and Grover’s search.
While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. Early attempts either suffer from the lack of automation or parametrized reasoning, or target high-level abstract algorithm description languages far from the current de facto consensus of circuit-building quantum programming languages. As a consequence, no significant quantum algorithm implementation has been currently verified in a scale-invariant manner. We propose Qbricks, the first formal verification environment for circuit-building quantum programs, featuring clear separation between code and proof, parametric specifications and proofs, high degree of proof automation and allowing to encode quantum programs in a natural way, i.e. close to textbook style. Qbricks builds on best practice of formal verification for the classical case and tailor them to the quantum case: we bring a new domain-specific circuit-building language for quantum programs, namely Qbricks-DSL, together with a new logical specification language Qbricks-Spec and a dedicated Hoare-style deductive verification rule named Hybrid Quantum Hoare Logic. Especially, we introduce and intensively build upon HOPS, a higher-order extension of the recent path-sum symbolic representation, used for both specification and automation. To illustrate the opportunity of Qbricks, we implement the first verified parametric implementations of several famous and non-trivial quantum algorithms, including the quantum part of Shor integer factoring (Order Finding - Shor-OF), quantum phase estimation (QPE) - a basic building block of many quantum algorithms, and Grover search. These breakthroughs were amply facilitated by the specification and automated deduction principles introduced within Qbricks.
While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. Early attempts either suffer from the lack of automation or parametrized reasoning, or target high-level abstract algorithm description languages far from the current de facto consensus of circuit-building quantum programming languages. As a consequence, no significant quantum algorithm implementation has been currently verified in a scale-invariant manner. We propose Qbricks, the first formal verification environment for circuit-building quantum programs, featuring clear separation between code and proof, parametric specifications and proofs, high degree of proof automation and allowing to encode quantum programs in a natural way, i.e. close to textbook style. Qbricks builds on best practice of formal verification for the classical case and tailor them to the quantum case: we bring a new domain-specific circuit-building language for quantum programs, namely Qbricks-DSL, together with a new logical specification language Qbricks-Spec and a dedicated Hoare-style deductive verification rule named Hybrid Quantum Hoare Logic. Especially, we introduce and intensively build upon HOPS, a higher-order extension of the recent path-sum symbolic representation, used for both specification and automation. To illustrate the opportunity of Qbricks, we implement the first verified parametric implementations of several famous and non-trivial quantum algorithms, including the quantum part of Shor integer factoring (Order Finding - Shor-OF), quantum phase estimation (QPE) - a basic building block of many quantum algorithms, and Grover search. These breakthroughs were amply facilitated by the specification and automated deduction principles introduced within Qbricks.
Quantum mechanics based computing systems are expected to have high capabilities and are considered good candidates to replace classical cryptography and supercomputing systems. Among many implementations, quantum optics systems provide a promising platform to implement universal quantum computers, since they link quantum computation and quantum communication in the same framework. Recently, several quantum gates, circuits, and protocols have been experimentally realized using optics. Despite the fact that big advances in building the physical quantum computers were achieved, there are no currently available industrial computer aided tools that can perform the modeling, analysis, and verification of optical quantum computing systems. In this thesis, we tackle the idea of design automation for quantum circuits, where we use a sound language, higher order logic, to model and reason about quantum circuits formally. In particular, we propose a framework for the hierarchical modeling and automated verification of quantum computing circuits. The modeling approach captures quantum models built hierarchically from quantum gates, which models are readily available in a library. The analysis and verification of composed circuits is done seamlessly based on dedicated mathematical foundations formalized in the theorem prover. \nSpecifically, the tensor product and linear projection are used to extract the quantum circuit outputs. Subsequently, a rich library of quantum gates which includes 1-qubit, 2-qubit, and 3-qubit gates is formalized. In order to automate the analysis process, we developed a decision procedure to eliminate the need of user guidance throughout the formal proofs. To demonstrate the effectiveness of the proposed framework, we conduct the formal analysis of a benchmark of quantum circuits including the Shor's integer factorization algorithm, the Grover's oracle, and the quantum full adder.
Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny's automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm.
Quantum circuit optimization is crucial for realizing the full potential of quantum computing. However, the inherent complexity of quantum circuits and the potential for errors introduce significant challenges in ensuring the correctness and efficiency of optimization algorithms. This paper proposes a novel approach to formally verify quantum circuit optimization algorithms. We translate these algorithms into formal specification languages and leverage model checking and theorem proving techniques to rigorously demonstrate that the algorithms meet their intended objectives – primarily minimizing circuit complexity – without introducing unintended side effects. The core contribution lies in applying formal verification methodologies to this largely unexplored area, offering a path towards building trust and confidence in quantum optimization strategies. The presented framework provides a systematic method for ensuring the reliability of quantum circuits, a critical step towards practical quantum computation. The verification process relies on defining the desired behavior as a set of logical properties and then employing automated tools to check whether the optimized circuit satisfies these properties. This approach addresses the fundamental need for rigorous assurance in quantum systems, moving beyond empirical validation and towards mathematically proven correctness.
ABSTRACT- This paper presents an integrated framework for the automated verification and visualization of quantum circuits, addressing the critical need for reliable quantum software development tools. We implement and analyze eight fundamental quantum circuits Bell states, GHZ states, Quantum Fourier Transform (QFT), Grover's search algorithm, the Variational Quantum Eigensolver (VQE) for H₂ molecules, Quantum Teleportation, Superdense Coding, and the Bernstein-Vazirani algorithm through a comprehensive verification pipeline. The system generates publication-ready circuit diagrams and performs formal verification via automated theorem proving, achieving an overall verification success rate of 93.7% across all circuits. Notably, basic circuits such as Bell and GHZ states achieve perfect verification (100% success), whereas the Quantum Teleportation circuit presents the greatest challenge, attaining only 88.9% success. Results demonstrate a strong linear correlation (R² = 0.89) between circuit complexity (gate count) and verification time, with the framework processing 348 verification conditions per second. This work establishes quantitative benchmarks for quantum software verification, highlights specific gaps in protocol-level verification, and provides an integrated toolset that bridges the gap between circuit visualization and formal correctness assurance, thereby advancing the state of quantum software engineering.