I think the key bottleneck for formal methods in "normal" software is that formal methods imply a formal model that you're checking against -- and most software doesn't have that.

For example, deployment software. There's probably some way to formally model deployment. But most deployment software in the wild is written like, "here are 100 things that can go wrong while you're deploying, and 100 corresponding business rules for what to do."

I do sometimes fantasize about a more pure-Computer-Science world where all text formats are a formally-defined grammar, all systems are state machines, and everything has a spec ;-)