Youwei Zhong

I am a senior undergraduate of John Hopcroft Class (John Class) at Zhiyuan College, Shanghai Jiao Tong University.

Currently, I'm a visiting student at Yale University. I'm fortunate to work with Prof. Ruzica Piskac and Research Scientist Timos Antonopoulos at Yale, and Prof. Ning Luo at UIUC.

Previously, I was fortunate to be advised by Prof. Yu Feng and Dr. Yanju Chen, and collaborate with Prof. Ranjit Jhala in developing bug finders for zero-knowledge virtual machines using the Flux refinement type checker. I also developed an analyzer for Circom, a domain specific language for zero-knowledge circuits.

Before that, I was fortunate to be advised by Prof. Qinxiang Cao and Prof. Yuncong Hu. We worked on formal verification of zero-knowledge virtual machines, using the Coq proof assistant, with a paper accepted by OOPSLA'24 SRC and another paper in submission to Asiacrypt'25.

🌟 I will be a Ph.D. student at Yale University starting in the fall of 2025!

🎉 News: I recently won the 2nd place in the OOPSLA 2024 SRC!

You can reach me by youwei[AT]ywzh[DOT]org

9854 DF14 ED06 789C

CV  /  X (Twitter)  /  Github

profile photo

Research

I'm currently interested in Formal Verification and Zero-Knowledge Proof. I'd also like to explore fields like Program Analysis, compilers, Program Synthesis, Functional Programming, and other areas related to Programming Languages.
I believe applying methods in logic, verification, and programming languages to cryptography, computer systems, software engineering and artificial intelligence can lead to breakthrough contributions and change the world.

Publication

A Parameterized Framework for the Formal Verification of Zero-Knowledge Virtual Machines
Youwei Zhong
OOPSLA 2024
Poster PPT

🥈 The 2nd Place Winner in the Student Research Competition

This paper first proposed a parameterized framework for the formal verification of zkVMs in Coq. We prove the soundness and completeness of the constraint generation algorithm from machine instructions to semantics-level constraints. Existing works target specific zkVMs, and require repeated proof work in this phase, whereas our proofs are parameterized and can be reused in development and by all zkVMs. We also demonstrate the generality of our framework by instantiation on two examples: Cairo VM and a simplified zkEVM.

Manuscript

A Parameterized Verification Framework for the Constraint Generation Algorithms in Zero-Knowledge Virtual Machines
Youwei Zhong, Zihan Xu, Yuncong Hu, Xiang Xie, Yu Yu, Qinxiang Cao
In submission to Asiacrypt'25

This paper is an extension work based on my OOPSLA'24 SRC paper.
We formalize the cryptographic security properties of zkVMs in the Coq proof assistant, including soundness, completeness, knowledge soundness, and zero-knowledge, by formalizing probabilistic programs using monads.

Awards and Honors

    🥈 The 2nd Place Winner in OOPSLA 2024 SRC (300 USD)
    🏆 Longfor Scholarship (10’000 yuan, 10 winners each year, Zhiyuan College), 2022
    🏆 Zhiyuan Honorary Scholarship (5’000 yuan per year, Top 5%, Shanghai Jiao Tong University), 2021, 2022, 2023, 2024
    🏆 Three Good Student of Shanghai Jiao Tong University (one person per class per year), 2022, 2023, 2024
    🥇 A-class Academic Excellence Scholarship, Shanghai Jiao Tong University, 2024

Last updated on 2025-5-19.
The source code of this website is modified from Jon Barron's personal website.