# Formal Verification Engineer at MatX

- Company: MatX
- What the company does: We make the best chips physically possible for the large model needs of frontier labs.
- Company website: https://matx.com
- Type: Startups
- Level: Mid level
- Location: Mountain View (HQ) or Remote
- Work setup: Remote
- Pay: $160K to $275K base salary per year (USD)
- Posted: 2026-05-19
- Apply by: 2026-10-08
- Apply: https://jobs.ashbyhq.com/matx/20f2ce61-2e1e-4009-8539-b460344ee018
- Page: https://www.1752.vc/careers/jobs/matx-formal-verification-engineer/

## About the role

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

## What they're looking for

- 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. CompCert-style or translation validation) is a strong plus
- 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
- Able to work in a small team where the scope of what you own will be large and shift quickly

Tags: Hardware