This work has the objective to present a simple, clear and intuitive framework for compilers verification of functional languages in the proof assistant Coq, that, as a final product, can obtain a standalone verified compiler capable of being used in real life. With this in mind, we propose to use natural semantics as unifying framework, that is to say, to use this formalism to define each of the compiler’s components in order to perform this task. To show this method, we present a correct compiler of the small functional language with call by value Mini-ML, formalized in Coq. As a result of following this approach, we introduce a new big-step machine inspired by Landin’s SECD and Leroy’s Modern SECD as target machine. To the best of the authors’ knowledge, this is the first correct compiler that is verified by using natural semantics as unifying framework in Coq from which we can obtain a verified compiler capable of being used in real life.