工程師們正對軟體驗證感到興奮！這或許令人意外，因為驗證長期以來一直被認為僅在非常小眾的案例中有用（頂多如此；最糟的情況則是實務上不可行、無用或完全浪費時間）。然而，圍繞它的炒作顯然已經來臨：Google Trends 顯示，過去兩年對形式驗證/形式方法的搜尋量大幅飆升，大家都在學習 Lean，新的規格語言不斷出現，並且有專案致力於端對端驗證大型應用程式（例如 Signal Shot 專案）。

這種興奮的主要驅動因素是 AI 程式碼生成。首先，AI 代理程式在我們對其編寫的程式碼的理解上留下了一個空白，從而產生了對其他正確性保證手段的需求。其次，它們使驗證本身更快、更容易融入實際軟體開發。第三，或許對企業來說最重要的是，如果程式編寫變得超快速，那麼未來所有的進展都將在軟體正確性保證領域。

Antithesis 的 Will Wilson 在其題為「我們贏了，接下來呢？」的演講中，宣告了這個傳統上小眾領域的勝利（這場演講是 Bug Bash 2026 的開幕演講，非常精彩，並為驗證社群在主流採用後的未來提供了一些好點子）。

在這種勝利的背景下，回顧一篇反對形式驗證的經典論文「Social Processes and Proofs of Theorems and Programs」是很有趣的。該論文寫於 1979 年，作者們表示：「我們相信……程式驗證注定會失敗。我們看不出它將如何能夠影響任何人對程式的信心。」

我將逐一檢視論文中的論點，並探討最近的發展（如果有）是否使其失效。這是一次有趣的練習，而非完全嚴肅的探討：論文實際上並未聲稱所有形式方法都注定失敗（只針對完全驗證）。此外，驗證是否會成為軟體工程的常規部分，這一點遠未確定（我們所見的僅是早期興趣的跡象）。儘管如此，在 2026 年重新審視 50 年前被視為根本性障礙的問題，希望能有所助益且有趣。

在論證中，論文作者反對將程式設計變得更像數學的觀點，即每個程式都對應一個需要證明定理。他們說：等等，即使在數學中，證明定理也不是過程的終點。相反，證明是第一步，也是溝通的手段。真正重要的部分發生在其他數學家內化證明時，以及該聲明與其他數學分支或物理現實接觸時。整個過程有助於聲明的可信度。

對此沒有異議：程式的證明不必完全等同於數學。（該論點是針對特定的動機，而非軟體驗證的根本原理。）

論點的第一部分是這樣的：存在一個非形式化的現實世界需求（相關人員對需求有共同的直觀理解）。這個直觀的、非形式化的需求需要被轉化為形式規格，而這個過程本身是非形式化的。在這個未經驗證的過程中，很多東西可能會丟失或被誤解。

這是一個合理的觀點。反駁的觀點是，規格比實現更接近非形式化需求（因此更容易發現錯誤）。此外，現代規格語言（如 Quint）能夠以互動方式檢查規格及其所有邊緣情況，以確保其真正符合我們的直覺。

論點的第二部分說，規格只有在獨立於實現時才具有價值。鑑於軟體開發的迭代性質，這幾乎是不可能的。一旦獨立性喪失，我們實際上只是在對齊規格和實現（並可能在兩者中引入類似的錯誤）。

我認為這即使在過去也不是一個強有力的論點，尤其是在有程式碼生成代理程式參與的情況下。每當獲得額外的理解時，這對整個開發過程都是有益的。人類作為最終仲裁者，決定如何修改規格，重新審視最初的假設。程式碼生成代理程式可以被允許生成和修改程式碼，以及生成證明。然而，如果需要修改規格，只有人類才能作為正確性的最終仲裁者——這將我們帶回論點 2 的第一部分。

在論證了驗證作為溝通手段的弊端後，作者們將注意力轉向了全自動驗證器的潛力（在這種情況下，我們可以對程式被證明是正確的事實感到高興，即使證明沒有引發同事之間的社會過程）。作者們認為，全自動驗證器極不可能被製造出來。

在此期間，自動驗證器的開發取得了一些進展，儘管人類的努力（無論是編寫證明，還是編寫合適的模型進行模型檢查）仍然至關重要。然而，由 LLM 驅動的工具正在迅速縮小這一差距。Igor Konnov 在他的文章「Formal proofs for distributed protocols with AI may be closer than you think」中，描述了他使用 Lean 證明 Ben-Or 協定安全性的經驗。

作者們聲稱，僅回應「已驗證」或「未驗證」的驗證器無助於理解，並會讓程式設計師對如何進一步修改程式碼感到茫然。此外，他們認為，擁有一個已驗證的程式可能會降低對其他防禦層（例如監控、速率限制等）的激勵。

這是一個薄弱的論點，依賴於對驗證工具和程式設計師在自動驗證存在下的行為方式的最壞假設。

演算法和現實世界系統之間存在巨大差異，這點被正確地指出。雖然演算法的規格通常簡潔明瞭，但現實世界系統的規格是臨時的、不穩定的且混亂的。此外，在大多數現實世界系統中，演算法簡單易懂（因此驗證它們的價值不大）。

確實，並非所有系統都需要驗證。然而，在過去幾十年和幾年中，出現了一些推動更多驗證的變化：

「追求程式正確性的願望是建設性的且有價值的。但驗證的整體觀點忽略了接受類似於真實數學證明正確性標準，或類似於真實工程結構可靠性標準所能帶來的益處。在追求經濟可行性的過程中，願意通過回收成功的設計來引導創新，信任同行社群的運作——所有這些使工程和數學真正起作用的機制，都被掩蓋在對完美可驗證性的徒勞追求之下。」

我完全贊同這個論點。事實上，對系統進行完全驗證很少是實現可靠性的最佳途徑。所有其他追求軟體正確性的努力都同樣有價值。而且這兩者並非競爭關係：對帶來正確性的最佳方法的關注增加才是最重要的。

結論：這是一篇非常有趣的論文。作者們提出了關於形式驗證不是解決所有正確性問題的萬靈丹的觀點。事實上，正如他們指出的，軟體正確性遠不止驗證：還有工程流程、商業考量、額外的防禦層等等。

由於他們專注於完全驗證，論文作者錯誤地低估了形式方法的不同部分對於整體理解、更好的設計選擇或更高的開發速度的有用性。所有這些都隨著 AI 程式碼生成代理程式編寫程式碼而得到放大，使人類負責指定需要編寫的內容，並檢查其是否按照給定規格編寫。這也使程式碼生成代理程式的工作更容易：驗證為它們提供了一種閉環的方式，以判斷它們所寫的內容是否正確。

感謝兩位 FM 同業，Thomas Pani 和 Ranadeep Biswas，就這篇論文和這篇文章進行了有益的討論。也很想聽聽那些仍然認為形式方法無用的人的看法。