FloatLib enables verified and efficient floating-point math in Lean
FloatLib: Verified Floating-Point Arithmetic in Lean
Logic in Computer ScienceProgramming Languages
Summary
Floating-point arithmetic is used by computers to handle numbers with decimals, but it can be tricky to get exactly right due to rounding and special values. The authors developed FloatLib, a software library in the Lean programming language, that supports many types of floating-point formats and checks correctness with mathematical proofs. This library also runs efficiently and has been tested extensively to ensure results match expected standards. FloatLib helps programmers trust the accuracy of complex number calculations in their software.
What this means in practice
- •For software developers: Implement high-assurance numerical computations with certified correctness across multiple floating-point formats.
- •For hardware designers: Validate and verify new floating-point hardware implementations against formal specifications using this certified arithmetic library.
Authors
Robert Joseph George, Will Adkisson, Anima Anandkumar
Abstract
We present FloatLib, a verified arbitrary-precision floating-point arithmetic library in Lean 4 that combines broad format coverage, machine-checked correctness, and efficient certified execution. To our knowledge, FloatLib is the first Lean library to unify IEEE binary and decimal arithmetic, arbitrary-width posits, P3109, and user-defined formats and rounding rules behind interchangeable certified software backends. Every certified backend is proved equal to a complete encoded specification, preserving signed zeros and exceptional values, while numerical theorems connect execution to real rounding, error bounds, and exactness. FloatLib combines exhaustive certified tables for small formats with verified word and limb kernels based on guard-and-sticky invariants and independently checked quotient candidates. Its posit development additionally proves standard rounding thresholds and exact quire accumulation within capacity for arbitrary widths. Across matched workloads, FloatLib achieves speedups of up to 1.46x over FLoPS and 116x over Universal, while remaining slower in some regimes such as binary arithmetic against MPFR. Independent conformance testing includes more than 102 million TestFloat evaluations with zero differences under the tested relation. We release the library, proofs, benchmarks, evaluation data, and guide as open source.