  We present an approach to obtain formally verified implementations of
classical Computational Logic algorithms. We choose the Why3 platform because
it allows to implement functions in a style very close to the mathematical
definitions, as well as it allows a high degree of automation in the
verification process.
  As proof of concept, we present a mathematical definition of the algorithm to
convert propositional formulae to conjunctive normal form, implementations in
WhyML (the Why3 language, very similar to OCaml), and proofs of correctness of
the implementations. We apply our proposal on two variants of this algorithm:
one in direct-style and another with an explicit stack structure. Being both
first-order versions, Why3 processes the proofs naturally.
