Djinnlang 將 LLM 放進編譯器，並以可證明無歧義的規格作為後盾

程式設計師日益傾向撰寫形式規格，再讓 LLM 實作，並證明每個實作都符合其規格。推到這個極致，規格語言就成了新的程式語言——但有一個問題阻礙了這個替換：兩個程式可以都滿足同一份規格，行為卻仍然不同，所以還是得有人去讀產生的程式碼，才知道自己拿到的是哪一種行為。

Djinnlang 的答案是無歧義約束。除了證明其實作滿足規格外，LLM 還必須證明：任何其他滿足同一份規格的實作，在相同輸入上都會產生相同的輸出。這堵住了漏洞：產生的程式碼永遠不需要被閱讀，且隨時可以從規格重新產生，而不可信的模型可以撰寫程式碼，同時由驗證器嚴格檢查其成果。

這樣的安排使 LLM 實際上成為編譯器工具鏈的一部分。Djinnlang 程式只由規格組成——程式設計師從不撰寫可執行程式碼。取代傳統編譯器的，是一個符號轉譯器，將每份規格降為 Dafny 樁（stub）與證明義務，再由一個驅動程式框架（driver harness）統籌一個 LLM 來填入實作與證明，全部由 Dafny 驗證器檢查。

作為此範式可行的證據，作者展示 Djinnlang 能夠自我託管（self-hosting）：一個 LLM 依其自身的規格實作了 Djinnlang 轉譯器，而這個重新實作驗證了它自己。

證明規格無歧義，然後讓不可信的 LLM 擔任編譯器後端

若一份規格的所有實作行為都相同，閱讀產生的程式碼就不會提供任何程式設計師能據以行動的資訊。

證明決定性（determinism）限縮了模型能改變的範圍，因此不可信的模型可以撰寫程式碼，而由驗證器承擔信任。

經驗證的程式碼隨時可以從規格重新產生，因此它不再是必須維護與審查的資產。

在正確性證明的同時要求無歧義證明，會讓模型多花工夫，但把「看起來對」轉變成機器檢查過的宣稱。

當產生成本低廉而信任稀缺時，把人類的產物往上移一層：讓規格成為程式，讓決定性成為證明義務，把程式碼視為可拋棄的建置產物。

這篇論文於 2026 年 9 月 21 日提交至 arXiv，在多個範例上展示了此範式，並報告了自我託管：一個 LLM 依其規格實作了 Djinnlang 轉譯器，而這個重新實作驗證了它自己。作者將此結果定位為一種強形式的 AI 控制——不可信的模型負責撰寫，驗證器負責裁決。