The Ada programming language has been used successfully in hundreds of military projects in the US and the rest of the world. Ada is the programming language that helped build the mainstay of the Air Force or Navy, as it is used on combat aircraft programs such as the F-15 Eagle, the F-16 Fighting Falcon, the F-18 Hornet as well as many other allied programs such as the Eurofighter Typhoon or the JAS 39 Gripen.
The SPARK technology builds on the strengths of the Ada programming language to provide evidence-based assurance, completely removing many classes of dangerous defects, and significantly simplifying subsequent verification efforts. In a context of increasing cybersecurity threats with the development of cyber warfare capabilities by many actors, an effective protection requires more automation than is possible with traditional verification methods based on tests and reviews. The guarantees provided by automatic verification as demonstrated in SPARK will be critically useful in this context.