Outil formel dédié à l'analyse de la robustesse des systèmes embarqués face aux attaques par injection de fautes. Il combine la description RTL d'un processeur, le binaire d'un logiciel et un modèle d'attaquant pour évaluer la sécurité d'un système intégrant des contre-mesures. µArchiFI permet de prouver formellement la sécurité d'un système ou d'identifier des contre-exemples illustrant des vulnérabilités exploitables.

VeriFast est un outil d'analyse statique conçu pour vérifier la sécurité et la correction des programmes. Il permet de détecter des vulnérabilités potentielles dans le code source, notamment en Java, en s'appuyant sur des annotations et des propriétés formelles. L'outil est utilisé pour garantir la robustesse des systèmes critiques, comme les cartes à puce ou les applications embarquées, en identifiant les erreurs de logique ou les failles de sécurité avant leur déploiement.