AI TRENDS | Category Labs Shares How Formal Verification Found Monad Bugs Missed by Claude Opus 4.8 and Codex

Category Labs, the Monad development team, said it identified vulnerabilities in key Monad blockchain modules using formal verification, including issues that it said were not detected during code reviews by large language models such as Claude Opus 4.8 and Codex. According to Foresight News, the team described its experience using formal verification methods to investigate and uncover these flaws. The disclosed issues involved the “Reserve Balance” design within Monad’s asynchronous execution mechanism and a C++ undefined behavior problem related to storage optimization in MIP-8. Category Labs said that, rather than directly asking models to “review code,” it found it more effective to first write precise correctness propositions and then ask models to search for counterexamples, which it said made hidden vulnerabilities easier to surface. The team added that formal verification can now be substantially supported with AI assistance.