You could very much design and verify that a CPU such that execution of arbitrary code has no observable side effects. However attempting to do so is multi yea

You could very much design and verify that a CPU such that execution of arbitrary code has no observable side effects. However attempting to do so is multi year, for modern CPUs certainly multi decade project. This is not feasible as long as Moore's Law goes on. Formal verification of kernels (SEL4) and a micro processors it runs on have been performed together to proof properties. Large ALU blocks and vector units (such as multipliers) can be formally verified. However efforts of end-to-end formal verification of entire processors won't happen unless there is demand to justify the huge investment of engineering resources and the market would be fine with chips many years behind. Unless everyone is running dozens of clients on all their hardware it is cheaper to give everyone their own machine instead of investing the engineering time in to verifying chips. The economic incentives for Intel that selling more machines for isolation brings them more revenue without having to make investments in to decade long verification projects means it is not a mathematical certainty that it can't happen but just an economic one. After all speculative execution is just extra state and extra logic which can be formally verified. After all programs are just bit patterns and all quarters can be addressed in the formalism of Quantified Boolean Formulas. But nobody is gonna undo 20 years of performance. You will just be told to buy more machines to isolate workloads.