# Research Engineer, Formal Methods at Harmonic

- Company: Harmonic
- What the company does: Mathematical Superintelligence. Backed by Index, Kleiner Perkins and Sequoia.
- Company website: https://harmonic.fun/
- Type: Startups
- Level: Mid level
- Location: Palo Alto
- Work setup: On-site
- Posted: 2026-08-24
- Apply by: 2026-10-08
- Apply: https://jobs.ashbyhq.com/harmonic/74f2ed85-b1cc-40b1-825d-fefd2fcf557c
- Page: https://www.1752.vc/careers/jobs/harmonic-research-engineer-formal-methods/

## About the role

We are seeking a highly motivated and skilled Research Engineer to join our Formal Methods team. The initial focus of this position will be on pushing the limits of AI based theorem proving for verification of software and/or hardware. The successful candidate will play a key role in developing new approaches to express and prove important software and hardware properties, work with AI researchers to train and develop AI systems to reliably check them.

## What they're looking for

- BS or MS in Computer Science, Mathematics, a related technical field, or equivalent industry experience
- Basic proficiency in python
- Proficiency and practical experience with at least one proof assistant (e.g., Lean, Coq, Isabelle, Agda) and a strong foundation in formal methods and mathematical logic
- Experience driving highly technical research projects from early concept to delivery
- Expert level knowledge of Lean4
- PhD in Computer Science, Mathematics, or related technical field

Tags: Engineering