“程序测试能证明错误的存在,但不能证明错误不存在”。Edsger Dijkstra（1972年图灵奖获得者、形式化方法核心思想的提出者）如此评述。

在实践中，尤其是在代码足够复杂的场景中，形式化验证（Verification）与程序测试方法（Testing） 的验证效果有如云泥之别。

举个例子来说：2009年，澳大利亚的科学家使用形式化方法对工业级操作系统seL4微内核进行了完整功能性验证，验证方式同时以形式化验证和程序测试两种方式分别展开，验证的结果是：形式化方法共发现460多个Bug，而程序测试只发现了16个Bug。更有趣的是，在以高验证成本著称的形式化验证领域，完全验证seL4微内核只需要600万美元的验证成本，而以测试的方式通过CC EAL6级认证的成本竟高达8700万美元。

由此可见，通过形式化验证可以更经济的为seL4微内核提供更强的安全性保证。