尽管机器学习（ML）和神经网络近年来取得了长足的进步，但对这些系统行为的正式保证仍然是一个悬而未决的问题，也是它们在受监管或安全关键场景中应用的关键要求。我们考虑训练可微分 ML 模型的任务，该模型保证满足设计者选择的属性，这些属性以输入-输出蕴涵的形式给出。由于严格验证和强制执行现代神经模型中的合规性的计算复杂性，这非常具有挑战性。我们提供了一种基于三个组成部分的创新方法：1) 一种通用、简单的架构，能够以保守的语义进行有效的验证；2) 基于投影梯度法的严格训练算法；3) 搜索强反例问题的公式化。所提出的框架几乎不受模型复杂性的影响，能够很好地扩展到实际应用中，并产生提供完整属性满足保证的模型。我们评估了在回归中由线性不等式定义的属性，以及在多标签分类中相互排斥的类别上的方法。我们的方法与基线方法相比具有竞争力，该基线方法包括在预处理（即在训练数据上）和后处理（即在模型预测上）期间执行属性强制。最后，我们的贡献建立了一个框架，打开了多个研究方向和潜在改进。