NSA shows us how to write secure code

The Tokeneer project was commisioned by the NSA, and has now been released to the community. The idea is to show that code can be written to comply with the Common Criteria EAL 5:
http://www.adacore.com/home/gnatpro/tokeneer/