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 交易者而言，這是長遠安全發展的潛在方向，並非已公布的部署，也不是代幣的即時催化因素。