Equipa da Monad Descobre Bugs de Segurança Não Detetados por Claude Opus e Codex Usando Verificação Formal

De acordo com a Foresight News, a equipa Category Labs da Monad partilhou recentemente descobertas da verificação formal da blockchain Monad, revelando múltiplas vulnerabilidades de segurança que modelos avançados de IA, incluindo Claude Opus 4.8 e Codex, não conseguiram identificar durante a revisão de código.

Os bugs descobertos envolvem o design do Reserve Balance no mecanismo de execução assíncrona da Monad e problemas de comportamento indefinido em C++ na otimização de armazenamento MIP-8. A equipa demonstrou que a verificação formal capturou com sucesso estas falhas, destacando como definir proposições de correção precisas antes de pedir à IA para encontrar contraexemplos é mais eficaz a expor vulnerabilidades ocultas do que solicitações diretas de revisão de código.