2026年7月9日 AutoVerus將40小時的證明編寫變成3次LLM呼叫。訣竅在於知道何時放棄。 AutoVerus利用LLM智慧體網路為Rust程式碼產生Verus正確性證明，透過由SMT求解器回饋驅動的生成-修復-消除迴圈，自動化超過90%的證明義務。 model-checkingautoverusrustverification
2026年7月8日 LLM可以生成Rust程式碼，但形式化證明完全是另一回事。 大型語言模型能寫出品質驚人的Rust程式碼，但當你要求形式化證明時，它們會幻覺出不變量，並編造出沒有任何驗證器接受的語法。本文介紹它們真正做對了什麼、在哪裡崩潰，以及如何善用牠們。 model-checkingllmrustformal-proofs
2026年7月5日 不寫一行證明也能證明 Rust 程式碼正確，但狀態空間就是代價 像 Kani 這樣的模型檢驗工具讓你可以用斷言代替形式化證明來驗證 Rust 性質。棘手之處在於，當你的迴圈沒有小的邊界時會發生什麼。 model-checkingrustverificationformal-methods
2026年6月26日 你的依賴項目可以讀取磁碟上的任何檔案。cap-std 讓它們必須先取得權限。 Rust 的標準函式庫將環境檔案系統權限授予每一個依賴項目。cap-std 以權能式 API 取而代之，強制程式碼在開啟路徑之前先證明自己擁有存取權。 capability-based-securityrustcap-stdsandboxing
2026年6月22日 讓 Type Checker 看得見的錯誤：停止拋出，開始回傳 拋出的例外會讓型別系統看不到失敗路徑。以下是為什麼明確回傳錯誤能讓你的程式碼更誠實，以及如何在不折磨自己的前提下採用這種做法。 type-level-correctnesserror-handlingtypescriptrust
2026年6月21日 Rust newtype 讓錯誤狀態在編譯期就無法被表示，而且完全免費 一個單欄位的 wrapper struct 就能在不增加任何位元組開銷的情況下，抓出單位混淆與型別錯用的 bug。 type-level-correctnessrustnewtypeszero-cost-abstractions
2026年5月28日 Rust 的 Mutation Testing 確實有效，但編譯時間會讓你痛苦 cargo-mutants 能找出那些只會假裝驗證程式碼的測試。以下是 mutation testing 在 Rust 中的運作原理、它能抓到什麼問題，以及編譯時間的成本是否值得。 deep-divesmutation-testingrustcargo-mutantstest-quality
2026年5月23日 Rust 的 Property-Based 測試：找出單元測試漏掉的 Bug 範例導向的測試只涵蓋你想得到的輸入。Property-based 測試會產生隨機資料、檢查不變條件，並將失敗縮減到最小的反例。 deep-divesrustproperty-based-testingquickcheckproptest
2026年5月21日 Rust Runtime Contracts 在 Release Build 中可以零成本，但編譯器不會幫你做到 Rust 會自動剝除 debug assertions，但真正的 design-by-contract 需要的遠不止 debug_assert!。以下說明如何建立零成本的 runtime contracts，讓它們從你的 release binary 中完全消失。 deep-divesrustruntime-contractsperformance
