Well, a lot of x86 actually does get proven using formal methods. Clearly not all of it, but we've realized that was a bad plan, and that we should go back to formally verifying all of our hardware.