# Blockchain formal verification @ category labs

**URL:** <https://discourse.rocq-prover.org/t/blockchain-formal-verification-category-labs/3043>\
**Category:** Jobs\
**Created:** [June 6, 2026, 12:01am UTC](https://discourse.rocq-prover.org/t/blockchain-formal-verification-category-labs/3043 "2026-06-06T00:01:16Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![aa755](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/aa755/32/937_2.png) [@aa755](https://discourse.rocq-prover.org/u/aa755)\
**Post date:** [June 6, 2026, 12:01am UTC](https://discourse.rocq-prover.org/t/blockchain-formal-verification-category-labs/3043/1 "2026-06-06T00:01:16Z")

</div>

Monad is like Ethereum but aims to be faster using higher parallelism/pipelining across the entire stack. We use [iris](https://iris-project.org/) and [BRiCk](https://skylabsai.github.io/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](https://category-labs.github.io/category-research/formalverif/blogs/frontier-models/)

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](https://jobs.ashbyhq.com/category-labs/4717412e-8243-4eb9-bed1-4c585d7ff977).  
Email me (aanand@category.xyz) if you have any questions.

---

<div class="post-metadata">

**Author:** ![discourse\_ai\_spam](https://avatars.discourse-cdn.com/v4/letter/d/c68b51/32.png) [@discourse\_ai\_spam](https://discourse.rocq-prover.org/u/discourse_ai_spam)\
**Post date:** [June 6, 2026, 12:01am UTC](https://discourse.rocq-prover.org/t/blockchain-formal-verification-category-labs/3043/2 "2026-06-06T00:01:19Z")

</div>



---

<div class="post-metadata">

**Author:** ![system](https://us1.discourse-cdn.com/flex001/uploads/coq/original/2X/5/594ae4f4100bbfb124daa5506e475bf73c1738f5.png) [@system](https://discourse.rocq-prover.org/u/system)\
**Post date:** [June 6, 2026, 12:06pm UTC](https://discourse.rocq-prover.org/t/blockchain-formal-verification-category-labs/3043/3 "2026-06-06T12:06:34Z")

</div>