Things like this are why I think Tezos, when/if it comes out, has a bright future. I want a formal proof for any contract I use with real-money.
There is a paper[1] written by some researchers on how using a more powerful language (Such as Idris) could prevent a whole category of errors in smart contracts development, but it doesn't necessary talk about formal verification of smart contracts.
1. https://publications.lib.chalmers.se/records/fulltext/234939...