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月7日 乾等 race condition 是最爛的測試策略 model checking 如何在數秒內碾壓你在生產環境跑幾天才能發現 concurrency bug 的做法，以及如何把它用在自己的程式碼上。 model-checkingrace-conditionsconcurrencytesting
2026年7月6日 無需學習時序邏輯即可對程式碼進行模型檢驗 像Kani這樣的有界模型檢驗器和像Alloy這樣的關係模型搜尋器，讓你能以普通的斷言和限制條件來驗證性質。你放棄了活性證明，換來的是以小時而非週為單位的學習曲線。 model-checkingtemporal-logicformal-methodsverification
2026年7月5日 不寫一行證明也能證明 Rust 程式碼正確，但狀態空間就是代價 像 Kani 這樣的模型檢驗工具讓你可以用斷言代替形式化證明來驗證 Rust 性質。棘手之處在於，當你的迴圈沒有小的邊界時會發生什麼。 model-checkingrustverificationformal-methods
2026年7月4日 無法對分散式protocol做單元測試，但可以做模型檢驗 分散式缺陷在部署後修復成本高昂。模型檢驗能讓你在寫下第一行實作程式碼之前就發現它們。以下是如何使用 TLA+ 做到這一點。 model-checkingdistributed-systemstlaplusprotocol-design
