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

> I'm normally aghast at people writing new code in plain C,

Why?

There have been some attempts at formally verifying lack of timing attacks (to the extent allowed by hardware). This is the one I know the most about: https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 but there are likely others

Also in around side channel topic for example:

E. Prouff and M. Rivain, Masking against Side-Channel Attacks: A Formal Security Proof, EUROCRYPT 2013, LNCS 7881

S. Dziembowski and K. Pietrzak, "Leakage-Resilient Cryptography, 10.1109/FOCS.2008.56.

Side-channel: https://en.wikipedia.org/wiki/Side-channel_attack

Time complexity > Constant time: https://en.wikipedia.org/wiki/Time_complexity#Constant_time

"Masking against side-channel attacks: A formal security proof" (2013) https://link.springer.com/chapter/10.1007/978-3-642-38348-9_... https://scholar.google.com/scholar?cites=1479355492097437276...

"Leakage-Resilient Cryptography" (2008) https://ieeexplore.ieee.org/abstract/document/4690963 https://scholar.google.com/scholar?cites=5581902451405085906...

"FaCT: A DSL for Timing-Sensitive Computation" https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 citations in gscholar: https://scholar.google.com/scholar?cites=1570199926308101856...