资金费率
资金费率热力图
多空比
大户多空比
币安/欧易/火币大户多空比
Bitfinex杠杆多空比
账号安全
资讯收藏
自选币种
形式化验证：新的编程范式
一种新的软件开发方法正在以太坊研究领域获得关注。开发者们开始使用低级语言或直接使用Lean（一种用于可验证数学证明的语言）编写代码。其目标是实现代码的正确性能够被自动且数学化地验证。
Buterin认为这种方法可能具有变革性，并引用了研究员Yoichi Hirai的观点，称其为“软件开发的最终形态”。该方法将效率与可读性完全分离：一个版本的代码追求运行速度，另一个版本则写得清晰易懂以供人类理解，并通过数学证明将两者关联起来。
这种方法对于ZK-EVM、抗量子签名和共识算法等高价值系统尤为重要。这些系统构建复杂，但其安全属性却能够相对直接地进行形式化表述。这种复杂性与清晰性之间的差距，恰恰是形式化验证最能发挥作用的领域。
像Arklib和evm-asm这样的项目已经将此方法应用于以太坊基础设施。evm-asm项目直接在RISC-V汇编中构建EVM实现，然后通过形式化证明其与一个可读的高级版本相匹配。
对网络安全悲观论的回应
业界一些声音认为，AI驱动的漏洞发现将使安全、无需信任的软件成为不可能。Buterin直接反驳了这一观点。他将当前阶段视为一个过渡性的挑战，而非攻击者将永久占据上风的根本性转变。他认为一旦格局稳定，防御方将比以往更强大。
他以Mozilla的研究作为佐证。Mozilla指出安全缺陷是有限的，并且防御者现在拥有一条现实的路径去发现所有缺陷。建立在“数字防御者拥有优势”这一理念上的密码朋克传统，不必被抛弃。
Buterin提出的模型将软件分为可信的安全核心和信任度较低的边缘组件。边缘组件在权限极少的沙盒环境中运行。而被刻意保持小巧的核心部分，则能充分受益于AI辅助的形式化验证。
形式化验证的局限
Buterin也谨慎地避免过分夸大形式化验证的作用。一些已记录的失败案例显示了其实际局限。
在某些约束条件根本未被指定的情况下，经过形式化验证的C语言编译器中依然出现过漏洞。2025年libcrux中的一个漏洞表明，未经验证的内部函数封装可能会在特定硬件平台上破坏输出。另一个漏洞则因已验证部分之外的代码中一个未处理的解密错误，导致了进程崩溃。
这些失败的案例模式是一致的：要么只有部分代码被验证，要么证明中从未包含某个关键属性。形式化验证并不能在人类语言的完整意义上证明软件的正确，它只能证明在特定假设下，指定的属性得以成立。
侧信道攻击构成了另一个边界。即使是一个被完美证明的加密方案，也可能通过电力波动泄露私钥。攻击者的数学模型并不总能捕捉到现实世界中所有的信息泄露类型。
Buterin的结论是审慎的：形式化验证并非一个完整的解决方案，但它是对一个已在进程中的安全趋势的强大助推剂——而AI正使这一趋势变得显著更易实现。
