There should actually be a big market for formal verification tools: malicious users can use them to find and exploit buggy contracts. I imagine this will happ

There should actually be a big market for formal verification tools: malicious users can use them to find and exploit buggy contracts. I imagine this will happen after the low-hanging fruit (the front-runners described in this article) is gone. Providing formal security proofs may be forever out of reach, but if the tools get expressive eventually it'll be a battle of who can throw the most CPU at the solver, to the point where no cost incentive remains. Either way, it will spur developers to use these tools before their attackers do.