Contiki is an open-source OS for the IoT. It provides basic OS features on an event-based kernel, including the scheduler, and a networking stack. Contiki focuses on low-power IPv6 connectivity and typically targets devices with an 8 to 32-bit MCU without Memory Management Unit. This makes such devices a target of choice for attackers. In the scope of the VESSEDIA project, that aims at making formal methods more accessible for IoT targets, a task is dedicated to the verification of the Contiki OS. In this talk, I will present the past and present efforts of verification with Frama-C/WP for different modules of Contiki, namely the memory allocation module, the AES-CCM cryptographics functions, and the linked list module.