Babel

CDuce

Coq

C-SHORe

CUDF

Kappa

Ocsigen

Stamina

Vaucanson

CELIA · Analyseur statique de programmes C avec structures dynamiques et allocateurs de mémoire, développé comme plugin de la plate-forme Frama-C

Equations · Définition de fonctions par filtrage dépendant et récursion bien fondée en Coq

Js_of_ocaml · Compilateur de bytecode OCaml en Javascript

Knowledge · Package LaTeX pour la gestion facile d'hyperliens internes et externes ou de tables d'indexes

Lwt · Bibliothèque OCaml pour les threads coopératifs

Menhir · Générateur d'analyseurs syntaxiques OCaml

Morbig · Analyse syntaxique de scripts shell POSIX

Rewr · Bibliothèque de réécriture algébrique

Semigroupe · Calcul de semigroupes finis

Shncpd · Implémentation d'un sous-ensemble important du protocole Homenet

SPEN · Solveur pour la logique de séparation avec prédicats inductifs, pour la vérification de programmes manipulant des structures de données dynamiques