前言

AI 寫代碼越來(lái)越快，真正的問(wèn)題卻越來(lái)越尖銳：生成成本在下降，正確性卻不會(huì)自動(dòng)提升。

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

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

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

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

MoonBit 0.9 版本最新進(jìn)展

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

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

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

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

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

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

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

MoonBit 與形式化驗(yàn)證

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

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

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

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

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

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

2、把形式化驗(yàn)證做成語(yǔ)言的一等能力

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

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

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

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

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

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

3、MoonBit 中的形式化驗(yàn)證：寫代碼的同時(shí)寫證明

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

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

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

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

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

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

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

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

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

• 驗(yàn)證過(guò)程：驗(yàn)證的不是樣例，而是所有可能輸入

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

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

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

展望

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

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

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

而 MoonBit，正在嘗試把這件事從理念，往工程實(shí)踐里推進(jìn)。