A mechanized proof of total correctness enables one to verify a program with utmost confidence. Yet, setting up a methodology for reasoning formally on nontrivial code written in a general-purpose language has appeared to be a highly challenging task. In this paper, we propose a framework for modular verification of purely functional code. By embedding the syntax and semantics of a call-by-value functional language in a proof assistant, we are able to specify programs through lemmas describing their big-step behaviour and to verify programs through proofs of such lemmas. Our framework imposes no restriction on the code, apart from its purity, and from a logical perspective is as expressive as the theorem prover being used. The practical result of this work is a technology for proving total correctness of pure Caml programs using the Coq proof assistant. We have applied our approach to fully specify and verify OCamls list library as well as a bytecode compiler and interpreter for mini-ML.