Senior Software Engineer, Formal Verification

Role Overview

You’ll be a Senior Software Engineer in Formal Verification at Category Labs, helping prove the correctness of the Monad implementation. The work focuses on machine-checked proofs for real production C++ code, including concurrent features.

Responsibilities

• Formally verify the highest-risk parts of the Monad codebase, especially concurrent and parallel execution logic.
• Write and refine Rocq (formerly Coq) models of system designs.
• Prove the C++ implementation is equivalent to the formal models.
• Develop specifications and weakest-precondition proofs for production C++ using BRiCk and Iris separation logic.
• Strengthen theorem statements and improve proof automation.
• Propose methods to scale verification to a fast-moving codebase.

Requirements

• 5+ years of software engineering experience, with substantial C++ systems development.
• Hands-on experience with an interactive theorem prover, ideally Rocq (Coq).
• Ability to write machine-checked proofs about real, running code.
• Strong reasoning about concurrency and memory.
• Solid instincts for software architecture, memory management, and performance profiling.
• Bachelor’s, Master’s, or PhD in Computer Science (or equivalent experience).
• Clear communication and ability to thrive in a small, high-ownership team.

Nice to Have

• Experience formalizing novel system mechanisms like reserve balance and optimized page-level storage (implied by the implementation).
• Interest in proof engineering techniques that improve verification throughput as the codebase evolves.