
I am the Tang Family Assistant Professor of Computer Science at Columbia University.
My research spans a range of areas in Programming Languages, Operating Systems, and Blockchain, with a focus on systems verification and proof automation.
I also co-founded CertiK, a Web3 cybersecurity unicorn startup valued at $2 billion and backed by Insight Partners, Tiger Global, Sequoia, Coatue, and Goldman Sachs. Press on CertiK: The Wall Street Jounrnal, CNBC, Bloomberg, Forbes, Yahoo Finance.
[CV] [Bio] [Google Scholar] [Research Statement]
Hiring!
My Columbia lab is looking for Ph.D. students and Postdocs. Check out our recent OSDI'22, PLDI'22, SOSP'21, OSDI'21 (best paper award), S&P'21, and CACM Research Highlights (and the press release) for an overview of our latest breakthrough on building certified systems software.
News
Janurary 2023 | Awarded NSF CAREER Award. |
April 2022 | Awarded Amazon Research Awards (3rd times). |
April 2022 | CertiK closed the $88M series B3 round at $2 Billion valuation. |
March 2022 | Three papers are accepted to appear at OSDI 2022. |
February 2022 | Giallar is accepted to appear at PLDI 2022. |
August 2021 | VRM is accepted to appear at SOSP 2021. |
July 2021 | DistAI won the Jay Lepreau Best Paper Award at OSDI 2021. |
April 2021 | Grant on Verified Enclave Layers ($4,563,980) is funded by DARPA. |
Education
- Ph.D. in Computer Science, Yale University, December 2016
- Advisor: Prof. Zhong Shao.
- Distinguished Dissertation of Yale Graduate School of Art and Science.
- B.S. in Computer Science, Tsinghua University, June 2011.
- Graduation with Highest Distinction (3 out of 140).
Selected Publications
-
[New][OSDI 2022] Design and Verification of the Arm Confidential Compute Architecture. X. Li, X. Li, C. Dall, R. Gu, J. Nieh, Y. Sait, and G. Stockwell Media coverage: Columbia Engineering News
-
[New][OSDI 2022] DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. J. Yao, R. Tao, R. Gu, and J. Nieh
-
[New][PLDI 2022] Giallar: Push-button Verification for the Qiskit Quantum Compiler R. Tao, Y. Shi, J. Yao, X. Li, A. Javadi-Abhari, A. Cross, F. Chong, and R. Gu
-
[SOSP 2021] Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware. R. Tao, J. Yao, X. Li, Shih-Wei Li, J. Nieh, and R. Gu
-
[USENIX Security 2021] Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. S. Li, X. Li, R. Gu, J. Nieh, and J. Hui
-
[OSDI 2021] DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. J. Yao, R. Tao, R. Gu, J. Nieh, S. Jana, and G. Ryan. OSDI Jay Lepreau Best Paper Award
-
[PLDI 2021] Gleipnir: Toward Practical Error Analysis for Quantum Programs. R. Tao, Y. Shi, J. Yao, J. Hui, F. Chong, and R. Gu
-
[S&P (Oakland) 2021] A Secure and Formally Verified Linux KVM Hypervisor. S. Li, X. Li, R. Gu, J. Nieh, and J. Hui Media coverage: Columbia Engineering News
-
[PLDI 2020] Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks. J. Yao, G. Ryan, J. Wong, S. Jana, and R. Gu
-
[ICLR 2020] CLN2INV: Learning Loop Invariants with Continuous Logic Networks. G. Ryan, J. Wong, J. Yao, R. Gu, and S. Jana
-
[CACM] Building Certified Concurrent OS Kernels. R. Gu, Z. Shao, H. Chen, J. Kim, J. Koenig, X. Wu, V. Sjoberg, and D. Constanzo. Research Highlights See "Technical Perspective: The Scalability of CertiKOS" by Andrew W. Appel.
-
[SOSP 2019] Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. L. Nelson, J. Bornholt, R. Gu, A. Baumann, E. Torlak, and X. Wang SOSP Best Paper Award
-
[PLDI 2018] Certified Concurrent Abstraction Layers. R. Gu, Z. Shao, J. Kim, X. Wu, J. Koenig, V. Sjoberg, H. Chen, D. Constanzo, and T.Ramananandro
-
[OSDI 2016] CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. R. Gu, Z. Shao, H. Chen, X. Wu, J. Kim, V. Sjoberg, and D. Constanzo Media coverage: Yale News, International Business Times, Yale Daily News
[POPL 2015] Deep Specifications and Certified Abstraction Layers. R. Gu, J. Koenig, T. Ramananandro, Z. Shao, X. Wu, S. Weng, H. Zhang, and Y. Guo
Selected Awards
VMware Systems Research Award, February 2023. |
NSF CAREER Award, Janurary 2023. |
Builders and Innovators, Goldman Sachs, May 2022. |
Amazon Research Awards, April 2022. |
Amazon Research Awards (co-PI), July 2021. |
OSDI Jay Lepreau Best Paper Award, July 2021. |
The Top 100 Yale Alumni In Technology Of 2021, June 2021. |
Amazon Research Awards, April 2021. |
Named the inaugural Tang Family Assistant Professor, Janurary 2021. |
Columbia University’s Final Nominee for the Packard Fellowship, March 2020. |
SOSP Best Paper Award, October 2019. |
Communications of the ACM (CACM) Research Highlights, October 2019. |
Distinguished Dissertation Award, Yale University, December 2016. |
Program Committees
PLDI 2022 | ASPLOS 2022 ERC | POPL 2022 | OSDI 2021 | PLDI 2020 |
SecDev 2020 | NSDI 2019 | SoCC 2019 | SecDev 2019 | CoqPL 2019 |
PLDI 2018 ERC | SecDev 2018 | ICFP 2018 SRC |
Students
- PhD: Runzhou Tao, Jianan Yao, Xupeng Li, Xuheng Li, Raphael Sofaer, Kele Huang, and Fanqi Yu. .
- Student collaborators: Shih-Wei Li, John Hui, Yunong Shi (UChicago), Gabriel Ryan, Mengqi Liu (Yale), and Xinhao Yuan.
- BS: Justin Wong, River Dillon Keefer, Jerry Lin, and Amanda Liu.
Teaching
- COMS 4115 Programming Languages and Translators (Fall 2022).
- COMS 4115 Programming Languages and Translators (Spring 2022).
- COMS E6998 Formal Verification of System Software (Fall 2021).
- Blockchain Cyberdefense Design Challenge (Summer 2021).
- COMS E6998 Formal Verification of System Software (Fall 2020).
- COMS 4115 Programming Languages and Translators (Spring 2020).
- COMS E6998 Formal Verification of System Software (Fall 2019).
- COMS 4115 Programming Languages and Translators (Spring 2019).
- COMS E6998 Formal Verification of System Software (Fall 2018).
- COMS W3101 Programming Languages (Spring 2018).
- Graduate Seminar on Systems.

Office
515 CSB, Columbia University
Phone
+1 (212) 939-7111
CertiKOS Video (for CACM)
CertiKOS Layers (for fun)
