Using ACL2, Tom Lynch (the algorithm's designer), Matt Kaufmann and I proved the following theorem:
Correctness of the AMD5k86 Floating-Point Division: If p and d are double extended precision floating-point numbers (d /= 0) and mode is a rounding mode specifying a rounding style and target format of precision n not exceeding 64, then the result delivered by the K5 microcode is p/d rounded according to mode.
We also proved that every intermediate result is a floating-point number that fits in the resources allocated to it.
To carry out these proofs with ACL2 it was first necessary to formalize and prove much ``floating-point folklore.''
For details see