Spinellis and "Zero Defect" Code

Diomidis Spinellis posted last week about Tokeneer, a National Security Agency case study carried out by UK software firm Praxis of "...how to develop zero-defect code in a cost-effective manner". Problem is, Diomidis found something that looked a lot like a bug, and his suspicions have now been confirmed.