Computing systems that engage people physically with high degrees of autonomy need to provide rigorous guarantees of safety. Formal methods can been used on such systems to provide mathematical proofs to ensure correct behavior. However, machine learning and data-driven approaches are now an indispensable part of autonomous-systems design, and their reliance on highly nonlinear continuous functions and probabilistic reasoning has largely been at odds with the logical and symbolic-analysis frameworks in formal methods. As a result, the lack of formal assurance has become the key bottleneck that impedes the wider deployment and adoption of autonomous systems. This project targets this open challenge by developing formal synthesis and verification techniques for learning-based and data-driven control and planning methods for autonomous systems.