币圈界报道：

Aptos实现链上智能合约动态调度的AI驱动形式化验证

作为首条支持动态调度智能合约形式化验证的第一层区块链，Aptos推出基于AI生成规范与Move Prover工具的自动化验证系统。该功能被定位为链上“预言机”，以数学方法确保合约行为符合设计预期，为机器驱动交易与市场间建立可信赖的执行层。此次能力上线，是其5000万美元AI赋能链上金融生态计划的关键一步。

AI生成规范与数学验证协同工作流落地

Aptos网络现已具备对高阶函数及动态调度场景下的智能合约进行形式化验证的能力，成为全球首个实现此目标的L1链。团队在公开渠道详解其技术流程：由大语言模型生成形式化规格说明，经由Move Prover完成自动化正确性验证。这一闭环机制将开发效率与安全性结合，使非软件工程背景的领域专家亦能参与链上程序的可信审计。

Move语言原生支持扩展至复杂动态逻辑

Move作为唯一内建形式化验证机制的智能合约语言，现已被成功拓展以支持命令式一流函数与动态调度。研究团队在保持原有威胁模型完整性的前提下，重构了验证条件的生成与检查逻辑，成功将复杂代码结构纳入验证体系。该能力已应用于协议核心模块——包括质押机制、资源计量、代码部署及数据结构管理，旨在降低专业门槛，提升透明度。

技术突破呼应机构级链上市场建设蓝图

2026年5月发表的《Move中命令式一流函数的形式化验证》论文揭示，动态调度显著扩大状态空间复杂度，促使Aptos重新设计验证器架构。伴随该技术推进，公司同步启动5000万美元资助计划，聚焦构建加密内存池与保密永续合约，打造抵御对抗性机器人与高级算法策略的“机构友好型”交易通道。此举不仅强化技术壁垒，更试图将形式化方法确立为未来智能合约监管的可扩展标准，尤其在AI代理实时部署与对冲操作日益普遍的背景下，意义深远。