Un modèle émergent est récemment devenu très populaire : les essaims de robots mobiles. Ces robots autonomes peuvent réaliser en collaboration différentes tâches complexes, par exemple l'exploration de zones dévastées pour planifier et aider aux opérations de recherche et secours. Une extrême _dynamicité_ caractérise ce modèle, tant pour la structure, la charge, les données que pour l'environnement d'exécution. Les possibles fautes byzantines, bien connues pour être remarquablement difficiles à appréhender lors de raisonnements informels (et donc sources d'erreurs aux conséquences potentiellement désastreuses une fois le système déployé), rendent cruciale l'obtention de _garanties fortes_ sur le comportement des agents et la correction des protocoles distribués. SAPPORO propose un cadre pour la preuve formelle (mécanisée pour l'assistant à la preuve Coq) destiné au développement sûr des protocoles distribués en interaction locale qui sont au cœur des réseaux dynamiques de capteurs mobiles. L'ambition du projet est : 1) De poser les fondations d'un cadre formel mécanisé destiné aux concepteurs et développeurs pour essaims de robots mobiles, 2) De permettre la démarche de certification de (candidats) protocoles distribués dans ce contexte vis-à-vis de propriétés attendues sur le comportement spatio-temporel de l'essaim, 3) D'établir formellement, si le cas échoit, l'impossibilité d'existence pour de tels protocoles. Au cœur de SAPPORO se trouve une formalisation du modèle des essaims de robots mobiles pour l'assistant à la preuve Coq. Sa conception s'accompagne : - Du développement de _techniques de preuve_ , automatisées, afin d'aider autant que faire se peut les utilisateurs dans le développement, - D'une sémantique opérationnelle claire munie d'un langage d'annotation afin de _spécifier_ le comportement de programmes et de permettre la génération de conditions de vérification, - Enfin, d'un importante _bibliothèque_ d'algorithmes, de _classes_ d'algorithmes, de théorèmes certifiés corrects, lesquels serviront aux développements de nouveaux protocoles distribués.