The White House highlights the use of formal methods in a new report.
Three points very interesting:
It is possible to demonstrate correctness using mathematical techniques called formal methods. These techniques, often used to prove a range of software outcomes, can also be used in a cybersecurity context and are viable even in complex environments like space.
Model checkers can answer questions about a number of higher-level properties. These algorithms can be used during production; however, they are limited in their scaled use due to their computational complexity.
Formal methods can accelerate market adoption in ways that traditional software testing methods cannot. They allow for proving the presence of an affirmative requirement, rather than testing for the absence of a negative condition.
CLEARSY has been developing the B method for 30 years, a formal method with proof, successfully used for the most critical systems and software.