币圈界报道：

Aptos率先实现动态调度合约的AI驱动形式化验证

Aptos正式推出基于人工智能生成规范与数学证明相结合的形式化验证系统，成为全球首条支持动态调度智能合约自动化验证的第一层公链。该功能依托其自主研发的Move Prover工具，将合约行为的正确性交由可信赖的“链上预言机”进行数学级验证，为机器驱动交易与市场机制之间建立可审计、可信任的底层通道。

AI生成规范与数学验证双轮驱动的技术闭环

Aptos强调其网络已具备对高阶函数及动态调度场景下的智能合约进行形式化验证的能力，突破传统静态分析局限。团队在公开渠道披露了“大模型撰写形式化规格—自动化验证器执行逻辑校验—结果作为链上可信依据”的完整流程。其中，大语言模型负责生成符合语义预期的规范描述，而Move Prover则以严谨的数学方法验证代码是否严格遵循设计意图。

Move语言作为唯一原生集成形式化验证能力的智能合约框架，现已扩展至支持动态调度逻辑。研究团队在维持原有安全威胁模型完整性前提下，成功将一流函数调用与运行时调度纳入验证体系。目前，该验证机制已在协议核心模块中落地应用，涵盖质押机制、资源计量、代码部署及数据结构管理等关键环节，使非软件工程背景但具备数学素养的领域专家亦能独立审查链上程序的实际行为。

前沿研究支撑机构级可信交易生态建设

2026年5月发表的《Move中命令式一流函数的形式化验证》论文揭示，动态调度显著扩大状态空间复杂度，迫使Aptos重构验证条件的生成与检查逻辑。此次技术突破与其推出的5000万美元资助计划同步推进，旨在打造面向机构用户的加密内存池与保密永续合约基础设施，抵御对抗性机器人与高频策略侵蚀。

将Move Prover定位为“市场与机器之间的预言机”，不仅是战略宣传举措，更体现了其长远愿景——将形式化方法确立为智能合约监管的唯一可扩展路径。尤其在人工智能体可实时编写、部署并执行对冲操作的未来场景中，该技术将成为确保系统稳定性与公平性的关键基石。