From Software Abstractions - Logic, Language and Analysis by Daniel Jackson (MIT Press, 2006):
The case for formal methods is often based on the prospect of catching subtle bugs that elude testing. But in practice the less glamorous analyses that are applied repeatedly during the development of an abstraction and which keep the formal model in line with the designer's intent, are far more important. Software, unlike hardware, rarely fails because of a single tiny but debilitating flaw. In almost all cases, software fails because of poor abstractions that lead to a proliferation of bugs, one of which happens to cause the failure.