NEAR AI推进核心合约形式化验证

NEAR AI正致力于降低形式化验证的门槛，初期重点是NEAR协议及其核心智能合约。形式化验证通过数学证明检查软件是否符合既定规则，可与测试和代码审查互为补充，但不能保证系统绝对安全。 这项工作建立在NEAR AI此前取得的成绩之上：该团队据报在Lean Eval v1形式化基准排行榜上以解题总数排名第一。在PutnamBench测试中，其系统使用Lean解决了672道题目。据报平均每题成本约为0.17美元，而代码库记录的此次提交模型成本为111.85美元。NEAR提醒，基准测试结果并不代表验证生产环境软件所需的全部成本和工作量。 要将形式化验证用于已部署的合约，仍需建立准确的模型、明确待验证的属性，并确保证明与实际实现相符。验证结论仅适用于所检查的属性和假设，因此形式化验证仍需与测试、代码审查及运营安全措施结合。这项计划也反映了业界对AI辅助证明的广泛关注，Aptos Labs和以太坊联合创始人Vitalik Buterin也曾谈及相关工作。对NEAR交易者而言，这可能是长期安全建设的一部分，但目前并非已宣布的部署，也不是直接的代币催化剂。