This chapter summarizes the contributions of IV of this book, which explores the challenge of verifying the correctness of 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