There is something roundly unsatisfactory about the way in which we normally develop software systems, especially large systems. Try as we might, bugs tend to get into the development cycle and they can prove to be very hard to eliminate. We have learned to live with statistics that say that we should expect roughly one residual defect for every one thousand lines of delivered code, post testing. Meanwhile, code sizes for typical applications continue to grow. The control software for a spacecraft, for instance, has grown in the last few decades from a few thousand to a few million lines of code. Do we know any better today than thirty years ago how to write such code reliably?

Although truly rigorous formal software verification techniques will probably remain out of reach for large-scale software development for a while longer, I will show that some very practical uses of formal methods have quietly reached the point where they can be used routinely. My example with be the use of two light-weight tools, Scrub and Spin, in the development of mission critical software at JPL.