检查程序是否工作正常的传统方式是跑测试。程序员们会给程序大量输入（或单元测试），以确保它符合设计要求。如果你的程序是给无人驾驶汽车规划路径的算法，你也许会用多个不同的位置点来测试它。这一基于测试的方法能得到运行正确的软件，但只是在大多数时候针对大多数应用而言。不过，单元测试并不能确保软件永远运行正确，因为没有办法用所有可能的输入来测试程序。即便程序能通过每一个测试，也不能排除它在一些极端情况下运行不正常，进而形成漏洞。在实际的程序中，这种漏洞也许会简单到只是一个缓冲溢出错误，即程序拷贝多了一丁点数据，并覆盖了某一小块计算机内存。这个看起来无害的错误很难彻底根除，是黑客们攻入计算机系统的捷径。

　　Bryan Parno 说道：“只要程序中有一个缺陷，就能成为安全弱点。很难测试所有可能输入的所有路径。”

　　实际的形式规范要比自动驾驶去百货商店细致得多。比如编写一个确认收到文件，并按收到时间对文件进行排序的程序，形式规范需要规定计数器永远只能增长（好让后面接收的文件序号总比前面收到的文件高），以及程序永远也不会泄露给文件签名的密钥。

　　这么说着容易，真正要用形式语言来编写一个计算机能应用的规范却很难，更何况还是要在整个软件编写过程中都这么做。

　　Bryan Parno 表示：“写出机器能识别的形式规范或目标非常考验智商。站在高处说‘不要泄露密码’很容易，真正要把它用数学定义的形式写出来却需要很多思考。”

　　再比如，atv，给列表或数字排序的程序，程序员可能会这么给它写形式规范：

　　For every item j in a list, ensure that the element j ≤ j+1

　　（对于列表中的每一项 j，确保 j ≤ j+1）

　　然而这个形式规范却有一个漏洞：这个程序员默认输出会是输入的排序结果，即假设列表为 [7, 3, 5]，这个程序应该返回 [3, 5, 7]，这样就满足了定义。但列表 [1, 2] 也满足定义，因为“这是一个排序好了的列表，只不过可能不是我们希望的那种排序好了的列表。”

　　换言之，要把你想要让程序做的事，用排除了所有可能不正确解释的形式规范表示出来很难。上面的例子还只是一个简单的排序程序，想象一个更抽象的例子，比如保护密码。Bryan Parno 说道：“这在数学上是什么意思？定义它也许要写出保护密码的数学描述。安全的加密算法又是什么意思呢？这也是我们一直在研究中一直在思考并取得进展的问题，但要正确应用必须非常小心。”

　　基于代码块的安全

　　编写这种程序需要同时编写形式规范以及帮助编程软件推导代码所必须的额外注释， 因此其长度达到了传统程序的五倍。

　　用合适的工具可以在一定程度上减轻这一负担，比如专门的编程语言和辅助证明程序。但这些东西在上世纪 70 年代时还不存在。同时担任形式验证计算机系统开发团体 DeepSpec 首席研究员的 Andrew Appel 表示：“当时的很多技术都不成熟，因此到 80 年代，很多人就对它失去了兴趣。”

　　即便工具得到了改进，atv，形式验证计算机程序还有另一个问题要解决：没人确定是否有必要用它。虽然形式方法爱好者们总是在说小的程序错误最后会变成灾难性漏洞，但大家看到的却是计算机程序工作得相当好。

　　的确，这些计算机程序有时候会崩溃，但和巨细无遗地一条条用形式逻辑系统的语言来编写程序相比，丢失未保存的数据或时不时重启机器貌似也可以接受。有时候，连形式规范最早期的领导者也会怀疑其是否有用。在上世纪 90 年代，霍尔逻辑(Hoare logic，首批推导计算机程序正确性的形式系统之一)的发明者 Hoare 就承认，也许形式规范是一个不存在的问题的劳动密集性解决方案。他在 1995 年写道：

　　十年前，形式方法的研究者们（我是其中错得最厉害的一个）预测，计算机世界会拥抱并感激形式化带来的每一点协助……结果是，全世界并没有碰到我们一开始打算解决的那种问题。

　　后来出现了互联网。 互联网之于编程错误就像是飞机之于传染病：当所有电脑都连接在一起时，不方便但可以忍受的软件漏洞会导致一系列安全问题。