Once I went to a talk about applications of model checking to the verification of software. A programmer was constantly changing a state-based algorithm for call setup in a telephone switch, and was having trouble keeping it correct. Enter model checking. Two people wrote temporal specifications of call setup, and every night or so, they'd grind the model checker on the latest version of the code. No, that didn't prove the code was correct, but it did catch an enormous number of bugs in a tricky piece of concurrent code.
Oh. The programmer was Ken Thompson. The people applying the model checker were Gerard Holzmann (the designer of SPIN) and Margaret Smith.
I'm not saying the technology is applicable everywhere, but you gotta give Clarke, Emerson, and Sifakis a lot of credit for opening a good door.