Formal Verification of Quantum Circuits Performance Analysis Across Algorithmic and Protocol-Based Implementations

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.