Aptos Move Prover 工作流路由为 AI 智能体编排规格推理、验证与测试的实战指南【免费下载链接】aptos-coreAptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.项目地址: https://gitcode.com/GitHub_Trending/ap/aptos-core导读在 Aptos 的 Move Prover 研究代码库中higher-order-paper-26/examples包内的 CLAUDE.md 定义了一套面向 AI 编码智能体如 Claude Code的Move 工作流路由规则针对规格推理、形式化验证、单元测试与编译修复四类任务明确指定应加载的 Skill 与 Agent并规定禁止直接调用底层 MCP 工具。本文将以这份路由文档为骨架结合同目录下的 README.md、论文级示例源码amm_example.move/find.move及 Prover 配置完整讲解该路由体系的设计动机、每种工作流的适用场景、环境搭建与真实运行方式以及背后的证明原理帮助读者掌握在 Move Prover 研究中正确、高效地驱动 AI 智能体完成形式化验证的全流程。一、Move 工作流路由一份写给 AI 智能体的操作手册higher-order-paper-26/examples是一个自包含的 Move 包承载论文《Formal Verification of Imperative Higher-Order Functions》的全部示例。包内的 CLAUDE.md 开头声明了「Move Workflow Routing」路由规则核心思想是当智能体需要在该包内处理 Move 代码时必须先选择正确的工作流再选择正确的工具形态。路由规则原文如下当用户要求「in an agent」或「as a subagent」运行时使用 Agent 工具并指定 agent 名称否则使用 Skill 工具并通过/skill-name将工作流加载进当前对话。这一区分十分重要Agent 形态适合把任务委派给独立的子智能体并行、隔离上下文而Skill 形态适合把工作流指令直接注入当前会话共享上下文、连续多轮。二者共享同一套工作流定义只是加载方式不同。该路由小节同样出现在inference-paper-26/v1/examples/CLAUDE.md与inference-paper-26/v2/examples/CLAUDE.md中说明这是 Move Prover 论文示例包通用的智能体协作约定而非单一实验的临时配置。二、四种核心工作流Skill 与 Agent 的映射路由文档把 Move 开发任务划分为四类工作流每一类都有对应的 Skill 与 Agent映射关系如下工作流适用场景SkillAgentSpec inference推断规格、生成规格、执行 WP最弱前置条件分析/move-infmove-infVerification验证、证明、运行 Prover、检查规格/move-provemove-verifyTesting生成测试、单元测试、提升覆盖率/move-testmove-testFix compilation检查编译错误、修复编译问题/move-checkmove-check2.1 Spec inference/move-inf/move-inf面向「从代码推断规格」的任务。在 Move Prover 的实践中规格是验证的前提——spec块中的invariant、ensures、aborts_if、requires等需要人工或工具生成。该工作流同时覆盖WPweakest precondition分析即从函数后置条件反向推导调用方必须满足的前置条件这与 Prover 的验证机制同源但目的更偏「生成/补全规格」而非「证明」。2.2 Verification/move-prove/move-verify面向「运行 Prover、证明规格成立」的任务。这是 Move Prover 的核心工作流对应 README.md 中的aptos move prove命令。验证工作流持有完整的上下文包括验证目标文件、语言版本要求2.4、后端超时配置Prover.toml中的vc_timeout 40、以及针对高难度模块的特殊 flag如--split-vcs-by-assert。2.3 Testing/move-test/move-test面向「生成/运行单元测试、提升覆盖率」的任务对应 Move 生态的aptos move test体系。该工作流与验证工作流互补测试提供可执行的具体反例体验验证提供全输入的数学保证。2.4 Fix compilation/move-check/move-check面向「编译失败、语法/类型错误修复」的任务。示例包依赖MoveStdlib见 Move.toml 中MoveStdlib { local ../../../../move-stdlib }且示例使用了较新的语言特性闭包、-state 标签编译错误并不罕见需要独立工作流专门处理。三、MCP 工具调用规则为什么禁止直连底层工具路由文档给出了明确禁令不要直接调用move_package_wp或move_package_verifyMCP 工具——始终使用拥有完整工作流上下文的 skill 或 agent。这条规则的技术动机在于move_package_wp与move_package_verify是 Move Prover MCP 服务的底层原语仅暴露「对单个包执行 WP 分析 / 验证」的裸调用。而一次成功的验证往往需要前置环境判断——确认语言版本是否 ≥ 2.4-state 标签与状态量化语法要求参数组合选择——是否需要--split-vcs-by-assert拆分验证条件后端约束——遵守Prover.toml的vc_timeout预算错误诊断与迭代——根据 Prover 输出反推规格修正方案。这些上下文被封装在/move-inf、/move-prove等 Skill/Agent 中。绕过它们直接调用 MCP 原语会丢失参数默认值、依赖解析顺序与超时策略等关键信息容易产生超时或误报。因此路由文档将其列为硬性禁令而非建议。此外对于常规 Move 开发编写代码、阅读代码、解释概念路由文档指示使用/moveskill 获取语言与工具参考把「日常开发」与「验证专项」两类任务在工具入口上做了彻底分离。四、路由体系的落地场景高阶函数验证示例包要理解这套路由为何存在需要先看清它服务的包。examples/是论文《Formal Verification of Imperative Higher-Order Functions》的自包含 Move 包见 README.md其核心研究点是可验证的一等函数first-class functions / 动态分派Move 允许把函数作为值传递闭包例如 AMM 中的可插拔定价曲线、Vault 中存储的策略、注册的事件回调。这类模式在现代智能合约中很常见但历史上极难形式化验证。包内sources/下共 5 个 Move 文件amm_example.move——AMM 池定价函数以闭包形式存储在Pool结构体中find.move——基于行为谓词描述的高阶findcalculator.move、followed_by.move、vault.move——其余论文示例。包的依赖配置Move.toml声明了defi与std两个地址占位符dev 地址分别为0x100与0x1并将MoveStdlib以本地相对路径引入使其不依赖网络即可独立构建。在论文写作流程中见上级目录 CLAUDE.md该包是论文 listing 的「事实来源」——所有 Move 代码先在examples/中修改并验证再把片段复制进.tex。这意味着对包的任何规格改动都必须通过上述四种工作流验证后才能进入论文这正是路由规则存在的最直接动因。五、环境准备与运行 Prover 的完整流程README.md 给出了从零到运行 Prover 的三步流程这是验证工作流/move-prove背后真实的 CLI 操作。5.1 安装 Aptos CLI二选一Aptos CLI 内置了 Move Prover。方式一为下载预编译二进制推荐安装后确认aptos --version方式二为从源码构建在当前 aptos-core 仓库内安装 Rust/Cargo 后执行cargo build --package aptos --profile cli二进制产物位于target/cli/aptos将其加入PATH或以全路径调用即可。5.2 安装 Prover 依赖Move Prover 依赖Boogie验证器与Z3SMT 求解器CLI 提供一条命令自动安装aptos update prover-dependencies5.3 在示例包上运行 Prover在examples/目录下执行aptos move prove --dev --language-version2.4--language-version2.4是硬性要求该包的规格使用了-state 标签与状态量化S |~ ...语法只有语言版本 2.4 才支持。--dev表示使用 dev 地址defi 0x100编译验证。命令会在sources/下逐模块验证规格并打印结果。六、源码级深入AMM 示例中的验证难点与证明策略amm_example.move是理解「为什么需要路由与证明提示」的最佳案例。其核心设计第 19-47 行是Pool结构体直接保存定价闭包pricing: |u64, u64, u64| u64 has copy store drop并在spec Pool中声明四条池级不变量约束任意被赋值的闭包No-abortforall S in *, ...: S |~ !aborts_ofself.pricing(r_in, r_out, amt)——定价函数对任意输入都不得 abortSafetyresult_ofself.pricing(...) r_out——输出不得超过输出储备Monotonicitya1 a2 result(a1) result(a2)——输入越多输出越多Constant-product preservation(r_in amt) * (r_out - result) r_in * r_out——储备乘积不减少。由于不变量量化的是「池中存储的任意闭包」验证义务集中在闭包被写入Pool的时刻pack time——即三个构造函数create_constant_product_pool、create_noncompliant_fee_pool、create_compliant_fee_pool第 228-264 行。而swap第 191-215 行对闭包泛型化仅凭池不变量即可完成验证。三种定价实现展示了验证的「通过 / 预期失败 / 提示辅助」三分法constant_product无手续费恒积公式——满足全部四条不变量其spec用pragma opaque封装并逐一声明ensuresconstant_product_with_fee_non_compliant第 155-183 行——直接读取Fee[owner].bps在Fee缺失时 abort故意违反 no-abort 不变量。其spec明确声明aborts_if !existsFee(owner)用于演示预期的requires违例诊断正确报错而非超时constant_product_with_fee合规版第 102-150 行——Fee缺失或越界时回退到DEFAULT_FEE_BPS 5005%手续费吃掉全部输入时返回 0通过split amount_in 0证明提示拆解非线性验证条件。prover.exp 记录了运行 Prover 后的预期输出create_noncompliant_fee_pool在amm_example.move第 30、34、38、45 行处产生 4 条error: data invariant does not hold错误回溯链create_noncompliant_fee_pool→signer::address_of→ 闭包调用完整展示了 pack-time 义务的触发路径——这正说明「合规构造通过、非合规构造报错」是有意设计的教学行为。6.1 为什么需要--split-vcs-by-assert上级 CLAUDE.md 明确警告AMM 示例会「把求解器逼到极限」不加--split-vcs-by-assert时该模块单核运行约 85 秒勉强超出Prover.toml默认的 40 秒vc_timeout预算。拆分后的运行方式为cargo run -p move-prover -- \ --language-version 2.4 \ -d third_party/move/move-stdlib/sources \ -a std0x1 \ --split-vcs-by-assert \ third_party/move/move-prover/doc/higher-order-paper-26/examples/sources/amm_example.move--split-vcs-by-assert将单条巨型验证条件VC按 assert 边界拆分为多条线性义务规避非线性算术给 Z3 带来的压力。6.2 规格书写惯例影响 Z3 启发式的细节上级 CLAUDE.md 记录了三条直接影响验证成功率的编辑惯例|~运算符绑定优先级最低S.. |~ a b解析为S.. |~ (a b)书写时保持无括号风格不要「好心」加括号改变语义Pool 规格中 no-abort 不变量必须写在第一条顺序影响 Z3 启发式该顺序能让swap在不把定价函数的非线性 CP ensures 暴露给调用方的情况下稳定验证通过constant_product_with_fee的规格直接把 CP-preservation 不等式写进ensures这样create_compliant_fee_pool无需从手续费调整后的输入公式重新推导即可消解对应requires函数自身验证则用split amount_in 0把非线性函数体的 VC 拆成两条线性义务。七、源码级深入find.move中基于行为谓词的高阶规格find.move 展示了如何用行为谓词描述闭包参数化函数。模块级辅助函数第 11-23 行将「谓词行为」符号化fun no_matchT(v: vectorT, pred: |T|bool, k: u64): bool { forall j in 0..k: !result_ofpred(v[j]) } fun no_abortT(v: vectorT, pred: |T|bool, k: u64): bool { forall j in 0..k: !aborts_ofpred(v[j]) }find函数第 27-58 行的循环不变量量化前缀元素上的result_ofpred与aborts_ofpred函数级spec则完全通过行为谓词刻画返回值aborts_if精确到「扫描到达 j 当且仅当之前所有调用既不 abort 也不匹配」ensures分别覆盖找到result len(v)与未找到result len(v)两种情形。这套写法正是路由文档中 Spec inference / Verification 工作流要处理的「动态分派」核心难题——推理被传入函数的行为而不绑定具体实现。八、路由规则与 Move Prover AI 集成的整体定位将本文主题放回更大图景见 one-pager.md这套路由是 Move Prover AI 化改造的一部分Prover 通过MCP 服务暴露给 AI 编码智能体配合机械分析与 AI 结合的规格推理、可验证一等函数、证明提示proof hints与 AI skill 自动生成四块能力。其中规格推理→ 对应/move-inf工作流推断、生成规格、WP 分析验证与证明提示→ 对应/move-prove工作流运行 Prover、检查规格、按需生成proof { ... }提示可验证一等函数→ 对应amm_example.move/find.move中result_of/aborts_of/requires_of行为谓词体系MCP 服务→ 对应路由文档中「不直接调用move_package_wp/move_package_verify」的禁令——底层原语交由携带完整上下文的 Skill/Agent 封装。路由文档正是这四块能力的操作入口层它规定智能体在什么任务下加载什么工作流、以何种工具形态执行、哪些底层调用被禁止从而保证「AI 智能体 形式化验证」的协作既灵活可并行子代理又可靠上下文完整、参数正确、超时不失控。九、实操建议小结判断任务类型规格推断走/move-inf验证证明走/move-prove测试走/move-test修编译走/move-check日常开发走/move选择工具形态需要隔离上下文或并行执行时用对应 Agent否则用 Skill 加载进当前会话遵守禁令任何情况下不直接调用move_package_wp/move_package_verifyMCP 原语环境前置确保aptos --version可用、aptos update prover-dependencies已执行、语言版本 ≥ 2.4运行验证在examples/目录执行aptos move prove --dev --language-version2.4AMM 模块压力过大时加--split-vcs-by-assert并将超时预算按 Prover.toml 的vc_timeout 40为基线调整。以上流程与规则均可在当前仓库的 examples/CLAUDE.md、examples/README.md、sources/amm_example.move 与 sources/find.move 中直接复现验证是学习「AI 智能体驱动 Move 形式化验证」最贴近一线的参考路径。【免费下载链接】aptos-coreAptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.项目地址: https://gitcode.com/GitHub_Trending/ap/aptos-core创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考