About the role#
As a Formal Methods PhD Intern, you will work alongside researchers and engineers to formally verify a new low-level, production programming language and compiler. You will write formal specifications and complex mechanized proofs in Rocq. This role offers mentorship, clear milestones, and the opportunity to publish and open-source your artifacts.
What you'll do#
- Contribute to the design, development, and maintenance of mechanized theorems and proofs in Rocq.
- Propose and validate solutions to technical problems.
- Participate in code reviews and design discussions.
- Anticipate and communicate potential roadblocks.
- Formally articulate, reason about, and verify low-level security, safety, and correctness properties of languages such as Rust, C, and C++.
What you'll need#
- Current enrollment in a PhD program in Formal Methods or Programming Languages with experience using Rocq.
- Ability to commit to a full-time 21+ week term.
- Previous professional software engineering experience.
- Understanding of type systems and logic systems.
- Ability to read, write, and understand formal programming language specifications and implementations.
- Familiarity with SMT or constraint solving.
- Familiarity with, or a willingness to learn, Rust and OCaml.
- High level of independence and autonomy.
Location & details#
- This is a remote, full-time, paid internship.
- This position is based in the United States.
