Equipe do Monad descobre bugs de segurança que passaram despercebidos por Claude Opus e Codex usando verificação formal

Segundo o Foresight News, a equipe do Category Labs da Monad compartilhou recentemente descobertas da verificação formal do 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 equipe demonstrou que a verificação formal capturou essas falhas com sucesso, destacando como definir proposições precisas de correção antes de solicitar que a IA encontre contraexemplos é mais eficaz para expor vulnerabilidades ocultas do que solicitações diretas de revisão de código.