2.
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
1 appearance on the backlist front page in the last 30 days.
Frontier models missed bugs in ordinary review but found them when asked to construct Rocq proofs against real C++ code