本篇文章997字，读完约2分钟
第二天，以太博物馆的开发者大会Devcon2继续迎来许多技术高潮，这个场景更像是一个粉丝会议。会上，来自英国的区块链金融算法的初创公司imandra推出了其在以太网运行的智能合同正式验证平台。随着系统和算法变得越来越复杂，它可以使用交互式验证和其他工具来验证金融交易。
imandra的创始人格兰特·帕斯莫尔博士说:“之所以研究正式验证，主要是因为目前这个行业已经发生了一些事情，这表明我们仍然需要从根本上建立稳健的风险控制工具，比如投资银行，它们可能有很大的风险。漏洞，他们在Ethereum进行投资，以防止数十万个投资组合在未来面临风险。”
Imandra是金融算法公司美学整合下的一个项目。经过去年的发展，imandra取得了许多好成绩:在620家区块链公司的竞争中，它赢得了瑞银集团的“未来金融全球挑战”。第一名；今年8月，他获得了谷歌支持的种子基金融资。Imandra主要开发基于区块链的金融股票交易算法，如Blackpool等用于不同交易系统间验证的算法，可以自动检测交易风险。该公司的联合创始人丹尼斯是一名博士后研究员。他曾是银行风险交易的负责人，也负责公司算法的安全性。
为什么使用正式验证？格兰特·帕斯莫尔博士告诉雷锋。搜索雷锋的公开号码。com)，“形式验证使用自动数学模拟技术来确保系统参数的一致性，然后使用相同的技术来检测实际生产系统是否一致。这种技术已经应用于安全要求极高的行业，如空.金融和航空业"
智能合同用过于模仿的字节码来表示，imandra可以证明智能合同的性能规格。帕斯莫尔说，imandra smart contract中有两个层次的算法分析——第一个是高层策略层，用于确保高层合约规范和设计的一致性。在契约运行之前，它将被转换成低级字节码。“第二层分析属于字节码层，用于分析在区块链实际执行的字节码。”
“imandra技术的最新突破在于添加了约束语言smt，它结合了技术和数学理论，还包括线性和非线性程序等。以及基于模型自动化的演绎。因为有时逻辑可能被表达为递归，我们必须使用写演绎等不变量。这对于正式验证非常重要。”
帕斯莫尔说，在道遭遇惨败之前，区块链社区总是抱着创建网络应用的心态来创建智能合同，所以我们看到了像道这样的灾难性损失。这一事件的启示是，在创建智能合同时，我们应该具有严格的软件工程意识，并以建立关键安全控制算法的思路进行设计。
