暴走时评：本月在上海召开的以太坊开发者大会上（Devcon2），形式化验证成为社区的热门话题，引起极大关注和热烈讨论。作为solidity语言的补充，它有强化区块链智能合约安全性的潜力，可以防止The DAO类似事件的发生。然而目前还有一些技术难题需要攻克，也不是所有症结的万能灵药，但是它的潜力已经得到开发者社区的高度认可。
翻译：Annie_Xu
最近区块链领域出现新热词——形式化验证。
这个短语指的是用数学算法验证软件程序，频频出现在媒体报道中。但是上周在上海的区块链峰会给了我们一些提示，目前智能合约和区块链都存在安全问题，因此形式化验证的重要性应该会越来越大。
以太坊开发者大会Devcon2的多个相关会议表明，开发者社区显然是欢迎这个可以帮助以太坊编码员的新程序。这个概念已经增加了人们对以太坊协议和权益证明区块链项目的信心。
The DAO是目前为止在去中心化应用开发平台上最大的智能合约项目，它的突然崩溃显然解释了这个概念为何能获得关注。
尽管形式化验证看似复杂，可以简单理解为以太坊中的应用。编码员现在基本用solidity语言编写智能合约，然后编译为字节码，用于以太坊虚拟机(EVM)，分布到网络的节点，并执行代码程序。
形式化验证可以看作保证不同网络元件接收到指令的客观方式，然后以用户的身份按预定程序执行。
Aesthetic Integration创始人Grant Passmore看到促成这个技术的机会，在Devcon2上发布了Imandra Contracts——区块链和智能合约的形式化验证平台。
Grant Passmore
他在会议上提出，鉴于社区的目标以及对代码寄予的重大责任，以太坊可以作为形式化验证的“天堂”。
“以太坊社区很独特，The DAO事件之后，我们发现了强大计算机工程的必要性。不可能让智能合约看起来像一个网页应用”。
另外演讲者Cornell's Philip Daian更加广泛地讨论了这种方法论，表示他相信形式化验证可以帮助以太坊解决主要问题。
“这将成为重要的组成部分，我很期待通过以太坊制定标准，并分享这个经验”。
辅助轮
最近金融公司一直在强调智能合约语言，因此整合Solidity语言和形式化验证成为最近最热门的话题。
Solidity是为以太坊平台开发的，由于该语言未经测试，编写难度高，所以受到很多批评。之后由于该语言编译器缺少代码库以及The DAO系统崩溃，这些问题被放大了。
因此Solidity创始人Christian Reitweissner承认，应该用形式化验证帮助以太坊编码员更有效地发现漏洞。
他说，将来智能合约开发者可以用形式化验证确定他们的工作中是否有漏洞。还可以用这个工具判定，两个平均值相加的结果是否优于编译器分配的结果。
“这有发生的可能性，而形式化验证可以自动发现。你可以很早发现并对智能合约做出调整”。
Reitweissner说Solidity团队已经在探索怎样整合形式化验证。去年十月已经开发出原型，研究Why3工具包如何帮助实现这个目标，尽管该产品还没有对全部Solidity公开。
试验场
峰会上还重点讨论了怎样用以太坊探索如何把形式化验证应用于金融业。
Passmore说2014年开始就和金融机构合作探索该系统整合方法。客户已经开始一些应用，比如公平性受到交易员诟病的黑池。
Passmore说，以太坊社区可以推动智能合约的应用。
“刚与银行客户合作时，很多客户都对该领域表现出极大的兴趣，但是我们担心智能合约的正确性”。
形式化验证的发展还吸引了Yoichi Hirai，他是目前就职于以太坊基金会（Ethereum Foundation）的形式化验证工程师；早在还是研究员，就职于网络安全领导企业FireEye时，就已经对该技术感兴趣。
Hirai在会上说，在没有源代码或者任务过于复杂的情况下，他无法采用形式化验证。
“我发现以太坊、以太坊虚拟机、黄皮书中只有32页的介绍，我认为我可以翻译出来，并编写智能合约的证明”。
而以太坊可以提供他所说的“较小规格”和“可解决的问题”，让开发者决定如何有效地把Solidity编译成字节码。
“我相信会有更多形式化验证研究员”。
不是灵丹妙药
然而尽管这个概念引起极大关注，目前必须谨慎关注形式化验证会以哪些形式出现。开发者Alex Beregszaszi正致力于升级EVM，他说目前正在探索帮助开发者保证智能合约代码功能的解决方案。
Passmore也指出，目前无法确定新系统是否发现了The DAO的问题，因为形式化验证工具还需要人工输入。
“你可以将The DAO事件进行编码，然后检查相关漏洞；但是首先你得知道注意事项有哪些”。
Reitweissner和Passmore都认可这个限制性的存在，并警告开发者不要把形式化验证看作灵丹妙药。
然而Reitweissner认为随着应用推广，这个方法论会继续发展，开发者也会逐渐学会更好地发现问题并开发相应的代码库，记录必要的常见问题。
Passmore相信这样，以太坊社区才可以成功推广该概念，而且它最终会推动区块链研发。
“尽管很多人都还不熟悉它，可是我们需要它。我们还在学习，但是我们必须拥抱它，这非常让人激动”。
声明：此文出于传递更多信息之目的，并不意味着赞同其观点或证实其描述。本网站所提供的信息，只供参考之用。
