Cyber-physical systems (CPS) integrate computation with physical processes. The past decade has seen tremendous growth in autonomous and semi- autonomous CPS, including autonomous vehicles and robotics, enabled by inno- vations in artificial intelligence (AI) and machine learning. However, the wider deployment of AI-based autonomy is being held back by the limitations of current technology with respect to safety, reliability, security, and robustness.

Verified artificial intelligence (AI) is the goal of designing AI-based systems that have strong, ideally provable, assurances of correctness with respect to formally specified requirements [3]. This talk will review the challenges to achieving Veri- fied AI, and the initial progress the community has made towards this goal. Build- ing on this progress, there is a need to develop a new generation of design au- tomation techniques, rooted in formal methods, to enable and support the routine development of high assurance AI-based autonomy. I will describe our work on the design and verification of AI-based autonomy in CPS, implemented in the open-source Scenic [2] and VerifAI [1] toolkits. The use of these tools will be demonstrated on industrial case studies involving deep learning-based autonomy in ground and air vehicles. Our vision is to facilitate the computer-aided design of provably safe and robust AI-based autonomy in a manner similar to that enabled today by tools for the design automation of reliable integrated circuits.