3 months ago
Responsibilities
- Translate design intent and customer requirements into precise formal properties and specifications.
- Use Aristotle intensively to execute formal proofs and diagnose verification failures.
- Scope customer requirements, manage project scope and technical risk, and maintain clear customer communication.
- Develop a technical understanding of complex production-ready code across unfamiliar domains.
- Identify critical properties that customer teams need verified and deliver reproducible workflows.
- Improve Aristotle based on field observations and travel to customer sites.
Requirements
- BS in Computer Science, Mathematics, a related field, or equivalent industry experience.
- Direct experience in hardware verification, software verification, or interactive theorem proving.
- Practical proficiency with at least one proof assistant, such as Lean, Coq, Isabelle, or Agda.
- Strong foundation in formal methods and mathematical logic.
- Proficiency in one or more programming languages, such as Python, C++, or Matlab.
- Ability to independently navigate complex concepts and manage risks and deadlines.
- Ability to communicate effectively in deep technical discussions and high-level customer education or value justification.
- Preferred: MS or PhD, Lean 4 expertise, industrial or commercial formal-verification experience, research publications or patents, and open-source or software-tool contributions.
Benefits
- Unlimited paid time off.
- 401(k) matching.
- Employer-paid health, vision, and dental benefits for employees, with 50% dependent coverage.
- Health Savings Account available for qualifying health plans.
About Harmonic
We are forging the worlds most advanced mathematical reasoning engine