AI-assisted formal verification of real C++ in the Monad execution client

Frontier models missed bugs in ordinary review but found them when asked to construct Rocq proofs against real C++ code

At Category Labs, we’ve been using AI-assisted formal verification to prove correctness of real C++ code in the Monad execution client. In our experience, frontier models often missed bugs in ordinary review, but found them when asked to do