Monad is like Ethereum but aims to be faster using higher parallelism/pipelining across the entire stack. We use iris and BRiCk C++ semantics to formally verify monad’s C++ implementation.
A blog post explaining our verification experience and roadmap in detail: Finding bugs that frontier models miss
A lot remains to be formally verified:
- concurrent merkle patricia triedb (C++)
- EVM to x86 compiler (C++)
- monadBFT consensus with pipelining and multiple concurrent proposers (Rust)
We are looking for someone experienced in using AI (e.g. codex-cli with skills/hooks) to accelerate formal proof/spec development. We do manually review top-level specs.
Apply here.
Email me (aanand@category.xyz) if you have any questions.