Finite-precision representation and approximation of continuous and infinite real numbers causes unavoidable rounding towards discrete and finite values in that precision. Computation with rounded numbers in turn makes the rounding accumulate and further diverge from the exact real-valued computation. Sound and accurate estimation of potential errors caused by this divergence is essential for being able to correctly find an upper bound for the errors of finite-precision computation.

In this talk I will present FloVer, a formally verified certificate checker for automated verification of finite-precision error bounds. I will focus on the ongoing work of formalizing affine arithmetic for FloVer and using it to increase accuracy of the verified roundoff errors. This ongoing work is the subject of my Masters thesis at Saarland University.