This is the dissemination page for the Cameleer tool and project. Here, one can find links to videos and online resources about the GOSPEL specification language, the Cameleer tool itself, and the ongoing verification projects.

TLDR: the main documentation about Cameleer is the CAV 2021 paper. To get a quick insight of the tool and immediately start using it, we advise you to read the CAV 20021 paper, clone the GitHub repository and play with some of the available examples.


As a companion to the CAV 2021 paper, we submitted a complete and reusable artifact, publicly available here. This artifact is the prefered way if you want to safely reproduce our proof results and as a step-by-step guide to use Cameleer.


We gave a three hours long tutorial during ICFP 2021. The video is publicly available here. This is mainly an hands-on introduction to the tool and the verification of OCaml programs, annotated with GOSPEL specification elements. The following five case studies are used during the tutorial: