I was fascinated by J Strother Moore’s presentation at the International Lisp Conference 2005. Especially because he gave a live demo of the ACL2 program verifier. It was used to verify the AMD Athlon floating point unit before it went into production:

The ACL2 proofs uncovered bugs that had remained hidden through hundreds of millions of test cases in RTL simulators. The bugs were fixed and the new RTL verified before the Athlon was fabricated. This work was done primarily by David Russinoff and Art Flatau, of AMD.