> An Intel CPU is a pretty large design. I'm not sure it's feasible to run all formal verification benchmarks on a full RTL design of the entire chip, including

> An Intel CPU is a pretty large design. I'm not sure it's feasible to run all formal verification benchmarks on a full RTL design of the entire chip, including caches, memory controllers, etc. Agreed. It's still possible to verify smaller components of the design, though. > [...] These sort of fault injection attacks are way past issues in high-level RTL. [...] Simulating those effects sounds prohibitively expensive, and I'm not sure there is any existing formal verification suite that can even do that. It's possible to have a "high-level RTL" design that inherently resists some types of fault injection attacks. TMR is a trivial example: https://en.wikipedia.org/wiki/Triple_modular_redundancy https://en.wikipedia.org/wiki/Triple_modular_redundancy In fact, there is a wide body of literature studying the application of formal verification to side-channel and fault-injection analysis. Some systems can even synthesize a fault-injection resistant design. Unfortunately it is not realistic to be resistant to "all types of [fault injection] attacks according to the current laws of physics". We can, however, make different models of fault attacks and then prove (or synthesize) that some design is resistant to attacks in that model. If you're interested, look for publications in CHES, TCAD, FMCAD, DAC, DATE, etc. with keywords like "DFA", "DFIA", "SAT", "fault injection", etc.