2026年8月23日 Symbolic Execution 找到了我 94% 測試覆蓋率都漏掉的整數溢位 你的單元測試只檢查特定輸入。Symbolic execution 檢查所有可能的輸入。以下是它的運作原理、成本，以及從哪裡開始。 additional-strategiessymbolic-executiontestingverification
2026年8月3日 如何證明你的程式沒有執行時錯誤（以及為什麼你很可能會放棄嘗試） 抽象解釋讓你在執行前就能證明執行時錯誤不可能發生。以下說明它實際上如何運作、為什麼很困難，以及它在你的工具鏈中扮演什麼角色。 abstract-interpretationstatic-analysisruntime-errorsverification
2026年7月25日 真的有人驗證了 1 萬行程式碼零缺陷嗎？IBM 做到了，而且方法比結果更離奇。 Cleanroom software engineering 承諾透過 mathematical verification 而非 debugging 實現零缺陷增量。我們查看 IBM 的實際專案資料，看看這一說法是否成立。 cleanroom-correctnesszero-defectsverificationcase-study
2026年7月9日 AutoVerus將40小時的證明編寫變成3次LLM呼叫。訣竅在於知道何時放棄。 AutoVerus利用LLM智慧體網路為Rust程式碼產生Verus正確性證明，透過由SMT求解器回饋驅動的生成-修復-消除迴圈，自動化超過90%的證明義務。 model-checkingautoverusrustverification
2026年7月6日 無需學習時序邏輯即可對程式碼進行模型檢驗 像Kani這樣的有界模型檢驗器和像Alloy這樣的關係模型搜尋器，讓你能以普通的斷言和限制條件來驗證性質。你放棄了活性證明，換來的是以小時而非週為單位的學習曲線。 model-checkingtemporal-logicformal-methodsverification
2026年7月5日 不寫一行證明也能證明 Rust 程式碼正確，但狀態空間就是代價 像 Kani 這樣的模型檢驗工具讓你可以用斷言代替形式化證明來驗證 Rust 性質。棘手之處在於，當你的迴圈沒有小的邊界時會發生什麼。 model-checkingrustverificationformal-methods
2026年6月14日 測試無法證明兩個函式等價。真正有用的是這個。 N-version programming 假設你的實作結果一致。我們來看看為什麼測試不夠、SMT solver 如何真正證明等價，以及該在「夠好就好」和「形式化驗證」之間劃下哪條界線。 n-version-programmingequivalence-testingformal-methodsverification
