L'équipe Monad découvre des bugs de sécurité manqués par Claude Opus et Codex en utilisant la vérification formelle.

Selon Foresight News, l'équipe Category Labs de Monad a récemment partagé les résultats de la vérification formelle de la blockchain Monad, révélant plusieurs vulnérabilités de sécurité que des modèles d'IA avancés, dont Claude Opus 4.8 et Codex, n'avaient pas réussi à identifier lors de la revue de code.

Les bugs découverts concernent la conception du solde de réserve dans le mécanisme d'exécution asynchrone de Monad et des problèmes de comportement indéfini en C++ dans l'optimisation du stockage MIP-8. L'équipe a démontré que la vérification formelle a permis de capturer ces défauts, soulignant qu'il est plus efficace, pour exposer les vulnérabilités cachées, de définir des propositions de correction précises avant de demander à l'IA de trouver des contre-exemples, que de faire directement des demandes de revue de code.