**The DAO 安全基金与以太坊基金会合作,启动 Vyper 编译器形式化验证项目**
The DAO 安全基金日前宣布,将与以太坊基金会合作,共同资助 Vyper 编译器的形式化验证工作。 以太坊基金会已承诺提供 10 万美元的资金。
目前,Vyper 智能合约的安全审计和验证主要集中在源代码层面,而以太坊实际执行的却是编译后的字节码。两者的一致性取决于编译器的正确性。这一差距凸显了加强 Vyper 编译器可靠性的必要性。
该项目旨在通过机器证明技术,确保 Vyper 编译过程不会意外改变代码原意,从而保障智能合约在执行时的安全性和一致性。项目预期最终将在 Vyper 官方编译器中推出经过形式化验证的编译模式。
值得一提的是,The DAO 安全基金本身就源于 2016 年 The DAO 黑客事件中无人认领的 ETH 资金,目前规模约 2.5 亿美元,主要用于加强以太坊生态的安全建设。此次合作是该基金在支持以太坊安全技术方面的又一重要举措。