LLMs generate code quickly. They also generate code that compiles and is wrong, reports tasks as done when they are not, silently forgets rules from earlier in a session, and loses track of plans agreed upon at the start. A new project called emetgate takes a hard position on this: the model holds no authority at all. A small deterministic kernel holds all of it. The model proposes. The kernel verifies. Nothing unverified reaches the disk.
The Golem and the gate
The project's name comes from the Hebrew word emet, meaning truth, the word written on the Golem of Prague's forehead in the rabbinical legend. The idea is that a language model is a golem in the precise sense: it produces work quickly but has no way of knowing whether that work is correct. Emetgate is the gate in front of the disk. Every proposal the model makes passes through a verification kernel before any file is written.
This is not a novel architecture. It is the design of LCF-style theorem provers, where tactics may suggest anything but only a small trusted kernel can produce a theorem. It is what de Bruijn argued when he said a proof checker should rest on a core small enough to be trusted by inspection. Emetgate applies the same discipline to code written by a model.
How the kernel works
Every proposal passes through six steps. The model names a symbol and a 128-bit content hash of the current content. If the file changed since the model last read it, the hash mismatches and the proposal is rejected. The model cannot overwrite code it has not seen.
The new body is spliced into the source by byte range and the entire file is re-parsed with tree-sitter. The kernel checks that the result parses cleanly, that the body did not break out of its braces, that it is not an empty or placeholder body, and that every byte outside the target span is untouched.
Before running anything, the kernel computes whether the change can affect code beyond the symbol itself. This is a positive, closed-world analysis: a change is BOUNDED only when every way it could escape has been ruled out. Anything the analysis cannot account for is UNBOUNDED.
UNBOUNDED changes are applied to a shadow copy and the project's test command runs against it inside a sandbox. On Windows, this is a Job Object with kill-on-close, wall-clock and memory limits, and an output cap. The command runs under a low-integrity restricted token, so a body proposed by the model cannot write outside the shadow copy. If the token cannot be built and verified, the command is refused rather than run unconfined.
Accepted changes go through a write-ahead journal and an atomic write-rename. A crash at any point leaves either the old file or the new one, never a torn write. The recover command replays the journal and refuses anything it cannot prove: zero-byte files, entries that no longer re-parse, and malformed tags.
Fail-closed by design
The kernel is fail-closed. When it cannot prove that a change is safe, the change is refused. Uncertainty is never resolved in favor of the proposal. This is the opposite of how current AI coding tools work, which compete on autonomy and speed, increasing the volume of unverified output.
The engine layer, which contains the tree-sitter parsing, symbol table, content hashing, AST-verified mutation, and boundedness analysis, is pure and deterministic with no I/O. The platform layer handles the disk, sandbox, shadow workspace, and test runner. The protocol layer is the MCP surface. The dependency direction is strict: protocol to platform to engine. The engine cannot import the platform. Everything that decides whether a change is valid is a pure function of its inputs.
Verification of the verifier
A verification layer that has not been verified is only a more elaborate way of hoping. Emetgate mutation-tests its own guards. Guards and branches that protect an invariant are mutated: a check removed, a condition weakened, a comparison flipped, and the test suite runs against each mutant. At least one test must fail. A surviving mutant is either killed by a new test or recorded in tests/mutations.json with the reason it cannot be: an equivalent mutant, with the grammar or code fact that makes it one, or a redundant guard kept on purpose.
For the engine today, that is 44 mutants: 37 killed, 4 proven equivalent, 1 redundant guard kept as defense in depth, 2 open. Dedicated red-team suites attack the gate directly with bodies that escape their braces, stale hashes, torn journal entries, poisoned repository configuration, and attempts to open files outside the repository.
What it does not do
Semantic correctness. Code that parses, stays in bounds, and passes the tests can still implement the wrong behavior. The kernel raises the floor; it does not replace tests that encode intent, or a human decision where one is needed.
The quality of the test suite. For unbounded changes, the test gate is only as strong as the tests it runs. Mediation. The guarantees hold for changes that go through the gate. Edits made by other tools bypass it, which is why lockdown exists. The model cannot supply the test command or the typecheck command. Those come from the repository configuration or the command line.
Taste. Architecture, API design, and user experience are not properties a kernel can check.
Current state and limitations
The project supports TypeScript and JavaScript. New languages are added as profiles and must pass a conformance suite. It runs on Windows only, because the sandbox relies on Job Objects. The decision ledger is built but not yet exposed as MCP tools. Rule enforcement at the edit gate is in progress.
The MCP server exposes tools for listing symbols, reading symbol bodies, verifying proposed mutations without writing, and committing verified changes. The lockdown mode starts Claude Code with only these tools available, so the model has no path to the disk other than the gate.
On a token benchmark, editing through symbol-level proposals uses a median of 1.80 times fewer tokens than search-and-replace editing, with a range of 1.15 to 3.77 times. On real files the gain is modest. Token savings are a side effect, not the point.
The project is built with Zig, requires version 0.16.0, and ships as a single Windows binary. It is at github.com/emetgate/emetgate.