Sure, but this isn't a static analysis tool in the same way a type system is. This is an analysis tool which checks for mostly platform-unrelated, entirely runtime behavior which can vary based on a lot of external factors.
When you say "Static analysis tools that check timing assertions have been around for a very long time.", what are you referring to? I've used analyzers that check for potentially-inescapable loops, do assembly/machine code operation counts, and look for the presence of interruptions that are known to take a potentially infinite/nondeterministic amount of time (waiting for I/O), or ones whose lower bound in time is known (scheduler interactions like sleep). How would you analyze for instructions which have theoretically-constant times, but which in practice are vulnerable to "constant plus or minus"-type timing attacks like Spectre? How would that analysis yield results we don't already know, a la "in this section of code, you should obfuscate/prevent the gathering of timing data, and/or try to defeat speculative execution"?
There is no one here saying that there is a runtime that can protect against Spectre. Spectre is just one of extreme example of timing attacks which have been troubling our industry for the better part of a decade.
It's entirely possible to prove that some types of code do not significantly very they're running time based on the character of their input. A classic example of this is hashing algorithm whose execution time is only dependent on the length of the input.
I'm not sure if people recall password oracles but they're still valid attacks today. We can only eliminate these by starting at the bottom and working our way up.
If your response to Spectre is to give up on your computer security, I don't think I want you writing software for me. These are the challenges our industry has to face. Failure is not really an option.
When you say "Static analysis tools that check timing assertions have been around for a very long time.", what are you referring to? I've used analyzers that check for potentially-inescapable loops, do assembly/machine code operation counts, and look for the presence of interruptions that are known to take a potentially infinite/nondeterministic amount of time (waiting for I/O), or ones whose lower bound in time is known (scheduler interactions like sleep). How would you analyze for instructions which have theoretically-constant times, but which in practice are vulnerable to "constant plus or minus"-type timing attacks like Spectre? How would that analysis yield results we don't already know, a la "in this section of code, you should obfuscate/prevent the gathering of timing data, and/or try to defeat speculative execution"?