Obtaining useful guarantees about the behaviour of trained neural networks is a famously difficult task. In this talk, I will discuss some of the recent progress and algorithms in this area, and demonstrate the tool I've been building to express and formally verify high-level specifications for neural networks.