  Autonomous systems -- such as self-driving cars, autonomous drones, and
automated trains -- must come with strong safety guarantees. Over the past
decade, techniques based on formal methods have enjoyed some success in
providing strong correctness guarantees for large software systems including
operating system kernels, cryptographic protocols, and control software for
drones. These successes suggest it might be possible to ensure the safety of
autonomous systems by constructing formal, computer-checked correctness proofs.
This paper identifies three assumptions underlying existing formal verification
techniques, explains how each of these assumptions limits the applicability of
verification in autonomous systems, and summarizes preliminary work toward
improving the strength of evidence provided by formal verification.
