构筑AI软件工程安全的根本前提,MoonBit 推出代码形式化验证

AI Coding 带来软件工程开发效率的急速提升，也在放大一个长期被低估的结构性风险，代码的生产速度与可靠性验证能力之间的差距正在以前所未有的速度扩大。MoonBit 团队意识到 AI 时代软件开发中的下一个核心命题：当AI可以大规模生成代码，如何确保这些代码真正可靠？

软件质量保障长期依赖测试与人工审查，然而测试只能针对有限的具体场景逐一验证，无论用例设计多么周全，都无法对程序在所有可能情况下的行为作出完备保证；人工审查则依赖工程师的经验与注意力，其可靠性随代码规模增大而系统性下降。

为此，MoonBit 0.9 版本将形式化验证作为重点突破方向，在全球范围内率先设计并落地了一套AI原生的形式化证明系统：让 AI 自动构造复杂的证明、生成规范，并证明规范的准确性，从而可以保证AI生成大规模可靠的高质量代码。形式化验证不再需要逐一验证具体场景下的程序行为，而是通过数学方法直接证明程序在任意输入、任意条件下都满足预先定义的约束，无论 AI 以何种方式、何种速度生成代码，每一段输出都必须通过独立的数学验证才能进入下一环节。

随着 AI Coding 在软件工程中承担越来越核心的角色，这道数学层面的全面防线，将成为安全可靠开发的根本前提。

以二分查找这个经典例子为例。二分查找看似简单，却是出了名的”容易写错”——Joshua Bloch 在 2006 年曾撰文指出，Java 标准库中的二分查找实现存在整数溢出 bug，这段代码在生产环境中运行了近十年才被发现。

上面这张截图展示了 MoonBit 中对二分查找的完整验证。左侧是带有合约和循环不变量的函数实现，右侧是谓词定义文件，底部终端显示验证全部通过。

合约：函数的数学承诺。 函数开头的 proof_requires(sorted(xs)) 和 proof_ensures(binary_search_ok(xs, key, result)) 是这个函数与外界立下的契约——调用方承诺输入数组有序，函数承诺返回值一定是正确的：找到了就确实是目标元素，没找到就意味着目标值确实不在数组中。这不是注释或文档，而是会被机器严格检验的约束。

谓词：用数学语言消除歧义。 右侧的 .mbtp 文件精确定义了合约中每一个概念的含义。比如”有序”被定义为”对任意合法下标 i ≤ j，都有 xs[i] ≤ xs[j]”；”查找正确”被定义为”返回 Some(i) 时 xs[i] 等于目标值，返回 None 时数组中不存在等于目标值的元素”。所有概念都用量词和逻辑连接词表达，没有自然语言的模糊空间。

循环不变量：连接代码与证明的桥梁。 代码底部 where 块中的 proof_invariant 描述了循环每一轮迭代都必须维持的性质：搜索区间 [i, j) 始终合法，区间左侧的元素都小于目标值，区间右侧的元素都大于目标值。正是这些不变量将一段普通的循环代码，变成了可以被逐步推理的证明对象。

验证过程。  当开发者执行 moon prove 时，MoonBit 工具链会将程序逻辑和谓词定义翻译为约束求解问题，再交由 Z3 等 SMT 求解器进行自动化验证。求解器会逐一检查：循环不变量在初始状态是否成立、每次迭代后是否仍然维持、循环结束时能否推导出后置条件。这里验证的不是”某几组输入下程序碰巧返回了正确结果”，而是一个覆盖所有可能输入的数学证明——对于任意长度的有序数组和任意目标值，这段二分查找实现都满足其合约承诺。

更进一步，MoonBit还可以通过AI完成一棵 AVL 树的验证：https://github.com/moonbit-community/verified/tree/main/avl

形式化验证最令人望而却步的部分，历来是证明的编写。循环不变量需要恰到好处——足够强才能推导出后置条件，又足够弱才能在每次迭代中维持

MoonBit 的一个重要探索方向，是利用 AI 来降低这个门槛。

事实上，前文中的二分查找和 AVL 树的证明——包括循环不变量、谓词定义和 proof_assert 引导链——大部分是由 AI Agent 辅助生成的。开发者给出函数实现和合约意图，AI 推导出候选的不变量和中间断言，再由定理证明器进行严格的机器检验。

这形成了一个精妙的协作模式：AI 负责”猜”，证明器负责”查”。AI 可能会犯错——它生成的不变量可能太弱、中间断言可能遗漏——但错误的猜测不会通过证明器的审查。证明器要么确认每一步推理都成立，要么明确指出哪个目标无法证明，AI 据此修正再试。最终交付的始终是经过数学验证的结果，不存在”AI 幻觉”蒙混过关的可能。

这意味着开发者无需精通形式化方法，也能获得形式化验证级别的可靠性保障。当大多数 AI 编程工具还停留在”帮你写代码”的阶段时，MoonBit 的 AI 辅助验证走向了更深一层：不仅帮你写代码，还帮你证明代码是对的。（https://github.com/moonbit-community/verified）

目前形式化验证方案大致可以分为两类。

第一类是对现有语言叠加验证能力，如 C 语言的 Frama-C、Java 的 OpenJML、Rust 的 Creusot。这类方案的优势在于可以直接验证生产代码，但它们面临一个结构性问题：验证和语言是分离的。合约和规约只能通过注释或宏注入，对语言本身而言是不可见的”外挂”。这意味着 IDE 无法原生理解验证注解，补全、跳转、错误提示都需要额外的插件支持；构建系统不知道验证步骤的存在，开发者需要手动维护额外的工具链；当语言本身升级时，验证工具往往要滞后数月甚至数年才能跟上。

第二类是专门为验证设计的语言，如微软的 Dafny、Rocq（原 Coq）、Lean 等。这类方案的验证能力更强，语言和证明系统天然一体。但它们缺乏作为通用编程语言的生态基础——没有成熟的包管理、没有广泛的第三方库、没有大规模的工业用户群。其中 Rocq 和 Lean 表达力极强，但如果要验证 C 或 Java 这样的现有语言，需要在证明器中重新建模目标语言的语义，工程量巨大且难以维护。Ada/SPARK 是少有的兼具工业验证能力和实际部署经验的方案，但它绑定在 Ada 生态中，与现代云原生和 Web 开发场景几乎没有交集。

MoonBit 的差异化在于垂直整合：合约、谓词、循环不变量和 proof_assert 都是语言语法的一等成员，而不是藏在注释或宏里的二等公民。编译器直接理解这些结构，这意味着 IDE 可以像处理普通代码一样对验证注解提供语法高亮、自动补全、类型检查和错误定位；moon prove 作为构建系统的内置命令，与 moon build、moon test 并列，开发者不需要配置额外的工具链或切换工作流。从编写代码到编写证明，再到运行验证，全部在同一套语言、同一个 IDE、同一条命令行中完成。

再加上 AI 辅助降低了证明编写的门槛，MoonBit 试图同时解决”不好用”和”门槛高”这两个历史性难题——不仅让验证更强大，更让它对普通开发者真正可用。

在这样的背景下，形式化验证的意义也在发生变化。它不再只是面向极少数安全关键场景的专门技术，而正在成为提升软件可信度的一条现实路径。MoonBit 希望通过语言设计、AI 辅助和工具链整合，持续降低验证的使用门槛，让约束表达、证明生成和结果检查更自然地进入开发流程。

我们期待，随着这套能力不断完善，“证明代码正确”能够像编写测试和运行构建一样，逐步成为软件工程中的常规实践。

本次0.9发布还伴随着其他关键性更新，详情请查看MoonBit 2026.4 Jaderabbit