We present Cameleer, an automated deductive verification tool for OCaml. We leverage on the recently proposed GOSPEL (Generic OCaml SPEcification 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 one in WhyML, the programming and specification language of the Why3 verification framework. We report on successful case studies conducted in Cameleer.

** Note to ML workshop organizers: given our tool clearly targets verification of OCaml programs, we feel this could also be of interest for the OCaml workshop. However, we believe a deductive verification tool for programs written in an important language of the ML family can interest a wider audience, hence we are submitting to the ML workshop in the first place.