VCFloat2 is an extension of the VCFloat tool, designed to verify floating-point C programs in Coq. It improves upon VCFloat1 by offering higher accuracy, better performance, and more generality for non-standard number formats. VCFloat2 supports user-defined operators, exact division, and efficient optimization for multinomial floating-point expressions. It also includes a new functional modeling language and a library for reasoning about functional models. The tool has been applied to various verification projects, including differential equations, matrix-vector operations, and iterative solvers. The paper provides a detailed description of VCFloat2, its contributions, and its applications, along with a review of round-off error analysis and floating-point arithmetic.VCFloat2 is an extension of the VCFloat tool, designed to verify floating-point C programs in Coq. It improves upon VCFloat1 by offering higher accuracy, better performance, and more generality for non-standard number formats. VCFloat2 supports user-defined operators, exact division, and efficient optimization for multinomial floating-point expressions. It also includes a new functional modeling language and a library for reasoning about functional models. The tool has been applied to various verification projects, including differential equations, matrix-vector operations, and iterative solvers. The paper provides a detailed description of VCFloat2, its contributions, and its applications, along with a review of round-off error analysis and floating-point arithmetic.