9 posts
AutoVerus利用LLM智慧體網路為Rust程式碼產生Verus正確性證明，透過由SMT求解器回饋驅動的生成-修復-消除迴圈，自動化超過90%的證明義務。
形式化驗證中最困難的部分從來不是驗證器本身，而是編寫證明。 給一位資深Rust工程師Verus——微軟研究院開發的基於SMT的驗證器——他可以在一個下午內為函式新增前置條件和後置條件註解。然後驗證器會以機械確定性告訴他，該函式是否對所有可能的輸入滿足這些契約。這部分令人滿意。…
大型語言模型能寫出品質驚人的Rust程式碼，但當你要求形式化證明時，它們會幻覺出不變量，並編造出沒有任何驗證器接受的語法。本文介紹它們真正做對了什麼、在哪裡崩潰，以及如何善用牠們。
LLM能寫出可以編譯甚至通過的Rust程式碼。但牠們目前還無法可靠地寫出形式化證明，來證實程式碼對所有可能的輸入都是正確的。…
像 Kani 這樣的模型檢驗工具讓你可以用斷言代替形式化證明來驗證 Rust 性質。棘手之處在於，當你的迴圈沒有小的邊界時會發生什麼。
不寫一行證明也能證明 Rust 程式碼正確。幹這活的工具叫做模型檢驗器，目前對 Rust 最實用的一個是 AWS 開發的 Kani。你寫普通的 Rust 斷言，Kani 把它們轉成數學命題，對所有可能的輸入進行檢驗。不需要定理證明器，不需要證明輔助工具，也不需要一頭栽進 Coq 半年出不來。…
Rust 的標準函式庫將環境檔案系統權限授予每一個依賴項目。cap-std 以權能式 API 取而代之，強制程式碼在開啟路徑之前先證明自己擁有存取權。
依賴樹中的任何 crate 都可以開啟 、寫入你的 目錄，或是列舉專案中的每一個檔案。Rust 的標準函式庫不會要求任何權限。它預設任何有能力呼叫 的程式碼，都有權碰觸作業系統允許的任何路徑。 cap-std 改變了這個預設。它是 Rust I/O module…
拋出的例外會讓型別系統看不到失敗路徑。以下是為什麼明確回傳錯誤能讓你的程式碼更誠實，以及如何在不折磨自己的前提下採用這種做法。
你的函式簽名說它回傳 。其實不然。它回傳 ，不然就爆炸。型別系統根本不知道有第二條路。 這就是基於例外的錯誤處理最根本的不誠實。每一次 都是一條編譯器看不見、無法檢查、也無法強制的控制流路徑。你會得到型別檢查完美通過、卻還是在正式環境崩潰的程式碼，只因為有人在三層呼叫之外忘了寫 。…
一個單欄位的 wrapper struct 就能在不增加任何位元組開銷的情況下，抓出單位混淆與型別錯用的 bug。
把 的使用者 ID 傳給一個預期接收訂單 ID 的函式，Rust 不會抱怨。兩者都是 。編譯器看到的是完全相同的型別，所以幫不上忙。你會在執行期才發現，通常是在正式環境，通常是在一次你以為安全的重構之後。 這正是 newtype 存在要消滅的 bug 類別。 newtype 是一個單欄位的 tuple…
cargo-mutants 能找出那些只會假裝驗證程式碼的測試。以下是 mutation testing 在 Rust 中的運作原理、它能抓到什麼問題，以及編譯時間的成本是否值得。
你已經達到 100% 的行覆蓋率。每個分支都被執行過，每個函式都被呼叫過。然後有人把你的計價邏輯裡的 改成 ，跑了一下測試，全部通過。 這不是理論上的問題。這就是你的測試執行了程式碼，卻沒有真正驗證行為時會發生的事。Coverage 衡量的是哪些行被執行過，而不是哪些輸出被檢查過。Mutation testing…
範例導向的測試只涵蓋你想得到的輸入。Property-based 測試會產生隨機資料、檢查不變條件，並將失敗縮減到最小的反例。
你寫了一個 函式。你用 和 測試它。通過了。你發布出去。 有個使用者傳入了一個單元素的 slice。你的函式把它遺漏了。他們開了一個 issue。你盯著測試檔案，納悶自己怎麼會漏掉這麼明顯的東西。 你之所以漏掉，是因為範例導向的測試只能抓到你預期中的 bug。測試套件裡的每一個…
Rust 會自動剝除 debug assertions，但真正的 design-by-contract 需要的遠不止 debug_assert!。以下說明如何建立零成本的 runtime contracts，讓它們從你的 release binary 中完全消失。
Rust 可以在開發階段強制執行 runtime contracts，並在 release build 中將它們完全抹除。但書在於，這門語言並未將 contracts 視為 first-class concept。你拿到了積木，但得自己動手組裝。 是最顯而易見的起點。它在 debug build 中執行，在…