Contexte et objectifs

Le projet a mobilisé des agents d'intelligence artificielle pour transcrire le code source de CPython, l'implémentation de référence du langage Python, en Lean, un langage de preuve assistée par ordinateur. Au total, 613 318 lignes de Lean ont été générées, réparties dans 1 539 fichiers, contenant 18 898 théorèmes et lemmes. Chaque fonction a d'abord été reproduite ligne à ligne, puis testée contre l'exécutable CPython sur des dizaines de milliers d'entrées avant toute tentative de preuve.

Le processus de validation repose sur un double contrôle : un second agent vérifie la copie et confirme la validité de la preuve. À ce jour, 4 071 fonctions ont franchi cette étape, ce qui montre la capacité du pipeline à gérer une partie importante du code C de CPython.

Mécanisme de formalisation

La traduction conserve les détails arithmétiques du code C, y compris les dépassements de capacité qui surviennent avec de très grands entiers. Un exemple présenté montre la fonction C comptant les nombres dans un intervalle, reproduite en Lean avec la même logique de débordement. La preuve associe cette version lente à la version rapide utilisée par CPython, garantissant l'égalité des résultats pour toutes les entrées testées.

Les premières itérations ont produit des preuves triviales, comme « si la fonction renvoie un nombre, ce nombre est ≥ 0 », qui ne détectaient pas les dysfonctionnements. Un mécanisme de revue a donc introduit la question « une version défectueuse de la fonction pourrait‑elle satisfaire la preuve ? », ce qui a conduit à renforcer les spécifications et à éliminer les preuves faibles.

Détection de bugs et limites

Chaque preuve acceptée est exécutée sur l’interpréteur réel. Cette double exécution a permis d'identifier 418 rapports de bugs, dont environ 55 sont capables de provoquer un plantage ou une corruption de mémoire avec du code Python standard. Parmi les cas critiques, on trouve :

class Key(StrEnum):
    NAME = "name"
class User: pass
a = User(); a.name = "ada"
b = User(); b.age = 36
vars(b).setdefault(Key.NAME, "anon")
# Segmentation fault

Cette séquence déclenche un segfault lorsqu'un dictionnaire d'attributs utilise une clé StrEnum et que la même classe possède un attribut différent.

e = ET.Element("root")
e[:] = [ET.Element(f"a{i}") for i in range(7)]
e[5:2] = [ET.Element("X")]
[c.tag for c in e]
# 'a2' apparaît deux fois, 'a4' disparaît

Le même problème apparaît dans le module ElementTree, où une tranche inversée duplique un nœud et en supprime un autre, corrompant la structure interne.

Un troisième exemple concerne le parseur d'e‑mail : un identifiant de message contenant un espace entre crochets entraîne une exception non gérée, révélant une incohérence entre la spécification RFC et l'implémentation.

Analyse des implications

Les bugs découverts proviennent souvent d'hypothèses non explicites dans le code C, comme l'absence d'échec d'allocation mémoire ou la stabilité des adresses libérées. La formalisation a mis en évidence ces hypothèses, par exemple le code du set qui supposait que l'adresse d'un bloc libéré ne serait jamais réutilisée. En réalité, les allocateurs réaffectent fréquemment les adresses, ce qui rend la vérification de l'intégrité du set vulnérable.

Le processus montre que la preuve formelle ne garantit pas la conformité du modèle à la réalité tant que le modèle lui‑même n'est pas complet. La combinaison de tests massifs, de revue humaine et de preuves machine‑checked constitue une méthode robuste pour réduire le risque de régression dans un projet de la taille de CPython.