Excited to share FloatLib, our verified arbitrary-precision floating-point arithmetic library in Lean. We’ve spent several months trying to bring together the best of both worlds: arithmetic we can prove correct and implementations that run efficiently. We built FloatLib to support verified machine learning and scientific computing, where rounding, overflow, and accumulation can change a program’s result. FloatLib supports IEEE binary and decimal, arbitrary-width posits, P3109, and small ML formats. You can also define your own formats and rounding rules. Each certified software backend comes with a Lean proof that it computes the specified result, including signed zeros and exceptional values. A lot of the work went into making those implementations faster, with lookup tables for tiny formats, machine-word kernels, and limb algorithms for wider arithmetic. They share the same specifications, so each optimization must come with a proof that it preserves the result. We also put FloatLib through extensive numerical checks and speed comparisons with established libraries, including MPFR, Flocq, FLoPS, Berkeley SoftFloat/TestFloat, and the posit libraries SoftPosit and Universal, across a range of formats, operations, and precisions. @Robertljg Project & Paper: Code: