Explainable Verification: Survey, Situations, and New Ideas
• SEI Report
Publisher
Software Engineering Institute
Topic or Tag
Abstract
Many software-intensive systems of current and future application domains require (or will require) approval from a certification authority before being deployed. Formal methods (FMs) verify properties of software by proving them mathematically rather than running tests of the software. FMs have the potential to help certification. But unfortunately, FMs are currently rarely used because software practitioners do not understand how FM tools work internally and do not understand the underlying theories that these tools depend on. Since it is hard to trust something that you do not understand and have not used before, software practitioners tend to not trust FM tools. If FM tools could explain their output, however, then software practitioners would be more likely to trust them and this could bring the benefits of (i) faster fielding (because of less testing), and (ii) improved safety (because of better coverage).
Therefore, this report focuses on potential changes in software development practice and the research needed for this to be realized. Specifically, it discusses explanations generally, it discusses the way explanations can be used in different types of verification, and it presents ideas for creating explanations for FMs.
Cite This SEI Report
Andersson, B., de Niz, D., & Klein, M. (2024, April 16). Explainable Verification: Survey, Situations, and New Ideas. Retrieved August 17, 2026, from https://www.sei.cmu.edu/library/explainable-verification-survey-situations-and-new-ideas/.
@techreport{andersson_2024,
author={Andersson, Bjorn and de Niz, Dionisio and Klein, Mark},
title={Explainable Verification: Survey, Situations, and New Ideas},
month={Apr},
year={2024},
institution={Software Engineering Institute, Carnegie Mellon University},
url={https://www.sei.cmu.edu/library/explainable-verification-survey-situations-and-new-ideas/},
note={Accessed: 2026-Aug-17}
}
Andersson, Bjorn, Dionisio de Niz, and Mark Klein. "Explainable Verification: Survey, Situations, and New Ideas." Software Engineering Institute, Carnegie Mellon University. Software Engineering Institute, April 16, 2024. https://www.sei.cmu.edu/library/explainable-verification-survey-situations-and-new-ideas/.
B. Andersson, D. de Niz, and M. Klein, "Explainable Verification: Survey, Situations, and New Ideas," Software Engineering Institute, Carnegie Mellon University. Software Engineering Institute, 16-Apr-2024 [Online]. Available: https://www.sei.cmu.edu/library/explainable-verification-survey-situations-and-new-ideas/. [Accessed: 17-Aug-2026].
Andersson, Bjorn, Dionisio de Niz, and Mark Klein. "Explainable Verification: Survey, Situations, and New Ideas." Software Engineering Institute, Carnegie Mellon University, Software Engineering Institute, 16 Apr. 2024. https://www.sei.cmu.edu/library/explainable-verification-survey-situations-and-new-ideas/. Accessed 17 Aug. 2026.
Andersson, Bjorn; de Niz, Dionisio; & Klein, Mark. Explainable Verification: Survey, Situations, and New Ideas. Software Engineering Institute. 2024. https://www.sei.cmu.edu/library/explainable-verification-survey-situations-and-new-ideas/