AlphaProof Code : vérification formelle de logiciels
Original : AlphaProof Code
Pourquoi c'est important
La vérification formelle automatisée pourrait transformer la sécurité logicielle à grande échelle.
Google DeepMind annonce AlphaProof Code, un système capable de vérifier formellement des logiciels complexes, dont le protocole de messagerie chiffrée de Signal, via Gemini.
Google DeepMind a présenté le 10 novembre 2026 AlphaProof Code, une extension de son système AlphaProof appliquée cette fois à la vérification formelle de code logiciel. L'annonce phare : le système aurait vérifié le protocole cryptographique de Signal, l'application de messagerie chiffrée de référence. AlphaProof avait initialement démontré ses capacités en mathématiques formelles, notamment en résolvant des problèmes de niveau olympique. AlphaProof Code reprend cette approche — raisonnement formel assisté par Gemini — pour l'appliquer à des bases de code réelles. La vérification formelle, longtemps réservée à des spécialistes et à des systèmes critiques comme l'avionique ou les microprocesseurs, reste rare dans le développement logiciel grand public en raison de sa complexité. Si les détails techniques complets restent à publier, l'objectif affiché est de détecter des classes entières de bugs et de failles de sécurité avant tout déploiement, sans se limiter aux tests unitaires traditionnels.