Ronghui Gu is a fifth year Ph.D. student at Yale FLINT Group and supervised by Prof. Zhong Shao. His work focuses on building reliable and secure low-level systems. During the past few years, he and his Yale colleagues built CertiKOS, the first fully verified hypervisor. Ronghui earned his B.S. at Tsinghua University and his undergraduate thesis is about verifying the preemptive scheduler of uC/OS-II.