As a tidbit, this was part of how one of the teams involved in the original Spectre paper found some of the vulnerabilities. Basically the idea was to design a

As a tidbit, this was part of how one of the teams involved in the original Spectre paper found some of the vulnerabilities. Basically the idea was to design a small CPU that could be formally shown to be free of certain timing attacks. In the process they found a bunch of things that would have to change for the analysis to work... maybe in a small system those wouldn't actually lead to vulnerabilities, but they couldn't prove it (or it would require lots of careful analysis). And in big systems, those features do lead to vulnerabilities.