I used Z for radiation therapy machine software (Score 4, Informative)

I used Z to design the control software for a radiation therapy machine.

I expressed the safety requirements in Z, and also expressed the detailed design in Z, and argued (I wouldn't say "proved") that the design didn't violate the safety requirements.

We coded the control program in C from the detailed design in Z. Of course we tested the program thoroughly too - you still have to do all that, of course.

The machine has been in use treating patients since July 1999. We haven't killed anyone yet (unlike some other products in this category).

There are some papers and reports about the project at

http://staff.washington.edu/~jon/cnts/index.html

There is a short (3-page) report about our use of Z in this project at

http://staff.washington.edu/~jon/cnts/iccr.html

There is a longer report about the whole project at

http://staff.washington.edu/~jon/cnts/cnts-report. html

The Z for the radiation therapy machine itself is at

http://staff.washington.edu/~jon/z/machine.html