Cet article présente un retour d'expérience lié à un enseignement de Frama-C pour la cybersécurité dispensé dans plusieurs formations d'ingénieurs et universitaires de niveau master. Il est constitué d'un cours et d'un TP de trois heures chacun. Frama-C est une plateforme open source d'analyse de code C offrant un grand nombre d'analyseurs. Le cours est articulé autour des trois techniques et analyseurs principaux offerts par la plateforme, à savoir la vérification déductive avec Wp, l'interprétation abstraite avec Eva, et la vérification d'annotations à l'exécution avec E-ACSL. Le but du cours est de faire découvrir ses techniques formelles aux étudiants en insistant sur les aspects pratiques en cybersécurité.