前言

AI 写代码越来越快，真正的问题却越来越尖锐：生成成本在下降，正确性却不会自动提升。

代码能跑，不等于代码是对的；功能看起来完整，也不代表系统真的可靠。对于金融清算、操作系统内核、自动驾驶、航空航天等高可靠场景，软件需要的不只是“能运行”，而是“可以被严格证明正确”。

这也是形式化验证重新进入大众视野的原因。所谓形式化验证，就是用数学和逻辑的方法，对程序进行严格证明，确保代码在所有可能情况下都满足预期性质。它不是多跑几轮测试，也不是继续堆测试覆盖率，而是直接回答一个更底层的问题：程序是否始终满足某个关键约束。

最近，硅谷 AI 圈也开始重新重视这个方向。，核心目标就是打造能自动验证代码的 AI 系统，让大模型的推理过程像数学证明一样严格，每一步都可验证。AI 不再只是“猜一个大概正确的答案”，而是把问题转化为严格的逻辑推演，再交给验证器做确定性检查。

这也说明，形式化验证正在从少数安全关键领域，重新进入 AI 软件工程的主视野。 而 MoonBit 最近公布的 0.9 版本，最值得关注的地方就在于：它正在尝试把形式化验证从“少数专家才能使用的高门槛能力”，推进为“普通开发者也能逐步采用的工程能力”。而且可以用 AI 自动构造证明，证明程序的可靠性。

MoonBit 0.9 版本最新进展

如果只看最值得关注的变化，MoonBit 0.9 其实主要回答了两件事： 一是如何让代码的可靠性更早进入开发流程，二是如何让多模块工程的组织方式更自然。

过去几个月，MoonBit 生态增长很快：库的数量从约 2500 增长到 7000 多，累计下载超过 300 万，核心用户规模和海外社区热度也在持续上升。它正在从“有潜力的新语言”，走向“工程可用、AI 友好、生态快速扩展”的新阶段。

在工程组织上，MoonBit 0.9 引入了 workspace 支持，更适合多模块项目的开发方式。开发者可以在一个仓库中组织多个模块，并用统一的 moon.work 进行管理。模块边界依然清晰，但检查、测试、清理和信息查看都可以在 workspace 根目录统一完成；如果依赖版本不一致，还能通过同步机制自动对齐。

这意味着 MoonBit 对大型项目的支持又往前走了一步。对于包含多个模块、相互依赖、但又需要独立维护和复用的工程来说，这类能力不是锦上添花，而是决定项目能否长期演进的基础设施。

除了多模块工程组织能力，MoonBit 0.9 还把形式化验证进一步推进到了工具链层面。开发者已经可以直接在代码中通过 proof_ensure 写下函数应满足的性质，在 moon.pkg 中开启证明选项，再通过 moon prove 执行验证。换句话说，这不再只是一个停留在概念层面的方向，而是开始真正进入日常开发流程的能力。

当然，MoonBit 0.9 不是只做了形式化验证这一件事。无论是工作区支持、稳定的正则表达式能力，还是 Java 后端和标准库层面的持续调整，背后都指向同一个方向：MoonBit 正在把“新语言”的潜力，继续落到更完整的工程体验上。

• MoonBit 0.9 版本详情：https://www.moonbitlang.cn/blog/moonbit-0-9-release

MoonBit 与形式化验证

1、为什么 MoonBit 现在开始谈形式化验证

MoonBit 团队这段时间一直在强调一个方向：AI 原生的软件构建环境。

对于一门新语言来说，这件事并不容易。大模型的代码能力很大程度上依赖训练语料，而新语言天然缺少历史数据。MoonBit 的做法不是等待“语料足够多”，而是通过 AI 原生的语言设计和对 Agent 友好的工具链，让模型更多依赖语言语义和工具反馈去推理，而不是单纯依赖记忆。

在这样的条件下，大模型已经能够在较少人工干预的情况下生成数万行规模的高质量 MoonBit 代码，甚至在一些实验性案例中，根据规范和工具反馈合成接近编译器级别的软件系统。

问题也正出在这里：当 AI 已经可以大规模生成代码，软件工程接下来的核心矛盾，就不再只是“怎么写得更快”，而是“怎么确认这些代码真的可靠”。

测试和模糊测试当然依然重要，但它们本质上依赖样例和覆盖范围，只能说明程序在某些输入下没有出错，很难证明程序在所有情况下都满足关键性质。要真正打开 AI 软件黑盒，形式化验证几乎是绕不过去的一步。

2、把形式化验证做成语言的一等能力

今天主流的形式化验证方案，大致分成两类：一种是在现有语言上叠加验证能力，优点是能直接作用于生产代码，但缺点是验证与语言本身割裂；另一种是专门为验证设计的语言，验证能力更强，但通常缺乏通用编程语言所需的工程生态。

MoonBit 想做的，是尽量补上这两者之间的断层。

它的差异化，在于垂直整合。合约、谓词、循环不变量和 proof_assert 都是语言语法的一等成员，而不是藏在注释或宏里的补丁。编译器直接理解这些结构，IDE 可以像处理普通代码一样处理验证注解，moon prove 也直接成为工具链内置命令，与 moon build、moon test 并列存在。

更关键的是，MoonBit 还在尝试用 AI 降低形式化验证最难的那部分门槛。过去，证明最难写的是循环不变量、中间断言、规约设计这些需要高度经验的内容。MoonBit 0.9 的探索方向，是让开发者能够直接在代码中写下性质约束，再借助 AI 生成候选证明结构，并交给验证器做严格审查。 AI 负责“猜”，证明器负责“查”。

需要说明的是，形式化验证并不取代测试，也不自动替代规约设计本身。测试仍然负责发现性能、集成和运行环境中的问题，而形式化验证关注的是：在给定前提下，程序是否必然满足某个关键性质。

当然，形式化验证证明的是“实现是否满足规约”，而不是自动替代规约设计本身。规约是否完整、前提是否成立、外部系统是否可信，依然是工程上必须认真处理的问题。

3、MoonBit 中的形式化验证：写代码的同时写证明

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

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

在 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 在这里做的事情，是把“这段代码为什么一定是对的”从口头解释，变成了机器可以逐步检查的逻辑链条。

MoonBit 还展示了借助 AI 完成 AVL 树验证的能力。这也引出了一个更关键的问题：如果形式化验证本身仍然过于复杂，它又该如何真正走向大规模使用？

展望

过去几年，软件行业已经反复见过类似教训：系统表面上看起来工作正常，但真正决定可靠性的关键约束，并没有被清晰表达，也没有被系统验证。一旦进入高复杂度、高后果场景，这种隐患就会被迅速放大。

形式化验证是目前少数能够提供数学级正确性保证的路径之一，但它长期受困于门槛高、成本高、工作流割裂。MoonBit 正在尝试打破这个局面：把验证融入语言设计本身，用 AI 自动化最困难的证明环节，再用现代工具链把它接进普通开发者的日常流程。

如果 AI 时代的软件工程真的要进入下一个阶段，那么“让代码不仅能写出来，还能被证明是对的”，很可能会成为其中最关键的一步。

而 MoonBit，正在尝试把这件事从理念，往工程实践里推进。