I am a third-year PhD student at CMU, advised by Aayush Jain and Riad Wahby. Before that, I got my MA in Math at the University of Michigan, where I worked with Paul Grubbs.

Research Interests: I work at the intersection of cryptography and formal verification. My goal is to build new verification tools for advanced cryptographic primitives, such as succinct zero-knowledge proofs (SNARKs), and to use these tools to verify the security of existing constructions. I also work on post-quantum cryptography, with a focus on building new primitives from code-based assumptions.

Projects: I am the creator of ZKLib, a Lean library for formally verifying SNARKs. I also work on VCV-io, a Lean framework for reasoning about cryptographic protocols, which ZKLib is built on top of.

My research is generously supported by the Quad Fellowship, the CyLab Presidential Fellowship, and funding from the Ethereum Foundation.

Quang Dao

qvd@andrew.cmu.edu

Carnegie Mellon University
Pittsburgh, PA

Google Scholar
Twitter
LinkedIn

Preprints

Publications

(* = first author(s). The rest are alphabetical order)

Miscellaneous