&gt;most modern processors have a bunch because it&#x27;s impossible to test every possible edge case a priori.<p>Only with the sort of engineering most current CPU manufacturers use.<p>It&#x27;s possible to have formally verified hardware; it&#x27;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.