The CakeML project has grown from its beginnings as a formally verified compiler for an ML-like language to a full ecosystem today capable of producing various end-to-end verified applications.

This talk will start with an introduction to CakeML, including its compiler’s novel verified bootstrapping process. Then, I will outline how the CakeML ecosystem can be used to build verified proof checking tools that are capable of efficiently scrutinizing the outputs of automated reasoning solvers. By developing these checkers in close collaboration with tool developers, CakeML can provide practical proof checking for various automated reasoning theories with a remarkably small and shared trusted base.