Résumé : e développement de SMA auto-organisateursmanque encore de méthodes rigoureuses de vérification garantissant la robustesse et la résilience du Systèmes conçu. De telles assurancespeuvent être obtenues grâce à l’application deméthodes formelles. Mais l’intégration de cestechniques de vérifications reste encore modestedue à la complexité liée à la dynamique desSMA auto-organisateurs qui fait émerger leurfonction globale. Dans cet article, nous explorons le potentiel des langages formels, en particulier B-événementiel et la logique TLA, pourprouver des propriétés liées à la robustesse.Nous supposons que ces propriétés pourrontd’abord être observées au niveau global parsimulation. Les techniques formelles nous permettront ensuite d’en faire la preuve. Notre travail est illustré par l’étude de cas des fourmisfourrageuses.