Coq est un système de gestion de preuves formelles. Il fournit un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, ainsi qu'un environnement pour le développement semi-interactif de preuves formelles vérifiables par machine.

Opam est un gestionnaire de paquets source pour le langage de programmation OCaml. Il supporte plusieurs installations de compilateurs simultanées, des contraintes flexibles de paquets et un workflow de développement Git-friendly.

La plateforme Coq est une distribution du logiciel Coq, un assistant de preuve pour les mathématiques, accompagnée d'une sélection de bibliothèques et de plugins. Elle vise à être indépendante du système d'exploitation, fiable, facile à installer et complète.

Zelus est un langage synchrone étendu avec des équations différentielles ordinaires (ODE) pour programmer des systèmes hybrides qui mélangent des modèles discrets et continus. Il partage les principes de base des langages synchrones Lustre et Lucid Synchrone, avec des fonctionnalités supplémentaires telles que la déduction de types, les automates hiérarchiques et les fonctions d'ordre supérieur.

Clangml est une interface écrite en OCaml permettant d'analyser et de générer des informations à partir de code source C en utilisant Clang.

Ce bot, écrit en OCaml, est principalement utilisé dans le développement du projet Coq. Il permet la synchronisation entre GitHub et GitLab, la gestion des pull requests depuis des forks, la gestion des milestones des issues et la gestion du processus de backporting.

Necro est un projet OCaml développé à Inria Rennes en juin 2018, en relation avec l'article de recherche Skeletal Semantics and their Interpretations. Le projet fournit une boîte à outils pour manipuler les squelettes sémantiques, un format pour représenter la sémantique des langages de programmation.

JSkel est un projet skeletal permettant la représentation formelle de la sémantique du langage JavaScript. Il vise à fournir une sémantique aussi proche que possible de la sémantique réelle du langage, en équilibrant une approche formelle et une approche plus pratique.

Necro ML est un outil d'analyse de données et de traitement automatisé de texte permettant de créer des modèles prédictifs. Il est basé sur le langage de programmation OCaml et offre une API pour intégrer ses fonctionnalités dans d'autres applications.

Catala est un langage de programmation conçu pour la littérature juridique programmée en matière socio-fiscale. Il permet de dériver des algorithmes fidèles aux textes législatifs en annotant chaque ligne d'un texte législatif avec sa signification en termes de code.