Aptos推出动态调度Move合约的AI辅助形式化验证功能
Aptos宣布成为首个支持动态调度智能合约形式化验证的第一层区块链,该功能依托AI生成的规范及其Move Prover工具实现。团队将Move Prover定位为链上“预言机”,通过数学方法证明合约行为,旨在构建市场与机器驱动交易系统间的可信层。此次升级是Aptos推进5000万美元AI驱动市场与链上金融基础设施计划的重要环节。
技术实现路径
Aptos宣称其网络现为“首个支持动态调度形式化验证的L1链”,强调即使合约采用高阶函数与动态调度,Move智能合约栈仍可通过数学方法验证其符合设计预期。Aptos实验室在社交媒体中阐释了“AI编写规范、数学证明正确性、Move Prover作为预言机”的工作流程,即大语言模型生成形式化规范后,交由Move Prover进行自动化验证。
团队进一步说明,Move是唯一内置原生形式化验证的智能合约语言,现已扩展支持动态调度功能。据悉,近期研究在保持验证器威胁模型完整的前提下,成功将一流函数与动态调度纳入Move工具链。根据官方文档,该验证器已在协议层应用于验证核心逻辑——包括质押、计量、代码部署及支持数据结构,其设计目标在于让具备数学背景(未必拥有软件工程背景)的领域专家能够审计链上程序的实际行为。
技术突破与生态布局
2026年5月发表的《Move中命令式一流函数的形式化验证》论文指出,动态调度极大增加了状态空间的复杂性,促使Aptos工程师重新设计验证器生成与检查高阶Move代码验证条件的方式。这项AI辅助验证技术的推进,与Aptos针对链上市场及AI系统设立的5000万美元资助计划同步展开。该公司承诺提供加密内存池与保密永续合约,以构建能抵御对抗性机器人与新一代机器驱动策略的“机构友好型”交易通道。
在此背景下,将Move Prover定位为市场与机器间的“预言机”,不仅是市场宣传策略,更是试图将形式化方法塑造为智能合约监管的唯一可扩展路径——尤其在AI智能体实时编写、部署并进行对冲交易的环境中,这一技术路线显得尤为重要。

资金费率
资金费率热力图
多空比
大户多空比
币安/欧易/火币大户多空比
Bitfinex杠杆多空比
账号安全
资讯收藏
自选币种