Show Us the Proof: Formal Methods Can Be Applied at Large Scale

Home / Articles / External / Government


March 28, 2023 | Originally published by DARPA on March 27, 2023

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.