Abstract. Formal veriﬁcation of numerical programs is notoriously difﬁcult. On the one hand, there exist automatic tools specialized in ﬂoatingpoint arithmetic, such as Gappa, but they target very restrictive logics. On the other hand, there are interactive theorem provers based on the LCF approach, such as Coq, that handle a general-purpose logic but that lack proof automation for ﬂoating-point properties. To alleviate these issues, we have implemented a mechanism for calling Gappa from a Coq interactive proof. This paper presents this combination and shows on several examples how this approach oﬀers a signiﬁcant speedup in the process of verifying ﬂoating-point programs.