PANews 5月18日消息，Vitalik發布部落格文章稱，以太坊社群正在嘗試用Lean 等形式化工具直接在底層語言（如EVM 字節碼、RISC‑V 彙編）上編寫程式碼，並透過機器可驗證的數學證明來確保正確性與安全性。 Vitalik 指出，形式化驗證可用於驗證Signal 等加密通訊協定、TLS、STARK、ZK‑EVM、共識演算法和EVM 實現的端對端安全與等價性，並在AI 自動找bug 的新環境下大幅提升防禦方優勢。不過他也強調，形式化驗證並非萬能，容易遺漏未建模假設、側頻道、未覆蓋模組等風險。 Vitalik 認為，未來軟體將圍繞少量「安全核心」構建，AI 負責大量程式碼生成，形式化驗證負責把關關鍵基礎設施安全。