> But formal methods (and TLA+ for distributed computation) don't eliminate side channels.

True, but they eliminate whole classes of attack. I'm normally aghast at people writing new code in plain C, but formally verified plain C counts as a whole other and better paradigm to me.