> But formal methods (and TLA+ for distributed computation) don't eliminate side channels. True, but they eliminate whole classes of attack. I'm normally aghas

> 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.