In this case the CPU does function exactly as designed. Any correctness prover would agree. It does show the problem of all theorem provers: they are only as g

In this case the CPU does function exactly as designed. Any correctness prover would agree. It does show the problem of all theorem provers: they are only as good as the specification.