NEAR AI 推進核心合約的形式化驗證

NEAR AI 正致力讓形式化驗證更容易普及，初期目標是 NEAR Protocol 及其核心智慧合約。形式化驗證運用數學證明，檢查軟體是否符合既定規則。它能補足測試和程式碼審查，但無法保證完全安全。 這項工作以 NEAR AI 所報告的成果為基礎：在 Lean Eval v1 排行榜上，依解題總數排名第一。在 PutnamBench 上，其系統解決了 672 道 Lean 題目。據報每題成本約為 0.17 美元，而程式碼儲存庫則列出該次提交的模型成本為 111.85 美元。NEAR 提醒，基準測試結果並不代表驗證正式環境軟體的全部成本或所需工作量。 要將形式化驗證應用於已部署的合約，仍需要準確的模型、明確定義的屬性，以及與實作相符的證明。保證僅涵蓋已檢查的屬性和假設，因此形式化驗證必須與測試、程式碼審查及營運安全並行。這項計畫反映了人們對 AI 輔助證明的廣泛興趣，其中包括 Aptos Labs 和 Ethereum 共同創辦人 Vitalik Buterin 討論過的相關工作。對 NEAR 交易者而言，這是長期安全發展的潛在方向，並非已宣布部署，也不是代幣的即時催化因素。