This is the companion artifact page for the INForum 2026 paper ”Comaleer: A Translation Pipeline for Deductive Verification”. It provides access to the tools, repositories, and case studies used in the paper.
The following tools are needed to try the examples.
Follow the four steps below to install Cameleer and run your first verification. These steps assume you already have OPAM installed on your machine.
The case studies below correspond to the examples discussed in the paper. Each data structure is specified in three styles: top-level style, in-depth style, and smart style. Click on view source to see the GOSPEL specifications and OCaml implementations and proof results to view the obligations discharged by each prover.