Summer Internship - Research

New York, NY /
Research & Development /
Summer Research Internships at CertiK

CertiK is a world-leading cybersecurity firm based in NYC that focuses on smart contract analysis and blockchain auditing. It was founded by prof. Ronghui Gu (Columbia) and prof. Zhong Shao (Yale), drawing on their research about formal verification.

Currently the CertiK research department is developing an operating system kernel (CertiKOS) and a certified compiler (DeepSEA), both of them verified using the Coq proof assistant. We are looking for summer interns to help us transition these from academic research projects into production-ready software. 

Available project include adding new system calls needed to run useful applications on CertiKOS; adding new language features, optimizations, or new verified backends to DeepSEA; and laying the foundations for decentralized proof-checking. The internship is suitable for current master/phd students, or strong undergraduates looking for research experience. Because of the current Covid-19 epidemic, these positions are completely remote.


You should be familiar with one of the following areas:

Formal verification using an interactive proof assistant (e.g. from taking the Software Foundations textbook or similar).
[Preferred] Experience with non-trivial projects written in Coq.


Basic familiarity with Operating Systems implementation (e.g. from taking an OS class), and able to program in C.
[Preferred] Previous experience working on an OS kernel or low-level libraries.


Familiar with compiler implementation (e.g. from taking an Compilers class), and experience with functional programming (e.g. Ocaml, Gallina).
[Preferred] Previous experience working on a big compiler; or experience specifying programming languages using operational semantics; or experience working with WASM, LLVM, or EVM.