区块链国际周

以太坊开发者大会DEVCON2第二天继续迎来了多次技术高潮，现场更像是粉丝见面会。会上，来自英国的区块链金融算法初创公司Imandra推出了其针对以太坊运行的智能合约形式化验证平台，在系统和算法越来越复杂之际，通过它可利用互动验证等工具进行金融交易验证。

Imandra创始人 Dr.Grant Passmore介绍：“之所以研究形式化验证，主要是因为目前行业内发生了一些事情表明，我们还需要在根本上建立稳健的风险控制工具，比如说投行，他们可能有很大的风险漏洞，他们投资了以太仿，以防止未来其数十万个投资组合暴露在风险当中。”

Imandra是金融算法公司Aesthetic Integration旗下的项目，在去年的Devcon1之后，Imandra取得了多个不错的成绩：在620家区块链公司的竞争中，获得了瑞银集团（UBS）“未来金融全球挑战”的第一名；今年8月获得谷歌支撑的种子基金融资。Imandra主要基于区块链研发针对金融股票交易的算法，比如黑池和其他用于不同交易体系之间的验证的算法，能够自动检测交易的风险。该公司联合创始人Denis是一名博士后，曾是银行风险交易负责人，也负责该公司算法的安全性。

为什么要运用形式化验证呢？Grant Passmore博士表示，“ 形式化验证使用自动的数学模拟技术来保证系统的参数一致性，然后利用同样的技术来检测实际生产系统是否一致。这样的技术已经被应用于安全性需求极高的行业，比如金融和航空。”

智能合约用以太仿的字节码来表示，Imandra可以证明智能合约的性能规范。Passmore介绍说，Imandra智能合约有两个层面的算法分析——第一是高级策略层，用来确保高层合约规范和设计的一致性。在合约运行之前，它会被转换成低层级的字节码。“第二层级的分析属于字节码层，用来分析区块链中实际被执行的字节码。”

“Imandra技术方面的最新突破在于，加入了约束变成语言SMT，把技术和数学的理论结合在一起，此外还包括线性和非线性程序等等，以及基于模型自动化的推导，因为有时候逻辑可能表示为递归，所以我们就必须要采用写推导的不变式等等来表示。这对于形式化验证都是非常重要的。”

Passmore表示，在DAO惨败之前，区块链社区一直以创建网页app的心态来创建智能合约，所以我们见到了DAO那样的灾难性损失。这一事件给我们的启示是，创建智能合约时应该抱着严格的软件工程意识，以建立关键性安全控制算法的心态来设计。