Youwei Zhong

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

Currently, I'm fortunate to be advised by Prof. Qinxiang Cao. We are working in the formal verification of zero-knowledge virtual machines, using the Coq proof assistant, with a long abstract to appear at OOPSLA'24 SRC and a paper in submission to IEEE S&P 2025.

I'm currently applying for a Ph.D. position starting in the fall of 2025! If you are interested in recruiting me, please feel free to contact me!

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

9854 DF14 ED06 789C

CV  /  Twitter  /  Github

profile photo

Research

I'm currently interested in Formal Verification and Zero-Knowledge Proof. Specifically, I enjoy constructing significant prototypes in code which also have theoretical values. I'd also like to explore fields like Functional Programming, compilers, Program Synthesis, Program Analysis, and other areas related to Programming Languages.

Publication

A Parameterized Framework for the Formal Verification of Zero-Knowledge Virtual Machines
Youwei Zhong
To appear at SPLASH/OOPSLA 2024 SRC

This long abstract introduces 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 Framework for the Formal Verification of Zero-Knowledge Virtual Machines
Youwei Zhong, Zihan Xu, Yuncong Hu, Xiang Xie, Yu Yu, Qinxiang Cao

This paper is an extension work based on my long abstract with the same name, which is accepted by SPLASH 2024 SRC.

Awards and Honors

  • 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
  • Three Good Student of Shanghai Jiao Tong University (one person per class per year), 2022, 2023

Last updated on 2024-09-07.
The source code of this website is modified from Jon Barron's personal website.