对话Web3安全超级独角兽CertiK：「誉满天下，谤满天下」(7)

03 从学术圈到 Web3 世界，技术实用主义与去中心化信仰
极客公园：你最早接触区块链是什么时候？
顾荣辉：大概是 2012、2013 年。当时我刚从清华本科毕业，进入耶鲁大学计算机系「高可信软件联合研究中心」，跟着邵中教授（注：邵中为中科大－耶鲁高可信软件联合研究中心主任）读博。
当时跟我在同一个办公室的师兄叫蒋信予，他的化名叫「Friedcat 烤猫」（注：烤猫被称为「国内币圈第一人」）。我第一次对区块链产生兴趣，就是从他那知道的。
极客公园：烤猫在区块链世界非常有名，是国内比特币最早的布道者。
顾荣辉：他是比较早一批开始用 ASIC 机器去挖矿的，做矿机做的很成功，对整个区块链世界影响很大。最后他博士辍学，回国做了这个。
回过头来，为什么烤猫在区块链世界做的很成功，我觉得可能是一种科研的思维方式。我们会从一个更基础的层面考虑这些问题，所以大家会做出很多创新性的东西。
极客公园：当时你自己买币吗？
顾荣辉：当时没有买过。
极客公园：像烤猫这样一个偏原教旨主义的人，他对你有什么影响吗？
顾荣辉：我觉得他对我学术上影响大一点。因为他是我的师兄，在科研上他帮助我很多，包括形式化验证（formal verification）的很多知识。我们甚至在同一个项目 CertiKOS，但是他后来离开了。
极客公园：CertiKOS 也是你后来创业的重要技术基础。
顾荣辉：对。我们研究的形式化验证技术，简而言之就是通过数学方法，证明你的代码和你的设计是等价的，没有漏洞（bug）。
这项技术在软件（操作系统）上的应用一直是学术痛点。它过去一直被应用在硬件上，因为硬件是固定的，证明空间有限。但软件是可编程的，证明空间可以到无穷大。我在读博的时候，就想解决这个问题。
2016 年，我们终于完成了这个技术突破，做出了 CertiKOS。这是目前世界上第一个、也是唯一一个完全经过形式化验证的多核操作系统内核。当时我们把它用在了无人车 Landshark 上面，被评价为「无懈可击」。2018 年我们创立了 CertiK，希望把这项技术用于实际生产中。
极客公园：这项技术可以应用的领域有很多，为什么最终你选择应用到区块链或 Web3 领域？
顾荣辉：因为当年 Web3 发生了几起很大的安全事件。2016 年，The DAO attack，被认为几乎是人类历史上最大的一起攻击事件，超过几百万枚以太币被盗，换算到现在就是几十亿美金的损失。那时候区块链才刚刚开始火，这些攻击事件让大家意识到，Web3 安全非常非常重要。大家希望能改变区块链的安全状况。