前言

AI 寫代碼越來越快，真正的問題卻越來越尖銳：生成成本在下降，正確性卻不會自動提升。

代碼能跑，不等于代碼是對的；功能看起來完整，也不代表系統(tǒng)真的可靠。對于金融清算、操作系統(tǒng)內(nèi)核、自動駕駛、航空航天等高可靠場景，軟件需要的不只是“能運行”，而是“可以被嚴格證明正確”。

這也是形式化驗證重新進入大眾視野的原因。所謂形式化驗證，就是用數(shù)學(xué)和邏輯的方法，對程序進行嚴格證明，確保代碼在所有可能情況下都滿足預(yù)期性質(zhì)。它不是多跑幾輪測試，也不是繼續(xù)堆測試覆蓋率，而是直接回答一個更底層的問題：程序是否始終滿足某個關(guān)鍵約束。

最近，硅谷 AI 圈也開始重新重視這個方向。，核心目標就是打造能自動驗證代碼的 AI 系統(tǒng)，讓大模型的推理過程像數(shù)學(xué)證明一樣嚴格，每一步都可驗證。AI 不再只是“猜一個大概正確的答案”，而是把問題轉(zhuǎn)化為嚴格的邏輯推演，再交給驗證器做確定性檢查。

這也說明，形式化驗證正在從少數(shù)安全關(guān)鍵領(lǐng)域，重新進入 AI 軟件工程的主視野。而 MoonBit 最近公布的 0.9 版本，最值得關(guān)注的地方就在于：它正在嘗試把形式化驗證從“少數(shù)專家才能使用的高門檻能力”，推進為“普通開發(fā)者也能逐步采用的工程能力”。而且可以用 AI 自動構(gòu)造證明，證明程序的可靠性。

MoonBit 0.9 版本最新進展

如果只看最值得關(guān)注的變化，MoonBit 0.9 其實主要回答了兩件事：一是如何讓代碼的可靠性更早進入開發(fā)流程，二是如何讓多模塊工程的組織方式更自然。

過去幾個月，MoonBit 生態(tài)增長很快：庫的數(shù)量從約 2500 增長到 7000 多，累計下載超過 300 萬，核心用戶規(guī)模和海外社區(qū)熱度也在持續(xù)上升。它正在從“有潛力的新語言”，走向“工程可用、AI 友好、生態(tài)快速擴展”的新階段。

在工程組織上，MoonBit 0.9 引入了 workspace 支持，更適合多模塊項目的開發(fā)方式。開發(fā)者可以在一個倉庫中組織多個模塊，并用統(tǒng)一的 moon.work 進行管理。模塊邊界依然清晰，但檢查、測試、清理和信息查看都可以在 workspace 根目錄統(tǒng)一完成；如果依賴版本不一致，還能通過同步機制自動對齊。

這意味著 MoonBit 對大型項目的支持又往前走了一步。對于包含多個模塊、相互依賴、但又需要獨立維護和復(fù)用的工程來說，這類能力不是錦上添花，而是決定項目能否長期演進的基礎(chǔ)設(shè)施。

除了多模塊工程組織能力，MoonBit 0.9 還把形式化驗證進一步推進到了工具鏈層面。開發(fā)者已經(jīng)可以直接在代碼中通過 proof_ensure 寫下函數(shù)應(yīng)滿足的性質(zhì)，在 moon.pkg 中開啟證明選項，再通過 moon prove 執(zhí)行驗證。換句話說，這不再只是一個停留在概念層面的方向，而是開始真正進入日常開發(fā)流程的能力。

當然，MoonBit 0.9 不是只做了形式化驗證這一件事。無論是工作區(qū)支持、穩(wěn)定的正則表達式能力，還是 JavaScript 后端和標準庫層面的持續(xù)調(diào)整，背后都指向同一個方向：MoonBit 正在把“新語言”的潛力，繼續(xù)落到更完整的工程體驗上。

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

MoonBit 與形式化驗證

1、為什么 MoonBit 現(xiàn)在開始談形式化驗證

MoonBit 團隊這段時間一直在強調(diào)一個方向：AI 原生的軟件構(gòu)建環(huán)境。

對于一門新語言來說，這件事并不容易。大模型的代碼能力很大程度上依賴訓(xùn)練語料，而新語言天然缺少歷史數(shù)據(jù)。MoonBit 的做法不是等待“語料足夠多”，而是通過 AI 原生的語言設(shè)計和對 Agent 友好的工具鏈，讓模型更多依賴語言語義和工具反饋去推理，而不是單純依賴記憶。

在這樣的條件下，大模型已經(jīng)能夠在較少人工干預(yù)的情況下生成數(shù)萬行規(guī)模的高質(zhì)量 MoonBit 代碼，甚至在一些實驗性案例中，根據(jù)規(guī)范和工具反饋合成接近編譯器級別的軟件系統(tǒng)。

問題也正出在這里：當 AI 已經(jīng)可以大規(guī)模生成代碼，軟件工程接下來的核心矛盾，就不再只是“怎么寫得更快”，而是“怎么確認這些代碼真的可靠”。

測試和模糊測試當然依然重要，但它們本質(zhì)上依賴樣例和覆蓋范圍，只能說明程序在某些輸入下沒有出錯，很難證明程序在所有情況下都滿足關(guān)鍵性質(zhì)。要真正打開 AI 軟件黑盒，形式化驗證幾乎是繞不過去的一步。

2、把形式化驗證做成語言的一等能力

今天主流的形式化驗證方案，大致分成兩類：一種是在現(xiàn)有語言上疊加驗證能力，優(yōu)點是能直接作用于生產(chǎn)代碼，但缺點是驗證與語言本身割裂；另一種是專門為驗證設(shè)計的語言，驗證能力更強，但通常缺乏通用編程語言所需的工程生態(tài)。

MoonBit 想做的，是盡量補上這兩者之間的斷層。

它的差異化，在于垂直整合。合約、謂詞、循環(huán)不變量和 proof_assert 都是語言語法的一等成員，而不是藏在注釋或宏里的補丁。編譯器直接理解這些結(jié)構(gòu)，IDE 可以像處理普通代碼一樣處理驗證注解，moon prove 也直接成為工具鏈內(nèi)置命令，與 moon build、moon test 并列存在。

更關(guān)鍵的是，MoonBit 還在嘗試用 AI 降低形式化驗證最難的那部分門檻。過去，證明最難寫的是循環(huán)不變量、中間斷言、規(guī)約設(shè)計這些需要高度經(jīng)驗的內(nèi)容。MoonBit 0.9 的探索方向，是讓開發(fā)者能夠直接在代碼中寫下性質(zhì)約束，再借助 AI 生成候選證明結(jié)構(gòu)，并交給驗證器做嚴格審查。AI 負責(zé)“猜”，證明器負責(zé)“查”。

需要說明的是，形式化驗證并不取代測試，也不自動替代規(guī)約設(shè)計本身。測試仍然負責(zé)發(fā)現(xiàn)性能、集成和運行環(huán)境中的問題，而形式化驗證關(guān)注的是：在給定前提下，程序是否必然滿足某個關(guān)鍵性質(zhì)。

當然，形式化驗證證明的是“實現(xiàn)是否滿足規(guī)約”，而不是自動替代規(guī)約設(shè)計本身。規(guī)約是否完整、前提是否成立、外部系統(tǒng)是否可信，依然是工程上必須認真處理的問題。

3、MoonBit 中的形式化驗證：寫代碼的同時寫證明

以二分查找這個經(jīng)典例子為例。二分查找看似簡單，卻是出了名的“容易寫錯”。Java 核心開發(fā)者、 《Effective Java》作者 Joshua Bloch 在 2006 年曾專門撰文指出，Java 標準庫中的二分查找實現(xiàn)存在整數(shù)溢出 bug，而這段代碼在生產(chǎn)環(huán)境中運行了近十年才被發(fā)現(xiàn)。

上圖展示了 MoonBit 中對二分查找的完整驗證。左側(cè)是帶有合約和循環(huán)不變量的函數(shù)實現(xiàn)，右側(cè)是謂詞定義文件，底部終端則顯示驗證全部通過。

在 MoonBit 里，形式化驗證并不是額外附加的一層文檔，而是和代碼本身一起構(gòu)成程序的一部分。

• 合約：函數(shù)的數(shù)學(xué)承諾

函數(shù)開頭的 proof_requires(sorted(xs)) 和 proof_ensures(binary_search_ok(xs, key, result))，就是這個函數(shù)與外界立下的契約：調(diào)用方承諾輸入數(shù)組有序，函數(shù)承諾返回值一定正確——找到了，就確實是目標元素；沒找到，就意味著目標值確實不在數(shù)組中。這不是注釋，也不是文檔，而是會被機器嚴格檢驗的約束。

• 謂詞：用數(shù)學(xué)語言消除歧義

右側(cè)的 .mbtp 文件精確定義了合約中每一個概念的含義。比如，“有序”被定義為“對任意合法下標 i ≤ j，都有 xs[i] ≤ xs[j]”；“查找正確”被定義為“返回 Some(i) 時 xs[i] 等于目標值，返回 None 時數(shù)組中不存在等于目標值的元素”。所有概念都通過量詞和邏輯連接詞表達，沒有自然語言留下的模糊空間。

• 循環(huán)不變量：連接代碼與證明的橋梁

代碼底部 where 塊中的 proof_invariant，描述了循環(huán)每一輪迭代都必須維持的性質(zhì)：搜索區(qū)間 [i, j) 始終合法，區(qū)間左側(cè)的元素都小于目標值，區(qū)間右側(cè)的元素都大于目標值。正是這些不變量，把一段普通的循環(huán)代碼變成了可以被逐步推理的證明對象。

• 驗證過程：驗證的不是樣例，而是所有可能輸入

當開發(fā)者執(zhí)行 moon prove 時，MoonBit 工具鏈會將程序邏輯和謂詞定義翻譯為約束求解問題，再交由 Z3 等 SMT 求解器進行自動化驗證。求解器會逐一檢查：循環(huán)不變量在初始狀態(tài)是否成立、每次迭代后是否仍然維持、循環(huán)結(jié)束時能否推出后置條件。這里驗證的，不是“某幾組輸入下程序碰巧返回了正確結(jié)果”，而是一個覆蓋所有可能輸入的數(shù)學(xué)證明——對于任意長度的有序數(shù)組和任意目標值，這段二分查找實現(xiàn)都滿足其合約承諾。

說得更直白一點，MoonBit 在這里做的事情，是把“這段代碼為什么一定是對的”從口頭解釋，變成了機器可以逐步檢查的邏輯鏈條。

MoonBit 還展示了借助 AI 完成 AVL 樹驗證的能力。這也引出了一個更關(guān)鍵的問題：如果形式化驗證本身仍然過于復(fù)雜，它又該如何真正走向大規(guī)模使用？

展望

過去幾年，軟件行業(yè)已經(jīng)反復(fù)見過類似教訓(xùn)：系統(tǒng)表面上看起來工作正常，但真正決定可靠性的關(guān)鍵約束，并沒有被清晰表達，也沒有被系統(tǒng)驗證。一旦進入高復(fù)雜度、高后果場景，這種隱患就會被迅速放大。

形式化驗證是目前少數(shù)能夠提供數(shù)學(xué)級正確性保證的路徑之一，但它長期受困于門檻高、成本高、工作流割裂。MoonBit 正在嘗試打破這個局面：把驗證融入語言設(shè)計本身，用 AI 自動化最困難的證明環(huán)節(jié)，再用現(xiàn)代工具鏈把它接進普通開發(fā)者的日常流程。

如果 AI 時代的軟件工程真的要進入下一個階段，那么“讓代碼不僅能寫出來，還能被證明是對的”，很可能會成為其中最關(guān)鍵的一步。

而 MoonBit，正在嘗試把這件事從理念，往工程實踐里推進。