Zhong Shao is the Thomas L. Kempner Professor of Computer Science at Yale University. He currently leads the FLINT group, which aims to develop new languages and tools for building large-scale certified system software. He earned his PhD in Computer Science from Princeton University in 1994. During the last 30 years, Shao and his team at Yale have led and pioneered work on language-based approaches to safety and security, formal verification of consensus protocols and distributed systems, certified OS kernels and hypervisors, compositional certified compilation, and formal methods. He was also a PI on the DARPA CRASH CertiKOS Project (2010-2014), the DARPA HACMS CARS Project (2012-2017), and NSF's Expeditions-in-Computing project on the Science of Deep Specification (2015-2021). Shao's work on CertiKOS is widely considered a breakthrough toward building hacker-resistant operating systems that are provably free from cyber vulnerabilities. Shao is also co-founder of the blockchain security startup CertiK, which aims to secure the web3 world by developing a formal verification platform for next-generation smart contracts and blockchain ecosystems.