L'objectif de l'équipe Démons est de proposer des méthodes et des outils pouvant s'intégrer dans le cycle de développement logiciel et permettant de produire du code correct vis-à-vis de comportements attendus.

L'équipe développe une plateforme générique de vérification de programmes (la platforme Why), qui produit des obligations de preuve à partir de programmes annotés de spécifications formelles et les transmet ensuite à des outils de preuve, interactifs ou automatiques. Des instances pour les langages C (Caduceus) et Java (Krakatoa) sont bâties sur cette infrastructure générique.