The real interesting part of this is the formal verification tools they described which were used to uncover these vulns.

It seems that, while not a silver bullet, FV tools of this sort would be the most reliable way of discovering (and preventing) these sort of issues in microarchitecture.