KMADe est un outil d'analyse et de modélisation des activités humaines dédié à la conception et à l'évaluation ergonomique des systèmes interactifs. Il permet de décrire, d'analyser et de formaliser les activités des utilisateurs dans des environnements (informatisés ou non), en situation réelle ou simulée. KMADe est basé sur un modèle formel qui facilite la description, l'examen et l'analyse des tâches, limite les variations interindividuelles, augmente le niveau de complétion des descriptions, autorise des traitements ultérieurs, et facilite les passages entre les modèles de terrain et les étapes du cycle de vie des logiciels.

Le projet atsyra-dev vise à développer des plugins et un studio pour l'analyse de modèles formels, la transformation de langages spécifiques de domaines et la génération de code à partir de modèles. Il s'appuie sur des outils tels qu'Xtend, MapStruct, Testcontainers, OSGi, SLF4J, Entity Framework Core, Guava, OpenTracing, Simple Injector, Apache Ant et Markdown.

CADBIOM est un logiciel open source de modélisation permettant de donner un cadre formel à la modélisation de systèmes biologiques tels que les réseaux de signalisation cellulaire. Il est basé sur la sémantique des transitions surveillées et offre une interface graphique pour faciliter la conception et l'analyse de ces modèles.

Ce projet concerne la transformation de modèles et l'analyse de code réactif, en vérifiant des propriétés spécifiques grâce à la sémantique formelle de Haskell.

Ce projet permet de simuler des systèmes à l'aide de modèles formels, de générer des modèles à partir de spécifications et d'analyser les comportements de ces systèmes.

MCsimCoq est un outil de simulation de systèmes de mémoire informatique. Il permet d'analyser les performances de différents types de mémoire, tels que DDR3 et DDR4, en utilisant des modèles formels générés par Coq. Il vérifie également la conformité des commandes de mémoire avec les protocoles spécifiés.

Le projet vle est un environnement opérationnel de multi-modélisation, de simulation et d'analyse de systèmes complexes dynamiques. Il s'appuie sur la théorie des systèmes de modélisation et de simulation proposée par B. Zeigler avec la spécification DEVS formelle (Discrete Event System Specification).