Formal methods are needed now more than ever because military infrastructure depends on complex software working correctly, and the nation's security also depends on secure computing infrastructure. There are no better alternatives for providing high levels of confidence. Demands placed on software require that formal methods capabilities be substantially increased. This requires research, education and training, and deployment of more integrated tools.
Technology based on formal methods has now reached into standard computing and design practice (in the normal time frame of 17 to 20 years since their appearance in research labs). Type inference algorithms are used in programming languages along with decision procedures to detect array bounds errors; model checkers are components in industrial CAD tools, and specification languages are part of programming environments. In all cases these tools have brought greater assurance that hardware and software will not fail. It is now widely recognized that formal methods define the highest possible levels of trust, assurance, accountability and security. But much more can be done - both to further develop the best ideas discovered in the 80s and 90s and to investigate new ideas of great promise.