>most modern processors have a bunch because it's impossible to test every possible edge case a priori. Only with the sort of engineering most current CPU manu

>most modern processors have a bunch because it's impossible to test every possible edge case a priori. Only with the sort of engineering most current CPU manufacturers use. It's possible to have formally verified hardware; it's just expensive with current tech. Tools are improving, though. I suspect the next cutting edge will be the unification of functional-language-to-hardware compilers like Clash or Lambda-CCC with fully dependent languages like Agda or Idris, where you can statically verify arbitrary properties though the type system.