Formal verification totally makes sense for smart contracts as they are relatively small most of the time (around 500 LOC). When your program is tied to so much money, this is probably what you should be doing.