The number of Internet of Things (IoT) applications israpidly increasing and allows embedded devices today tobe massively connected to the Internet. This raises softwaresecurity questions. This paper demonstrates the usageof formal verification to increase the security of Contiki,a popular open-source operating system for the IoT. Wepresent a case study on deductive verification of encryptiondecryptionmodules of Contiki (namely, AES–CCM*) usingFrama-C, a software analysis platform for C code.