Here’s the transcript. The best part is the students adding to the project. It showed a combination of low effort to learn with good results achieved.
“ Finally, the software was sent to the NSA’s independent assurance team (SPRE) in Albuquerque, New Mexico, who reported that the software contained zero defects… The NSA were startled by the productivity figures because they were much higher than had ever been achieved on an NSA project despite having gone beyond the minimum requirements for Evaluation Assurance Level EAL5; Altran’s C by C development process includes activities from the much more rigorous EAL6 and EAL7 levels.”
“The students were given 3-4 days training on reading and writing Z, 3 days training on the Tokeneer ID Station, 2 days training on Ada and 4-5 days training on SPARK and the SPARK tools. Beyond that they only had Z and SPARK textbooks and manuals, and email support from Altran/Praxis if they needed it.”
“In the following years, a small number of errors have been found in the Tokeneer software by academic researchers[xxxv]. The authors of the cited paper say It is a remarkable achievement that this complete redevelopment of an actual system by 3 people over 9 months (part-time) achieved such a level of quality that only a few problems can be found several years later using so many new approaches not available at the time.”
It is remarkable indeed. If you interested in learning more about SPARK, there’s a good book out there which I can easily recommend: Building High Integrity Applications with SPARK.