Machine learning models are increasingly being incorporated into real-world systems, targeting domains such as robotics, healthcare, and software systems. A key challenge is ensuring that such systems are trustworthy. I will describe a novel strategy for composing machine learning models while providing provable correctness guarantees. First, we show how to quantify the uncertainty of any given model in a way that satisfies PAC correctness guarantees. Second, we show how to compose guarantees for individual models to obtain a guarantee for the overall system. Then, I will discuss applications to ensuring safety in reinforcement learning from visual inputs, and to speeding up inference time of deep neural networks. I will conclude with ongoing work on preserving correctness guarantees in the face of distribution shift.