Yes, there can still be side-channel and out-of-band attacks in FV systems. For example, pouring water into the server rack. That’s a cheeky example, but things like timing side-channels via speculative execution and cache hits wouldn’t be addressed by FV at the software level. I think there is some ongoing research for verifying software/hardware interactions but I’m not aware of a product in widespread use that checks this.
The use of constant-time algorithms for crypto is a way to mitigate things like timing side-channels, and there are other techniques like disabling hyper-threading that can help.
The depressing fact is that side channels exist any time there’s a shared computing resource. The question is how noisy the channel is, the data rate, etc.
It might be argued that side channels exist whenever there is a shared channel; which is always, because plenoptic functions, wave function, air gap, ram bus mhz, nonlocal entanglement
> Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all?
Side-channel attack https://en.wikipedia.org/wiki/Side-channel_attack