NEAR 以 AI 辅助形式化验证强化协议安全，单题证明成本约 0.17 美元

摘要

NEAR Protocol 计划以 AI 辅助形式化验证来强化协议与核心智慧合约安全，起因是一项里程碑：一个 AI 代理在 Lean／PutnamBench 风格的题目中解出 672 题，模型成本约 111.85 美元，平均每题约 0.17 美元。NEAR 认为这可降低专家人力与运算成本，但正式上线仍须具备准确的软体模型、明确的性质定义，以及与实际部署程式码相连的形式化证明。计划把验证套用到协议、核心合约与生态工具，并强调形式化保证只涵盖特定性质，不等于整个应用的安全保证，仍需搭配测试、程式码审查与既有安全实务。