Emetgate's maintainers claim their released Windows MCP kernel confines coding-agent changes to hash-checked, structurally validated function-body replacements with sandboxed test gates and atomic commits, providing an enforceable source-editing boundary rather than relying on agent compliance.

Open article · Retrieved 2026-09-20T20:22:44.608584+00:00

[Emetgate](https://github.com/emetgate/emetgate/blob/main/assets/banner.png)

[Status: early](https://camo.githubusercontent.com/1f64ae8fc1aa5953a2c1a2c332d3d56dbaa6a45df5da08ab410305e167977806/68747470733a2f2f696d672e736869656c64732e696f2f62616467652f7374617475732d6561726c792d4530343046423f7374796c653d666c61742d737175617265)
[Zig 0.16.0](https://camo.githubusercontent.com/c59bebb8b84e1d781bc449e6d18b8670258796df8cefcfb82c00992bc55ec00f/68747470733a2f2f696d672e736869656c64732e696f2f62616467652f7a69672d302e31362e302d4637413431443f7374796c653d666c61742d737175617265266c6f676f3d7a6967266c6f676f436f6c6f723d7768697465)
[Platform: Windows](https://camo.githubusercontent.com/1a3e02815a672e2fd85c44c882eff907f2027c74e48dd3cb2259fea9f786d005/68747470733a2f2f696d672e736869656c64732e696f2f62616467652f706c6174666f726d2d77696e646f77732d3030373844363f7374796c653d666c61742d737175617265)
[Languages: TypeScript, JavaScript](https://camo.githubusercontent.com/081ee1b7fb8c200848e892c01eea2d3e2bf40faf76d0e2d386b4dcca34119fa7/68747470733a2f2f696d672e736869656c64732e696f2f62616467652f6c616e6775616765732d747970657363726970742532302537432532306a6176617363726970742d3331373843363f7374796c653d666c61742d737175617265)
[Protocol: MCP](https://camo.githubusercontent.com/8e872e32a03db04ed92cdfca8f27929991cc0e6679aa4bdd6ea2cb1a8741b772/68747470733a2f2f696d672e736869656c64732e696f2f62616467652f70726f746f636f6c2d4d43502d3145314232363f7374796c653d666c61742d737175617265)

**Nothing passes but the truth.**  
A deterministic verification kernel that sits between a language model and your source tree.

[Five proposals through the gate: four refused, one committed](https://github.com/emetgate/emetgate/blob/main/assets/demo.gif)

A real session, rendered: a placeholder body, an escaped body, a stale hash and a write outside the shadow copy are all refused; a correct body is committed.

---

## The name

In the legend of the Golem of Prague, a rabbi shapes a figure out of river clay. It is strong, tireless and obedient, and it has no judgment of its own. What animates it is a single word written on its forehead: **אמת**, *emet*, "truth". When the golem runs out of control, the rabbi erases the first letter. What remains is **מת**, *met*, "dead", and the golem falls back into clay.

The three letters of *emet* are the first, the middle and the last letter of the Hebrew alphabet. The traditional reading is that truth has to hold from beginning to end; take one piece away and it is no longer truth.

A language model is a golem in the precise sense of the story. It produces a great deal of work, quickly, and it has no way of knowing whether that work is correct. Emetgate is the word on the forehead and the gate in front of the door: the model may propose anything, and only what can be verified is allowed through.

## Why this exists

The failure modes of LLM-generated code are well known to anyone who has used it seriously:

- The code compiles and is still wrong.
- The model reports a task as done when it is not.
- A rule stated three turns ago is silently forgotten.
- A plan agreed at the start of a session has evaporated by the end of it.

These look like separate problems. They share one cause: **nothing between the model and the disk is responsible for checking what the model produced.** The current generation of tools competes on autonomy and speed, which increases the volume of unverified output. The model itself cannot close the gap. It is a sampler, not an oracle; it has no persistent memory, and it cannot verify its own work.

Emetgate takes the opposite position. The model holds no authority at all. A small deterministic kernel holds all of it.

## Core principle

> **The model proposes. The kernel verifies. Nothing unverified reaches the disk.**

- The model can read code, and it can propose a change to a symbol. It cannot write a file, it cannot mark work as finished, and its claims about its own output carry no weight.
- The kernel decides. Every proposal is checked structurally and, where the change is not provably contained, against the project's test command. It is either committed atomically or rejected with a reason.
- The kernel is **fail-closed**. When it cannot prove that a change is safe, the change is refused. Uncertainty is never resolved in favour of the proposal.

This is not a new idea. It is the architecture of LCF-style theorem provers, where tactics may suggest anything but only a small trusted kernel can produce a theorem, and it is what de Bruijn meant when he argued that 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 a change moves through the gate

```
 model ──propose──▶ ┌──────────────────────────────── kernel ────────────────────────────────┐
                    │                                                                          │
                    │  1. address     symbol + content hash must match what is on disk         │
                    │  2. parse       new body is spliced by byte range and re-parsed          │
                    │  3. guard       no syntax errors, no escape from the body, no            │
                    │                 placeholders, nothing outside the span may change        │
                    │  4. bound       blast radius is computed: BOUNDED or UNBOUNDED           │
                    │  5. test        UNBOUNDED changes run the full test gate in a sandbox    │
                    │  6. commit      journaled, atomic write-rename, or reject with a reason  │
                    │                                                                          │
                    └──────────────────────────────────────────────────────────────────────────┘
                                          │                          │
                                     committed                   rejected
```

**Content addressing.** Every symbol is identified by a reference (`Class.method`, `add`) and a 128-bit hash of its current content. A proposal must name the hash it was based on. If the file changed in the meantime, the hash no longer matches and the proposal is rejected. The model cannot overwrite code it has not seen.

**AST-verified mutation.** A change replaces exactly one function body. The new body is spliced into the source by byte range and the whole file is re-parsed with tree-sitter. The kernel then 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.

**Boundedness.** Before running anything, the kernel computes whether the change can affect code beyond the symbol itself. The analysis is a positive, closed-world count: a change is `BOUNDED` only when every way it could escape has been ruled out, and the verdict carries its provenance. Anything the analysis cannot account for is `UNBOUNDED`.

**Test gate.** `UNBOUNDED` changes are applied to a shadow copy and the project's test command is run against it inside a sandbox (a Windows 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 anywhere outside the shadow copy; if that token cannot be built and verified, the command is refused rather than run unconfined. If the tests fail, the change is rejected and the output is returned to the model.

**Durable commit.** 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. `recover` replays the journal and refuses anything it cannot prove: zero-byte files, entries that no longer re-parse, and malformed tags.

## Architecture

```
src/
├── engine/      pure and deterministic, no I/O
│   ├── tree_sitter, loader, traversal, skeleton
│   ├── symbol, ref, functions        symbol table, references, content hashes
│   ├── cas                           AST-verified mutation and structural guards
│   └── boundedness                   closed-world blast-radius analysis
├── platform/    everything that touches the machine
│   ├── disk                          journal, atomic write, recovery
│   ├── sandbox                       Job Object isolation and resource limits
│   ├── shadow, repo, lockdown        shadow workspace, repo lock, locked-down launch
│   ├── runner, gate, batch           cas → boundedness → test gate
│   └── memory                        append-only decision ledger
└── protocol/    the MCP surface
    ├── server, handlers, wire        tools and typed results
    ├── policy, telemetry             repo-config trust, event log
    └── read_tools, diagnostics       scoped reads, tsc diagnostics
```

The dependency direction is strict: `protocol → platform → engine`. The engine cannot import the platform. Everything that decides whether a change is valid is a pure function of its inputs, which is what makes it testable to the standard described below.

### MCP tools

| Tool | Purpose |
| --- | --- |
| `emetgate_symbols` | Symbols in a file, with references, positions and content hashes |
| `emetgate_skeleton` | Signatures and structure without bodies |
| `emetgate_read_symbol` | The source of one symbol |
| `emetgate_mutate` | Verify a proposed body structurally and return the result without writing |
| `emetgate_try` | Verify, gate and commit a proposed body |
| `emetgate_try_batch` | Several proposals as one unit |
| `emetgate_read_file`, `emetgate_list`, `emetgate_search` | Reads confined to the repository |
| `emetgate_scan` | Measure one check expression against the repository, optionally within a `where` scope; writes nothing |

`emetgate lockdown` starts Claude Code with only these tools available, so the model has no path to the disk other than the gate.

The repository ships a Claude Code skill, `.claude/skills/md-audit/SKILL.md`, that audits a CLAUDE.md or AGENTS.md file: it sorts every instruction sentence into enforceable, waiting for a mechanism, unverifiable or belief, proposes a check and scope for the enforceable ones, measures each with `emetgate_scan` and reports, changing nothing. To use it in every project, copy the `md-audit` folder into `%USERPROFILE%\.claude\skills\` (`~/.claude/skills/` elsewhere).

## How the kernel itself is verified

A verification layer that has not been verified is only a more elaborate way of hoping. Two rules apply to every guard in the kernel.

**Mutation kill.** Guards and branches that protect an invariant are mutated (a check removed, a condition weakened, a comparison flipped) and the test suite is run 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. Mutants with no killing input and no proof of equivalence are marked open rather than hidden. The harness lives in `tools/mutate`.

For the engine (`cas`, `boundedness`, `symbol`, `functions`) that is 44 mutants today: 37 killed, 4 proven equivalent, 1 redundant guard kept as defense in depth, 2 open.

**Adversarial tests.** Dedicated red-team suites attack the gate directly: bodies that escape their braces, stale hashes, torn journal entries, poisoned repository configuration and attempts to open files outside the repository.

## Status

Emetgate is early and deliberately narrow.

| Area | State |
| --- | --- |
| AST-verified mutation, content hashes, structural guards | Built, mutation-tested |
| Boundedness analysis and test gate | Built, mutation-tested |
| Journal, atomic commit, recovery, sandbox | Built |
| MCP server and locked-down launch | Built |
| Decision ledger (append-only, supersession, compaction, torn-tail recovery) | Built, not