In this paper, we present an example of the implementation and verification of a functional program. We expose an experience in developing an application in the area of symbolic computation: the computing of Gröbner basis of a set of multivariate polynomials. Our aim is the formal certification of several aspects of the program written in the functional language Caml. In addition, efficient computing of the algorithm is another issue to take into account.