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.
AI TRENDS | Category Labs Shares How Formal Verification Found Monad Bugs Missed by Claude Opus 4.8 and Codex
2026-06-26 12:53:53
Disclaimer:
1. The information provided does not constitute investment advice. Investors should make independent decisions and bear all risks themselves.
2. The copyright of this content belongs to the original author. The views expressed herein are solely those of the author and do not represent the stance or position of this website.
