Engineering practices for software-reliant systems have evolved steadily over many decades, and so too have the assurance techniques that confirm systems’ correctness and security.
Mathematically rigorous techniques, known as formal methods, have shown great promise to prove and provide continuous evidence of correctness for software systems. For example, DARPA’s High Assurance Cyber Military Systems (HACMS) program demonstrated how these techniques could effectively secure U.S. Department of Defense (DoD) military systems.