The theory of minimal explanations offers a rigorous, model-based solution to the problem of producing explanations for the decisions of AI models. In some high-stakes contexts, there is a need to generate all possible explanations for a particular decision using certified programs, whose output can be trusted. We used the proof assistant Coq to certify a recently proposed algorithm for the enumeration of explanations in the case of monotonic classifiers. Our experimental results on the extracted code showcase the scalability of this approach, underscoring its potential for improving trust and reliability in AI systems.