There is a verified optimizing C compiler, CompCert. Admittedly, it is not gcc, and it is not easy to do, but still. Writing a verified SSL implementation is probably not more difficult than that.
Also, verification isn't a magic bullet, you need a good spec.
Total market cap of the top three tech companies is more than a trillion dollars. Even a hundred times more resources is affordable for them given the criticality of the project. The replacement does not have to be written in C, it can be written in ML-like languages and expose an external C interface.
> Also, verification isn't a magic bullet, you need a good spec.
True, but drawing from the CompCert anecdote, I suspect bugs in a verified implementation would be orders of magnitude less likely.
Only by moving crypto functions to a separate user maintainable black box will this tide ever be stemmed. Of course, verifying that black box then becomes problematic, but it would be easier than the current situation.