AI 編碼迴圈的正式驗證閘

AI 編碼代理（AI coding agents）的興起，為軟體開發生命週期引入了一個強大但不可預測的元素。雖然 LLM 能夠生成大量的程式碼，但它們在一致性、遵循嚴格的業務邏輯以及避免走捷徑方面往往面臨挑戰。挑戰不再僅僅是讓 AI 「更聰明」或改進提示詞（prompt），而是要建立一個系統，讓 AI 在物理上無法違反架構規則。

結構性背壓的概念

這種方法的核心思想是「結構性背壓」（structural backpressure）。開發者不應依賴 AI 遵循提示詞中提供的指令——因為 AI 可能會忽略或產生幻覺——而是可以將這些規則移入型別系統（type system）和編譯器中。

當規則被編碼進型別時，編譯器就成了最終的守門人。如果 AI 代理嘗試生成違反業務規則或安全約束的程式碼，編譯器將拒絕構建專案。這會建立一個回饋迴圈，讓 AI 因為編譯器的拒絕而「彈回」（bounced），迫使它修正其方法以滿足系統的正式要求。

正如專案作者 pyrex41 所指出的：

將規則從提示詞移至編譯器拒絕違反的型別中，然後讓 AI 編碼迴圈在這些拒絕中彈回。

實作防護型別

為了實作這一點，開發者使用「防護型別」（guard types）或能力（capabilities）。這些型別作為特定條件已滿足的證據。例如，與其傳遞一個原始字串作為使用者 ID，系統可能會要求一個 TenantAccess 型別。為了獲得此型別的實例，AI 必須呼叫一個特定的驗證函數，該函數會執行實際的檢查。

透過將這些防護型別的建構函式（constructor）設為私有或受限，你可以確保 AI 不會簡單地「幻覺」出一個成功的驗證。AI 必須與系統的真實狀態進行互動，以產生編譯器繼續執行所需的證據。

關鍵觀點：未經驗證建構函式的危險

雖然結構性背壓的理論框架非常強大，但其實作需要嚴格注意細節。社群討論中提出的一個關鍵點是：允許 AI 代理直接呼叫建構函式所帶來的風險。

如果 AI 可以簡單地呼叫像 (tenant-access user-id tenant-id true) 這樣的建構函式，它實際上就繞過了驗證程序。AI 並不是在證明存取權限；它是在斷言它。正如 @singron 指出的：

如果 AI 在呼叫建構函式，那麼它就能做出自己的斷言並推導出它想要的任何結果。這看起來很反常。AI 應該使用 tenant-access 的結果來推導出使用者是租戶的成員，但如果它們可以直接呼叫 (tenant-access user-id tenant-id true)，那麼它們就能為任何事物「證明」tenant-access。

為了減輕這種風險，防護型別的建構函式應該被命名並受到極度嚴格的審查。一個常見的模式是將這些建構函式命名為 newUnverified，並將其使用限制在系統中最受信任的部分，例如 JWT 解析器或直接的資料庫查詢。這確保了 AI 代理無法建立「偽造」的證據來滿足編譯器。

結論：決定論優於智能

將 AI 整合進編碼迴圈的目標並非建立一個更聰明的代理，而是建立一個更具決定論（deterministic）的環境。透過將證明責任從提示詞轉移到執行期（runtime）和編譯器，開發者可以建立「夠陡峭，讓 AI 無法翻越圍欄」的護欄。

最終，最穩健的 AI 輔助開發工作流是將 AI 視為不可信的參與者，並使用健全的程式設計原則——例如強型別（strong typing）和基於能力的安全性（capability-based security）——來強制執行軟體的架構完整性。