The CakeML project has built an ecosystem of proofs and tools around an ML dialect called CakeML. The ecosystem includes a proven-correct compiler that can bootstrap itself within the logic of an interactive theorem prover (HOL4). In this talk, I will give an overview of the entire ecosystem; I will show how HOL4 provides an architecture that scales to such large developments; and I will explain where and how the CakeML project uses proof automation. The talk will conclude with a discuss of where I believe CakeML would gain most from improved proof automation. For more: https://cakeml.org/