CPU design is in a large part an exercise in formal verification. On the other hand it does not help you much when the bug in question is in the specification t

CPU design is in a large part an exercise in formal verification. On the other hand it does not help you much when the bug in question is in the specification that you verify against in the first place or, as is almost certainly this case, is based on some behavior that is not specified by the specification at all.