L'équipe de Monad partage ses pratiques de vérification formelle et découvre plusieurs failles de sécurité on-chain omises lors des audits de modèles IA.

Foresight News rapporte que l'équipe de développement de Monad, Category Labs, a publié un article partageant son expérience dans l'utilisation de la vérification formelle pour détecter les failles dans les modules clés de la blockchain Monad. L’article révèle que plusieurs vulnérabilités, que des modèles avancés tels que Claude Opus 4.8 et Codex n’avaient pas pu détecter lors de l’audit de code, ont été trouvées avec succès lors du processus de démonstration formelle. Cela concerne la conception du « Reserve Balance » dans le mécanisme d’exécution asynchrone de Monad et un problème de comportement non défini en C++ dans l’optimisation de stockage MIP-8. L’équipe estime que, plutôt que de demander directement à un modèle d’« auditer le code », il est plus efficace d’écrire d’abord des propositions de correction précises puis d’exiger du modèle qu’il recherche des contre-exemples ; cette méthode met plus facilement en lumière les failles cachées, et la vérification formelle peut désormais largement s’appuyer sur l’IA pour être menée à bien.