Intel's work is great. The hardware industry in general is light-years ahead of software industry on applied formal methods. The reason is straightforward: bad circuits can't be fixed with an update. That recall made Intel and others look at the balance sheet a second time with nice results. :)

And thanks for the links1