This article presents my feedback on introducing Frama-C for cybersecurity in several engineering and master’s level university courses. It consists of a single lecture and a single lab session. Frama-C is an open source platform providing C  code analyzers based on formal methods. The course focuses on its three main techniques provided through dedicated analyzers, namely deductive verification with Wp, abstract interpretation with Eva, and runtime annotation verification with E-ACSL. The aim of the course is to introduce students to these formal techniques, emphasizing their practical aspects in cybersecurity.