A Review of Formal Methods in Quantum Circuit Verification

Quantum computing uses the laws of quantum mechanics to perform computation. Information is stored in qubits and processed using quantum gates arranged as quantum circuits. As quantum hardware grows in size and complexity, verifying these systems becomes increasingly difficult. Traditional verification methods do not scale well and quickly become computationally infeasible. This creates a strong need for more powerful and scalable verification techniques. Formal methods provide a potential solution to this problem. Techniques such as theorem proving, model checking, and symbolic reasoning offer mathematically rigorous ways to verify correctness, equivalence, and implementation. They also help detect design errors early in the development process. This review examines how formal methods are applied to quantum circuit verification. It focuses on barrier certificates, abstract interpretation, model checking, theorem proving, and emerging hybrid approaches. The review discusses both the theoretical foundations and practical applications of these techniques. Their strengths and limitations are analysed through representative case studies. Finally, the review highlights open challenges and identifies promising directions for future research. An extensive set of references is included to support further study and exploration.