FormalPass est un outil qui transforme automatiquement du code source écrit en C en un modèle formel exprimé en SMT (Satisfiability Modulo Theories). Cela permet aux développeurs et chercheurs de vérifier la correction et la sécurité de leurs programmes via des techniques de vérification formelle avancées, sans nécessiter de connaissances approfondies en SMT.