Formal Methods at NASA: Past, Present, and Future

This talk explores the evolution of formal methods both at NASA and in the general community, tracing their historical roots, examining their current applications, and envisioning future directions, focusing on the increasing importance of formal methods in building safe, complex systems. Formal methods, initially viewed as a highly theoretical area, has seen a shift from niche applications to mainstream adoption, driven by the need for rigorous verification in increasingly complex software and hardware systems. The talk will trace the history of formal methods at through this evolution, with a focus on NASA’s catalyzing influence. Today, formal methods are used across various industries, including the software, hardware, web services and distributed database management, transportation (e.g., aviation, railways, automotive etc.), communications, nuclear power, finance and medical sectors, with tools based on theorem proving, model checking, abstract interpretation and other techniques proving their value in ensuring safety, security, and high confidence operations. The talk will explore current NASA efforts in these domains. Looking ahead, the talk will also discuss the potential of formal methods in areas like artificial intelligence and/or machine learning, embedded human-centric cyber-physical systems, and robotics, highlighting the need for continued research and development to address emerging challenges and opportunities.