Ronghui Gu is an Assistant Professor at Columbia University. He obtained his Ph.D. in Computer Science from Yale University in 2016. His dissertation won the Distinction Dissertation Award of Yale and was nominated for ACM Dissertation Award. He obtained his B.S. from Tsinghua University in 2011. Gu focused on the research of the formal verification of system software and was the principal developer and author of CertiKOS, the world's first fully verified concurrent OS kernel. He co-founded a blockchain startup, CertiK, which aims to build trustworthy blockchain ecosystems using formal verification techniques.