I feel like that became apparent with Spectre and Meltdown - they really opened the floodgates. I do wonder if there is some way to have formally proven correct

I feel like that became apparent with Spectre and Meltdown - they really opened the floodgates. I do wonder if there is some way to have formally proven correctness for speculation - a sort of analogue to the borrow checker in Rust if you like.