From "How did software get so reliable without proof? (1996) [pdf]" (2024) https://news.ycombinator.com/item?id=42425617 :

> From "The Future of TLA+ [pdf]" (2024) https://news.ycombinator.com/item?id=41385141 :

>> Formal methods including TLA+ also can't/don't prevent or can only workaround side channels in hardware and firmware that is not verified. But that's a different layer.

>> Things formal methods shouldn't be expected to find: Floating point arithmetic non-associativity, side-channels