PANews 5月18日消息，Vitalik发布博客文章称，以太坊社区正在尝试用 Lean 等形式化工具直接在底层语言（如 EVM 字节码、RISC‑V 汇编）上编写代码，并通过机器可验证的数学证明来保证正确性与安全性。Vitalik 指出，形式化验证可用于验证 Signal 等加密通信协议、TLS、STARK、ZK‑EVM、共识算法和 EVM 实现的端到端安全与等价性，并在 AI 自动找 bug 的新环境下显著提升防御方优势。不过他也强调，形式化验证并非万能，容易遗漏未建模假设、侧信道、未覆盖模块等风险。Vitalik 认为，未来软件将围绕少量“安全核心”构建，AI 负责大量代码生成，形式化验证负责把关关键基础设施安全。