Monad team shares formal verification practices, discovers multiple on-chain security vulnerabilities overlooked during AI model audits

Foresight News reported that the Monad development team, Category Labs, shared their experience using formal verification methods to identify vulnerabilities in key modules of the Monad blockchain. They disclosed several vulnerabilities that cutting-edge large models such as Claude Opus 4.8 and Codex failed to detect during code review, but which were successfully caught during the formal verification process. These issues involve the "Reserve Balance" design in Monad's asynchronous execution mechanism and undefined behavior in C++ during storage optimization in MIP-8. The team believes that, compared to directly asking the models to "review code," first writing precise correctness propositions and then asking the model to find counterexamples is more likely to expose hidden vulnerabilities. At present, formal verification can already be greatly assisted by AI.