I have used them to prove equivalence between pseudo code and optimized production code. Several rounding-related tricks and a too large search space made it very difficult to prove with traditional testing.