Monad Improvement Proposal (MIP) 8 is primarily a user-facing gas improvement: if a contract has already paid to load one storage slot, then nearby slots should be cheaper to access. Today, the EVM exposes storage as individual 32-byte slots, and the Merkle Patricia Trie hashes storage keys before committing to them. Keys are therefore committed through trie paths whose keys are uniformly distributed. This constrains how the implementation can affect gas costs. The goal of MIP-8 is to align the commitment model to extend the EVM storage model to account for the reality that physical SSDs read and write data in much larger chunks.
MIP-8 changes this by making pages visible to both the gas schedule and the storage commitment. The trie commits to pages rather than individual slots. The page commitment must be fast to recompute, especially for sparse pages, but still bind the exact occupied slots and values. The inclusion and exclusion proofs should also be as small as possible. MIP-8 does this with an induced-subtree Merkle commitment. The 128 slots are grouped into 64 adjacent 64-byte pair leaves. Active pair leaves are hashed and merged while empty branches are skipped, and singleton nodes are carried upward. Finally, the resulting subtree root is sealed together with the full 128-bit slot bitmap.
At the model level, we proved the binding property for the page commitment scheme. The Rocq model is deliberately simpler than the C++ implementation: unlike C++, it explicitly builds the compact induced tree, hashes it via straightforward tree recursion, and seals the root with the bitmap. The main theorem is phrased as a collision extractor. If two different normalized pages produce the same commitment root, then the two computations must contain an aligned hash collision: either at the final bitmap seal, at a pair leaf, or at an internal merge node. This is a stronger theorem statement than simply assuming “no BLAKE3 collisions anywhere.”
Then we connected the model to the actual C++ function
monad::page_commit. The spec
of the function says that the returned bytes32_t is exactly
the Rocq model root of the page represented by
storage_page_t. Because we proved the equivalence, the
model-level binding theorem applies to the C++ implementation as well.
These proofs were done in May 2026. Codex CLI did both the model and C++
code proofs almost completely automatically. Our time was mainly spent
reviewing the statements of the theorems it proved. The versions that
Codex proved initially were weaker and not as intuitive.
For background on the BRiCk-based verification workflow used here, see How C++ verification works in the main report.
While doing the Rocq proof that upper bounds the size of inclusion proofs, we realized that the bound can be significantly improved if we use a different merge schedule: put the slot pairs in a balanced binary tree instead of the geometric schedule which merges active siblings when they meet in the 64-pair complete tree and skips unary stretches (and empty parts). Not only does it result in a tighter bound on the size of inclusion proofs, root computation gets faster and less variable. The balanced schedule exposes more parallelism to BLAKE3 by avoiding long dependency chains from unlucky page geometry. In preliminary benchmarks, we observed 10–20% faster root computation when the pages are not over 60% full. Codex later produced a Rocq model and binding proof for the balanced variant. The theorem statement remains the same.
The C++ compiler we use (GCC) is not verified. A bug in the compiler could make the produced code behave in a way that is different from the BRiCk semantics we use, which formalizes the C++ standard. A year ago, verifying a competitive C++ compiler would have been a multi-person-year project. With the recent advances in agentic proofs, it seems much easier. But we currently don't have any plans to tackle this and hope someone else solves this in the next few years.