LLM可以生成Rust程式碼，但形式化證明完全是另一回事。
大型語言模型能寫出品質驚人的Rust程式碼，但當你要求形式化證明時，它們會幻覺出不變量，並編造出沒有任何驗證器接受的語法。本文介紹它們真正做對了什麼、在哪裡崩潰，以及如何善用牠們。
LLM能寫出可以編譯甚至通過的Rust程式碼。但牠們目前還無法可靠地寫出形式化證明，來證實程式碼對所有可能的輸入都是正確的。…
想法與洞見
探索 AI 優先開發、編碼護欄和可處置架構。
乾等 race condition 是最爛的測試策略
model checking 如何在數秒內碾壓你在生產環境跑幾天才能發現 concurrency bug 的做法，以及如何把它用在自己的程式碼上。
在生產環境裡等 race condition 冒出來，那不叫測試。那叫披著勤奮外衣的僥倖。 你可以把應用跑上幾週，盯著 metrics dashboard，最後照樣發布一個 concurrency bug——它只會在兩個 request 剛好打進同一個 cache eviction window…
無需學習時序邏輯即可對程式碼進行模型檢驗
像Kani這樣的有界模型檢驗器和像Alloy這樣的關係模型搜尋器，讓你能以普通的斷言和限制條件來驗證性質。你放棄了活性證明，換來的是以小時而非週為單位的學習曲線。
使用模型檢驗器不需要學習線性時序邏輯。Kani、CBMC和Alloy等工具讓你能以普通的斷言和關係限制條件來驗證性質。你放棄了證明活性性質的能力，換來的是以小時而非週為單位的學習曲線，而對於大多數軟體錯誤來說，這是一筆值得的交易。…
不寫一行證明也能證明 Rust 程式碼正確，但狀態空間就是代價
像 Kani 這樣的模型檢驗工具讓你可以用斷言代替形式化證明來驗證 Rust 性質。棘手之處在於，當你的迴圈沒有小的邊界時會發生什麼。
不寫一行證明也能證明 Rust 程式碼正確。幹這活的工具叫做模型檢驗器，目前對 Rust 最實用的一個是 AWS 開發的 Kani。你寫普通的 Rust 斷言，Kani 把它們轉成數學命題，對所有可能的輸入進行檢驗。不需要定理證明器，不需要證明輔助工具，也不需要一頭栽進 Coq 半年出不來。…
無法對分散式protocol做單元測試，但可以做模型檢驗
分散式缺陷在部署後修復成本高昂。模型檢驗能讓你在寫下第一行實作程式碼之前就發現它們。以下是如何使用 TLA+ 做到這一點。
你無法對分散式protocol做單元測試。單元測試在一台機器上以單一順序執行一個程序。而你的protocol在五台機器上以十個程序、以你無法控制的順序執行。這兩種現實之間的鴻溝，正是缺陷藏身之處。…
跨環境複製 `.env` 檔案不是配置策略
基礎設施團隊如何使用按上下文劃分的 DSL 來管理 dev、staging 和 production 之間的配置，使環境差異顯式且類型安全。
staging 環境運作正常。production 環境運作異常。它們的 檔案之間的差異高達 400 行，其中一半是再也沒人相信的註解。上個月有人往 staging 裡加了 。沒人往 production 裡加。應用程式還是啟動了，使用了硬式編碼的預設值，現在你的功能旗標不同步了。…
語法約束解碼: 讓每個 token 都強制 LLM 輸出有效語法
LLM 會對語法產生幻覺，因為它們以機率方式採樣 token。語法約束解碼在每一步過濾詞表，只輸出保持語法有效性的 token。
讓 LLM 產生一個 JSON 物件，它最終一定會輸出一個末尾逗號、字串裡未轉義的換行符，或者在一個本該有引號鍵的位置輸出 bare word。這個錯誤不是模型的 bug。它是自迴歸採樣工作方式的必然結果：在每一步，模型都會把自己的詞表裡每個 token 都當作候選，包括那些會讓部分輸出在語法上 invalid 的…
從英語翻譯到主題很容易。使其具備確定性才是真正的問題。
你可以從簡單的英語描述中生成設計令牌，但前提是將該描述視為帶有模式契約和snapshot test的限界上下文DSL。
是的，你可以用英語描述一個主題，並得到一個可用的設計系統。關鍵在於，這段英語描述不是提示詞。它是源檔案。和任何源檔案一樣，它需要編譯器、類型系統和測試。…
丟掉語法檔案：用純 TypeScript 寫你的 DSL parser
對於大多數 bounded-context 的 DSL 來說，parser generator是大材小用。parser combinator讓你可以用與應用程式相同的語言建構可用的parser，無需產生程式碼，也無需建置步驟。
如果你曾經開啟過 Yacc 的語法檔案，並疑惑為什麼建構一門語言需要學習第二門語言，那麼你並不孤單。parser generator很強大，但對於在 bounded context 中自然湧現的小型 DSL 來說，它們幾乎總是大材小用。…
執行時設定錯誤是你選擇允許的生產故障
如何使用模式驗證和建置時檢查，在應用程式開始處理流量之前捕獲設定錯誤。
你的應用程式在週五晚上三小時後拋出了 。stack trace指向設定物件中一個深層巢狀的屬性。值是 。有人在未更新驗證邏輯的情況下，將 變更推送到了生產環境。 這不是執行時缺陷。這是策略失敗。你讓不受信任的資料未經檢查就進入了系統。 大多數團隊被動地驗證設定。缺少環境變數會導致當機。無效的 URL…