Autonomous systems are poised to become an integral part of our economy, infrastructure, and society. They are rapidly gaining more capabilities via AI components and serving in ever more safety-critical roles. However, as their complexities grow, the more impossible it becomes to provide safety guarantees for their decisions and overall performance. In this talk, I argue that formal methods combined with control theory and machine learning techniques can form powerful tools to address this problem. To this end, I present our recent contributions that focus on data-driven approaches to formal analysis and control of highly uncertain systems.  Specifically, I focus on a framework for correct-by-construction control synthesis based on Gaussian regression, finite abstraction, and automata learning. I also discuss the importance of explanations in autonomous decision making and present our recently developed explanation scheme that provides easily-interpretable and verifiable explanations in the context of multi-agent planning.