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.


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.



  • 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

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




515 CSB, Columbia University


+1 (212) 939-7111

CertiKOS Video (for CACM)

CertiKOS Layers (for fun)

Layout based on BASIC by Download Website Templates