Python est devenu le langage dominant pour le développement informatique général, mais il manque de outils solides pour la vérification formelle. À l’inverse, les programmeurs utilisant des langages comme C bénéficient de vérificateurs de modèles matures, tels que CBMC, qui permettent une raisonnement symbolique exhaustif et une localisation précise des défauts. La complexité intrinsèque de Python, combinée à la verbose et à la nature bas niveau des transpilers existants (par exemple Cython), a historiquement limité l’application de la vérification formelle aux programmes Python.Dans cet article, nous proposons PyVeritas, un cadre novateur qui exploite les grands modèles linguistiques (LLM) pour effectuer une transpilation de haut niveau de Python vers C, suivie d’une vérification par modèle borné et d’une localisation de défauts basée sur MaxSAT sur le code C généré. PyVeritas permet ainsi la vérification et la localisation des bogues dans les programmes Python en utilisant des outils existants de vérification formelle pour C. Notre évaluation empirique sur deux benchmarks Python montre qu’une transpilation basée sur les LLM peut atteindre un haut degré de précision, allant jusqu’à 80 à 90 % pour certains modèles, ouvrant la voie à un environnement de développement efficace qui soutient la vérification basée sur des assertions et une diagnostic des erreurs interprétable pour des programmes Python de taille modeste mais non triviaux.