Cameleer: a Deductive Verification Tool for OCaml

Despite all the advances in deductive verification and proof automation over the past few decades, little attention has been given to the family of functional languages. We present Cameleer, a tool for the deductive verification of programs written in OCaml, with a clear focus on proof automation. Cameleer uses the recently proposed GOSPEL (Generic OCaml SPEcification Language) to attach rigorous, yet readable, behavioral specification to OCaml code.