Bohua Zhan is a technical expert at Huawei Programming Language Lab. He earned his Ph.D. in mathematics from Princeton University in 2014 and later held postdoctoral positions at MIT and the Technical University of Munich. His research covers automated reasoning, interactive theorem provers, embedded-system modeling and verification, and applications in operating systems, distributed systems, and quantum programs.