Emetgate : une porte de vérification entre LLM et code

Ce qu'est Emetgate

Emetgate est un projet open source hébergé sur GitHub (emetgate/emetgate). Son README le décrit comme « un noyau de vérification déterministe placé entre un modèle de langage et votre arbre de sources ». Sa devise : « Nothing passes but the truth. » (Seule la vérité passe.) Le README précise que le projet est à un stade précoce et volontairement étroit. Il cible uniquement Windows, il est écrit en Zig 0.16.0, il traite le code TypeScript et JavaScript, et il parle le Model Context Protocol (MCP). Un client MCP comme Claude Code peut donc s'y connecter.

L'idée est simple à énoncer. Un modèle de langage peut lire le code et proposer une modification d'un symbole. Il ne peut pas écrire un fichier, ni déclarer un travail terminé. Un petit noyau examine chaque proposition et la valide de façon atomique, ou la rejette en donnant une raison. Le README résume : « Le modèle propose. Le noyau vérifie. Rien de non vérifié n'atteint le disque. »

Pourquoi l'auteur l'a construit

Le README énumère des défaillances que connaît quiconque utilise sérieusement du code généré par un LLM : du code qui compile et reste faux, un modèle qui annonce une tâche terminée alors qu'elle ne l'est pas, une règle posée trois tours plus tôt qui est oubliée en silence, un plan convenu au début d'une session qui s'est évaporé à la fin. L'auteur soutient que ces problèmes semblent distincts mais ont une seule cause : rien entre le modèle et le disque n'est chargé de vérifier ce que le modèle a produit.

Selon le README, les outils actuels rivalisent d'autonomie et de vitesse, ce qui augmente le volume de sortie non vérifiée. Le modèle ne peut pas combler cet écart seul, car il est « un échantillonneur, pas un oracle », sans mémoire persistante. Emetgate ne donne donc aucune autorité au modèle et place toute l'autorité dans le noyau. Le README compare cela aux prouveurs de théorèmes de type LCF, où les tactiques peuvent tout suggérer mais où seul un petit noyau de confiance peut produire un théorème. Le nom vient de la légende du Golem de Prague : le mot *emet* (« vérité ») inscrit sur le front du golem l'anime, et effacer une lettre laisse *met* (« mort »).

Le parcours d'un changement à travers la porte

Le README décrit six étapes.

1. **Adressage.** Chaque symbole est identifié par une référence, comme `Class.method` ou `add`, et par un hachage de 128 bits de son contenu actuel. Une proposition doit nommer le hachage sur lequel elle repose. Si le fichier a changé entre-temps, le hachage ne correspond plus et la proposition est rejetée. Le modèle ne peut donc pas écraser du code qu'il n'a pas vu.

2. **Analyse.** Le nouveau corps de fonction est inséré dans la source selon une plage d'octets, et le fichier entier est ré-analysé avec tree-sitter.

3. **Garde.** Le noyau vérifie que le résultat s'analyse proprement, que le corps ne déborde pas de ses accolades, qu'il n'est ni vide ni un simple espace réservé, et que chaque octet situé hors de la zone visée reste intact.

4. **Bornage.** Le noyau calcule le rayon d'impact. L'analyse est un décompte positif en monde clos : un changement n'est `BOUNDED` que si toutes les manières dont il pourrait s'échapper ont été écartées. Tout ce que l'analyse ne sait pas expliquer est `UNBOUNDED`.

5. **Test.** Les changements `UNBOUNDED` sont appliqués à une copie fantôme, et la commande de test du projet s'exécute contre elle dans un bac à sable. Ce bac à sable est un Job Object Windows avec kill-on-close, limites de temps réel et de mémoire, et plafond de sortie. La commande tourne sous un jeton restreint de faible intégrité. Si ce jeton ne peut pas être construit et vérifié, la commande est refusée plutôt que lancée sans confinement. Un test en échec rejette le changement et renvoie la sortie au modèle.

6. **Validation.** Les changements acceptés passent par un journal à écriture anticipée et par un renommage atomique. Un plantage laisse soit l'ancien fichier, soit le nouveau, jamais une écriture tronquée. La commande `recover` rejoue le journal et refuse tout ce qu'elle ne peut pas prouver.

Le README qualifie le noyau de fail-closed : quand il ne peut pas prouver qu'un changement est sûr, il le refuse.

La surface MCP et le mode lockdown

Le serveur expose des outils de lecture et de modification. Côté lecture : `emetgate_symbols`, `emetgate_skeleton`, `emetgate_read_symbol`, `emetgate_read_file`, `emetgate_list` et `emetgate_search`, les trois derniers étant confinés au dépôt. `emetgate_mutate` vérifie la structure d'un corps proposé sans rien écrire. `emetgate_try` vérifie, fait passer la porte et valide un corps. `emetgate_try_batch` traite plusieurs propositions comme une seule unité. `emetgate_scan` mesure une expression de contrôle sur le dépôt et n'écrit rien.

La commande `emetgate lockdown` démarre Claude Code avec ces seuls outils, de sorte que le modèle n'a aucun chemin vers le disque en dehors de la porte. Le dépôt fournit aussi une compétence Claude Code, `md-audit`, qui classe chaque phrase d'instruction d'un fichier CLAUDE.md ou AGENTS.md en applicable, en attente d'un mécanisme, invérifiable ou croyance, puis mesure les phrases applicables avec `emetgate_scan`. Elle ne modifie rien.

Comment le noyau lui-même est vérifié

Le README affirme qu'une couche de vérification qui n'a pas été vérifiée « n'est qu'une manière plus élaborée d'espérer ». Il nomme deux pratiques. La première est le test de mutation : on mute les gardes (un contrôle retiré, une condition affaiblie, une comparaison inversée) et la suite de tests doit échouer pour chaque mutant. Pour les modules `cas`, `boundedness`, `symbol` et `functions` du moteur, le README rapporte 44 mutants : 37 tués, 4 prouvés équivalents, 1 garde redondante conservée en défense en profondeur et 2 restés ouverts. La seconde pratique consiste en des suites de tests d'équipe rouge qui attaquent des corps évadés de leurs accolades, des hachages périmés, des entrées de journal déchirées, une configuration de dépôt empoisonnée et l'accès à des fichiers hors du dépôt.

Le README fournit aussi un banc d'essai en jetons. Sur six scénarios (dont deux fichiers réels) avec le tokenizer `o200k_base`, les propositions au niveau du symbole ont consommé en médiane 1,80 fois moins de jetons que l'édition par recherche et remplacement, avec une plage de 1,15 à 3,77 fois. Sur les fichiers réels, le gain est de 1,15 à 1,17 fois. Le README qualifie l'économie de jetons d'« effet secondaire, pas le but ».

Notre analyse

Le choix de conception à retenir tient à l'endroit où l'on place la confiance. Beaucoup d'outils de programmation se demandent comment rendre le modèle plus fiable. Emetgate se demande comment rendre son manque de fiabilité inoffensif. Comme les contrôles sont des fonctions déterministes de leurs entrées, un relecteur peut les lire, les tester et les attaquer. C'est un autre type de garantie que l'affirmation du modèle selon laquelle la tâche est terminée.

Deux détails ressortent. Les hachages de contenu transforment « le modèle a édité du code périmé » d'un bogue silencieux en une proposition rejetée. Et la règle de bornage en monde clos lance les tests par défaut en cas de doute, ce qui échange de la vitesse contre de la sécurité.

Limites et questions ouvertes

Le README est franc sur les limites. Du code qui s'analyse, reste dans ses bornes et passe les tests peut encore implémenter un mauvais comportement. La porte de test n'est aussi solide que les tests. Les garanties ne valent que pour les changements qui passent par la porte : les modifications faites par d'autres outils la contournent, d'où l'existence de lockdown. Le jeton de faible intégrité empêche d'écrire hors de la copie fantôme, mais il ne restreint ni la lecture ni l'accès réseau : une commande de test hostile pourrait encore lire les fichiers auxquels elle a droit et joindre le réseau. Un AppContainer est prévu. L'architecture, la conception d'API et l'expérience utilisateur ne sont pas des propriétés qu'un noyau peut vérifier.

D'après le tableau d'état, le registre de décisions n'est pas encore exposé en outils MCP et l'application des règles à la porte d'édition est en cours. Le support se limite à TypeScript et JavaScript, et à Windows. Nous n'avons lu que le README. Nous n'avons pas exécuté l'outil, et les chiffres du banc d'essai et des mutations sont ceux de l'auteur.

Conseils pratiques

Les équipes sous Windows qui écrivent en TypeScript ou JavaScript peuvent télécharger le binaire de la version et sa somme de contrôle SHA-256, les comparer, puis enregistrer le serveur avec `claude mcp add`. Le README note que le binaire n'est pas signé, si bien que SmartScreen avertit au premier lancement. La compilation demande Zig 0.16.0 et `zig build`.

Les commandes de vérification de types et de test viennent de l'opérateur, via `--typecheck` et `--test`, ou depuis `.emetgaterc.json` avec `--allow-repo-config`. Le modèle ne peut jamais les fournir. Pour les autres lecteurs, le README se lit comme l'énoncé concis d'un principe utile : ne donner aucun accès en écriture au modèle, et faire passer chaque changement accepté par un contrôle qu'une personne peut inspecter.