Vitalik 预测智能合约的未来将无漏洞

来源：CryptoNewsNet 原始标题：Vitalik预测智能合约的无Bug未来 原始链接：

概述

根据以太坊联合创始人Vitalik Buterin的说法，优先考虑安全性的开发者可以期待在2030年代实现无Bug编码。

在Gnosis Chain为从Balancer黑客事件中恢复940万美元而进行的有争议的硬分叉之后，以太坊联合创始人Vitalik Buterin表示，“Bug不可避免，无法制作出无Bug代码”的观点将在2030年代不再成立。

Vitalik Buterin对编码说了什么？

Vitalik Buterin在社交媒体平台X上的互动中预测，到2030年代，无Bug代码将成为现实。

讨论始于Gnosis Chain于12月22日宣布执行硬分叉。此次硬分叉恢复了在2024年11月Balancer漏洞中被盗的940万美元，该漏洞在多个区块链上造成了超过$128 百万的损失。此次恢复需要大多数验证者采用新软件，未能更新的验证者将面临惩罚。

这一举措引起了一些区块链支持者的反对，他们批评此举违背了不可变性的原则。一位名为‘colluding node’的X用户表示，真正的问题在于区块链应用的构建方式。他们认为在可编程虚拟机中使用智能合约是错误的方法。

“只有7个值得编写的合约，它们应该被纳入基础层，并通过客户端多样性获得安全性，”该用户写道。

Buterin随后回应澄清，形式化验证并不等同于可证明无Bug。他进一步建议，或许根本不可能实现可证明无Bug的代码。

“我甚至可以说‘可证明无Bug’是不可能的，因为‘无Bug’意味着‘意图与代码执行之间没有差距’，而我们的意图是一个极其复杂的对象，我们只能有限地访问它。”

形式化验证使用数学方法检查安全关键系统是否正确运行。这一技术自20世纪60年代起就在航空航天工程等领域得到应用。

在智能合约中使用时，形式化验证可以证明合约的业务逻辑符合预定义的规范；然而，尽管Balancer的合约经过了11次审计，由四家不同的安全公司进行，但仍有一个关键缺陷漏网。

无Bug代码的未来可能吗？

Buterin提出，解决方案是多层冗余，以消除意图与执行之间的差距。他指出类型系统是一种冗余形式，而对代码的特定声明进行形式验证则是另一层。

形式化验证可以检测整数下溢和上溢、重入攻击以及可能被审计员和测试人员遗漏的低效Gas优化等问题。与此同时，传统测试只能检测错误的存在，而无法确保没有错误。

Buterin指出，某些软件仍会存在Bug，因为在某些情况下，功能的提升比完美更重要。但优先考虑安全性的开发者将拥有实现真正无Bug代码的工具。