Formal Verification Engineer

Hands-on experience with hardware model checking—writing SVA/PSL properties, running bounded or unbounded proofs, and closing out formal verification targets at block or subsystem level

Practical experience with at least one interactive theorem prover (Lean, Coq, Isabelle/HOL, Agda, or similar)

Experience embedding an existing language or IR into a theorem prover—whether an HDL, compiler IR, ISA, or similar—is a strong plus

Experience with compiler correctness proofs or verified compilation (e.g.

Comfort working across the hardware/software boundary: you understand both RTL microarchitecture and compiler IR design well enough to find the correctness properties that matter

The US base salary for this full-time position is determined based on a variety of factors including role, experience, location, job-related skills, and relevant education and training. Career length is only a guideline for compensation.

0–5 years of experience — $140,000–$220,000 + equity

5–10 years of experience — $140,000–$340,000 + equity

10+ years of experience — $140,000–$420,000 + equity

Our offers allow candidates to swap cash for equity.

Apply model checking and formal property verification to RTL blocks, memory subsystems, and interconnects, providing complete coverage wherever possible, using tools such as JasperGold or VC-Formal.

Develop and maintain machine-checked proofs for critical compiler transformations, ensuring correctness of lowering passes from our high-level programming model down to hardware

Build embeddings of our hardware description languages and simulator models into interactive theorem provers (e.g.

Lean 4, Rocq, Isabelle/HOL), and use those embeddings to prove functional correctness and microarchitectural properties directly against the designs

Collaborate with architecture, compiler, and silicon verification teams to identify correctness properties worth proving and translate them into tractable proof obligations

Drive methodology for integrating formal tools (JasperGold, SymbiYosys, or equivalent) into our existing practices