CFML est un outil qui permet de prouver en Coq la correction fonctionnelle de programmes Caml. CFML s'appuie sur la notion de formule caractéristique, qui permet de décrire la sémantique d'un programme impératif sous la forme d'une formule de la logique d'ordre supérieur. Les formules caractéristiques, qui sont à la fois correctes et complètes, sont de tailles linéaires et peuvent être générées automatiquement à partir du code source des programmes.

Elles s'appuient de plus sur la Logique de Séparation, qui permet d'effectuer des raisonnements modulaires, et intègrent la notion de crédits-temps, qui permet de vérifier des propriétés de complexité asymptotique. Dans cet exposé, je présenterai la théorie de CFML et j'illustrerai son utilisation en pratique, à travers plusieurs exemples.