5 posts
Cleanroom software engineering 承諾透過 mathematical verification 而非 debugging 實現零缺陷增量。我們查看 IBM 的實際專案資料，看看這一說法是否成立。
1980 年代軟體業的平均水平是每千行程式碼 30 到 60 個缺陷。IBM 的 Cleanroom 團隊交付了一個 2 萬行的編譯器增量，在測試中發現了 53 個缺陷。也就是每 KLOC 2.6 個。一些 1 萬行的獨立增量在進入系統測試時，沒有發現任何缺陷。 最離奇的部分？程式設計師被禁止執行自己的程式碼。…
AutoVerus利用LLM智慧體網路為Rust程式碼產生Verus正確性證明，透過由SMT求解器回饋驅動的生成-修復-消除迴圈，自動化超過90%的證明義務。
形式化驗證中最困難的部分從來不是驗證器本身，而是編寫證明。 給一位資深Rust工程師Verus——微軟研究院開發的基於SMT的驗證器——他可以在一個下午內為函式新增前置條件和後置條件註解。然後驗證器會以機械確定性告訴他，該函式是否對所有可能的輸入滿足這些契約。這部分令人滿意。…
像Kani這樣的有界模型檢驗器和像Alloy這樣的關係模型搜尋器，讓你能以普通的斷言和限制條件來驗證性質。你放棄了活性證明，換來的是以小時而非週為單位的學習曲線。
使用模型檢驗器不需要學習線性時序邏輯。Kani、CBMC和Alloy等工具讓你能以普通的斷言和關係限制條件來驗證性質。你放棄了證明活性性質的能力，換來的是以小時而非週為單位的學習曲線，而對於大多數軟體錯誤來說，這是一筆值得的交易。…
像 Kani 這樣的模型檢驗工具讓你可以用斷言代替形式化證明來驗證 Rust 性質。棘手之處在於，當你的迴圈沒有小的邊界時會發生什麼。
不寫一行證明也能證明 Rust 程式碼正確。幹這活的工具叫做模型檢驗器，目前對 Rust 最實用的一個是 AWS 開發的 Kani。你寫普通的 Rust 斷言，Kani 把它們轉成數學命題，對所有可能的輸入進行檢驗。不需要定理證明器，不需要證明輔助工具，也不需要一頭栽進 Coq 半年出不來。…
N-version programming 假設你的實作結果一致。我們來看看為什麼測試不夠、SMT solver 如何真正證明等價，以及該在「夠好就好」和「形式化驗證」之間劃下哪條界線。
你建了一個 n-version 系統。同一個關鍵函式的三份獨立實作、一個選出多數結果的 voter，以及一種自己已經搞定單點故障的溫暖感覺。 你並沒有證明這些函式是等價的。你只證明了它們編譯得過。 N-version programming 的概念是：如果其中一個實作有 bug，其他的大概不會有，所以 voter…