Monad Team Discovers Security Bugs Missed by Claude Opus and Codex Using Formal Verification

According to Foresight News, Monad's Category Labs team recently shared findings from formal verification of the Monad blockchain, revealing multiple security vulnerabilities that advanced AI models including Claude Opus 4.8 and Codex failed to identify during code review.

The discovered bugs involve the Reserve Balance design in Monad's asynchronous execution mechanism and undefined C++ behavior issues in MIP-8 storage optimization. The team demonstrated that formal verification successfully captured these flaws, highlighting how defining precise correctness propositions before requesting AI to find counterexamples is more effective at exposing hidden vulnerabilities than direct code review requests.