修復缺陷是容易的部分。弄清楚它為什麼存在才是重要的
大多數團隊修復缺陷後就繼續前進。同樣的缺陷反覆出現。以下是如何在費根審查內部執行因果分析，從而停止兩次編寫同樣的缺陷。
每個團隊都有一個反覆出現的缺陷。分頁中的差一錯誤。認證middleware中缺失的空值檢查。三個衝刺前有人「修復過」的結帳race condition。 你並不是三次寫了同一個缺陷。你寫了三個具有相同原因的不同缺陷。修復處理的是症狀。原因依然隱藏。…
想法與洞見
探索 AI 優先開發、編碼護欄和可處置架構。
Pull Request 審查能發現 15-30% 的缺陷。資料 50 年前就已給出答案。
IBM、AT&T、HP 與 Microsoft 的多項研究均證實，非正式程式碼審查大約能發現四分之一的缺陷。以下是資料實際說明的內容、該比例偏低的原因以及解決方法。
非正式程式碼審查能夠發現被審程式碼中 15% 到 30% 的缺陷。這不是觀點，而是在四十年、多家公司、數十項研究中反覆驗證的結論。 麥可·費根於 1976 年在 IBM 記錄了這一資料。1987 年 AT&T 貝爾實驗室的研究發現了 20%。1996 年惠普的研究發現了 25%。2013…
通用檢查清單什麼都抓不到。結構化檢查清單能發現60%的缺陷。
大多數審查檢查清單都是複製貼上的良好願望列表。Fagan inspection風格的結構化檢查清單基於實際缺陷數據構建，針對特定工件類型，並在個人準備階段使用。以下是如何構建一個有效的檢查清單。
如果你的團隊有一份程式碼審查檢查清單，它很有可能躺在沒人打開的維基頁面上。上面大概寫著「check for off-by-one errors」和「verify error handling」之類的話。這些話都是對的。但也過於籠統，不足以改變行為。 一份告訴你「check for…
大型語言模型可以預先審查你的程式碼，但它無法主持會議
費根審查需要四到六個人、兩小時才能審完250行程式碼。大型語言模型可以透過承擔準備工作與檢查清單的執行來削減這部分成本，但它無法取代人類角色去發現最昂貴的缺陷。
一次完整的費根審查需要一名主持人、一名朗讀員、兩到四名審查員，以及作者本人。團隊以每小時125行的速度，花費兩小時審查大約250行程式碼。這意味著一次小小的改動就要消耗八到十二人時。 大型語言模型可以在不到一秒內讀完250行程式碼。它可以執行檢查清單、標記可疑模式，並在任何人開啟檔案之前就產生一份結構化的缺陷紀錄。…
Fagan Inspections 在測試前發現90%的缺陷。然後我們不再使用它。
Michael Fagan 在 IBM 設計的結構化審查流程，能在程式碼進入編譯器之前捕獲幾乎全部缺陷。但它也消耗了專案總工時的15%–20%。本文解釋軟體史上最有效的審查方法為何消失，以及團隊究竟失去了什麼。
1976年，Michael Fagan 在 IBM Systems Journal 上發表了一篇論文，描述了一種審查流程，其有效性使之成為軟體品質的金標準。Fagan Inspections 在尚未執行任何測試之前，就能捕獲全部缺陷的60%到90%。NASA…
你最優秀的審查員也會遺漏大多數缺陷。Fagan 於1976年在IBM測量了這一點。
即使是高級工程師，在非結構化審查中也只能發現一小部分缺陷。Michael Fagan 在IBM的研究揭示了原因，並建構了結構化審查流程來解決這一問題。
兩位高級工程師審查同一份拉取請求。一位標記了缺失的空值檢查。另一位發現了清理路徑中的競態條件。兩人都沒有發現全部問題。 如果你只指派了一位審查員，那麼其中一個缺陷就會被發布上線。這不是技能差距。這是人類注意力的可預測特性，而 Michael Fagan 於1976年在IBM記錄了這一現象。 Fagan…
大多數程式碼審查只能發現20%的缺陷。Fagan Inspection能發現90%。
非正式的程式碼審查只能發現15%到30%的缺陷。Fagan Inspection是一種有50年歷史的結構化流程，持續報告60%到90%的缺陷移除率。以下是它的運作原理、團隊迴避它的原因，以及如何執行輕量級版本。
大多數程式碼審查只能發現本應找到的缺陷的15%到30%。這不是猜測。IBM在20世紀70年代就測量過，AT&T、惠普和微軟的研究也在數十年間反覆確認了這一範圍。 非正式審查成本低廉、非同步進行、 socially…
AutoVerus將40小時的證明編寫變成3次LLM呼叫。訣竅在於知道何時放棄。
AutoVerus利用LLM智慧體網路為Rust程式碼產生Verus正確性證明，透過由SMT求解器回饋驅動的生成-修復-消除迴圈，自動化超過90%的證明義務。
形式化驗證中最困難的部分從來不是驗證器本身，而是編寫證明。 給一位資深Rust工程師Verus——微軟研究院開發的基於SMT的驗證器——他可以在一個下午內為函式新增前置條件和後置條件註解。然後驗證器會以機械確定性告訴他，該函式是否對所有可能的輸入滿足這些契約。這部分令人滿意。…
LLM可以生成Rust程式碼，但形式化證明完全是另一回事。
大型語言模型能寫出品質驚人的Rust程式碼，但當你要求形式化證明時，它們會幻覺出不變量，並編造出沒有任何驗證器接受的語法。本文介紹它們真正做對了什麼、在哪裡崩潰，以及如何善用牠們。
LLM能寫出可以編譯甚至通過的Rust程式碼。但牠們目前還無法可靠地寫出形式化證明，來證實程式碼對所有可能的輸入都是正確的。…
乾等 race condition 是最爛的測試策略
model checking 如何在數秒內碾壓你在生產環境跑幾天才能發現 concurrency bug 的做法，以及如何把它用在自己的程式碼上。
在生產環境裡等 race condition 冒出來，那不叫測試。那叫披著勤奮外衣的僥倖。 你可以把應用跑上幾週，盯著 metrics dashboard，最後照樣發布一個 concurrency bug——它只會在兩個 request 剛好打進同一個 cache eviction window…