I am quite intrigued, given my background in Information Security:

http://www.adacore.com/home/gnatpro/tokeneer/

This reference project is using a formal process:

1. Requirements analysis (the REVEAL® process)
2. Formal specification (using the formal language Z)
3. Design (formal refinement of the specification and the INFORMED process)
4. Implementation in SPARK Ada
5. Verification (using the SPARK Examiner toolset)
6. Top-down system testing

The key statistics are rather remarkable:

• lines of code: 9939
• total effort (days): 260
• productivity (lines of code per day, overall): 38
• productivity (lines of code per day, coding phase): 203
• defects discovered since delivery: 1

That is a surprisingly LOW output. Is the essence of this reference project that enhancing security takes time to cast its nets, time that thins out the project? The raw coder performance of 200 odd lines a day sounds about right, so the time is “invested” in solid pre- and after-coding work (specs, reqs, des, vers, tests)…