Fundamental concerns exist on the trustworthiness of deep learning systems, with examples including robustness, fairness, privacy and explainability. Phenomena like adversarial examples prompt the need to train robust networks and to provide formal guarantees on their behaviour. In this talk, we will first introduce the neural network verification problem. Then, borrowing from convex and global optimisation techniques, we will present our contributions on approximate and exact verification algorithms for pre-trained networks. After a detour through multi-task optimisers, which will motivate a minimalist approach to algorithm design, we will present efficient methods to train networks that are provably robust. We will conclude the talk by highlighting persisting challenges in the area and directions for future work.