Cet article montre comment implémenter une fonction élémentaire efficace avec arrondi correct prouvé en double-précision. La méthodologie employée dans ce but par la bibliothèque crlibm présente deux aspects novateurs. Le premier concerne la preuve de l'arrondi correct, et plus généralement les techniques employées pour gérer les compromis entre performance et facilité de preuve. Le second est l'utilisation d'optimisations utilisant des caractéristiques les plus avancées des processeurs, ce qui permet d'obtenir une performance équivalente aux meilleures implémentations existantes. L'implémentation du logarithme népérien est décrite en détail à titre d'illustration.