Formal Verification Engineer

Job Title

Formal Verification Engineer

Role Summary

Work on formal verification and machine-checked proofs for MatX hardware, memory subsystems, interconnects, and compiler transformations. You will collaborate with architecture, compiler, and silicon verification teams to define and discharge correctness properties across the hardware/software stack.

Position is on-site/hybrid at Mountain View (HQ); employees are expected to work from the Mountain View office Tuesdays–Thursdays.

Experience Level

Mid-level (mid-career). The posting includes compensation bands for early, mid, and senior career levels, but the role title and scope align with a mid-career engineering level.

Responsibilities

Primary responsibilities focus on applying formal methods to hardware and compiler correctness and integrating formal tools into verification flows.

• Apply model checking and formal property verification to RTL blocks, memory subsystems, and interconnects using tools such as JasperGold or VC-Formal.
• Develop and maintain machine-checked proofs for critical compiler transformations and lowering passes.
• Embed HDLs and simulator models into interactive theorem provers (e.g. Lean 4, Coq, Isabelle/HOL) and prove functional and microarchitectural properties.
• Collaborate with architecture, compiler, and silicon verification teams to identify and translate correctness properties into proof obligations.
• Drive methodology for integrating formal tools (JasperGold, SymbiYosys, or equivalents) into verification practices.

Requirements

Clear technical expertise in formal verification and practical experience working across hardware and software boundaries are required.

• Must-have: Hands-on experience with hardware model checking (writing SVA/PSL properties, running bounded/unbounded proofs, and closing formal verification targets at block or subsystem level).
• Must-have: Practical experience with at least one interactive theorem prover (Lean, Coq, Isabelle/HOL, Agda, or similar).
• Must-have: Strong understanding of RTL microarchitecture and compiler IR design; able to identify correctness properties across the hw/sw stack.
• Must-have: Able to work in a small, fast-moving team with broad scope of ownership.
• Nice-to-have: Experience embedding a language or IR into a theorem prover (HDL, compiler IR, ISA, etc.).
• Nice-to-have: Experience with compiler correctness proofs or verified compilation (e.g. CompCert-style or translation validation).
• Employment requirement: Authorized to work in the United States and able to work from MatX offices in Mountain View on the stated in-office days.

Education Requirements

Not specified.

About the Company

Company: MatX

Headquarters: Mountain View, California, USA

MatX specializes in creating faster chips for large language models (LLMs), focusing on innovative hardware and software solutions. The company fosters a collaborative and supportive work environment, welcoming candidates of all experience levels. Their approach prioritizes deep understanding and consideration of novel methods to drive efficiency and performance in their projects, particularly in silicon design and related engineering roles.