当 AI 主宰写代码，MoonBit 嵌入「形式化验证」让 Bug 清零

前言AI 写代码越来越快真正的问题却越来越尖锐生成成本在下降正确性却不会自动提升。代码能跑不等于代码是对的功能看起来完整也不代表系统真的可靠。对于金融清算、操作系统内核、自动驾驶、航空航天等高可靠场景软件需要的不只是“能运行”而是“可以被严格证明正确”。这也是形式化验证重新进入大众视野的原因。所谓形式化验证就是用数学和逻辑的方法对程序进行严格证明确保代码在所有可能情况下都满足预期性质。它不是多跑几轮测试也不是继续堆测试覆盖率而是直接回答一个更底层的问题程序是否始终满足某个关键约束。最近硅谷 AI 圈也开始重新重视这个方向。Axiom 宣布完成 2 亿美元 A 轮融资核心目标就是打造能自动验证代码的 AI 系统让大模型的推理过程像数学证明一样严格每一步都可验证。AI 不再只是“猜一个大概正确的答案”而是把问题转化为严格的逻辑推演再交给验证器做确定性检查。这也说明形式化验证正在从少数安全关键领域重新进入 AI 软件工程的主视野。而 MoonBit 最近公布的 0.9 版本最值得关注的地方就在于它正在尝试把形式化验证从“少数专家才能使用的高门槛能力”推进为“普通开发者也能逐步采用的工程能力”。而且可以用 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 不是只做了形式化验证这一件事。无论是工作区支持、稳定的正则表达式能力还是 JavaScript 后端和标准库层面的持续调整背后都指向同一个方向MoonBit 正在把“新语言”的潜力继续落到更完整的工程体验上。MoonBit 0.9 版本详情https://www.moonbitlang.cn/blog/moonbit-0-9-releaseMoonBit 与形式化验证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正在尝试把这件事从理念往工程实践里推进。