形式化验证formal verification

形式化验证通过逻辑和证明来确认硬件或软件是否满足用数学定义的规格说明。与只检验部分输入的测试不同，它力求证明某项性质在规格说明涵盖的所有情况下都成立。常见技术包括模型检测和定理证明。

这一技术长期用于芯片设计、航空航天、操作系统内核和密码学等出错代价高昂的领域。在AI领域，它被用来以机器方式检验模型生成的代码和数学证明。

本条目依据AIPOST的文章与广为人知的事实整理。如有错误，请通过更正请求告诉我们。