The Tokeneer ID Station system’s key statistics are:In some ways I find this a little depressing since I see some of thee same people who were doing FM when I was doing my PhD in this area in the late 1980s (Tony Hoare, for example) and the number of lines of code that are being verified (my PhD advisor formally specificed and proved a secure UNIX kernel in the late 1970s, now doing voting machines).
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 said, this NASA formal methods workshop at Ames sounds encouraging, and I recognize some of the names from people I bumped into when working with the formal specification of the space shuttle jet select group at JPL.