Interpretable models are a key aspect of explainable machine learning. A model can be considered to be interpretable if for each decision there is an explanation involving only k features, for some small constant k. For boolean functions \(\kappa \) this means that both \(\kappa \) and its complement \(\overline{\kappa }\) are expressible as k-DNFs. Nested k-DNFs are one such family of interpretable models. We show how to find such models and provide software, based on a formally-verified SAT encoding, to do so. We report experiments indicating that nested DNFs are an interpretable alternative to random forests while retaining the same accuracy.