Outil dédié à la résolution de problèmes de satisfaction de contraintes (CSP) et à la validation de propriétés logiques sur des modèles formels. Il permet d'analyser des systèmes critiques en vérifiant leur cohérence et en générant des contre-exemples ou des preuves de validité. Développé dans le cadre d'un projet de recherche financé par l'ANR, il s'appuie sur des techniques avancées de logique et de satisfiabilité.

Le projet smt2d est un outil de vérification de formules mathématiques et d'analyse de contraintes logiques. Il permet de traiter des problèmes de satisfiabilité modulo théories (SMT) en utilisant la logique first-order avec équations et inégalités.

Wild_Life est un système de programmation qui intègre la logique et la programmation fonctionnelle, les types avec héritage et la programmation par contraintes. Il a été conçu pour être un outil robuste pour le prototypage d'applications nécessitant la représentation et la manipulation de structures de données complexes. Il est livré avec plusieurs outils puissants pour aider au prototypage, tels qu'un préprocesseur, des analyseurs, un kit d'interface graphique et un mode Emacs LIFE.