關于人工智能將如何改變軟件開發，人們已經討論了太多維度：效率提升、代碼生成、自動測試、低代碼乃至“人人都是程序員”。
但有一個關鍵變化，卻長期被忽視——人工智能正在把形式化驗證這一曾經高度學術化、門檻極高的技術，推向軟件工程的現實主流。
近日，一篇由劍橋大學分布式系統研究員 Martin Kleppmann 撰寫的博客講述了人工智能對形式化驗證的推動。
他在博客中表示，目前正有三個趨勢同時發生：
形式化驗證的成本正在快速下降；
AI 生成的代碼迫切需要一種可替代人工審查的可靠機制；
形式化驗證的確定性恰好彌補了大模型本身的概率性與不精確性。
這三者的疊加，很可能會把形式化方法從小眾研究領域，推向軟件工程的主流實踐。
真正的瓶頸，或許不再是技術，而是行業是否愿意更新認知，接受一個全新的軟件開發范式。
形式化驗證的困境
形式化驗證并不是新概念。數十年來，研究者已經開發出一系列證明助手和面向證明的編程語言，如 Rocq、Isabelle、Lean、F*、Agda 等。
這些工具允許開發者為代碼寫出精確定義的形式化規范，并通過嚴格的數學推理，證明程序在所有情況下都滿足這些規范——包括那些幾乎不可能通過測試覆蓋到的極端邊界條件。
借助這些工具，人類已經完成過一些“里程碑式”的工程實踐：例如經過形式化驗證的操作系統微內核、C 語言編譯器以及密碼學協議棧。這些成果充分說明，形式化驗證在技術上是可行的，甚至在理論上近乎完美。
但問題從來不在“能不能”，而在“值不值”。
長期以來，形式化驗證幾乎只存在于研究機構和少數高安全等級項目中。即便是在醫療設備、航空航天等傳統意義上的高可靠軟件領域，工業界對形式化方法的采用也極為有限。根本原因在于：證明本身太難、太慢、太貴。
一個經典案例是 seL4 微內核。到 2009 年為止，該內核的實現代碼只有約 8700 行 C 代碼，但為了完成形式化驗證，卻投入了大約 20 人/年的時間，編寫了超過 20 萬行 Isabelle 證明腳本。
平均下來，每一行實現代碼，需要配套 20 多行證明，并耗費接近半個工作日的人工成本。更重要的是，全球真正掌握這類證明技能的人可能只有幾百人，這種知識高度依賴經驗與“行話”，幾乎無法規模化。
從經濟學角度看，這是一筆算不過來的賬。對絕大多數軟件系統而言，軟件缺陷帶來的預期損失，往往低于采用形式化驗證所需的成本。更現實的一點是，軟件缺陷的代價往往由用戶承擔，而非開發者本身。這使得形式化驗證長期處于“理論正確、實踐不劃算”的尷尬位置。
AI 改寫形式化驗證
這種格局，正在被人工智能打破。
近幾年，基于大模型的編程助手不僅在生成實現代碼方面突飛猛進，也開始在證明腳本的編寫上展現出驚人的潛力。目前，這一過程仍然需要具備專業背景的人類工程師進行引導，但趨勢已經十分清晰：隨著模型能力的提升，證明生成本身有望在未來幾年內高度自動化。
一旦證明的主要成本從“人類專家”轉移到“機器計算”，形式化驗證的經濟學基礎將被徹底改寫。驗證不再是一項奢侈品，而可能成為軟件開發流程中的常規步驟。
更重要的是，AI 不僅降低了形式化驗證的成本，也制造了對形式化驗證的剛性需求。當越來越多的代碼由人工智能生成時，傳統的人工代碼審查將迅速成為瓶頸。相比讓人類逐行檢查 AI 寫出的程序，更合理的路徑是：讓 AI 為自己生成的代碼提供可驗證的正確性證明。
如果一段代碼能夠被形式化地證明滿足其規范，那么它是否由人類“手寫”已經不再重要。相比那些看似精巧、卻暗藏缺陷的“手工代碼”，一段附帶嚴格證明的 AI 生成代碼，反而更值得信任。
從這個角度看，證明腳本本身，可能正是大模型最理想的應用場景之一。即便模型在推理過程中產生“幻覺”，也不會造成實質性風險——因為任何不成立的證明都會被證明檢查器拒絕，迫使模型重新嘗試。而證明檢查器本身是一小段經過嚴格驗證的核心代碼，幾乎不可能被繞過。
當然，這并不意味著軟件世界將從此“零缺陷”。隨著證明過程被自動化，真正的挑戰將前移到規范本身的定義：如何確保我們證明的，正是我們真正關心的屬性？形式化規范的書寫依然需要經驗、判斷力與嚴謹思維。但即便如此，定義規范的成本，仍然遠低于手工完成完整證明。
未來，人工智能甚至有可能參與規范的編寫本身，在自然語言需求與形式化語言之間進行轉換。雖然這一過程存在語義細節丟失的風險，但相較于當前軟件工程中的不確定性，這是一種可管理、可校驗的風險。
如果這一切成為現實，軟件開發的范式將發生根本變化。開發者只需要用高層次、聲明式的方式描述“代碼應該具備什么性質”，剩下的實現與證明過程交由 AI 完成。就像今天的程序員早已不關心編譯器生成的機器碼一樣，未來我們或許也不再需要閱讀具體實現代碼。
參考資料：
https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html
分享
