About Me
I’m John Zhengyang Lü (吕正旸), a PhD candidate at the University of Waterloo. I have worked as a research intern at Google and Japan’s National Institute of Informatics (NII). I work on formal verification of AI systems and learning-guided automated reasoning.
Research theme 01
Verify AI
Formal methods for trustworthy AI systems.
Verify KV Cache Management and Transfer @ Google Cloud
Formally verify TPU Sync, a library for TPU KV cache management and data transfers, using Lean 4. Build a Lean-model-based agent to assist internal development and maintenance.
Verify RISC-V AI Accelerators @ Google Research
Build an automated formal verification pipeline for RISC-V AI accelerators such as Google’s Coral NPU.
Research theme 02
Learn to Reason
Learning-guided automated reasoning and formal verification.
Learning-Guided SMT Solver @ UWaterloo
Z3-alpha uses reinforcement learning and multimodal learning to optimize SMT solver heuristics. It won multiple divisions at SMT-COMP in 2024, 2025, and 2026.
Paper [IJCAI’24] · Paper [Acta Informatica’25] · Paper [CP’26] · GitHub
Learning for Hardware Model Checking @ Google Summer of Code
Btor2-Select uses graph learning to guide hardware model checking. It won two bronze medals at HWMCC 2025.