6 posts
AutoVerus利用LLM智慧體網路為Rust程式碼產生Verus正確性證明，透過由SMT求解器回饋驅動的生成-修復-消除迴圈，自動化超過90%的證明義務。
形式化驗證中最困難的部分從來不是驗證器本身，而是編寫證明。 給一位資深Rust工程師Verus——微軟研究院開發的基於SMT的驗證器——他可以在一個下午內為函式新增前置條件和後置條件註解。然後驗證器會以機械確定性告訴他，該函式是否對所有可能的輸入滿足這些契約。這部分令人滿意。…
大型語言模型能寫出品質驚人的Rust程式碼，但當你要求形式化證明時，它們會幻覺出不變量，並編造出沒有任何驗證器接受的語法。本文介紹它們真正做對了什麼、在哪裡崩潰，以及如何善用牠們。
LLM能寫出可以編譯甚至通過的Rust程式碼。但牠們目前還無法可靠地寫出形式化證明，來證實程式碼對所有可能的輸入都是正確的。…
model checking 如何在數秒內碾壓你在生產環境跑幾天才能發現 concurrency bug 的做法，以及如何把它用在自己的程式碼上。
在生產環境裡等 race condition 冒出來，那不叫測試。那叫披著勤奮外衣的僥倖。 你可以把應用跑上幾週，盯著 metrics dashboard，最後照樣發布一個 concurrency bug——它只會在兩個 request 剛好打進同一個 cache eviction window…
像Kani這樣的有界模型檢驗器和像Alloy這樣的關係模型搜尋器，讓你能以普通的斷言和限制條件來驗證性質。你放棄了活性證明，換來的是以小時而非週為單位的學習曲線。
使用模型檢驗器不需要學習線性時序邏輯。Kani、CBMC和Alloy等工具讓你能以普通的斷言和關係限制條件來驗證性質。你放棄了證明活性性質的能力，換來的是以小時而非週為單位的學習曲線，而對於大多數軟體錯誤來說，這是一筆值得的交易。…
像 Kani 這樣的模型檢驗工具讓你可以用斷言代替形式化證明來驗證 Rust 性質。棘手之處在於，當你的迴圈沒有小的邊界時會發生什麼。
不寫一行證明也能證明 Rust 程式碼正確。幹這活的工具叫做模型檢驗器，目前對 Rust 最實用的一個是 AWS 開發的 Kani。你寫普通的 Rust 斷言，Kani 把它們轉成數學命題，對所有可能的輸入進行檢驗。不需要定理證明器，不需要證明輔助工具，也不需要一頭栽進 Coq 半年出不來。…
分散式缺陷在部署後修復成本高昂。模型檢驗能讓你在寫下第一行實作程式碼之前就發現它們。以下是如何使用 TLA+ 做到這一點。
你無法對分散式protocol做單元測試。單元測試在一台機器上以單一順序執行一個程序。而你的protocol在五台機器上以十個程序、以你無法控制的順序執行。這兩種現實之間的鴻溝，正是缺陷藏身之處。…