This talk will introduce the CakeML project and some of the major milestones we have achieved since our last appearance at the ML Workshop in 2014. These include a new optimizing compiler backend, new language frontends, new tools for program verification, and new verified applications. I will give particular focus to recent applications of CakeML in verified proof checking. Here, CakeML-based tools offer state-of-the-art, end-to-end verified correctness guarantees for the automated reasoning community. Conversely, building verified proof checkers has highlighted pain points in CakeML’s tooling and workflows for end-to-end verified software, which we are working to address in ongoing work.