Framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning models using Lean 4.