Basis 推出 LLM 驗證的解譯器
Ship Your Interpreter
Basis 發布了利用 LLM 撰寫並在 Lean 中證明的解譯器，證明其行為與實際 RISC‑V 編譯後的程式完全一致。
- 驗證方法：LLM 先自動生成 WHILE 語言的形式語義，然後在 Lean 中證明該語義與編譯後的二進位在所有程式上相符，並以此推匯出四個工具（型別檢查器、程式邏輯、抽象解譯器、編譯器）。
此研究展示 LLM 能自動撰寫語言語義並以 Lean 驗證，為將驗證擴充套件至真實語言奠定基礎。
譯文尚未完整，完整內容請切換至原文。
發布: 2026年10月16日
文章: Kiran Gopinathan, Nikhil Pimpalkhare, Yiyun Liu, Zenna Tavares
我們讓 LLM 撰寫精確的數學規則，或是小型程式語言的正式語義，說明該語言應如何運作。接著，我們使用 Lean（檢查數學證明的工具）證明，該語言的直譯器——執行該語言程式碼的程式——即使被編譯成 RISC‑V 計算機晶片能理解的低階指令後，也仍遵循這些規則。
LLM 的能力在發現並利用生產環境軟體漏洞方面急速提升，野外報導的 AI 助攻駭客案例亦日益增多。幸好，LLM 在撰寫經驗證軟體方面進展迅速：這類程式附帶經電腦檢驗的數學證明，能排除整體類別的錯誤。四月，我們的代理人建立了一個 JavaScript-to-WebAssembly 編譯器，但無法證明它保留了程式行為。數月後，我們的代理人驗證了 Linux 的 nftables 編譯器，該編譯器將防火牆規則轉譯為核心執行的指令。九月，MIT 研究人員 Frans Kaashoek 與 Nickolai Zeldovich 使用 AI 代理人驗證 xv6 作業系統核心，直至機器碼層面。
Basis 的目標是開發可行地擴充套件至所有軟體的驗證方法，確保支撐關鍵基礎設施的系統在設計上即安全，並能跟上攻擊者日益增長的能力。隨著 LLM 能力提升，瓶頸正由定理證明轉向規範問題：我們如何確信所證明的敘述真正捕捉到我們關心的行為？
要證明任何程式的特性，我們首先需要對它的行為進行數學描述。這從描述其所寫程式語言開始：每一條語句、迴圈與函式呼叫在執行時代表什麼。這些描述稱為 正式語義，雖可用筆與紙寫成，但越來越多地以 Lean 等證明助理呈現。少數語言已有正式語義（Standard ML、WebAssembly 以及透過 CompCert 的 C），RISC‑V 指令集亦擁有，許多處理器執行此指令集。開發每一種語義都耗費數年專業努力。
然而，大多數程式使用的語言並沒有正式語義，這成為在大規模部署驗證軟體的主要瓶頸：缺乏語義，便無法針對具體內容進行證明。自然的做法是利用 LLM 撰寫語義，但 LLM 會犯錯，破碎的語義會破壞所有基於其的證明。測試雖有幫助，但如下所示，語義即使通過所有測試仍可能錯誤。真正需要的是驗證語義本身的方法。
Languages without a formal semantics still have interpreters or compilers, which in practice define what their programs mean. Here we consider a radical idea: make the LLM prove that its semantics agrees with the real interpreter on every program, treating the interpreter as ground truth. To do this, we compile the interpreter to RISC-V, whose meaning is already formally defined. That gives an exact, if unreadable, description of what the interpreter does with any program. The LLM then writes readable rules for the language and proves in Lean that, for every possible program, those rules predict exactly what the compiled interpreter prints. If a rule is wrong, the proof gets stuck.
We report on an experiment where we had LLMs develop a semantics and its proof together for a small language. We used Lean to prove that the interpreter, the program that runs code written in that language, follows those rules even after being compiled into low-level machine instructions. The whole development, semantics and proof, is on GitHub. The rest of this post walks through this experiment, explaining first why semantics are the bottleneck for larger verification efforts and why tests aren’t sufficient to build trust in them. We then show how the proof process refined the semantics, how we handled the memory reasoning, and what tools we built on the result.
Every verified program starts from a semantics
Before you can prove a program does anything, you have to define how each operation transforms its state, that is, define its semantics. Most languages describe their semantics informally in prose, in a reference manual, and leave the concrete details to the compiler or interpreter implementation. A formal semantics writes the rules down in mathematics, precisely enough for a proof checker like Lean 4 to use them. Notable examples include CompCert’s semantics for C, CakeML’s for ML, and JSCert’s for JavaScript. Each one took years of expert effort, and often covers only a restricted subset of its language.
For this experiment we used an extended version of WHILE, the small
imperative language used in textbooks such as Nielson and Nielson’s
Semantics with Applications.
Our version has integers, strings, first-class functions with closures, if, while
and for loops, and runtime errors. Its interpreter is 1,855 lines of
C, and a WHILE program looks like this (it prints 55):
var i = 0;
var sum = 0;
while (i < 10) {
i = i + 1;
sum = sum + i;
}
println(sum);
The semantics an LLM wrote for WHILE is a set of rules, one for each kind of expression and statement. These rules describe how to evaluate an expression in terms of its subexpressions. For integer addition, the rule is:
st, env ⊢ l ⇓ a, st' st', env ⊢ r ⇓ b, st'' a + b = c
──────────────────────────────────────────────────────────
st, env ⊢ l + r ⇓ c, st''
A rule reads from the bottom up. The line at the bottom is its
conclusion. Starting from state st in environment env, the
expression l + r evaluates (⇓) to c and leaves state st''.
The state holds variable values, closures and everything printed so
far; the environment says which variables are in scope. The premises
above the line explain how the result follows from the subexpressions.
First l evaluates to a, leaving state st'. Then r evaluates to
b in that state, leaving st''. The final premise, a + b = c,
adds the two integer values using WHILE’s 64-bit wrapping arithmetic.
Take (1 + 1) + x, with state [x ↦ 5] and environment {x}:
x holds 5 and is in scope. Applying the rule gives:
[x ↦ 5], {x} ⊢ (1 + 1) ⇓ 2, [x ↦ 5] [x ↦ 5], {x} ⊢ x ⇓ 5, [x ↦ 5]
2 + 5 = 7
─────────────────────────────────────────────────────────────────────
[x ↦ 5], {x} ⊢ (1 + 1) + x ⇓ 7, [x ↦ 5]
也就是要評估 (1 + 1) + x，我們先評估 (1 + 1) 得到
2，再查詢 x 得到 5，將兩個值相加得到 7。
兩個子表示式都不改變狀態，因此 [x ↦ 5] 保持不變。
為了證明第一個前提，我們再次套用加法規則：
[x ↦ 5], {x} ⊢ 1 ⇓ 1, [x ↦ 5] [x ↦ 5], {x} ⊢ 1 ⇓ 1, [x ↦ 5]
1 + 1 = 2
───────────────────────────────────────────────────────────────
[x ↦ 5], {x} ⊢ 1 + 1 ⇓ 2, [x ↦ 5]
這些規則應用形成一棵樹，從各部分的值推導整個表示式的值。
LLM 在 Lean 中寫了大約 400 行這類規則（完整語義）。 每條規則單獨看起來合理，但終端使用者無法嚴謹地判斷它們是否真實描述 WHILE 程式在實際執行時的行為。
語義可能通過所有測試，仍然是錯誤的
檢查語義的常用方法是執行它。取一套測試用例， 分別在語義和實際解譯器下執行每個程式， 並比較它們輸出的結果。不幸的是，在實務上， 這個流程不足以建立對生成語義的信任。
例如，我們語義的早期版本通過了為 WHILE 解譯器生成的測試套件， 但在函式名稱達到 59 個字元時，與二進位程式不一致：
fn aaa…aaa() {} // a name of 59 a's
println("" + aaa…aaa);
semantics: <fn aaa…aaa>
binary: <fn aaa…aaa
語義表示將函式與字串連線時，會將其完整名稱放在 <fn 和 > 之間。二進位程式丟棄了結尾的 >，對於更長的名稱也會丟失部分名稱。
測試套件中沒有嘗試過如此長名稱的函式。
原因在於 C 解譯器，它在將值與 + 連線時將該值轉換為字串：
static char *stringify(Value v) {
...
char buf[64];
switch (v.kind) {
...
case VAL_FN: {
const char *name = v.as.fn->fn_expr->as.fn.name;
if (name)
snprintf(buf, sizeof buf, "<fn %s>", name);
else strcpy(buf, "<fn>");
break;
}
default: strcpy(buf, "<native fn>"); break;
}
...
}
stringify 直接返回字串值。其他任何值首先被輸出到堆疊上的 64 位元組緩衝區，
然後再複製到新分配的字串中。具名閉包以 snprintf 形式輸出為 <fn name>，匿名閉包則為 <fn>，內建專案則落入預設情況 <native fn>。
snprintf 只會將最多 63 個字元寫入 64 位元組緩衝區。最初的語義對連線與輸出使用相同的渲染規則，忽略了這一限制。為了證明與二進位程式的一致性，LLM 必須為連線提供獨立的渲染器。修正後的語義將閉包的渲染裁切為前 63 個位元組：
"" + f ⇓ take 63 ("<fn " ++ f ++ ">")
這類細節是實作在內部累積但沒有人明確記錄的原因，正是手工抄寫或由 LLM 編寫的語義會遺漏它的原因。 它也不是程式不會注意到的細節：動態語言的程式碼經常依賴函式的字串形式，用於日誌、以名稱為鍵的分派或比較序列化值。 即使是這樣簡單的違規也會破壞任何建立在該語義之上的驗證工作，並可能留下隱藏安全漏洞的空隙。 為了構建安全且可擴充的語義，我們需要超越測試，因為測試套件僅檢查某人（或代理）所想撰寫的程式。
釋出你的解譯器
釋出你的解譯器意味著將語義與實際執行的實作進行比對。編譯語言已經存在的解譯器， 並讓 LLM 證明二進位程式 精簡化 了語義，即兩者在每個程式輸出上保持一致。
我們 證明 的定理是這個：
theorem endToEnd_refinement :
∀ p c, Loaded interpRunLayout p (fillZero c) →
(∀ out, BigStep p out ↔ Halts c out 0) ∧
(Diverges c → ¬ ∃ out, BigStep p out)
定理說，對於任何 WHILE 程式 p，以及 任何 機器配置 c，若該機器配置滿足性質 Loaded，則語義與編譯後的二進位執行結果相符。Loaded interpRunLayout p (fillZero c) 這裡說明 c 是即將透過解譯器二進位執行 p 的機器。第一個結論 (∀ out, BigStep p out ↔ Halts c out 0) 表示語義推匯出輸出 out 的條件，僅當機器以退出碼 0 停止且已印出 out 時成立，即對於成功結束的程式，預測輸出相等。第二個結論說，若機器在任何程式 p 上無限執行（Diverges c），則語義不推導出任何結束輸出。
我們可以將此定理視為一個 交換方塊，說明語義與二進位在程式輸出上如何一致。在下方圖示中，頂部箭頭將程式 p 與語義預測的輸出 out 連結。底部箭頭將機器狀態 c 與二進位成功停止時印出的輸出連結。左側虛線為 Loaded 條件，將程式連結至該機器狀態。在此條件下，定理指出兩個輸出相同，右側以雙線表示。橘色箭頭顯示證明此一致性失敗時，LLM 會返回以修訂語義規則。
定理能在兩個方向上捕捉語義錯誤。若語義過於寬鬆，會推匯出二進位從未印出的輸出，左到右的一半失敗；若過於嚴格，則對二進位執行的某些行為沒有規則，右到左的一半失敗。無論哪種情況，LLM 都會得到一個無法完成的證明負擔。經驗顯示，這個負擔通常指向錯誤的規則。
RISC‑V 是一個開放式處理器設計。我們使用其以 Sail 撰寫並翻譯成 Lean 的形式模型，定義每條機器指令的執行方式。二進位即實際的 ELF 可執行檔：1,855 行 C 介譯器程式碼，由 gcc 編譯、連結至 dlmalloc 與 newlib，總計 25,336 條指令。對照而言，經 MachCSL 驗證的 xv6 核心包含 8,697 條 RISC‑V 指令，源自 6,593 行 C 與組合語言，雖然其證明亦涵蓋併發，而我們不需要。C 編譯器輸出、C 標準函式庫與記憶體分配器皆包含於本定理之內。欲信任此結果者，只需閱讀上述敘述、假設 Loaded 以及 Halts 與 Diverges 的兩個簡短定義。無需信任 BigStep，因為證明已將其與二進位對照。
同時開發語義與證明
開發證明迫使 LLM 必須考慮語義中的四項細節：
- 整數運算必須在 64 位元時進行捲回，因為對機器而言，將最小整數取負是不可滿足的；
for迴圈的初始化器必須忽略突發狀態，因為 C 程式是這樣做的；- 內建函式在
print與串接時必須以不同方式呈現； - 長的閉包名稱必須截斷至 63 位元組。
每一次修正都始於無法閉合的證明負擔，或是二進位執行與語義不符的情況。
63 位元組的截斷是代表性的例子。串接情形的證明需要語義的呈現與二進位相同，而對於長名稱則不符，因此證明負擔無法解除，直到規則被修改。
證明也捕捉到 LLM 產生的關於 C 函式庫的命題錯誤。LLM 說明瞭每個函式的功能，並將該說法與機器碼進行證明。分配器保留沒有堆滿的情況在單一 malloc(24) 後，realloc 命題對於尺寸包裹時為假，exit 程式寫入 errno 而其命題未說明，這些都以相同方式出現，成為無法關閉的義務。
分離邏輯使二進位證明可處理
LLM 撰寫了整個證明。大部分困難在於對記憶體的推理。我們需要 malloc 的規格，即分配記憶體的函式，才能證明分配新區塊時保持解譯器已持有的資料不變。即使 println("n = " + x) 分配三個字串並釋放其中兩個，在這些呼叫過程中，程式變數和半建構的結果必須保持完整。
教科書式的方法是為每個函式提供一個 Hoare 三元組，並附上一個 足跡，即函式可能寫入的位元組集合。足跡之外的記憶體事實在呼叫時保持不變。三元組 { P } code { Q } 讀作「如果 P 在 code 執行前成立，則 Q 在其後成立」。對於 malloc，此規格大致如下，其中 F 為固定地址集合：
{ heap H }
p := malloc(n)
{ heap ((p, n) :: H) and p is fresh }
modifies F
遺憾的是，沒有這樣的 F 存在。從同一堆疊中，malloc(32) 在地址 0x82000238 寫入新頂區塊的標頭，因而 F 必須包含該地址。malloc(64) 反而返回區塊 [0x82000210, 0x82000250)，其中包含該地址。當呼叫者擁有該區塊後，對其位元組的事實必須在後續呼叫中存活，因此 F 也必須排除 0x82000238。LLM 在 Lean 中證明，沒有固定地址集合能同時滿足兩個要求，第一次嘗試在問題迴避後，一次一個事實停滯了三週。
malloc(32) 寫入一個位元組，malloc(64) 會將其交給呼叫者。分配器的寫入足跡必須隨記憶體所有權變化而改變。分離邏輯透過讓足跡依賴堆疊來解決此問題。我們將 MachCSL（xv6 證明背後的邏輯）移植至新發布的 iris-lean。1 在分離邏輯中，分配器 擁有 它領域的空閒位元組，malloc 的 規格 將其中一部分交給呼叫者：
{ isHeap H }
p := malloc(n)
{ (p = 0 ∗ isHeap H)
∨ (isHeap ((p, n) :: H) ∗ blockOwn p n) }
此處 ∗ 為 分離連線，表示其兩個部分持有記憶體的互不相交區域，結果 p 要麼為 null，要麼為新的區塊。isHeap H 擁有領域中除活躍區塊 H 之外的每個位元組。最初，分配器擁有 0x82000238，因此 malloc(32) 可以寫入它。若呼叫者改為請求 malloc(64)，該位元組通過 blockOwn 轉移給呼叫者，後續呼叫不能觸碰它。呼叫者持有的其他內容未在規格中提及，框架規則將其在一次呼叫中傳遞。移植後，剩餘證明在數天內完成。
高峰時，證明約有一百萬行 Lean 程式碼，其中三分之二由 LLM 撰寫的 35 個指令碼產生，這些指令碼讀取二進位並為約 11,800 條指令發出證明規則。後續通過一次過程將產生的證明族替換為一次性證明的抽象，例如機器碼的符號執行器，將證明縮減至 200,000 行以下。它除了 Lean 的標準公理（propext、Classical.choice、Quot.sound）外不使用其他公理。
該定理適用於實際程式
一個帶有假設的定理只有在該假設可被滿足時才有用。若 Loaded 描述的是從未發生的機器狀態，我們的定理將自動成立，卻無法告訴我們任何關於二進位檔案的資訊。
We had the LLMs 在 Lean 中證明 Loaded 在十個程式中成立.
對於每一個，他們在解譯器入口處建立了一個機器狀態，程式與二進位、執行環境及記憶體分配器一起存於記憶體。Lean 檢查每個狀態是否符合定理的前置條件。2
Loaded 指定了透過解譯器二進位執行程式所需的記憶體與暫存器。程式以語法樹（橙色）進入；周圍的程式碼與執行時狀態則來自解譯器。我們還從可執行檔回放了 85,483 次機器步驟，並檢查產生的記憶體與構造的狀態逐位相符。從可執行檔及其啟動追蹤到該狀態的連結由指令碼檢查；Lean 檢查前置條件以及從該狀態開始的執行。對於完整的 loop test program，它在前一個範例的基礎上再加入兩個總和，二進位在列印 55、2500、36（各自佔一行）後可證明終止。
前置條件包含足夠的堆疊與堆記憶體空間。later theorem 以在程式上執行的檢查器取代這兩個假設。
一旦你信任語義，工具就變得便宜。
經過驗證的語義也可作為介面。任何對 BigStep 可信的證明，在與細化定理組合後對二進位也可信，且該組合只需幾行 Lean。於是我們讓 LLM 建立了四個工具。
細化證明耗時約一個月，約 140,000 行 Lean。以下四個工具在三天內以 pull request 開啟，總共約 33,000 行，其中大部分為編譯器。
第一個工具是 type checker。它在程式執行前捕捉無效操作。例如，以下兩個程式被拒絕：
"a" - 1; // subtracting an integer from a string
var x = 1;
x = "s"; // assigning a string to an integer variable
以下 proofs for these examples 顯示兩個程式都無法通過檢查器。其可信度定理排除已接受程式中的型別錯誤，即使它們透過解譯器二進位執行。除零、assert 失敗以及解譯器的呼叫深度限制仍可能發生；這些需要同時推理值與型別。
第二個工具是 program logic，它允許我們證明特定程式計算的內容。本文開頭附近的迴圈將 1 到 10 的整數相加。完整的 test program 亦將 1 到 100 的奇數相加，使用 break 與 continue，並以巢狀迴圈計算第三個總和。LLM 使用此邏輯證明，將此程式透過解譯器二進位執行會終止並精確列印：
55
2500
36
第三個工具是 abstract interpreter，它是一種分析，追蹤程式中可能的值並針對潛在執行時錯誤發出警報。它對同一測試程式進行分析，no alarms，證明無執行時錯誤。它亦證明 sum、total、acc 的最終值分別為 55、2500、36。此分析自動計算這些結果，其可信度證明將其與二進位執行連結。
第四個工具完全不需要直譯器。在四月，我們的代理人構建了一個編譯器，但無法證明其正確性。在此，語義先行，LLM 建立了一個驗證編譯器，從 WHILE 的所有特性（字串、閉包、呼叫、for、return 和 assert）直接編譯到 RISC-V。編譯上面提到的 sum 程式，生成的機器碼會輸出相同的三個數字。正確性定理證明對於每個滿足其前置條件的程式都保持一致。檢查版本 分析分配成本，因此其定理不需要對可用堆空間做任何假設。
移除直譯器也使 WHILE 程式更快。我們在spike RISC-V 模擬器上，兩種方式都執行了直譯器測試套件中的每個程式。從它開始評估的那一刻起計算直譯器的指令數，這樣解析不會被計入，編譯後的程式在退化時的指令數比直譯器少 2.7 至 8.2 倍，且兩條路徑輸出相同。這些是模擬器上的指令計數，而非實體硬體上的時間。
一旦語義被信任，它就 是 語言，而我們起始的二進位不再需要執行 WHILE 程式。
接下來是什麼：Lua、OCaml，將來還有 CPython
我們對 WHILE 的實驗針對的是一個玩具語言。LLM 開發了它的正式語義，證明編譯後的直譯器遵循該語義，並在其上構建了驗證工具。現在我們正將此方法擴充套件到實際語言。
傳送你的 Lua 目標是將 Lua 5.4.7 編譯為裸機 RISC-V。二進位已經在 Sail 模型上執行，並與原生 Lua 一致，計畫在 VM 進行證明：首先將位元組碼直譯器對照位元組碼語義，逐段處理操作碼，然後將原始語言對照位元組碼。
傳送你的 OCaml 利用 OCaml 自己的引導方式。OCaml 的引導編譯器以位元組碼 boot/ocamlc 檢查到其倉庫中，並在 ocamlrun 上執行。我們已經在 Sail 模型上執行 ocamlrun，使用真正的 boot/ocamlc 編譯程式。計畫在那裡以固定點結束：如果源語義說編譯器將自己的原始碼編譯為恰好 boot/ocamlc 的位元組，且編譯器的後端已被證明正確，那麼這些位元組就能賦予意義，而不需要逐一驗證其 412,000 個位元組碼指令。
對於兩個專案，我們已經在 Lean 中陳述了主要定理。剩下的工作是完成它們的證明。
北極星是 CPython。我們相信目前的代理人能夠在擁有足夠算力的前提下，編寫並機器驗證 Python 的語義。這樣就能在此基礎上構建前面提到的工具，並提供可延伸至 CPython 二進位的保證。