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.