VCFloat2 is a tool for automated floating-point round-off error analysis in Coq, offering improved accuracy, performance, and support for nonstandard number formats. It extends the VCFloat tool by providing a new functional modeling language, efficient optimizer for floating-point expressions, and enhanced modularity for integration with other verification tools. VCFloat2 supports user-defined operators, any-precision literals, and non-IEEE formats, enabling tighter error bounds and more flexible analysis. It also includes a decomposition tactic to mitigate the dependency effect in interval analysis, allowing tighter error bounds on benchmarks where VCFloat1 failed. The tool is used in several verification projects, including differential equations, matrix-vector operations, and the Jacobi method, demonstrating its effectiveness in building end-to-end machine-checked proofs of accuracy and correctness. VCFloat2's soundness theorem ensures that error bounds are correctly derived, and its efficient simplifier reduces the complexity of interval goals, enabling faster verification. The tool is available as open-source and has been evaluated against common benchmarks, showing competitive error bounds and transparent certificates.VCFloat2 is a tool for automated floating-point round-off error analysis in Coq, offering improved accuracy, performance, and support for nonstandard number formats. It extends the VCFloat tool by providing a new functional modeling language, efficient optimizer for floating-point expressions, and enhanced modularity for integration with other verification tools. VCFloat2 supports user-defined operators, any-precision literals, and non-IEEE formats, enabling tighter error bounds and more flexible analysis. It also includes a decomposition tactic to mitigate the dependency effect in interval analysis, allowing tighter error bounds on benchmarks where VCFloat1 failed. The tool is used in several verification projects, including differential equations, matrix-vector operations, and the Jacobi method, demonstrating its effectiveness in building end-to-end machine-checked proofs of accuracy and correctness. VCFloat2's soundness theorem ensures that error bounds are correctly derived, and its efficient simplifier reduces the complexity of interval goals, enabling faster verification. The tool is available as open-source and has been evaluated against common benchmarks, showing competitive error bounds and transparent certificates.