Senior Software Engineer, Formal Verification at Category Labs

<p style="min-height:1.5em"><strong>Category Labs</strong> (formerly known as Monad Labs) is a team of systems engineers and researchers on a mission to design and build at the frontier of decentralized technology. We strive to deliver significant improvements over existing blockchain solutions. After raising $225M in series A funding, led by Paradigm, we are growing our team.</p><p style="min-height:1.5em">We’re the team behind Monad, a high-performance, EVM-compatible Layer 1 whose public mainnet is now live. We write the core software that runs it: a <a target="_blank" rel="noopener noreferrer nofollow" href="https://github.com/category-labs/monad"><u>parallel-execution EVM</u></a>, a custom state database, and a <a target="_blank" rel="noopener noreferrer nofollow" href="https://github.com/category-labs/monad-bft"><u>BFT consensus client</u></a>, all developed in the open.</p><p style="min-height:1.5em"></p><h2><strong>The Role</strong></h2><p style="min-height:1.5em">We’re hiring a Senior Software Engineer in Formal Verification to prove the correctness of the Monad implementation. Your work will involve writing machine-checked proofs about real production C++ code, including concurrent features like optimistic execution and novel Monad mechanisms such as reserve balance and optimized page-level storage. You’ll work in Rocq (formerly Coq), using the Iris separation logic framework and the BRiCk formal semantics of C++, building models of our designs and proving the implementation equivalent to them, as a vital member of a small, high-performing team.</p><p style="min-height:1.5em"></p><h2><strong>What You’ll Do</strong></h2><ul style="min-height:1.5em"><li><p style="min-height:1.5em">Formally verify the highest-risk parts of the Monad implementation, including concurrent and parallel execution logic.</p></li><li><p style="min-height:1.5em">Build and refine Rocq models of system designs, then prove the C++ implementation equivalent to those models, catching design and implementation bugs before they reach main.</p></li><li><p style="min-height:1.5em">Develop specifications and weakest-precondition proofs for production C++ using BRiCk and Iris separation logic.</p></li><li><p style="min-height:1.5em">Strengthen theorem statements and proof automation, and devise approaches that scale verification to a fast-moving codebase.</p></li></ul><p style="min-height:1.5em"></p><h2><strong>Who You Are</strong></h2><ul style="min-height:1.5em"><li><p style="min-height:1.5em">You have at least 5 years of software engineering experience in C++, much of it building performant systems from scratch – databases, device drivers, embedded systems, or the like.</p></li><li><p style="min-height:1.5em">You have hands-on experience with an interactive theorem prover, ideally Rocq (formerly Coq), and can write machine-checked proofs about real, running code.</p></li><li><p style="min-height:1.5em">You reason about concurrency and memory with a rigor most engineers ne