devgo.cn如果你认真用 LLM 写过代码，大概率撞上过这些场景：模型信誓旦旦说改完了，一跑测试就崩；它忘了三句话之前你定的规则；或者它给出的代码能编译，但逻辑完全是错的。市面上大多数 AI 编程工具的思路是让模型更自主、更快，结果只是让错误产出得更快。Emetgate 走了一条相反的路：模型没有任何权力，一个极小的确定性内核掌握全部权力。模型只能提议，内核负责验证，任何未经验证的东西都到不了磁盘。
这个思路的灵感来自一个古老的故事。布拉格犹太教拉比用河泥塑造了一个魔像（Golem），它强壮、不知疲倦、绝对服从，但没有任何判断力。赋予它生命的是写在额头上的一个词：emet，希伯来语的“真理”。当魔像失控时，拉比擦掉第一个字母，剩下的是 met，意为“死亡”，魔像便归于尘土。Emet 的三个字母分别是希伯来字母表的第一个、中间和最后一个字母，传统解读是真理必须从始至终成立，拿走任何一部分就不再是真理。
Emetgate 把 LLM 看作精确意义上的魔像：它能快速产出大量工作，却无法判断这些工作是否正确。Emetgate 就是写在额头上的词和门前的闸门——模型可以提议任何东西，但只有能被验证的才被放行。
具体怎么实现？内核的验证流程分六步。第一步是内容寻址（Content addressing）：每个符号（比如 Class.method 或 add）都由一个引用和它当前内容的 128 位哈希标识。提议必须指明它基于哪个哈希。如果文件在此期间被改动，哈希不匹配，提议就被拒绝。模型无法覆盖它没见过的代码。第二步是 AST 验证的变更（AST-verified mutation）：一次变更只替换一个函数体。新函数体按字节范围拼接到源码中，然后用 tree-sitter（一个解析代码为语法树的库）重新解析整个文件。内核检查结果能否干净解析、函数体有没有跳出花括号、是不是空函数体或占位符、目标范围之外的每个字节是否原封不动。第三步是有界性分析（Boundedness）：在运行任何东西之前，内核计算这次变更是否会影响符号之外的代码。这是一个正向的、封闭世界的计数：只有当所有可能的逃逸方式都被排除，变更才被标记为 BOUNDED，并且这个判定附带其来源依据。分析无法解释的任何情况都标记为 UNBOUNDED。第四步是测试闸门（Test gate）：UNBOUNDED 的变更被应用到一个影子副本（shadow copy）上，然后在沙箱里运行项目的测试命令。沙箱使用 Windows Job Object（一种 Windows 进程隔离机制，可限制进程组资源并强制终止），带 kill-on-close、墙钟时间和内存限制、输出上限。测试命令在低完整性受限令牌（low-integrity restricted token）下运行，所以模型提议的函数体无法在影子副本之外写任何东西；如果无法构建和验证这个令牌，命令会被拒绝而不是无限制地运行。测试失败则变更被拒绝，输出返回给模型。第五步是持久化提交（Durable commit）：通过的变更经过预写日志（write-ahead journal）和原子写-重命名（atomic write-rename）。任何时刻崩溃都只会留下旧文件或新文件，绝不会出现撕裂的写入。恢复过程会重放日志，并拒绝任何无法证明的东西：零字节文件、无法重新解析的条目、格式错误的标签。
这套架构并非全新想法。它本质上是 LCF 风格定理证明器的架构——在那里，策略（tactics）可以建议任何东西，但只有一个小型可信内核能产生定理。这也正是 de Bruijn 论证证明检查器应建立在足够小、可通过检查来信任的核心上的原因。Emetgate 把同样的纪律应用到模型写的代码上。
一个关键设计是依赖方向严格单向：protocol → platform → engine。engine 层是纯确定性的，没有 I/O，不能导入 platform 层。所有决定变更是否有效的逻辑都是其输入的纯函数，这让它达到了可测试的标准。
Emetgate 的验证层本身也经过验证。两条规则适用于内核中的每个守卫。一是变异杀死（Mutation kill）：保护不变量的守卫和分支会被变异（移除检查、削弱条件、翻转比较），然后对每个变异体运行测试套件。至少一个测试必须失败。存活的变异体要么被新测试杀死，要么记录在 tests/mutations.json 中并说明原因：等价变异体（附语法或代码事实）、或故意保留的冗余守卫。没有杀死输入且没有等价证明的变异体被标记为 open 而不是隐藏。目前 engine 层有 44 个变异体：37 个被杀死，4 个被证明等价，1 个冗余守卫作为纵深防御保留，2 个开放。二是对抗性测试：专门的红队套件直接攻击闸门——逃出花括号的函数体、过期哈希、撕裂的日志条目、被投毒的仓库配置、尝试打开仓库外文件。
一个让我意外的数据点是 token 效率。在基准测试中（tokenizer 为 o200k_base，六个场景，其中两个是真实文件），通过符号级提议编辑比搜索-替换编辑平均节省 1.80× 的 token，范围从 1.15× 到 3.77×。在真实文件上收益较小，只有 1.15× 到 1.17×。原因在于搜索-替换需要读取整个文件并发送新旧代码块，而内核只需读取骨架加一个符号体，发送符号引用、内容哈希和新函数体。但作者明确说 token 节省只是副作用，不是重点。
Emetgate 目前刻意保持狭窄。语言支持 TypeScript 和 JavaScript（.js、.mjs、.cjs），新语言以 profile 形式添加到 src/engine/lang 下，必须通过 tests/lang 中的一致性套件。平台仅限 Windows，因为沙箱依赖 Job Objects。已构建的功能包括 AST 验证变更、内容哈希、结构守卫、有界性分析和测试闸门、日志、原子提交、恢复、沙箱、MCP 服务器和锁定启动。决策账本（append-only，支持取代、压缩、撕裂尾部恢复）已构建但尚未暴露为 MCP 工具。编辑闸门处的规则执行正在进行中。
作者也坦诚列出了无法机械化的部分：语义正确性——能解析、在边界内、通过测试的代码仍可能实现错误行为，内核抬高了底线，但不能替代编码意图的测试或需要人类决策的地方；测试套件的质量——对于无界变更，测试闸门和它运行的测试一样强；中介——保证只对通过闸门的变更成立，其他工具做的编辑会绕过它，这就是 lockdown 存在的原因；沙箱范围——低完整性令牌阻止测试命令在影子副本外写入，但不限制读取或网络访问，恶意的测试命令仍能读取它有权限读的文件并访问网络，限制这些需要 AppContainer，已在计划中；品味——架构、API 设计和用户体验不是内核能检查的属性。
这个思路能直接用到什么场景？如果你在构建任何让 LLM 直接操作代码库的工具，Emetgate 的“模型提议、内核验证、fail-closed”原则值得借鉴。特别是内容寻址防止模型覆盖未见代码、AST 验证防止结构破坏、变异测试保证验证逻辑本身可靠这几点，都是可以直接复用的设计模式。要注意的坑是：验证层本身必须被验证，否则只是更复杂的碰运气；沙箱的边界要清楚，低完整性令牌挡不住读取和网络；以及不要指望内核能解决语义正确性和品味问题。Emetgate 是开源的，MIT 协议，代码在 GitHub 上，如果你想看一个“确定性内核夹在 LLM 和源码树之间”的完整实现，这是个很好的参考。
内容与图片版权归原作者所有 · 原文: https://github.com/emetgate/emetgate