I think there is no answer that doesn't involve sign-offs on certain things.
In the situation you described, we resorted to fully randomizing everything, and then adding constraints to ensure it remained legal. This is a tedious process, one that leads to multiple false-positive failing tests.
However, the opposite situation, writing constrained stimulus from the beginning, leads to gaps where you didn't think of randomizing something, or you over-constrained it.
It's similar to a top-down vs down-up approach, only one is difficult and tedious and riddled with false positives, whereas the other one is easier and simpler, but can hide bugs.
In the face of issues like what you said, we implemented randomized interface behavior. Interrupts are always meant to be program-order invisible, so you can randomize those (imagine, 100 interrupts back to back, or 1 every N cycles where N is random but smaller than 5 or 500 etc). Pure random isn't interesting on its own. You need controlled randomness. From that point, you have to then start adding constraints for illegal/impossible situations, and you have to be extremely careful about these. We found a bug a week before tapeout when a senior architect forced a junior engineer(wonder who this is) to add a constraint. He used his seniority to sign it off, without going through a group review, and it was a mistake.
As I understand it, the current consensus is to use a tagged architecture, then show that there are no observable differences when the tags involve secret data and the value of the tagged data changes.
There are a few rubs here. One is that this is pretty hard to do. The other is that no one wants to pay the overhead of using a tagged architecture. Yet another is that deciding what "observable difference" means is challenging (too little, and you probably miss attacks, too much, and you will probably discover information leaks).
Further, this kind of rigorous system hasn't been rigorously empirically evaluated by a third party (as far as I know, perhaps in part because it's so hard to create these systems). "Empirically evaluated?" you scoff, "there's a proof, what's the point of testing?" Well...
For a glimpse of what this looks like, consider the SAFE architecture: http://www.crash-safe.org/assets/verified-ifc-long-draft-201... and lowRISC: http://www.lowrisc.org/downloads/lowRISC-memo-2014-001.pdf
Cadence has a tool [1] to do this, but I'm not sure it would work for timing leaks.
[1] https://www.cadence.com/content/cadence-www/global/en_US/hom...
http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf
Formal verification of specs, microcode, and security policy they hold in ACL2. Part of that is embedding a separation kernel a la MILS or SKPP model. It also has triplicated registers for fault-tolerance. Then, they integrate high-level languages like SPARK and microCryptol with that using certified compilers or equivalence checking.
Here's some examples from CompSci work:
https://eprint.iacr.org/2016/846.pdf
http://users.ece.utexas.edu/~tiwari/pubs/tiwari-dissertation...
http://cs.ucsb.edu/~sherwood/glift/
http://ieeexplore.ieee.org/document/7927266/
http://www.eecs.ucf.edu/~jinyier/papers/VTS12.pdf
http://www.cse.psu.edu/~dbz5017/pub/asplos17.pdf
Just also found a super-old one that tries to do it with capability-based mechanisms.
https://dl.acm.org/citation.cfm?id=803030
Most hardware work in information-flow analysis and control is currently focused on making hardware that controls bad software. I don't think most of them consider a CPU failure. If anything, they might be more vulnerable from a practical strategy of trying to reuse existing cores by making info-flow components that operate side-by-side with them. Here's an example from that area, though, since they could be modified to address recent concerns.
http://www.crash-safe.org/assets/verified-ifc-popl2014.pdf
http://csl.stanford.edu/~christos/publications/2010.hari_kan...
The client (a now vanished startup) had a small 8-bit CPU design which they wanted validation for, using the technique of executing random sequences of instructions and comparing the result against an emulator. We wrote the emulator independently from their architecture description. Given that most instructions were a single byte plus arguments and most of those were valid, the test coverage was pretty thorough. All looked fine until I added support for interrupts, at which point we discovered that an interrupt during a branch would not return to the correct point in execution.
Verifying security properties of processors is really hard; you can go looking for specific types of failure, but I'm not aware of a general way of proving no information leakage.