据 PANews 称，5 月 28 日，Vitalik Buterin 分享了其自主语言模型（LLM）搭建的最新进展，强调以太坊基础设施与人工智能之间的交集正在不断加深。他提到，Deepseek V4 的 2-bit 量化版本在使用 Apple 硬件时可在 90GB 内存中运行，速度约为每秒 35 个 token；而在 AMD 上仅为每秒 7 个 token，强调多硬件、多个厂商的支持是区分“去中心化 AI”和“CROPS AI”的关键。Mistral 的 Leanstral 模型同样专注于编写 Lean 代码，在 70GB 内存下运行，其性能也与 1T 参数模型相当。
Vitalik 进一步阐述了形式化验证在提升代码安全性方面的作用，提出借助 AI 辅助的形式化验证可实现适用于 STARKs、共识算法以及 EVM 组件的“端到端”安全证明。他指出，区块链和 ZK-SNARKs 提供开放可验证性并实现隐私可扩展性；而将 AI 与形式化验证结合，则能在提高代码效率的同时恢复准确性，从而形成互补的技术栈。
