우리는 광범위한 형식 커버리지, 기계 검사 정확성, 그리고 효율적인 인증 실행을 결합한 Lean 4의 검증된 임의 정밀도 부동소수점 연산 라이브러리인 FloatLib를 소개합니다. 우리가 아는 한, FloatLib는 IEEE 이진 및 십진수 연산, 임의 너비 포지트(posits), P3109, 그리고 사용자 정의 형식 및 반올림 규칙을 상호 교환 가능한 인증 소프트웨어 백엔드 뒤에서 통합하는 최초의 Lean 라이브러리입니다. 모든 인증된 백엔드는 부호 있는 0과 예외 값을 보존하면서 완전한 인코딩 사양과 같음이 증명되며, 수치 이론들은 실행을 실제 반올림, 오차 경계, 그리고 정확성과 연결합니다. FloatLib는 작은 형식에 대한 포괄적인 인증 테이블과 가드-스티키 불변량(guard-and-sticky invariants) 및 독립적으로 검사된 몫 후보를 기반으로 하는 검증된 워드 및 임(limb) 커널을 결합합니다. 또한, 포지트 개발은 임의 너비 내에서 표준 반올림 임계값과 정확한 몫 누적을 증명합니다. 일치하는 작업 부하 전반에 걸쳐, FloatLib는 FLoPS 대비 최대 1.46배, 그리고 Universal 대비 116배의 속도 향상을 달성하며, 이진 연산 같은 일부 영역에서는 MPFR보다 느리게 유지됩니다. 독립적인 적합성 테스트에는 테스트된 관계 하에서 차이가 없는 1억 2백만 개 이상의 TestFloat 평가가 포함됩니다. 우리는 라이브러리, 증명, 벤치마크, 평가 데이터 및 가이드를 오픈 소스로 공개합니다.