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本文以 third_party/move/move-prover/doc/higher-order-paper-26/one-pager.md 为主体骨架结合该目录下完整的 LaTeX 论文源FMCAD26 投稿Formal Verification of Imperative Higher-Order Functions、自包含 Move 示例包与仓库内 Move Prover 源码系统讲解 Move 语言一等函数动态分发的可验证性、MCP/Claude 插件集成、AI 规格推断与证明提示proof hints四大能力并给出可复现的运行命令。写在前面为什么在这个时间点重写 Move Proverone-pager 由 Aptos Labs 的 WolfgangGrieskamp撰写开篇点明了重写 Move Prover 的核心动机AI 正在同时加速攻防两侧。过去 18 个月的公开安全研究里基于 LLM 的审计管线——微调模型、Agent 化的漏洞挖掘循环、包裹 AI 假设生成的自动化不变量 fuzzer——已经能稳定地在人工审计通过的代码中找出可利用漏洞白帽报告每周可见黑产利用率难以统计但大概率同步上升多起高调 DeFi 事件中都能看到 AI 在侦察或跨链洗钱阶段的痕迹。其背后的经济不对称极其残酷攻击方的一次边际尝试只花一次 API 调用防御方的一次边际审计却要花掉一名工程师一周的高技能劳动。因此正确的应对不是与攻击方拼 AI 算力而是构建数学上无懈可击的防御——这正是形式化验证的初衷针对精确规范的证明不会因为模型想到了一个巧妙的输入而失效要么性质对所有输入成立要么给出具体反例。一、四项落地能力总览one-pager 列出的四块能力与仓库中 FMCAD26 论文目录third_party/move/move-prover/doc/higher-order-paper-26/一一对应MCP 服务与 Claude 插件证明器成为 AI 编码 Agent如 Claude Code可直接调用的工具写规范变成与能实时访问验证器的 AI 之间的往返对话而非离线猜测规格推断机械分析与 AI 结合分析器从代码机械推导规范中的常规部分AI 负责开发者真正关心的高层性质显著降低从零写规范的工作量对应同目录的inference-paper-26/论文Combining Mechanical and Agentic Specification Inference for Move可验证的一等函数动态分发Move 支持将函数作为值传递——AMM 中可插拔的定价曲线、金库内存储的策略、注册的事件回调——并原生处理动态分发的验证调用方无需绑定某个具体实现即可推理传入函数做了什么任何具体实例化都在调用侧按契约验证证明提示proof hints与生成提示的 AI 技能当证明器卡在棘手性质通常涉及非线性算术时可在规范语言中给出提示并有经过训练的 AI 技能自动提出并迭代这些提示直至验证通过。目录内的CLAUDE.mdthird_party/move/move-prover/doc/higher-order-paper-26/CLAUDE.md进一步说明工程组织方式论文 LaTeX 源以main.tex为根intro.tex、move.tex、encoding.tex、validation.tex、conclusion.tex分节examples/是论文清单的事实来源Move 源优先编辑再回拷进.tex禁止原地改清单且该子树的 Move 工作统一路由到move-flow技能/Agent/move-inf、/move-prove、/move-test、/move-check、/move并明确不要直接调用move_package_wp/move_package_verifyMCP 工具。这也印证了 MCP 服务确实是面向 Agent 工作流的真实基础设施。二、动态分发的验证AMM 定价函数一例2.1 Pool 结构把闭包存进状态examples/sources/amm_example.move查看完整源码展示了把定价函数直接存进Pool结构的模式struct Pool has key { reserve_x: u64, reserve_y: u64, // let amt_out pricing(reserve_in, reserve_out, amt_in) pricing: |u64, u64, u64| u64 has copy store drop, }pricing是类型|u64, u64, u64| u64的一等函数值。验证的关键洞察是池级不变量约束任何赋给pool.pricing的闭包因此打包构造Pool的时刻就是证明义务的落点——每个具体的定价实现都必须先在构造点自证满足池级不变量。2.2 池级不变量状态量化与新语法Pool的 spec 用到了-状态标签与S |~状态量化语法要求语言版本 2.4定义了四条不变量spec Pool { reads_ofself.pricing *; // 无中止定价函数对任何输入都不得 abort。 invariant forall S in *, r_in: u64, r_out: u64, amt: u64: S |~ !aborts_ofself.pricing(r_in, r_out, amt); // 安全输出不得超过输出储备。 invariant forall S in *, r_in: u64, r_out: u64, amt: u64: S.. |~ result_ofself.pricing(r_in, r_out, amt) r_out; // 单调性输入越多输出至少不少。 invariant forall S in *, r_in: u64, r_out: u64, a1: u64, a2: u64: S.. |~ a1 a2 result_ofself.pricing(r_in, r_out, a1) result_ofself.pricing(r_in, r_out, a2); // 恒定乘积保持储备乘积永不减少。 invariant forall S in *, r_in: u64, r_out: u64, amt: u64: S.. |~ (r_in amt) * (r_out - result_ofself.pricing(r_in, r_out, amt)) r_in * r_out; }语法约定见目录内CLAUDE.md的编辑规范|~的绑定力弱于及一切逻辑/关系运算符S.. |~ a b解析为S.. |~ (a b)在 Pool spec 中no-abort 不变量必须最先陈述这一顺序对 Z3 的启发式有实际影响——按此顺序swap才能可靠通过验证而无需把定价函数的非线性 CP恒定乘积保证散发给调用方。swap本身对存储的闭包保持泛化仅凭池级不变量即可验证public fun swap(pool: mut Pool, amount_in: u64): u64 { let amount_out (pool.pricing)( pool.reserve_x, pool.reserve_y, amount_in, ); pool.reserve_x pool.reserve_x amount_in; pool.reserve_y pool.reserve_y - amount_out; amount_out } spec swap { // 定价函数因 Pool no-abort 不变量不会中止reserve_y - amount_out // 因安全不变量不会下溢。 aborts_if pool.reserve_x amount_in MAX_U64; ensures result old(result_ofpool.pricing(pool.reserve_x, pool.reserve_y, amount_in)); ensures pool.reserve_x old(pool.reserve_x) amount_in; ensures pool.reserve_y old(pool.reserve_y) - result; ensures result old(pool.reserve_y); ensures pool.reserve_x * pool.reserve_y old(pool.reserve_x) * old(pool.reserve_y); }2.3 三种定价实现合规与不合规的对照源码中三个构造函数正好构成验证语义的对照组create_constant_product_pool使用无手续费的constant_productUniswap v2 式amount_out reserve_out * amount_in / (reserve_in amount_in)spec声明aborts_if false并保护退化(0,0)情形满足全部四条池级不变量验证通过create_noncompliant_fee_pool闭包捕获 owner 地址并调用constant_product_with_fee_non_compliant该实现直接读Fee[owner].bps、缺少Fee资源时中止aborts_if !existsFee(owner);、aborts_if Fee[owner].bps 10000;打包时报data invariant does not hold产生的是符合预期的requires违规诊断而非超时——这正是动态分发验证期望的正确诊断行为create_compliant_fee_pool调用合规变体constant_product_with_fee当Fee缺失或越界时回退到DEFAULT_FEE_BPS500 bps 5%effective_in 0时返回 0验证通过。2.4 证明提示非线性算术的台阶合规费率的 CP 保持不等式是验证中最棘手的部分。constant_product_with_fee的 spec 直接把 CP 保持不等式写成ensures并用proof { post assert effective_in amount_in; }提示求解器——原因是CP 保持可从result的闭式与eff amt推出但 Z3 无法跨非线性费率公式eff amt * (10000 - fee) / 10000自行导出该边界提示负责把它喂给求解器。非合规变体则用proof { split effective_in 0; ... }把非线性函数体的验证条件拆成两个线性义务。这正对应 one-pager 的第 4 项能力提示写在规范语言里、由 AI 技能自动生成并迭代。三、其他一等函数模式策略金库与高阶查找examples/sources/vault.move查看完整源码演示金库内存储策略模式Strategy(|FungibleAsset|FungibleAsset)以闭包形式存储收益策略其 spec 用ensures_ofself.0要求返回金额至少等于输入金额struct Strategy(|FungibleAsset|FungibleAsset) has store, copy, drop; spec Strategy { modifies_ofself.0 *; invariant forall input: FungibleAsset, result: FungibleAsset: ensures_ofself.0(input, result) result.amount input.amount; }harvest取出全部资产、调用动态分发的策略、再存回其 spec 只需声明ensures Vault[vault_addr].store.balance old(Vault[vault_addr].store.balance);——即金库余额不减少无需知道具体策略实现。examples/sources/find.move查看完整源码则示范以行为谓词刻画闭包参数化的高阶函数模块级辅助函数no_match/no_abort用result_ofpred/aborts_ofpred在符号层面对前缀元素量化find的循环不变量与函数 spec 完全由这些谓词刻画requires要求pred对每个元素可调用、aborts_if精确刻画扫描中止条件、ensures刻画首个匹配索引或len(v)。find_zero与find_zero_lambdalambda 内联 spec|x| *x 0 spec { ensures result (x 0); }展示了具名谓词与 lambda 两种调用侧特化方式且都能把aborts_if false传播到顶层。四、规格推断与 MCP 集成AI 辅助的形式化验证工作流one-pager 强调手写规范长期以来是形式化验证的主要摩擦点规格推断把机械可推导部分交给分析器、把开发者真正关心的高层性质如协议永远不会破产费用只增不减没人能提取超过存入的金额交给 AI。配套论文Combining Mechanical and Agentic Specification Inference for Move的 LaTeX 源位于 third_party/move/move-prover/doc/inference-paper-26/v1/v2 两个版本含skills.tex、example.tex、evaluation.tex等章节仓库搜索可确认 MCP 相关基础设施已落地。在 examples/CLAUDE.md 中可以看到面向 Agent 的完整工作流路由规格推断走/move-inf验证走/move-prove测试走/move-test修复编译走/move-check并明确建议通过 Skill/Agent 调用而非直接调用move_package_wp/move_package_verifyMCP 工具。这意味着在 Claude Code 等环境中写规范 → 实时调用证明器 → 根据诊断迭代已经成为工程化闭环。五、动手复现在仓库中运行高阶函数示例5.1 方式一Aptos CLI推荐示例包位于third_party/move/move-prover/doc/higher-order-paper-26/examples/其 README.md 给出了完整步骤# 1. 安装 Aptos CLI自带 Move Prover确认在 PATH 中 aptos --version # 2. 安装证明器依赖Boogie 验证器 Z3 SMT 求解器CLI 自动安装 aptos update prover-dependencies # 3. 在 examples 目录内运行证明器 # 语言版本必须 2.4规范使用了 -状态标签与状态量化 aptos move prove --dev --language-version2.45.2 方式二cargo 直接运行 move-prover对于 AMM 这类对求解器压力很大的例子目录内CLAUDE.md给出了直接调用证明器二进制的方式并指出--split-vcs-by-assert与--language-version 2.4是必须的无该标志时模块单核约跑 85 秒几乎塞不进默认 40 秒预算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示例包的 Prover.toml 中[backend] vc_timeout 40验证条件超时 40 秒Move.toml 将MoveStdlib指向仓库本地路径../../../../move-stdlib。若从源码构建 CLI仓库 README.md 的通用构建入口与 README 中cargo build --package aptos --profile cli产物在target/cli/aptos可作参考。前提是环境已安装 Rust/Cargo 及 Boogie、Z3详见示例 README 第 1、2 节。六、路线图Decibel 与验证的工程化one-pager 明确指出下一个主攻目标是Decibel——Aptos 的高吞吐链上永续交易引擎。订单撮合、保证金与清算逻辑、资金费率、预言机处理、费用归集、结算记账每一处细微缺陷都可能掏空金库或错误结算头寸形式化验证在这类系统上为自身买单。上述四项能力——AI 可直接调用的 MCP 证明器、机械Agentic 的规格推断、一等函数的原生验证、自动生成证明提示的技能——正是让在 Decibel 的规模上、每个 PR 合入前跑证明器从愿景变成现实的底座。仓库中 Decibel 相关的永续/交易框架源码如 aptos-move/framework/aptos-trading 及 aptos-move/move-examples/defi可作延伸阅读。结语这篇 one-pager 的核心信息可以浓缩为一句AI 让攻防两侧都变快了而防御侧的正解是让数学严谨的证明器与能干形式化验证中枯燥一半工作的 AI配对——MCP 集成解决的是AI 如何实时用验证器规格推断解决的是规范从哪来一等函数验证解决的是现代合约模式怎么证明proof hints 技能解决的是卡住时如何收尾。四者叠加才是让 Decibel 级系统验证现实可行而非愿景的组合。论文细节可继续阅读仓库内 FMCAD26 投稿的 LaTeX 源main.tex 及各分节、examples/README.md 的复现指引。注one-pager 正文标注了两篇 arXiv 论文编号arXiv:2605.10007、arXiv:2605.10005写作本文时该编号属于原文档自述信息未在仓库内二次核实引用时请以原文为准。【免费下载链接】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），仅供参考