I am a PhD researcher at Yale University studying formal verification of distributed algorithms, advised by Prof. Zhong Shao. I lead efforts to verify both safety and liveness of distributed consensus protocols deployed in the blockchain industry, including HotStuff, Jolteon, Bullshark, and Mysticeti, using the Coq Proof Assistant. Our techniques can also be applied to more conventional consensus algorithms including Multi-Paxos and Raft that are widely-adopted in the industry. See my publications for details.