DEVCON2: Imandra合约：以太坊形式化验证

记者：Lydia

Dr. Grant Passmore对一个关于Aesthetic Integration出品的以太坊云形式化验证系统，Imandra合约的展示。

Dr. Grant Passmore：

我必须说下这对形式化工程师来说这是一个梦想，我们都花了很大精力在这个领域。

云上的智能合约平台是形式化验证的引擎，以太坊虚拟机在Imandra上形式化，指令放在EVM指令集上，符号执行自动化证明算法可以用来支持合约。

我们的公司研究金融算法和不同交易体系之间的联系，以及和不同参与者合作验证算法。我们获得了UBS未来金融全球挑战的第一名，这个挑战有652家公司参与。

这个夏天之前，在世界上第一个黑池算法之前，最近完成c轮融资，谷歌给我们提供资金。我的合伙人Dennis之前是德意志银行的负责人，我主要负责LInux程序算法，我们的目的是实现复杂算法的安全性。我们研究形式化验证是因为社区发生一些事情，我们需要自动化审计工具，我们还需要在根本上建立稳健的工具，投行投资以太坊，未来有50个智能合约，他们用的都是以太坊自解码。在形式化EVM都是围绕风险管理。

Imandra用硬件证明工具和数学理论结合在一起，如线性和非线性理论。有时候逻辑表现为递归，有时需要采用推倒的不变性，或用重写的规则，现在有更强大的工具可以实现。

对Imandra来说，实现技能民主化。根本上，Imandra智能合约用以太坊智能合约表示，Imandra可以证明合约的性能。

Imandra是一个编程语言，也是一个推论，设计时是一个梦想的验证工具，这样我们才可以进行计算。

接下来是演示：

EVM形式化，就像写一个模拟器一样，所有内存指令如何在状态内运行，知道用完所有的汽油，我们已经发布了EVM模型，希望我的社区可以将其导入不同的系统中。

现在以太坊是一个非常低级的界面，但是我夹在了Imandra的自解码，所有一切都会反映在数学中。

让解释器运行自解码，用符号的执行告诉我可能的行为，我们的自解码有非常简单的名字注册，如果还有汽油可以升级存储到其他的行为。

以太坊关于自解码执行的声明，这是名字注册表的规范，证明自解码的意义，什么时候证明算法会失败。

这是一个高级的语言，是I的子集，可以编辑到EVM，现在在证明其正确性，希望今年年底能完成。

这是一个有效定价的函数，只有170种可能行为，我们有树的表示，不同行为如何映射到状态中。

大家可以登录我们的网站，每周都会邀请一些人加入Imandra，希望大家加入我们。我们已经加入了栈，也有用于审计的智能合约。

作者：Lydia | 来源：Chainb