高级软件工程师，形式验证
Senior Software Engineer, Formal Verification
**Category Labs**（曾用名 Monad Labs）是一支系统工程师和研究人员组成的团队，致力于在去中心化技术的前沿设计和构建解决方案。我们努力在现有区块链方案上实现重大改进。在由 Paradigm 领投的 A 轮融资中筹集了 2.25 亿美元后，我们正在扩大团队。
我们是 Monad 的开发团队，Monad 是一个高性能、兼容 EVM 的 Layer 1 区块链，其公开主网现已上线。我们编写运行它的核心软件：一个[并行执行 EVM](https://github.com/category-labs/monad)，一个自定义状态数据库，以及一个[BFT 共识客户端](https://github.com/category-labs/monad-bft)，所有代码均在开源环境中开发。
### **职位描述**
我们正在招聘一名高级软件工程师，专注于形式化验证，以证明 Monad 实现的正确性。你的工作将涉及对实际生产环境中的 C++ 代码进行机器可检查的证明，包括乐观执行等并发特性，以及 Monad 的新型机制，如储备余额和优化的页面级存储。你将使用 Rocq（曾用名 Coq），结合 Iris 分离逻辑框架和 C++ 的 BRiCk 形式语义，构建我们设计的模型，并证明实现与模型等价，作为一支小型高效团队的重要成员。
### **你将负责**
- 对 Monad 实现中风险最高的部分进行形式化验证，包括并发和并行执行逻辑。
- 构建和优化系统设计的 Rocq 模型，然后证明 C++ 实现与这些模型等价，在主网发布前发现设计和实现中的错误。
- 使用 BRiCk 和 Iris 分离逻辑为生产环境中的 C++ 编写规范和最弱前提证明。
- 强化定理陈述和证明自动化，并设计能够扩展到快速迭代代码库的验证方法。
### **你应具备**
- 至少有 5 年 C++ 软件工程经验，其中大部分时间用于从零开始构建高性能系统——数据库、设备驱动程序、嵌入式系统等。
- 有使用交互式定理证明器的实际经验，最好是 Rocq（曾用名 Coq），并且能够对实际运行的代码编写机器可检查的证明。
- 对并发和内存有严谨的思考方式，大多数工程师不需要这样的严谨性——你被那些“可能正确”不够好的问题所吸引。
- 对软件架构、内存管理和性能分析有敏锐的直觉。
- 你拥有
查看英文原文
**Category Labs** (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.
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 [parallel-execution EVM](https://github.com/category-labs/monad), a custom state database, and a [BFT consensus client](https://github.com/category-labs/monad-bft), all developed in the open.
### **The Role**
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.
### **What You’ll Do**
- Formally verify the highest-risk parts of the Monad implementation, including concurrent and parallel execution logic.
- 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.
- Develop specifications and weakest-precondition proofs for production C++ using BRiCk and Iris separation logic.
- Strengthen theorem statements and proof automation, and devise approaches that scale verification to a fast-moving codebase.
### **Who You Are**
- 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.
- You have hands-on experience with an interactive theorem prover, ideally Rocq (formerly Coq), and can write machine-checked proofs about real, running code.
- You reason about concurrency and memory with a rigor most engineers never need – and you're drawn to problems where "probably correct" isn't good enough.
- You have sharp instincts for software architecture, memory management, and performance profiling.
- You hold a Bachelor's, Master's, or PhD in Computer Science, or have equivalent experience.
- You communicate clearly and thrive on a small team where everyone owns the result.
### **Why Work with Us**
- **Challenging problems:** You’ll work on extremely challenging problems with massive impact. See our [Blogs](https://www.category.xyz/blogs) and [Publications & Talks](https://www.category.xyz/papers-talks) for a flavor of the problems we are solving in the real world.
- **Huge opportunity:** The Ethereum Virtual Machine (EVM) standard is ubiquitous, but existing EVM-compatible chains are very slow. Monad’s core innovations offer developers the best of both worlds (portability and performance) and are a game-changer for mass user adoption in crypto.
- **The right team:** You’ll be part of a small, exceptional team (engineers and researchers make up 90% of the team).
- **Open by default:** Our core software is public on GitHub. You’ll build in the open, and your work ships where the whole ecosystem can see it.
- **Culture:** We’re a lean team working together to achieve very ambitious goals. We are united in our culture of collaboration, low ego, and high-quality output. As an early member of our team, you’ll help to shape our culture.
- **Compensation:** You’ll receive a competitive salary and equity package.
- **Resources and growth:** We’re well-capitalized, with [backing](https://x.com/monad_xyz/status/1777687376136982767) from leading venture funds like Paradigm, Electric Capital, Greenoaks, Dragonfly, and Coinbase Ventures. We keep a lean team, and this is a rare opportunity to join. You’ll learn a lot and grow as our company scales.
### **How We Use AI**
We’re an AI-native team, and we expect engineers to use coding agents and keep up as the tooling evolves. A few things we believe:
- AI is leverage, not a crutch. Review what it generates with the same scrutiny you’d give a teammate’s PR, and own every line you ship.
- Judgment is what matters, not how long you typed by hand. We won’t ask for “N years of [tool].” The stack turns over every few months, so what matters is that you pick up new tools fast and know where and when they apply.
### **Salary and Benefits**
The base salary range for this role is $180,000 – $250,000. This reflects the minimum and maximum range across US locations. It does not include benefits, token, or equity incentives. The final offer may vary based on factors such as relevant skills, experience, domain expertise, and work location. If you are based outside of the US, we have geographic considerations that may impact your final compensation.
Benefits for all Full-Time Employees:
- Private health insurance options
- Flexible paid time off
- Monthly wellness reimbursement
- Paid parental leave
Benefits for US employees:
- World-class benefits package with 100% paid medical, dental, and vision insurance including 75% coverage for dependents and HSA + FSA options
- 401(k) with company match
- Lunch and dinner stipend (in-office NYC)
Benefits for employees hired through an EOR (outside of the US) will be based on EOR offerings and country-specific requirements.
_Category Labs is an Equal Employment Opportunity (EEO) employer and welcomes all qualified applicants. Applicants will receive fair and impartial consideration without regard to race, sex, color, religion, national origin, age, disability, veteran status, genetic data, or other legally protected status._