Claude d'Anthropic écrit désormais du code et en prouve automatiquement la sûreté

L'enjeu est considérable pour l'industrie logicielle. Les tests ne peuvent démontrer que la présence de défauts, jamais leur absence, alors qu'une preuve formelle garantit qu'un programme respecte sa spécification pour toutes les entrées possibles. Jusqu'ici, cette approche restait réservée à quelques projets critiques, comme l'aérospatiale ou la cryptographie, car écrire des preuves exigeait des experts rares et un effort souvent supérieur à celui du développement lui-même. Si une IA peut produire ces preuves à grande échelle, des bibliothèques largement utilisées pourraient bénéficier de garanties de sûreté jusque-là hors de portée, ce qui réduirait le risque de failles de sécurité dans des composants dont dépendent d'innombrables applications.

Cette avancée s'inscrit dans une tendance plus large où les modèles de langage deviennent capables de raisonnement formel, notamment avec des assistants de preuve. Le volume de code généré par IA ne cesse de croître, et avec lui la difficulté de s'assurer de sa fiabilité par une relecture humaine. La vérification automatique apparaît donc comme une réponse naturelle : si la machine écrit le code, elle peut aussi en démontrer la validité, avec un vérificateur déterministe qui contrôle chaque preuve et écarte le risque d'erreur du modèle. Reste à voir si cette méthode s'étendra à des bases de code plus complexes et si les mainteneurs open source l'adopteront durablement.