形式验证

维基百科，自由的百科全书

在计算机硬件和软件系统中，形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。

[编辑] 解释

软件测试无法证明系统不存在缺陷，也不能证明它符合一定的属性。只有形式化验证过程可以证明一个系统不存在某个缺陷或符合某个或某些属性。系统无法被证明或测试为无缺陷，这是因为不可能形式的规定什么是「没有缺陷」。所有可以做的，就是证明一个系统没有任何可以想到的缺陷，并且满足所有的使系统符合功能要求的和有用的属性。