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 co-founded CertiK, a blockchain cybersecurity startup. Press on CertiK: Forbes, CACM, Cointelegraph, Coindesk.


My Columbia lab is looking for Ph.D. students and Postdocs. Check out our recent S&P'21, CACM Research Highlights, SOSP'19 (Best Paper Award), PLDI'18, OSDI'16, and POPL'15 papers (and the press release) for an overview of our latest breakthrough on building trustworthy systems software.



  • Ph.D. in Computer Science, Yale University, December 2016
    • Advisor: Prof. Zhong Shao.
    • Thesis: An Extensible Architecture for Building Certified Sequential and Concurrent OS Kernels.
    • Distinguished Dissertation of Yale Graduate School of Art and Science.
  • B.S. in Computer Science, Tsinghua University, June 2011.
    • Rank: 4/140. Graduation with Highest Distinction (3 out of 140).


Select Publications

Select Awards

    Amazon Research Awards, 2021.
    Named the inaugural Tang Family Assistant Professor, 2021.
    Columbia University’s Final Nominee for the Packard Fellowship, 2020.
    SOSP Best Paper Award, 2019.
    Communications of the ACM (CACM) Research Highlights, 2019.
    MIT Technology Review 35 Innovators Under 35 Semi-Finalist, 2019.
    Distinguished Dissertation Award, Yale University, 2016.
    Yale Nominee, ACM Doctoral Dissertation Award, 2016.
    Robert Willets Carle Scholarship, Yale University, 2016.
    Graduation with Highest Distinction (3 out of 140), Tsinghua University, 2011.
    Outstanding Undergraduate of Beijing City, China, 2011.
    Honors Undergraduate Thesis Award (5 out of 140), Tsinghua University, 2011.

Program Committees

    POPL 2022 OSDI 2021 PLDI 2020 SecDev 2020 NSDI 2019 SoCC 2019
    SecDev 2019 CoqPL 2019 PLDI 2018 ERC SecDev 2018 ICFP 2018 SRC




515 CSB, Columbia University


+1 (212) 939-7111

CertiKOS Video (for CACM)

CertiKOS Layers (for fun)

Layout based on BASIC by Download Website Templates