AMD went on to use ACL2 to verify their floating point square root algorithm. During that proof a problem was uncovered. While not indicating a clear example of an error in the algorithm, it was deemed of sufficient concern that the algorithm was modified so that the proof could be completed.
AMD is currently applying ACL2 to proof about the K7 cache.