Chamois est un fork du compilateur C formellement vérifié CompCert, avec des ajouts de Verimag et Kalray. Il s'agit d'un compilateur pour un sous-ensemble important du langage C, générant du code pour les processeurs PowerPC, ARM, x86, RISC-V et KVX. La particularité de CompCert est qu'il a été prouvé correct à l'aide de l'assistant de preuve Coq : le code assembleur généré est garanti de se comporter comme prescrit par la sémantique du code C source.

CompCert est un compilateur pour un large sous-ensemble du langage C qui génère du code pour plusieurs architectures de processeurs. Il est unique car il a été formellement vérifié à l'aide de l'assistant de preuve Coq, garantissant ainsi le comportement du code assembleur généré par rapport aux semantiques du code source C.

Outil d'aide à la compilation de code source pour le noyau Linux, avec la capacité de générer de la documentation technique au format HTML et PDF.

Aideweb est une collection d'utilitaires JavaScript côté serveur pour les applications et services web, utilisant Node.js et Express. Il permet de compiler et de lier du code source C/C++ avec un serveur web Express et de l'utiliser comme un service web.