Djinnlang：用 LLM 编译器实现无歧义规格的高级编程

程序员只写形式规格时，如何让 LLM 实现代码却对程序语义没有任何选择余地。

• 场景：作者设想的编程未来是人写规格、LLM 实现并证明实现符合规格。走到极端，规格语言就成为新的编程语言，像高级语言抽象机器指令那样，抽象掉纯粹的前后条件。
• 现有不足：作者称现有规格语言一般不可执行，得到实现仍要手写代码或手工精化。LLM 会误读规格、幻觉出错，也可能故意颠覆任务；作者引用的安全论证越来越不排除后一种可能。因此即便全部代码由 LLM 写出，它对程序语义也不应有任何余地。
• 核心观察：作者把“由一组约束无歧义地规定一个函数”定义为：这些约束构成的关系是确定性的。即任意两个满足约束的函数，在相同输入上必须给出相同输出。再加上存在性义务后，实现不再决定程序算出什么。
• 提出的东西：作者提出无歧义约束（unambiguity constraint）和 LLM-in-the-compiler 范式，并给出规格语言 Djinnlang。人只写规格；符号翻译器把规格降成 Dafny 桩与证明义务，驱动器调度 LLM 填实现与证明，由 Dafny 验证器检查。作者称这同时是一种强形式的 AI control：不可信模型写代码，其工作被验证器收紧检查。
• 作者的主张：在该约束和足够强的 LLM 下，规格语言与编程语言的差别变得基本没有意义，LLM 本质上成为编译工具链的一部分；生成代码几乎不必阅读，且可随时从规格重新生成。

相关工作在 Section 8，并在引言和第 3–4 节点名若干对照。

规格语言

• Z、VDM、B、TLA+、Alloy：以数学谓词、时序逻辑或轻量关系规格描述系统。作者称其中规格一般不可执行；B 要手工、机器检查的精化才能得到实现。作者称无人值守地实现规格，只因本文的无歧义约束与 LLM 的紧密集成才成为可能。
• Miyazono 等、Dodds：前者把自然语言文档与 Lean 形式化逐行对照，案例为 Signal 的 X3DH；后者认为多数系统没有连贯的形式规格，写规格本身像编程、需要工具。论文只作描述。

契约与面向验证的语言

• Eiffel、JML、Spec#，以及 Dafny、F*、Verus：把前后条件放进程序或静态验证代码是否满足契约。作者称这些语言里程序员同时写规格和实现，且没有东西强迫规格完整。Djinnlang 保留契约词汇、编译到 Dafny 并复用其类型与验证器，但去掉人写的实现，并用无歧义证明去掉“部分规格”这一选项。

程序合成与 LLM 证明

• Sketching（Solar-Lezama）、关系式编译（Pit-Claudel 等的 Rupicola）、Verse：Sketch 用洞加约束合成程序；Rupicola 把函数式模型证明式地译成底层代码。Verse 允许表达式产生多个值，并把选择写进项的语法；作者称其作者把求值策略留给未来工作，并称其语义“un-implementable”，因为没有重写系统能解 ∃x. x² − x − 6 = 0。Djinnlang 禁止歧义（除非程序其他部分能消解），把该负担交给 LLM，再用验证器检查。
• Clover、AlphaVerus、AutoVerus、Baldur，以及不变式推断与规格生成：Clover 检查代码、规格与文档字符串的一致性；AlphaVerus 无人工标签地自举已验证 Verus 代码；AutoVerus 与 Baldur 为已有代码生成证明。论文把它们放在“人仍写或已有代码、模型补证明或规格”一侧。文中还提到把 LLM 放进循环的工作。
• AI control（Greenblatt 等）：用可信编辑、不可信监控等协议降低后门等非期望输出穿过安全机制的概率。作者把无歧义约束视为一种很彻底的 AI control：形式地保证模型对程序输出没有权力，对性能仍有一些权力。

基线方法与基准

• 论文没有使用名为基线的既有攻击或防御方法。实现器是 Claude Fable 5.1（Claude Code） 与 GPT 6 Astra（Codex），互为对照。程序为 Sudoku、LZ77、Imp VM；正确性另用 LLM 生成的黑盒测试，期望输出来自 Python 与 C 的参考实现。性能优化是同一义务下的第二轮，不是另一个合成系统。

作者把本文定位为：规格是唯一可信的人工产物，LLM 位于编译器内部且输出被验证器钉死；与普通 vibecoding 不同，代码可丢弃、可从规格再生。作者称这是编译器设计中 LLM 一个尚未被充分探索的用法：与验证器配合时可以支持更强的抽象。

Djinnlang 里程序员只写约束。符号翻译器 djinnc 把规格降成可信 Dafny 规格与空体桩，现成编码智能体填实现和证明，Dafny 验证器检查，通过后才把实现交给 Dafny 编译器。

无歧义与存在性

记 pre(x̄) 为声明的前置条件合取，q(x̄, o) 为约束在输入与输出之间定义的关系。无歧义义务是

∀ x̄, o₁, o₂. pre(x̄) ∧ q(x̄, o₁) ∧ q(x̄, o₂) ⇒ o₁ = o₂

存在性义务是 ∀ x̄. pre(x̄) ⇒ ∃ o. q(x̄, o)。两者都成立后，q 是全且确定的关系，实现不再决定程序计算什么。论文里的 function 指一段可执行代码，不是数学上关系的特例。

语言构造

Djinnlang 不自带类型系统和标准库：签名可用任何 Dafny 类型，约束里可调用所处 Dafny 上下文的函数与谓词。三种顶层构造：

• func：译成 Dafny 函数，必须纯且无歧义；隐式要求存在性证明和会终止的实现。矛盾规格在编译期被拒绝。
• rel：纯但可以非确定，对 Dafny 而言是谓词、不带可执行代码，只给其他规格提供可再收紧的词汇。默认部分（partial）；标注 total 才加上与 func 相同的存在性义务。歧义必须由使用它的 func 或 proc 消解。x in domain(q) 表示 q 接受 x 且至少关联一个输出。
• proc：无歧义但可以有副作用。默认证明终止；noreturn 表示意图永远运行（如事件循环）。

语法借自带缩进的命令式程序，但 = 是相等不是赋值，函数体是各行的合取，行序一般无关。if C: B else: E 是 C⇒B 且 ¬C⇒E；for x in xs: B 是 ∀x∈xs. B。没有 else 的 if 表示否则输出不受约束，常会因歧义被拒。

函数的六类义务

对 func f(xs) -> o，翻译器在可信文件中发出 f_pre 与 f_spec：前者合取 requires，后者恰好在函数体约束把输入关联到输出时成立。solution 文件按序发出空体义务：

1. unambiguity：固定输入下，任意两个满足 f_spec 的输出相等。
2. postconditions：每条 ensures 一个引理，须从 f_spec 推出；不能从函数体推出的后条件被拒绝而不是被假定。
3. existence：每个 f_pre 允许的输入都存在满足 f_spec 的输出。
4. implementation：同签名、会终止的 Dafny 函数，是唯一作为代码而非证明的桩。
5. implementation correctness：在前置条件域上，实现的输出满足 f_spec。
6. call sites：函数体调用带 requires 的东西时，该前置条件在该点已知事实下成立；函数体没有此类调用则省略。

Figure 1 的 max 展示了这些义务。作者称左侧 Djinnlang 与两个 ghost 谓词是可信的，谓词是约束的机械转写；每条义务被钉住，模型只能加函数体，不能改定义。

过程与副作用

规格是同时成立的约束，而效应有先后。作者采用代数效应，把命令式代码写成从“上一步结果”到“下一步”的函数，再配一个直接用 Dafny 写的驱动器。proc 是这种构造的语法糖：翻译器自动生成必须无歧义的 step 函数（由 LLM 实现）和永不被 LLM 改动的 Dafny 驱动器。

• do 是顺序有意义的例外：do 调用按出现顺序链接。if 的条件被合取到内部事件的守卫上，前驱仍是 if 之前的事件。共享同一前驱的子句守卫互斥，因此机器按构造是确定的，该证明由翻译器自己 discharge。
• for 若含 do，必须写成 ordered for，从而规定执行顺序。被迭代集合没有固有顺序时不能用 ordered for。它是带下标的 while 的糖：边界进入时求值一次。while 的条件本身是一步，可以依赖循环中变化的外部因素。
• proc 里的纯约束在整个运行中成立，而不是只在写到的那一点成立。then: 块必须紧跟 do、while 或 ordered for，其约束只在该范围内成立。
• 每个事件的守卫点名前驱，因此事件按指定顺序发生；驱动器原样交还状态元组且不检查它，因此状态只在被指示处改变。契约证明使用实现者选择的、关于该状态的机器不变式。

工具链

Figure 2：人写只含规格的 .djinn（可以另用 LLM 协助，但是人的自由）；翻译器解析后发出两样东西。

• 第一模式：spec.dfy 为可信降级（每个声明的前置条件谓词与关系；每个 proc 还有编译后机器的数据类型与 step 关系）；solution.dfy 为义务桩。只对 spec.dfy 跑 Dafny 来做类型检查。solution.dfy 只在缺失或被强制时写出。
• verify 模式：先重新翻译规格，避免用过期或被篡改的 spec.dfy 来检查解答；再扫描解答中的 assume、{:axiom}、{:extern}、{:verify 这些逃生口；并检查每条重新生成的义务在解答中逐字出现（注释、签名、契约，大括号之间的函数体除外）。通过后调用 Dafny，每条义务限时 120 秒。
• Harness：论文称方法与具体 harness 无关。实验使用未修改的 Claude Code 与 Codex，指向含规格、所处 Dafny、桩文件和书面指南的目录。智能体循环是编辑、运行 djinnc verify、读错误、重复，实现通过即停止。智能体还自行把声明分成不相交组、分给多个智能体再合并；作者称这些支持工具不在可信基里。
• 性能：语义由规格定死，速度不是。通过验证后再用第二条提示做一轮加速，只在证明仍通过且在工作负载上确实更快时接受改动。Dafny 验证、Dafny 的 C# 后端编译；作者希望以后做基于 Verus 或新兴 Lean 验证系统的变体。

自举

djinnc 本身主要用 Djinnlang 写成（环境部分用 Dafny 与 C#）并自举。先由 LLM 写一个一次性的 Python 种子翻译器，其输出经人工检查；第二个 LLM 填种子发出的实现与证明；由此得到的二进制再逐字节再生自己的义务，并用自己的 verify 重跑全部证明，从而在翻译器和验证器两个角色上退役种子。

实验设置

• 被测实现器：Claude Fable 5.1，由 Claude Code 驱动；GPT 6 Astra，由 Codex 驱动。两者都不许改规格。各先产出已验证实现并做快照，再做单轮优化。每份规格因此有四份产物。
• 程序：Sudoku（70 行 Djinnlang，61 条义务）、LZ77（81 行，63 条义务）、Imp VM（166 行，132 条义务）。规格本身由 LLM 生成，作者称已仔细检查。三份合计 256 条义务。
• 工作负载设计：作者选择它们是为了能较优雅地写规格、工作流受 CPU 约束，且同一规格既允许明显较慢的实现，也允许快得多的实现。Sudoku 规定部分填充网格的字典序最小完成，或证明无解。LZ77 规定最优解析的压缩；压缩比是规格的性质，实现只能在速度上不同。Imp VM 规定带燃料界的小型命令式语言的小步语义，使解释器为全函数；实现可以走语法树或编译到寄存器机器，但燃料耗尽时必须停在同一步数。
• 正确性：独立于证明，用 LLM 生成的黑盒测试：分别 14、30、65 个用例，期望输出来自 Python 与 C 的参考实现；每套另有 9 个长时间任务用于计时。
• 性能环境：Table 2 为 Dafny release 构建，MacBook Pro、M4 Max、128 GB 内存、16 核、macOS 15.7.7，Dafny 4.11.0，.NET SDK 9.0.109。不足两分钟的工作负载每格三次取最快，超过两分钟的两次。>900 为该上限处超时；† 为约 0.1 秒后崩溃（栈溢出）。
• 成本口径：Table 3 的成本是相应模型的标价，是理论 API 成本；作者实际走订阅、并未支出该金额。Claude 一侧的数字主要来自所用一小时保留的 cache writes，Codex 日志不记录这一类，故两边不能直接比较。output tokens 含推理。三份程序由两家实现器并发编译。论文未报告统计显著性检验，也未报告评审模型。

主结果

语言设计（Section 5）是定性例子，不进下表。实证主结果是两家实现器都能 discharge 全部义务，但时间、成本和生成程序速度差很大。

Table 3 中实现加优化的理论 API 成本与墙钟（墙钟按阶段；all three 行未给合计墙钟）：

Swipe horizontally to read the table

程序 / 阶段	Claude 墙钟	Claude 成本	Codex 墙钟	Codex 成本
Sudoku impl	1.8 h	$51	13 m	$4.31
Sudoku opt	1.7 h	$36	7 m	$5.74
LZ77 impl	6.3 h	$236	23 m	$8.87
LZ77 opt	1.9 h	$84	8 m	$10.19
Imp VM impl	1.3 h	$73	13 m	$3.02
Imp VM opt	12.1 h	$546	13 m	$7.37
三者合计	未报告	$1026	未报告	$46.89

• 作者称两家实现器都在首次整体运行中 discharge 了三份规格的全部 256 条义务；运行内部会像人类证明工程师那样对着验证器迭代。编译器的 2,106 条义务也来自单次运行。
• 作者称 Codex 用 33 分钟、估计 $47 编译完全部三个程序，Claude Code 为 21 小时、$1026；作者称大约快三十倍、便宜二十倍。Codex 证明写得少得多，且一次写完。
• 作者称便宜的编译得到的已验证程序慢三百到四百倍，且 Codex 有两个未优化程序无法在合理超时内完成工作负载。对照传统编译器，作者称这些数字显得离谱（没有编译器用六小时或 $236 翻译 81 行）；对照人类手写证明的传统验证，作者称同样的数字显得小。

生成程序的速度

Table 2 为相同输入上重复运行的最快秒数。base 为首次通过的实现，opt 为一轮优化后。

Swipe horizontally to read the table

程序与负载	Claude base	Claude opt	Codex base	Codex opt
Sudoku hard puzzles	0.65	0.13	>900	47.84
Sudoku 3000 unique	0.40	0.31	>900	4.31
LZ77 4 MB text	0.91	0.63	†	25.63
LZ77 2 MB DNA	0.33	0.24	†	28.55
LZ77 1 MB periodic	0.32	0.12	†	3.26
Imp VM 10^9 steps	76.9	18.5	211.7	189.3
Imp VM Ackermann(3,10)	27.7	6.5	787.6	714.5
Imp VM sieve to 2·10^7	23.6	6.6	>900	61.7

• 作者称最难的 Sudoku 上 Claude 优化求解器 0.13 秒、Codex 47.8 秒；4 MB 文本上编码器分别为 0.63 秒与 25.6 秒。虚拟机更接近但仍分开：十亿解释步上 18.5 秒对 189 秒，即每秒 5300 万步对 500 万步。
• 一轮优化：作者称 Claude Code 把虚拟机从每秒 500 万、1300 万推到 5300 万步（naive、fast、optimized 三台机器）。Codex 这一轮把堆较重的程序改进很多——矩阵乘法从 217 秒到 38 秒，筛法从超时到 62 秒——但其余几乎不变。
• 作者称差异多半是实现器 ambition 的产物：Claude Code 似乎更优化生成代码的速度，Codex 编译更快但代码更慢。作者认为不清楚若给 Codex 同样的时间预算它会否追上，并称 Codex 或可当作编译更快的调试模式。

规模、自举与规格里的错误

• 行数（Table 1，非空非注释）：规格对两家相同。Sudoku 规格 70 行；Claude 的 code/proof 从 baseline 303/929 到 optimized 448/1274，Codex 从 76/348 到 197/468。LZ77 规格 81 行；Claude 448/2339 到 545/2585，Codex 72/206 到 210/356。Imp VM 规格 166 行；Claude 257/655 到 1440/2564，Codex 187/395 到 359/514。
• 成本分布：作者称三程序的实现与证明大约 $360（Claude Fable 5.1），分布很不均匀，LZ77 独占约三分之二，其中大部分是最优性论证。另有 $666 用于优化，大部分花在虚拟机上。这些数字与 Table 3 分项同属 Claude 一侧；Table 3 合计为 $1026。
• 自举（Section 6.5）：djinnc 为 4,088 行 Djinnlang、487 个声明，发出 2,106 条证明义务；discharge 它们用了 4,715 行实现和 31,823 行证明，外加 1,549 个辅助声明。产生该实现耗费 GPT 6 Astra 14 亿 token（若走 API 作者估计 $1,950，实际走包月订阅），历时多日。起草规格期间，编译器发现四处分Distinct 的规格错误：每次都是义务无法 discharge，因为草稿确实错了，而不只是难。规格改正后，整个编译器的合成在第一次尝试即成功。由这些函数体建成的二进制再逐字节再生自己的义务并自己重跑证明。

其他消融与分析

论文没有参数消融表。Section 5 用例子说明设计目标，不报告通过率。

• 排序：rel perm 只约束多重集与长度，func sort 再加升序，从而即使 perm 有歧义，sort 仍可被证明确定；LLM 须证明 <= 在 int 上是全序，换到不是全序的类型时验证器会标出问题。
• 整数转字符串：作者列出若把 % 10 写成 % 100、或下标写成 |s|-k 或 |s|-2-k，会被越界或“重复写出”的字符范围约束抓住；并称最后四行对功能并非必需，是 deliberate redundancy。
• 字符串转整数：stringtoint 只接受 inttostring 会生成的精确形式；用 nattomanystrings 的前像可接受前导空白，再靠首字符是数字消掉歧义。
• 过程中的纯约束：do 改写 x 之后，若中间一行把 stringtoint(x) 当成全程都成立的断言，规格矛盾并被拒绝。
• Sudoku 的读法：作者称同一段文字既可按命令式读成检查器（作者称嵌套循环为 6561 次迭代），也可按逻辑读成已解网格的集合；求解器只说答案属于该集合。实现可以做约束传播而不枚举每一对。
• 负面结果：Codex 未优化的 LZ77 三档均为约 0.1 秒后栈溢出，未优化 Sudoku 两档与未优化 sieve 为 >900 秒超时；优化后 sieve 为 61.7 秒，仍慢于 Claude 的 6.6 秒。Imp VM 上 Codex 优化轮对 10^9 步只从 211.7 秒到 189.3 秒，Ackermann(3,10) 从 787.6 秒到 714.5 秒。

作者指出的局限与后续方向

• 性能不在无歧义约束内（Section 2.4）：LLM 实现的细节仍决定性能等因素。作者认为这常常可取，因为 LLM 擅长优化代码，但也带来额外安全问题，例如时序敏感的密码代码，或在某些输入上故意变慢的 DoS 式攻击。
• 时序密码代码可能一直在范围外（Section 2.4）：作者认为，连几个周期的性能偏差就能导致侧信道成功的那种高度时序敏感密码代码，对这一类语言很可能始终在范围之外，许多高级语言也是如此。
• 验证器出错（Section 2.4）：若验证器或调用验证器的基础设施组件失败，就只能听任当时完全无人监督的 LLM，它可能以各种方式有害。作者感到一般来说对验证器的信任是有理由的，但风险总会留下。
• 规格仍会有错（Section 2.2）：作者同意这绝不是所有 bug 的终点。矛盾会因规格不可满足而在编译期失败，而不是到生产环境才出现；作者认为重复陈述自己的想法会成为好习惯，因为验证器可以检查。
• 语法可能误导（Section 4.1）：作者承认语法起初可能显得费解、陌生。行看起来有先后但同时成立；读起来像在累积的 for 并不能累积；没有 else 的 if 是留下输出不受约束。
• 后续方向（Section 2.4、Section 10，以及第 4 节末）：作者认为这一语言的未来扩展应包含用于规定基线性能界、伸缩行为和计算复杂度的简单语法。作者计划实现关于事件轨迹的更高层规格（Section 10）。作者还希望做基于 Verus 以及新兴 Lean 代码验证系统的变体，并认为这一规格语言的未来迭代甚至可以与实现语言无关。

实验覆盖范围

• 定性例子为排序、nattostring/inttostring 的冗余约束、stringtoint 作为前像，以及 Sudoku 规则书；一般用途的论据是编译器自身用 Djinnlang 写成（Section 5、6.5）。
• 实证程序为 Sudoku、LZ77、Imp VM 三份，义务数 61、63、132；实现器为 Claude Fable 5.1（Claude Code）与 GPT 6 Astra（Codex），各一轮优化（Section 7）。
• 黑盒测试分别为 14、30、65 例，另每套 9 个计时任务；期望输出来自 Python 与 C 参考实现。性能测量环境写在 Table 2 注中。
• djinnc 自举：4,088 行、487 个声明、2,106 条义务；种子翻译器为一次性 Python，输出经人工检查，之后由建成的二进制退役（Section 6.5）。
• 论文报告了墙钟、理论 API 成本、content lines 和运行秒数（Table 1–3），并写明 Claude 与 Codex 的成本不能直接比较、实际未按该标价支出。每条义务的验证时限为 120 秒。论文未报告多次独立合成的重复次数，也未报告人工与验证器不一致的案例数。

Djinnlang 让程序员只写规格，把 LLM 放进编译器，并用 Dafny 验证器加上无歧义约束钉住语义。

• 问题：作者认为 LLM 既会误读、幻觉，也可能故意颠覆任务。若规格留下多个合法输出，模型就仍在决定程序做什么。无歧义指约束关系是确定的：相同输入上，任何两个满足规格的输出必须相等，并且对每个合法输入输出必须存在。
• 做法：翻译器把 func、rel、proc 降成可信谓词和被钉住的空体义务（无歧义、后条件、存在性、实现、实现正确性、调用点前置条件）。模型只能填体。rel 可以非确定或偏，由调用方收紧；proc 用逐步函数加机械生成的驱动器表达副作用，do 的顺序有意义。verify 会重译规格、拒绝 assume 等逃生口，并按 120 秒上限调用 Dafny。速度用通过之后的单独一轮去改进。
• 语言例子：排序是排列关系加升序；整数打印用重复写出的数字范围抓住作者列举的取模和下标错误；解析写成打印的前像。
• 结果：Claude Fable 5.1 与 GPT 6 Astra 都 discharge 了三份规格的 256 条义务。Table 3 上三者实现加优化的理论 API 成本为 Claude $1026、Codex $46.89；Codex 合计墙钟约 33 分钟，Claude 约 21 小时。Table 2 上优化后的 hard Sudoku 为 0.13 秒对 47.84 秒；Codex 未优化的 LZ77 崩溃、未优化 Sudoku 超时。djinnc 自身 4,088 行规格发出 2,106 条义务，改正四处分 Distinct 规格错误后第一次合成成功，并能再生并再验证自己。
• 作者的结论：在该约束下，生成代码几乎不必阅读，可从规格随时再生；验证器保证实现满足规格，无歧义保证模型对语义没有余地，对性能仍有余地。作者把这看成一种形式化的 AI control，也承认验证器失效、时序侧信道和故意变慢仍是危险，并计划以后能直接规定性能界和事件轨迹。