Cet article présente une traduction de programmes OCaml spécifiés en Gospel vers Viper, un langage intermédiaire de preuves formelles supportant la logique de séparation. L'objectif pratique est d'ajouter à Cameleer un nouveau backend pour prouver des programmes OCaml manipulant le tas. La spécification logique de tels programmes OCaml est décrite dans le langage Gospel et nous détaillons ici les extensions apportées pour le support de la logique de séparation en Viper.