Don’t Test, Verify：哪个故事真正符合你对形式化验证的想象？

[billy.ryoko]

从诞生至今，形式化验证（Formal Verification）方法一直与“小众、冷门”等字眼挂钩。有人说形式化验证方法是一种“军用级别”的防黑客手段，更是为这项技术增添了一丝神秘感。

究竟什么是形式化验证方法？

维基百科对形式化验证的解释是这样的：

在计算机硬件（特别是集成电路）和软件系统的设计过程中，形式化验证的含义是根据某个或某些形式化规范或属性，使用数学的方法证明其正确性或非正确性。

神秘感大抵来源于定义中的两个严谨而且抽象的关键词——“形式化规范”和“数学方法证明”。事实上，揭开这层神秘的面纱，你会发现形式化验证的许多有趣之处。

下面这篇文章想要讨论的问题是：在现阶段，以下哪个故事能够真正满足你对形式化验证的想象？形式化验证真的可以作为一种技术在区块链领域流行起来吗？如果可以，怎样才能做到？

（PS：上文中提到的“形式化规范”的概念，在下文中也会讲到。）

要回答上面这些问题，我们可以先思考另一个更简单的问题：
现阶段，人们使用形式化方法来做什么？
这个问题的答案无非有两种：
1、 规避错误
2、 对抗攻击

| 规避错误
规避错误其实就是避免损失。

我们首先来探讨一下，哪些领域对程序错误是零容忍的？在哪些领域，程序错误带来的损失难以估量？

实际上，形式化方法是从硬件设计开始普及的。一个著名的例子是：当年Intel的Pentium CPU浮点运算单元出错(FDIV Bug)，数以万计的CPU不得不回收和替换，给Intel造成了巨大损失(475M $)[1]。

从那之后，Intel开始在其芯片设计中广泛采用形式化方法。

计算机硬件巨头如IBM，AMD， NVIDIA 和 CADENCE[2]等等也都是形式化方法的使用者…

要说起吃一堑才能长一智，其实各行各业都有试错者，在工业界也是如此。举个例子：1996年，欧洲航天局首次发射的阿丽亚娜5型（Ariane 5）火箭，由于惯性导航系统发送的错误指令（浮点数转换为整数造成溢出），导致火箭在发射仅仅37秒后便偏离了预定轨道，最终坠毁。欧洲航天局的巨额研发经费（8B $）[3]付之一炬。

在那之后不久，EADS公司开发阿丽亚娜火箭的任务调度模型就开始使用形式化方法。

美国国家宇航局NASA和英国国防部在90年代相继发布设计标准[4]，形式化方法的使用位列其中。我国的玉兔号月球车控制系统和我国第一个自主研发的空间飞行器嵌入式实时操作系统SpaceOS[5]，也都是通过形式化方法验证其正确性。

历史的发展告诉我们，金钱才是推动社会发展的第一动力！程序错误带来的巨额损失，任谁也只能叹一声伤不起。

http://m.8btc.com/which-story-do-u-prefer