Tokeneer

Tokeneer sounds like a fan of the Lord of the Rings books and movies (OK, that would be Tolkieneer) but it is the latest of a public example of a "fully" formal software development effort. You can read a few paragraphs about it in the most recent Dr. Dobb's here and peruse the official website. Software engineering students will be interested in some of the statistics, particularly about productivity

The Tokeneer ID Station system’s key statistics are:

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

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).

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.