SlipstreamJobs tracks this role from the company's public career site. Apply directly on the employer's site.
Harmonic is building a mathematical reasoning engine that combines Lean4 and reinforcement learning to perform rigorous, verifiable AI reasoning. The company recently achieved gold-medal performance on the 2025 International Math Olympiad and resolved long-standing open problems, demonstrating AI's capability in formal domains.
As a Research Engineer on the Formal Methods team, you will focus on advancing AI-based theorem proving for software and hardware verification. Your work will involve developing new approaches to express and prove critical system properties, collaborating with AI researchers to train and refine AI systems for reliable verification, and pushing the boundaries of what formal methods can achieve.
Key responsibilities include conducting research in formal methods across software, hardware, and mathematical domains; applying formal verification techniques using Lean or similar proof assistants to verify safety-critical systems; and developing algorithms and techniques to improve the efficiency and effectiveness of formal methods for AI systems.
You should have a BS or MS in Computer Science, Mathematics, or a related technical field (or equivalent industry experience), basic Python proficiency, and practical experience with at least one proof assistant (Lean, Coq, Isabelle, or Agda) with a strong foundation in formal methods and mathematical logic. You must have a track record of driving highly technical research projects from concept to delivery.
Preferred qualifications include expert-level Lean4 knowledge, a PhD in Computer Science or Mathematics, experience verifying programs in safety-critical domains (aerospace, defense, automotive, medical, cryptography), a proven track record in programming language research or development, high-quality research publications or patents, and open-source contributions.
