La semaine dernière à OOPSALA '25, nos développeurs Act ont présenté une version améliorée et évolutive de CheckMate, un prouveur automatisé pour vérifier formellement la sécurité théorique des jeux des protocoles blockchain. En résumé : l'outil vérifie si les incitations dans un protocole rendent la tricherie peu rentable.

Les protocoles ont besoin de 3 types de sécurité : • Cryptographique : Vos clés/mots de passe sont-ils solides ? • D'implémentation : Y a-t-il des bugs dans le code ? • Théorique des jeux : Les incitations sont-elles alignées pour que tricher ne soit pas rentable ? Ce dernier point est crucial, mais souvent ignoré.

La sécurité théorique des jeux consiste à s'assurer que même des acteurs rationnels et égoïstes préfèrent suivre les règles - car dévier coûte plus que cela ne rapporte. C'est l'"économie" de la sécurité.

CheckMate prouve formellement et automatiquement la sécurité théorique des jeux en utilisant des solveurs SMT. L'article introduit un algorithme « diviser pour régner » compositionnel qui s'adapte à des millions de nœuds, entrelaçant la génération de modèles et l'analyse pour plus d'efficacité.

Pourquoi cela est important : Nous pouvons désormais prouver automatiquement, formellement et à grande échelle que les incitations d'un protocole blockchain rendent la tricherie irrationnelle - avant le déploiement.