Resume
Experience
Formal verification of TPU infrastructure and RISC-V AI accelerators.
Project Numina
Natural-language and Lean 4 mathematical datasets.
National Institute of Informatics, Japan
Reinforcement learning for probabilistic program verification.
Google Summer of Code / LMU Munich
Adaptive Algorithm Selection for Hardware Verification
Education
University of Waterloo
Electrical and Computer Engineering
University of Waterloo
Electrical and Computer Engineering
Tongji University
Selected honors and activities
- NSERC Canada Graduate Scholarship–Doctoral, 2025–2027.
- Z3-alpha: multiple division wins at SMT-COMP 2024, 2025, and 2026.
- Btor2-Select: two bronze medals at HWMCC 2025.
- Co-organizer, Machine Learning for Solvers tutorial, AAAI 2025.
See Publications for papers and Research for current projects.