Dx est un outil en cours de développement permettant de dériver du code C à partir d'un code Gallina monadique, en passant par une représentation intermédiaire. Il fournit des commandes Coq pour générer automatiquement la représentation intermédiaire et des fonctions pour transformer cette représentation en modules dx contenant un arbre syntaxique abstrait pour C.