One of the major projects that's ongoing in the current decade is moving the standard math library functions to fully correctly-rounded, as opposed to the traditional accuracy target of ~1 ULP (the last bit is off).

For single-precision unary functions, it's easy enough to just exhaustively test every single input (there's only 4 billion of them). But double precision has prohibitively many inputs to test, so you have to resort to actual proof techniques to prove correct rounding for double-precision functions.