Traduttore, traditore : vérification formelle d'un compilateur