Vitalik最新长文：AI时代，代码如何变得更安全？
随着AI编程能力快速提升，软件安全面临新挑战：AI既能高效生成代码，也能高效发现漏洞。在加密行业，智能合约、ZK证明等一旦出现缺陷，可能导致不可逆的资金损失。Vitalik探讨了应对此问题的路径——形式化验证。这种方法将程序应满足的性质写成数学命题，再用机器可检查的证明验证这些性质是否成立。虽然形式化验证无法保证绝对安全（证明可能遗漏假设、规范可能写错等），但它提供了一种更可靠的安全范式：用多种方式表达开发者意图，再让系统自动检查这些表达是否兼容。
以太坊未来将依赖复杂底层组件（如STARK、ZK-EVM、共识算法等），这些系统的实现复杂，但安全目标往往可以相对清晰地形式化。AI辅助的形式化验证在此可发挥最大价值：AI负责编写高效代码和证明，人类负责检查被证明的命题是否对应真正的安全目标。
Vitalik认为，面对强大的AI攻击者，答案不是放弃开源或依赖中心化机构，而是将关键系统压缩为更小、更可验证的“安全核心”。AI可能导致粗糙代码增加，但也可能让真正重要的代码变得比过去更安全。形式化验证与AI结合，可推动软件分化为“安全核心”和“不安全边缘组件”，前者通过严格验证承载高信任负担，后者在沙箱中运行以限制风险。最终，形式化验证有助于在AI时代构建更可信的网络安全基础。
marsbit1小时前
