Imagine the difficulty in debugging modern CPUs. Remember the floating point problems Intel had? There are far too many possible edge cases to be confident that testing alone will reveal them. Consequently, both Intel and AMD use formal proof methodologies to verify the correctness of their processors. I know that AMD uses (or used to use) the work of Boyer and Moore for validation of their designs. Intel uses it own prover. [1]

[1] Fifteen Years of Formal Property Verification in Intel by L Fix, 2008 [http://www.cs.ucc.ie/~herbert/CS6320/EXS/LimorFix%20Intel%20...]