Internships

We offer research internships for PhD students (year-round). Internships usually last 3 to 4 month and are usually remote, with one or two visits in person at our San Francisco or NYC offices.

We are currently looking for a research intern (summer or fall) for a model-based testing project. If you are interested, please reach out to [email protected].

Past Interns

Joseph Tafese (spring 2025)

Joseph worked on formally verifying the Winch compiler. Results are on github and are the subject of a submission to FMCAD 2025 (under review).

Patrick Redmond (winter 2024)

Patrick worked on formally verifying consensus algorithms using the Ivy theory prover. His work resulted in a formally-verified implementation of Paxos running in the FBA model .

Yunqi Zhang (summer 2024)

Yunqi worked on distributed algorithms to build blockchain overlay networks in the FBA model. Part of his work appears in the paper Constellation: Peer-to-Peer Overlays for Federated Byzantine Agreement Systems, which was presented at FC 2025.

George Pîrlea (winter 2023)

George worked on the formal verification of Soroban smart contracts using Ivy. Results are on github. George also contributed a translation from Ivy to mypyvy, implemented in Ivy.