  OCaml is particularly well-fitted for formal verification. On one hand, it is
a multi-paradigm language with a well-defined semantics, allowing one to write
clean, concise, type-safe, and efficient code. On the other hand, it is a
language of choice for the implementation of sensible software, e.g.,
industrial compilers, proof assistants, and automated solvers. Yet, with the
notable exception of some interactive tools, formal verification has been
seldom applied to OCaml-written programs. In this paper, we present the ongoing
project Cameleer, aiming for the development of a deductive verification tool
for OCaml, with a clear focus on proof automation. We leverage on the recently
proposed GOSPEL, Generic OCaml SPE cification Language, to attach rigorous, yet
readable, behavioral specification to OCaml code. The formally-specified
program is fed to our toolchain, which translates it into an equivalent program
in WhyML, the programming and specification language of the Why3 verification
framework. Finally, Why3 is used to compute verification conditions for the
generated program, which can be discharged by off-the-shelf SMT solvers. We
present successful applications of the Cameleer tool to prove functional
correctness of several significant case studies, like FIFO queues (ephemeral
and applicative implementations) and leftist heaps, issued from existing OCaml
libraries.
