This chapter provides an overview of the contributions of Part IV of this book, which explores the challenge of verifying quantum circuits. The proposed methods employ a variety of techniques to efficiently and automatically check the equivalence of two quantum circuits. The resulting methods have been integrated into the open-source quantum circuit equivalence checking tool QCEC, which is available at https://github.com/munich-quantum-toolkit/qcec .