Formal Methods PhD Intern

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.