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 model our design in Coq and prove the key property: transactions accepted by consensus will be able to pay their fees. We also prove 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 starts from a compact, pedagogical induced-tree algorithm, connects it to the traced hash computation used for binding statements, and proves the central collision-extraction theorem for distinct openings. We then proved that the C++ implementation is equivalent to the Coq model.
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.