Abstract: Despite the emergence of alternative languages, the C programming language continues to constitute an important vehicle for implementing industrial applications and occurs ubiquitously in operating systems, cryptographic libraries, and communication stacks. To comprehensively protect critical infrastructure, personal devices, or cloud computing centers from attacks on the operational functionality or the safety, security, and privacy of data and communication, it is hence necessary to develop rigorous analysis and verification technology for C that applies to existing as well as novel software. The Verified Software Toolchain (VST) enables users to verify functional correctness of C programs modularly, using the expressive power of a rich mathematical model and the foundational rigor of an interactive proof assistant. VST's guarantee includes memory safety and protocol-adherent resource usage, and thus substantially reduces the code's attack surface. The talk will motivate design principles and exemplary applications of VST, highlighting not only its connection to the provably correct Compcert compiler but also its ability to connect code verification to model-level reasoning.