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.