Autonomous vehicles are highly complex systems, required to function reliably
in a wide variety of situations. Manually crafting software controllers for
these vehicles is difficult, but there has been some success in using deep
neural networks generated using machine-learning. However, deep neural networks
are opaque to human engineers, rendering their correctness very difficult to
prove manually; and existing automated techniques, which were not designed to
operate on neural networks, fail to scale to large systems. This paper focuses
on proving the adversarial robustness of deep neural networks, i.e. proving
that small perturbations to a correctly-classified input to the network cannot
cause it to be misclassified. We describe some of our recent and ongoing work
on verifying the adversarial robustness of networks, and discuss some of the
open questions we have encountered and how they might be addressed.