Publications Details

The First Tri-Lab Workshop on Formal Verification: Capabilities, Challenges, Research Opportunities, and Exemplars

Pollard, Samuel D.; Aytac, Jon M.; Kellison, Ariel E.; Laguna, Ignacio; Nedunuri, Srinivas; Reis, Sabrina A.; Sottile, Matthew J.; Thornquist, Heidi K.

The First Tri-Lab Workshop on Formal Verification was held in Santa Fe, New Mexico, on December 5th, 2023. This workshop gathered staff from Sandia, Los Alamos, and Lawrence Livermore National Laboratories and NASA’s Jet Propulsion Laboratory. This report summarizes and expands on the presentations given and discussion had at this workshop. In this report, we describe the current capabilities and research needs related to formal methods at the NNSA labs. In particular, we identify medium-term and long-term research gaps in programming languages, formalization efforts of complex systems, embedded systems verification, hardware verification, cybersecurity, formal methods usability, workflows, numerical methods, the use of formal methods for artificial intelligence (and its converse, artificial intelligence for formal methods), and collaboration opportunities and considerations on these topics. We conclude with a small number of exemplar research problems related to these topics.