Explores a class of methods that are capable of formally verifying properties of deep neural networks. The book introduces a unified mathematical framework for verifying neural networks, classify existing methods under this framework, provide pedagogical implementations of existing methods, and compare those methods on a set of benchmark problems.