The ZX-calculus is a graphical language for reasoning about quantum processes. In this talk I will give an overview of how we can use ZX-diagrams and a small set of rewrite rules to prove interesting properties regarding optimisation, verification, classical simulation and quantum error correction.