Babel

CDuce

Galène

Coq

C-SHORe

CUDF

Kappa

Ocsigen

Stamina

Awali · A generic C++-platform for computing with automata and transducers

Usuba

CELIA · Plugin for static analysis and verification of C programs with dynamic lists

Equations · Function definition by dependent pattern-matching and (well-founded) recursion in Coq

Js_of_ocaml · Compiler of OCaml bytecode in Javascript

Knowledge · LaTeX package for the easy management of internal and external hyperlinks in a document

Lwt · OCaml library for cooperative threads

Menhir · Generator of OCaml parsers

Morbig · Parser for POSIX shell

Rewr · Library for algebraic rewriting

Semigroupe · Computation of finite semigroups

Shncpd · Implementation of a large subset of the Homenet protocol stack with minimal dependencies

SPEN · Solver for separation logic entailments

Vaucanson-g · LaTeX macro package for drawing automata

Catex · LaTeX tool to produce string diagrams for morphisms in free strict monoidal categories

Dune · Dune is a build system for OCaml

jsCoq, pyCoq, CoqBot

SerAPI · Library for machine-to-machine interaction, now replaced by Coq LSP

Equations · Equations provides a notation for writing programs by dependent pattern-matching and (well-founded) recursion in Coq

Dose3 · Library and collection of tools to perform la large spectrum of analysis on package repositories

ReSMT · An implementation of compositional rewriting theory algorithms