Vitalik Buterin : La vérification formelle assistée par l'IA est l'avenir du développement de logiciels sécurisés

Vitalik Buterin a présenté un argumentaire optimiste quant à l'avenir de la cybersécurité, affirmant que la vérification formelle assistée par l'IA pourrait changer fondamentalement la façon dont les logiciels sécurisés sont écrits. Plutôt que de considérer l’IA comme une menace pour la sécurité du code, Buterin la considère comme un outil qui, associé à une vérification formelle, pourrait produire des logiciels mathématiquement prouvés et très efficaces. Son point de vue remet en question le pessimisme croissant du secteur à l’égard des cyberattaques basées sur l’IA. Une nouvelle approche du développement de logiciels gagne du terrain dans les cercles de recherche d’Ethereum. Les développeurs écrivent du code dans des langages de bas niveau ou directement en Lean, un langage utilisé pour les preuves mathématiques vérifiables. L’objectif est un code dont l’exactitude peut être vérifiée automatiquement et mathématiquement. Buterin décrit cette méthode comme potentiellement transformatrice, citant le chercheur Yoichi Hirai, qui la qualifie de « forme finale de développement logiciel ». L’approche sépare entièrement l’efficacité de la lisibilité. Une version du code s'exécute rapidement ; un autre est écrit clairement pour la compréhension humaine, et une preuve les relie. Cela est particulièrement important pour les systèmes à enjeux élevés tels que les ZK-EVM, les signatures résistantes aux quantiques et les algorithmes de consensus. Ces systèmes sont complexes à construire mais possèdent des propriétés de sécurité simples à énoncer formellement. C’est précisément dans cet écart entre complexité et clarté que la vérification formelle fonctionne le mieux. Des projets comme Arklib et evm-asm appliquent déjà cette méthode à l’infrastructure Ethereum. Le projet evm-asm construit une implémentation EVM directement dans l'assembly RISC-V, puis prouve formellement qu'elle correspond à une version lisible de haut niveau. Certaines voix dans l’industrie ont fait valoir que la découverte de bogues grâce à l’IA rend impossible l’utilisation de logiciels sécurisés et sans confiance. De nombreuses personnes ont affirmé qu’avec la recherche de bogues assistée par l’IA, il serait impossible de sécuriser le code (et donc de faire quoi que ce soit sans confiance). J'ai un point de vue beaucoup plus optimiste, et la vérification formelle assistée par l'IA est en grande partie la raison pour laquelle : https://t.co/0ceMBZ6uqj - vitalik.eth (@VitalikButerin) 18 mai 2026 Buterin repousse directement ce point de vue. Il considère la période actuelle comme un défi de transition plutôt que comme un changement permanent en faveur des attaquants. Une fois le paysage stabilisé, il pense que les défenses seront plus solides qu’avant. Il cite le travail de Mozilla comme preuve à l’appui. Mozilla a noté que les failles de sécurité sont limitées et que les défenseurs disposent désormais d'un chemin réaliste pour les trouver toutes. La tradition cypherpunk, fondée sur l’idée selon laquelle les défenseurs du numérique détiennent un avantage, ne doit pas être abandonnée. Le modèle de Buterin divise le logiciel en un noyau sécurisé et des composants périphériques moins fiables. Le Edge s'exécute dans des bacs à sable avec des autorisations minimales. Le noyau, intentionnellement réduit, bénéficie pleinement de la vérification formelle assistée par l’IA. Buterin veille à ne pas exagérer les arguments en faveur d’une vérification formelle. Plusieurs échecs documentés montrent ses réelles limites. Des bogues sont apparus dans des compilateurs C formellement vérifiés où certaines contraintes n'étaient tout simplement jamais spécifiées. Une vulnérabilité de 2025 dans libcrux a montré que des wrappers intrinsèques non vérifiés pouvaient corrompre les sorties sur des plates-formes matérielles spécifiques. Un autre bug a provoqué un crash du processus en raison d'une erreur de déchiffrement non gérée dans le code en dehors de la partie vérifiée. Le schéma des échecs est cohérent : soit seule une partie du code a été vérifiée, soit une propriété critique n’a jamais été incluse dans la preuve. La vérification formelle ne peut pas prouver qu'un logiciel est correct au sens humain du terme, mais seulement que les propriétés spécifiées sont valables sous des hypothèses spécifiées. Les attaques par canal secondaire présentent une autre limite. Même un système de cryptage parfaitement éprouvé peut divulguer une clé privée à cause de fluctuations électriques. Les modèles mathématiques des attaquants ne capturent pas toujours tous les types de fuites réels. La conclusion de Buterin est mesurée. La vérification formelle n’est pas une solution complète, mais elle constitue un puissant accélérateur d’une tendance en matière de sécurité déjà en cours – une tendance que l’IA rend considérablement plus accessible.