Vitalik Buterin, cofondateur d’Ethereum, a publié un billet le 18 mai expliquant comment l’intelligence artificielle associée à la vérification formelle pourrait améliorer la sécurité des logiciels, en particulier pour l’écosystème Ethereum. Il a mentionné que 90 % de sa valeur nette est détenue en ETH. Il a cité le vérificateur de théorèmes Lean comme outil clé et deux projets concrets : Arklib, une implémentation de STARKs formellement vérifiée, et evm-asm, une abstraction de machine virtuelle Ethereum. La vérification formelle utilise des preuves mathématiques pour démontrer l’exactitude du code dans tous les scénarios possibles, contrairement aux tests traditionnels. Deux limitations ont été identifiées : le risque de spécification et l’impossibilité de vérifier physiquement le matériel.
Source: Lire l’article original
