A Review of Formal Methods in Quantum Circuit Verification

Quantum computing exploits the principles, and 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 study examines how formal methods are applied to quantum circuit verification. It focuses on barrier certificates, abstract interpretation, model checking, and theorem proving approaches. The study discusses both the theoretical foundations and practical applications of these techniques. Their strengths and limitations are analysed through representative case studies. Finally, the study highlights open challenges and identifies promising directions for future research. An extensive set of references is included to support further study and exploration.