有了AI，形式化驗證的痛苦正在消失。OpenAI剛用Astra模型，給10個數學難題做出了機器能查的證明。這背後靠的是Lean——一門既能寫代碼、又能寫證明的語言。測試只能找bug，證明能消滅bug。普通測試測得再多，也總有漏網之魚。但Lean能覆蓋所有情況，直接證明程序沒錯。比如數組越界，你得先證明索引不越界，代碼才能跑通。AI把成本從「10倍」降到了接近零。以前做形式化驗證，花的時間是寫代碼的10倍。最煩的是後期維護，改一行代碼可能讓一堆證明全崩。現在有了AI，改證明就像改代碼一樣輕鬆。同事用AI一周就搞定了zlib庫的翻譯和關鍵證明，過去這活兒得干幾個月。Z3負責找錯，Lean負責證明。de Moura還創造了另一個工具Z3。它像全自動黑箱，適合找漏洞，但沒法證明漏洞不存在。而且稍微改下條件順序，它的證明就可能崩。Lean則是一步步交互著來，每一步都清清楚楚，AI也能跟著一步步學。人只管說目標，AI負責填步驟。以後人類只要寫好「規格說明」——也就是告訴AI你想要什麼。具體怎麼證明、怎麼優化，全交給AI。手寫證明不會死，但純人工的模式會越來越少。形式化驗證不再是專家特權，馬上就要變成日常工具了。
