Vitalik Buterin 认为，AI 辅助的形式化验证可能会改变关键区块链代码的编写方式。他的论点并非不惜一切代价加快开发速度，而是在将以太坊的关键部分部署到实时网络之前，使其在数学上可验证。
亮点
- Buterin 发表了一篇关于在区块链安全中使用形式化验证的文章。
- 以太坊前沿研究正在开发一种可以直接用 EVM 字节码、汇编或 Lean 编写代码的方法。
- Buterin 认为 AI 可以同时提高开发效率和代码安全性。
本文翻译自原文。点击此处阅读由我们的通讯员撰写的原文.
可被证明正确的代码
Buterin 描述了 以太坊前沿研究中出现的一种新范式：开发人员可以在底层编写代码，包括 EVM 字节码、汇编语言或 Lean，然后通过在 Lean 中自动检查的数学证明来确认其正确性。
这种方法的重点是用对程序属性的严格验证，来取代传统上对开发人员、审计师和测试的部分依赖。如果证明编写和检查正确，系统就会获得更强的保证，即代码完全按照预期执行。研究员 Yoichi Hirai 将这种模式称为“软件开发的最终形态”。
AI 可以提供帮助的地方
Buterin 认为，AI 辅助的形式化验证可以提高代码效率和安全性。这对于以太坊中那些一旦出错就可能导致数亿美元损失或损害基础设施信任的部分尤为重要。在这些模块中，他重点强调了 STARKs、ZK-EVMs、后量子签名和共识算法。
在这种模式下，AI 不应在没有监督的情况下简单地生成代码。它的角色更像是一个助手，负责加快证明编写、帮助发现错误并检查代码是否符合其规范。对于以太坊来说，这符合更广泛的发展路径：该网络越来越多地被定位为基础层，在这里，安全性和可验证性比单个交易的速度更重要，而不是追求成为最快的区块链平台。
核心与外围的分界线
Buterin 还强调，形式化验证并非万能。如果证明没有涵盖所有情况、规范本身编写错误，或者通过硬件侧信道出现漏洞，它仍然可能失败。
这就是为什么未来的软件架构可能会分为两部分：经过最严格形式化验证的小型“安全核心”，以及可以使用更灵活开发方法的不太关键的外围组件。在这样的模式下，以太坊可能成为数字经济的关键安全核心之一。如果这种方法得到普及，主要的转变将不是代码编写得更快，而是最重要的代码变得更难被攻破。
正如我们之前报道的，Vitalik Buterin 提议简化以太坊节点架构。
最新 Ethereum 新闻
-
中国
-
中国台湾
-
丹麦
-
乌克兰
-
乌兹别克斯坦
-
乌干达
-
乌拉圭
-
也门
-
亚美尼亚
-
以色列
-
伊拉克
-
伊朗伊斯兰共和国
-
保加利亚
-
克罗地亚
-
刚果
-
刚果（金）
-
利比亚
-
加拿大
-
加纳
-
匈牙利
-
北马其顿
-
南非
-
博茨瓦纳
-
卡塔尔
-
卢旺达
-
卢森堡
-
印度
-
印度尼西亚
-
厄瓜多尔
-
叙利亚
-
古巴
-
吉尔吉斯斯坦
-
哈萨克斯坦
-
哥伦比亚
-
哥斯达黎加
-
喀麦隆
-
土耳其
-
坦桑尼亚
-
埃及
-
埃塞俄比亚
-
塔吉克斯坦
-
塞尔维亚
-
塞浦路斯
-
墨西哥
-
多米尼加共和国
-
奥地利
-
委内瑞拉
-
孟加拉国
-
安哥拉
-
尼日利亚
-
尼泊尔
-
巴勒斯坦
-
巴哈马
-
巴基斯坦
-
巴布亚新几内亚
-
巴拉圭
-
巴拿马
-
巴林
-
巴西
-
希腊
-
德国
-
意大利
-
拉脱维亚
-
挪威
-
捷克
-
摩尔多瓦
-
摩洛哥
-
文莱达鲁萨兰国
-
斯威士兰
-
斯洛伐克
-
斯洛文尼亚
-
斯里兰卡
-
新加坡
-
新西兰
-
日本
-
智利
-
柬埔寨
-
格鲁吉亚
-
比利时
-
毛里求斯
-
沙特阿拉伯
-
法国
-
波兰
-
波多黎各
-
泰国
-
津巴布韦
-
海地
-
澳大利亚
-
爱尔兰
-
爱沙尼亚
-
牙买加
-
特立尼达和多巴哥
-
玻利维亚
-
瑞典
-
瑞士
-
留尼汪
-
白俄罗斯
-
科威特
-
科特迪瓦
-
秘鲁
-
突尼斯
-
立陶宛
-
索马里
-
约旦
-
纳米比亚
-
缅甸
-
罗马尼亚
-
美国
-
老挝
-
联合王国
-
肯尼亚
-
芬兰
-
荷兰
-
莫桑比克
-
莱索托
-
菲律宾
-
萨尔瓦多
-
葡萄牙
-
蒙古
-
西班牙
-
赞比亚
-
越南
-
阿塞拜疆
-
阿富汗
-
阿尔及利亚
-
阿尔巴尼亚
-
阿曼
-
阿根廷
-
阿联酋
-
韩国
-
香港
-
马来西亚
-
马耳他
-
马达加斯加
-
黎巴嫩
-
黑山
- Forex
- Crypto
