Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report)
Letitia W. Li, Denley Lam, Vu Le, Daniel Mitchell, Mark J. Gerken, Robert B. Ross
TL;DR
This paper tackles the challenge of integrating formal methods into industrial, safety-critical electronic warfare software by examining usability and adoption barriers. It reports a hands-on experience applying a diverse set of open-source C++ verification tools to a FAST Labs EW codebase, surveying capabilities and analyzing results. Key findings show that no single tool covers all vulnerability classes, annotation-based approaches impose substantial manual effort, and workflows must balance CI/CD practicality with verification depth. The authors offer concrete recommendations—improved documentation, standardized terminology, automated annotation support, and better handling of library code—to accelerate industrial adoption. Future work includes benchmark-based comparisons, deeper integration into CI/CD, and evaluation of automated assistants for interactive theorem proving.
Abstract
While using formal methods offers advantages over unit testing, their steep learning curve can be daunting to developers and can be a major impediment to widespread adoption. To support integration into an industrial software engineering workflow, a tool must provide useful information and must be usable with relatively minimal user effort. In this paper, we discuss our experiences associated with identifying and applying formal methods tools on an electronic warfare (EW) system with stringent safety requirements and present perspectives on formal methods tools from EW software engineers who are proficient in development yet lack formal methods training. In addition to a difference in mindset between formal methods and unit testing approaches, some formal methods tools use terminology or annotations that differ from their target programming language, creating another barrier to adoption. Input/output contracts, objects in memory affected by a function, and loop invariants can be difficult to grasp and use. In addition to usability, our findings include a comparison of vulnerabilities detected by different tools. Finally, we present suggestions for improving formal methods usability including better documentation of capabilities, decreased manual effort, and improved handling of library code.