Formal Verification @ Category Labs
Our goal is to formally verify the implementation of the Monad blockchain. Toward that goal, we have made significant progress. So far, we have verified parts of the implementation that we considered highest-risk, including concurrent features such as optimistic execution and novel Monad features such as reserve balance, which helps parallelize consensus and execution, and optimized page-level storage. To formally verify our actual C++ code, we use the BRiCk formal semantics of C++ in Coq, developed by SkyLabsAI. This semantics defines C++ abstract syntax trees and their weakest-precondition semantics in the Iris separation logic framework of Coq. This lecture series describes how we use this framework to formally verify concurrent C++ programs in Coq.
Reserve Balance
Reserve balance allows the consensus process in Monad to propose blocks even before previous blocks have been executed by the execution process. For some accounts, a portion of the account balance is reserved for transaction fees. We modeled our design in Coq and proved the key property: transactions accepted by consensus will be able to pay their fees. This proof caught several design bugs before implementation began. Later we also proved that the C++ implementation of the execution-side logic is equivalent to the Coq model. A separate part of the reserve balance mechanism is implemented in the consensus process, which is written in Rust, and that part has not been proven equivalent to the Coq model.
MIP-8 Page Commitments
The MIP-8 work formalizes the storage-page commitment algorithm used by the C++ implementation. The Coq model defines an induced-subtree Merkle commitment for sparse page-local storage and proves the central binding theorem: two distinct normalized page openings cannot produce the same commitment unless the underlying hash trace contains an aligned collision. We then proved that the C++ implementation is equivalent to the Coq model.
The proof scripts for both results were generated by Codex CLI, though we spent a few days iterating with it to make the theorem statements stronger and more intuitive. During that proof work, Codex CLI found a C++ undefined-behavior bug while the relevant code was still under review. We fixed it before the pull request was merged; the buggy version never reached main, much less a release. As of June 4, 2026, Codex CLI with GPT-5.5 and extra-high reasoning does not find the bug when asked only to perform an ordinary code review of the buggy C++ file, without carrying out the Coq correctness proof.
Optimistic Execution
A previous version of execute_block, which executes the next block, was verified down to the
specifications of the callees that execute individual transactions.
The proof shows that although execute_block executes transactions in parallel, the result is equivalent to running them sequentially.
The specs and proofs were covered as examples in the above-mentioned lecture series.
For this proof, we simplified the code by replacing shared pointers with raw pointers and dynamic allocation with static allocation.
We are working on porting these proofs to the latest code.
Proof repo release: coming soon.