Since the breakthrough of the world’s first formally verified OS kernel in 2009, seL4 has been extended with new features, ported to new platforms, embedded with high-assurance user-level software, demonstrated to protect against cyber attacks in unmanned helicopters, robot, autonomous trucks… In this talk we will give an overview of the latest achievements to make verified software a reality in real-world deployed systems and of the progress towards the remaining challenges to make verified software become mainstream.