A Review of Formal Methods in Quantum Circuit Verification

Quantum computing exploits the principles of quantum mechanics to perform computation by manipulating qubit states through sequences of quantum gates, known as quantum circuits. As quantum hardware continues to scale in both complexity and qubit count, conventional verification techniques quickly become computationally impractical, motivating the need for more advanced verification approaches. Formal methods, including theorem proving, model checking, and symbolic reasoning, offer systematic and mathematically rigorous techniques for verifying functional correctness, equivalence, and implementation, while enabling early detection of design errors. This review explores how formal methods are currently applied to the verification of quantum circuits, with a particular focus on barrier certificates, abstract interpretation, model checking, theorem proving, and emerging hybrid approaches. Examining the theoretical foundations and practical applications of these techniques, discussing their strengths, limitations, and comparative effectiveness through representative case studies, review hopes to provide a holistic understanding of the topic. Highlighting the open challenges and outlining promising directions for future research, the review aims to provide a roadmap towards more scalable and robust verification frameworks for quantum computing. For readers seeking deeper engagement, the review offers an extensive set of references to support further study and exploration.