MoonBit 0.9 发布：AI 自动生成可证明的代码
过去四个月，MoonBit 生态进入指数增长阶段。新增生态规模已接近此前三年的总和的三倍：库的数量从约 2500 增长到 7500 多，累计下载量达到 320 万，正逐步成长为中国智造相关基础软件领域中最具全球影响力的项目之一。
这背后，一个关键变化是 MoonBit 已经完成了在大模型上的冷启动。虽然 MoonBit 作为一门新语言，尚不具备丰富的历史语料，但凭借 AI 原生的设计和对 Agent 友好的工具链，大模型已经能够在极少人工干预的情况下，大规模生成高质量的 MoonBit 代码，甚至一次性生成完整的 C 编译器。
相关链接：https://www.moonbitlang.cn/blog/moonbit-c-compiler
随着代码生成能力快速提升，软件工程面临的核心问题愈发明显：如何确保 AI 在生成大量代码的同时，这些代码依然可靠，并满足应有的约束。
最近，外媒披露了一款借助 AI 生成并上线托管的应用。它表面上功能完整，但在认证、访问控制和数据库权限等基础环节存在一系列漏洞，最终导致上万条用户数据暴露。
相关链接：https://www.theregister.com/2026/02/27/lovable_app_vulnerabilities/
这个案例暴露出的核心问题恰恰在于：应用表面上可以正 常工作，但那些真正决定系统是否可靠的关键约束，既没有被清晰表达，也没有被系统验证。
测试和模糊测试仍然重要，但它们依赖样例和覆盖范围，难以直接回答“程序是否始终满足某个关键性质”这一问题。仅靠这些手段，仍难以从根本上杜绝这类问题。
形式化证明为这一难题打开了一条清晰的路径：不再依赖反复测试去逼近正确性，而是直接描述程序应满足的性质，并自动检查实现是否真正满足这些性质。更重要的是，在底层假设可靠的前提下，证明过程本身也可以由 AI 大规模自动生成。
MoonBit 0.9 的一项核心进展，是引入了一整套面向 AI 协作的形式化证明能力。它能够帮助 AI 自动构造复杂证明、生成规范，并对实现是否满足规范进行验证，从而为大规模生成高质量、可验证的代码提供支撑。这也是全球范围内在这一个领域的首次突破。