I don't see how this is fundamentally different than timing attacks and other side channel attacks that have been well known before, and to the best of my knowl

I don't see how this is fundamentally different than timing attacks and other side channel attacks that have been well known before, and to the best of my knowledge, simply hasn't been the focus of the "prove it correct" approach. Whenever you want to prove something correct, you need to make assumptions about the execution model, and about what correctness means. Now "we" as an industry found a bug that makes the actual model differ from the assumed model, so we need to fix it. The same is true when you can measure the power used by a microchip during some cryptographic operation, and infer the secret key from that -- even if the cryptographic operation has been proven correct, the definition of correctness likely didn't include this factor.