2026年7月6日 無需學習時序邏輯即可對程式碼進行模型檢驗 像Kani這樣的有界模型檢驗器和像Alloy這樣的關係模型搜尋器，讓你能以普通的斷言和限制條件來驗證性質。你放棄了活性證明，換來的是以小時而非週為單位的學習曲線。 model-checkingtemporal-logicformal-methodsverification
2026年7月5日 不寫一行證明也能證明 Rust 程式碼正確，但狀態空間就是代價 像 Kani 這樣的模型檢驗工具讓你可以用斷言代替形式化證明來驗證 Rust 性質。棘手之處在於，當你的迴圈沒有小的邊界時會發生什麼。 model-checkingrustverificationformal-methods
2026年6月15日 Differential Testing 不需要形式化證明也能運作，但 Common-Mode Failure 才是真正的陷阱 Differential testing 讓你在不知道正確答案的情況下找到 bug。問題是，有相關性的錯誤看起來就像一致。以下是找出盲點的方法。 n-version-programmingdifferential-testingformal-methodstrust
2026年6月14日 測試無法證明兩個函式等價。真正有用的是這個。 N-version programming 假設你的實作結果一致。我們來看看為什麼測試不夠、SMT solver 如何真正證明等價，以及該在「夠好就好」和「形式化驗證」之間劃下哪條界線。 n-version-programmingequivalence-testingformal-methodsverification
