Aptos宣称自己是首个实现AI辅助动态分派形式化验证的第一层区块链

：

Aptos宣称其成为首个支持AI辅助动态调度Move合约形式化验证的第一层区块链，将Move Prover定位为连接市场与机器代理的"预言机"。

• Aptos表示这是首个支持动态调度智能合约形式化验证的Layer-1区块链，采用AI生成的规范及其Move Prover工具。
• 团队将Move Prover构建为链上"预言机"，通过数学方法验证合约行为，作为市场与机器驱动交易系统间的信任层。
• 此次升级正值Aptos推进5000万美元投资计划，重点布局AI驱动市场及链上金融基础设施。

Aptos宣布其网络现已成为"首个支持动态调度形式化验证的L1"，强调即使合约采用高阶函数和动态分派，Move智能合约栈仍可通过数学方法验证其行为符合设计。

Aptos Labs在X平台发文称："AI编写规范，数学验证正确性，Move Prover充当预言机——这就是市场与机器之间的信任层"，概述了由大语言模型生成形式化规范后输入Move Prover进行自动化验证的工作流。

Aptos借力Move Prover进军AI驱动市场

Aptos团队在X公告中进一步强调："Move是唯一内置原生形式化验证的智能合约语言，现已扩展支持动态分派功能"，这源于近期将一等函数和动态分派纳入Move工具链同时保持在验证器威胁模型内的研究成果。

据Aptos Move Prover文档显示，该验证器已在协议层用于"验证核心逻辑——质押、计量、代码部署及支持数据结构"，设计目标是让具备数学背景但"未必有软件工程背景"的领域专家能审计链上程序的实际行为。

2026年5月发表的系统研究论文《Move中命令式一等函数的形式化验证》指出，动态分派极大增加了状态空间复杂度，迫使Aptos工程师重新设计验证器生成和检查高阶Move代码验证条件的方式。

这项AI辅助验证技术的推进，与Aptos针对链上市场和AI系统的5000万美元资助计划同步展开。该公司承诺提供加密内存池和保密永续合约，旨在构建能抵御恶意机器人和下一代机器驱动策略的"机构友好型"交易通道。

在此背景下，将Move Prover定位为市场与机器间的"预言机"，不仅是营销话术，更是试图将形式化方法推销为唯一可扩展的智能合约监管方案——尤其当AI代理开始实时编写、部署并交易这些合约时。