Model Checking for Fun and Profit

So, I'm starting to fall in love with model checking. It looks like it will lead to much of what I'm looking for from formal verification: user friendliness, push-buttonness, and utility in actual software development amongst other things. Now, it's never going to enable you to do full functional correctness on anything but the most trivial of programs, but that's not what's needed most of the time. Simply bring model checking to bear in a big way in normal software development would be a huge step forward for both formal methods and software engineering. Projects like SLAM are wonderful examples of the utility that a properly designed and integrated formal methods suite can bring to bear.