I am an Associate 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 startup valued at $2 billion. Press on CertiK: The Wall Street Jounrnal, CNBC, Bloomberg, Forbes, TechCrunch.


My Columbia lab is looking for Ph.D. students. Check out our recent OSDI'23, OSDI'22, and CACM Research Highlights for an overview of our latest breakthrough on building verified systems software.



  • Ph.D. in Computer Science, Yale University, December 2016
    • 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

Program Committees

    SOSP 2024 PLDI 2024 EuroSys 2024 ASPLOS 2024 APLAS 2023
    PLDI 2022 POPL 2022 OSDI 2021 PLDI 2020 SecDev 2020
    NSDI 2019 SoCC 2019 SecDev 2019 CoqPL 2019 SecDev 2018

Selected Awards

    VMware Systems Research Award, 2023.01.
    NSF CAREER Award, 2023.01.
    Builders and Innovators, Goldman Sachs, 2022.05.
    Amazon Research Awards, 2022.04.
    Amazon Research Awards (co-PI), 2021.07.
    OSDI Jay Lepreau Best Paper Award, 2021.07.
    The Top 100 Yale Alumni In Technology Of 2021, 2021.06.
    Amazon Research Awards, 2021.04.
    Named the inaugural Tang Family Assistant Professor, 2021.01.
    Columbia University’s Final Nominee for the Packard Fellowship, 2020.03.
    SOSP Best Paper Award, 2019.10.
    Communications of the ACM (CACM) Research Highlights, 2019.10.
    Distinguished Dissertation Award, Yale University, 2016.12.




515 CSB, Columbia University


+1 (212) 939-7111

MIT Technology Review

CertiKOS Video (for CACM)

CertiKOS Layers (for fun)

Layout based on BASIC by Download Website Templates