| Intel said the error occurred because of an omission in the translation of
| a formula into computer hardware. It was corrected by adding several dozen
| transistors to the chip.
the error arose in transcription at some stage. Is that right? Perhaps I
read too much into journalese. But if so, it may be that formal
verification wouldn't have helped unless it was very tightly coupled with
the production process.
Nevertheless, I believe floating point hardware is a particularly good
target for formal verification by theorem proving. Providing the necessary
mathematical infrastructure for such verification efforts was the
motivation for all my work on formalizing analysis in HOL (though it has
since become an interest in itself).
John.