Charguéraud presents a tool for the verification of purely functional programs consisting of two parts. The first part is used to generate characteristic formulas, and the second part is used to formulate a set of lemmas, notations, and tactics for the verification of the characteristic formulas. The characteristic formulas are generated from the source codes of the functional program by extracting the post-condition and the abstraction of the program. The characteristic formulas are then used for the verification of the functional program. Soundness and a completeness proof are used for verification purposes.

The main contribution of this paper is in the area of formalization of data abstraction. Note that the proposed tool can only be used for a purely functional program.