Deductive Verification of Realistic OCaml Code

We present the formal verification of a subset of the Set module from the OCaml standard library. The proof is conducted using Cameleer, a new tool for the deductive verification of OCaml code. Cameleer takes as input an OCaml program, annotated using the GOSPEL specification language, and translates it into an equivalent program writen in WhyML, the specification and programming language of the Why3 verification framework. We present our verification effort and detail on the main challenges. Carlos Pinto NOVA LINCS & Universidade da Beira Interior, Portugal Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology Simão Melo de Sousa NOVA LINCS & Universidade da Beira Interior, Portugal