Opportunity: Develop model wrappers that endow black-box models (i.e. deep networks) with formally verifiable explanations

Challenge: Diverse range of properties to guarantee for model explanations, ensuring computational efficiency and high performance