Frama-C est une boîte à outils pour l'analyse et la vérification de programmes C. Les différents greffons organisés autour d'un noyau commun communiquent via le langage de spécification ACSL (ANSI C Specification Language). Cet exposé fournira un aperçu de Frama-C et des résultats obtenus dans la vérification d'un module de Contiki, un système d'exploitation pour les objets connecté. D'autres travaux en cours et futurs autour de Frama-C, notamment dans le cadre d'une collaboration LIFO-LIFAT, seront également évoqués.