I think most bugs are the result of someone's attempt to do just that. As is test-driven development I suppose.

Then again proving code works isn't everything either. There's a reason Knuth once stated "Beware of bugs in the above code; I have only proved it correct, not tried it."

Type checking is a nice intermediate, though not all languages allow all properties you care about to be encoded in types.

Just express it as an n-state Turing machine and see if it halts within BB(n) steps. /s