根據 PANews，5 月 28 日 Vitalik Buterin 分享了他自主管理語言模型（LLM）設置的最新進展，強調以太坊基礎設施與人工智慧之間的交集正在擴大。他提到 Deepseek V4 的 2-bit 量化版本在蘋果硬體上可在 90GB 記憶體內以約每秒 35 個 token 的速度運行，但在 AMD 上則只有每秒 7 個 token，並強調多硬體供應商支援是區分「去中心化 AI」與「CROPS AI」的關鍵。聚焦於 Lean 程式碼編寫的 Mistral Leanstral 模型同樣可在 70GB 下運行，其效能也可媲美 1T 參數模型。
Vitalik 進一步闡述形式驗證在提升程式碼安全性方面的作用，提出由 AI 輔助的形式驗證能夠提供適用於 STARKs、共識演算法與 EVM 元件的「端到端」安全性證明。他指出區塊鏈與 ZK-SNARKs 提供開放可驗證性與隱私可擴展性，而將 AI 與形式驗證結合則能在恢復準確性的同時提升程式碼效率，形成互補的技術堆疊。
