In this paper, we present a formal proof, developed in the Coq system, of the correctness of an automatic differentiation algorithm. This is an example of interaction between formal methods and numerical analysis (involving, in particular, real numbers). We study the automatic differentiation tool, called O∂yssée, which deals with FORTRAN programs, and using Coq we formalize the correctness proof of the algorithm used by O∂yssée for a subset of programs. To do so, we briefly describe the library of real numbers in Coq including real analysis, which was originally developed for this purpose, and we formalize a semantics for a subset of FORTRAN programs. We also discuss the relevance of such a proof.