當 AI 主宰寫代碼，MoonBit 嵌入「形式化驗證」讓 Bug 清零

前言

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 不是只做了形式化驗證這一件事。無論是工作區支持、穩定的正則表達式能力，還是 JavaScript 后端和標準庫層面的持續調整，背后都指向同一個方向：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，正在嘗試把這件事從理念，往工程實踐里推進。