L’informatique est devenue omniprésente dans la vie de tous les jours au travers d’outils de plus en plus riches technologiquement et de plus en plus connectés à internet. Lorsque ces objets arrêtent de fonctionner suite à un concours de circonstances, cela peut avoir des conséquences dramatiques sur la sûreté des personnes qui en dépendent. Leur fonctionnement peut être aussi altéré par une volonté malveillante de nuire et qui lors d’une attaque créera la situation propice à un dysfonctionnement ciblé. Dans ce travail, nous explorons l’utilisation des méthodes formelles dans un environnement embarqué et cyber-physique. Dans un premier temps, nous utilisons F* pour modéliser la sûreté des programmes sur une Arduino. Puis nous implémentons LIO (Library Input Output) en F* dans un contexte système ou embarqué. Nous mettons ici en avant une approche qui permet de choisir entre une vérification statique et une vérification dynamique afin de réduire la charge de preuve ou le coût à l’exécution. Nous proposons également une mécanisation de la preuve de non-interférence en utilisant la métaprogrammation. Cette preuve porte sur l’interaction entre le programme et la librairie plutôt que sur la librairie seulement.