The National Security Agency has released a case study showing how to cost-effectively develop code with zero defects. If adopted widely, the practices advocated in the case study could help make commercial software programs more reliable and less vulnerable to attack.

The case study used Praxis High Integrity System's Correctness by Construction techniques, which include programming in the SPARK subset of Ada.

The project meets or exceeds the Common Criteria Evaluation Assurance Level (EAL) 5, demonstrating that it is possible to build products that are reliable, verifiable, and cost effect to this level.

For more information, see