My research aims to build trustworthy AI systems that can be safely and reliably used in mission-critical tasks, with a focus of using formal verification techniques to give provable worst-case performance guarantees. I proposed and advanced a novel bound-propagation-based verification framework for deep neural networks that enables formal verification for networks with millions of neurons. I am leading the development of the α,β-CROWN neural network verifier, which won VNN-COMP 2022 and VNN-COMP 2021. In addition, I studied the security and safety of AI models, especially their adversarial robustness. I am a receipient of IBM PhD Fellowship and Schmidt Futures AI2050 Early Career Fellowship.