Invariants comportementaux : évaluer un auditeur de code sur des bugs qui n'existent que dans le temps#

Note de : Rémi Viau (mainteneur d'Anatoly), avec Claude (Anthropic Opus 4.8) comme partenaire d'analyse. Dépôts référencés : Anatoly, anatoly-bench, Evolve.

Les défauts qu'une seule ligne ne peut pas montrer#

La plupart des benchmarks d'audit de code testent des défauts visibles à un seul endroit. Une constante fixée à la mauvaise valeur. Une vérification de nullité oubliée. Un bloc de logique recopié deux fichiers plus loin. La première fixture d'Anatoly, slot-engine, est bâtie sur ce modèle : 27 défauts plantés sur cinq axes notés, chacun rattaché à un fragment de code que l'on peut désigner du doigt.

Toute une catégorie de bugs réels échappe à ce schéma. Ce sont des violations de propriétés qui ne se vérifient qu'au fil d'une exécution :

• Vivacité : toute tâche finit par se terminer.
• Exclusion mutuelle : une ressource partagée n'a jamais plus d'un utilisateur à la fois.
• Ordre : les tâches prioritaires passent avant les moins prioritaires.
• Conservation : chaque élément est traité exactement une fois, jamais zéro, jamais deux.
• Séparation temporelle : deux évènements restent espacés d'au moins un intervalle minimal.

Dans aucun de ces cas vous ne pouvez pointer la ligne fautive. La ligne qui acquiert un verrou paraît correcte. La ligne qui compare deux éléments paraît correcte. Le défaut réside dans ce que le programme fait au fil du temps, à travers plusieurs acteurs, et qu'aucune ligne prise isolément ne révèle. Ce sont aussi les bugs qui coûtent le plus cher en production : interblocages, accès concurrents, double traitement, mises à jour perdues.

C'est précisément cet écart que train-dispatch cherche à mesurer. Un auditeur de code LLM sait-il repérer une violation d'invariant comportemental par revue statique, quand il n'y a aucun motif à reconnaître et que la seule voie vers le bug passe par un raisonnement sur le comportement ? slot-engine ne pouvait pas répondre, puisque chacun de ses défauts est local par construction. Il fallait une seconde fixture dont les défauts soient, par construction, non locaux.

La fixture : un répartiteur de trains déterministe#

train-dispatch est un petit projet TypeScript : le cœur d'ordonnancement d'un réseau ferroviaire miniature. Il expose une seule fonction pure, runSchedule(), qui déroule une simulation à évènements discrets sur des ticks entiers, à travers un réseau et un horaire fixes, et renvoie la trace des mouvements. Le moteur ne contient aucun générateur de nombres aléatoires. Le même réseau et le même horaire produisent toujours la même trace.

Ce déterminisme est le choix de conception qui porte toute la fixture. slot-engine embarque une machine à sous stochastique : mesurer son comportement réclame un tirage Monte-Carlo de 100 000 lancers. train-dispatch, lui, est déterministe, donc une seule exécution constitue la vérité terrain. Un run, une trace, aucune statistique.

Le répartiteur annonce quatre garanties de fonctionnement, inscrites dans le README.md fourni et considérées comme le contrat produit :

• Ponctualité : chaque train arrive dans une fenêtre de tolérance autour de son horaire prévu.
• Exclusivité : un bloc de voie ne contient qu'un train par tick.
• Vivacité : chaque train réparti atteint sa destination.
• Conservation : chaque train réparti arrive exactement une fois.

L'implémentation livrée enfreint les quatre, de six manières précises et cataloguées.

Les six défauts plantés#

Deux des trois défauts les plus durs, INV-MUTEX et INV-DEADLOCK, logent dans le même fichier (interlocking.ts), ce qui oblige l'auditeur à distinguer deux défaillances comportementales différentes au sein d'un même module.

La fixture est générée par Evolve à partir d'une spécification, puis figée. Cette spécification fait office d'unique source de vérité, aussi bien pour Evolve (qui fait converger le code jusqu'à ce qu'un script --check confirme que chaque garantie est mesurablement cassée) que pour le scoreur du bench (qui lit le même catalogue pour noter les constats d'Anatoly). Une règle stricte de la spec : les défauts doivent ressembler à du code de production ordinaire, un brin négligé. Aucun commentaire ne doit mentionner "intentionnel", "bug", "course", "deadlock" ni rien d'équivalent. Une fixture qui annote ses propres bugs ne mesure rien. Pour les trouver, l'auditeur doit raisonner sur le comportement du répartiteur, et c'est là tout l'intérêt.

Un seul axe noté, volontairement#

train-dispatch ne note qu'un seul axe : la correction. Le projet ne livre aucun test, presque aucune documentation, et quelques modules "de bruit" délibérément propres dont le seul rôle est d'offrir des occasions de faux positifs. Comme il n'y a qu'un axe noté, le F1 global est égal au F1 de correction. Aucune moyenne entre axes ne vient amortir une détection ou un oubli isolé.

Le signal en ressort net, et un peu brutal. Avec six défauts sur un seul axe, un constat détecté ou manqué déplace le F1 global d'environ 10 à 12 points. L'avantage : rien ne se dissimule. Le score se lit directement comme le nombre d'invariants comportementaux récupérés par l'auditeur, les modules de bruit maintenant la précision sous tension.

Quatre runs en une journée#

Les quatre runs ont été enregistrés le 2026-06-15. La fixture était toute neuve : contrairement au long historique de slot-engine, il n'existe pas encore d'ère à surface figée. La surface de code elle-même a bougé entre v1 et v3, le temps que la sortie d'Evolve converge vers sa forme finale. v3 et v4 partagent le même état de projet figé.

Trois défauts sont détectés à chaque run : INV-PRIORITY, INV-MUTEX et INV-CONSERVATION. Le fait mérite d'être dit franchement : un auditeur LLM récupère les violations d'exclusion mutuelle et de conservation par revue statique de façon plus fiable que je ne m'y attendais au départ. INV-HEADWAY est détecté dans trois runs sur quatre. La chute à 50.0% en v2 montre le côté tranchant de la conception à axe unique : un oubli de plus et deux faux positifs supplémentaires, sur un état de fixture encore en train de se stabiliser, coûtent plus de 20 points d'un seul coup.

La comparaison intéressante oppose v3 à v4. Le projet est identique octet pour octet entre les deux. Seul Anatoly lui-même a changé.

Le constat : un benchmark qui a trouvé un bug dans notre propre récupérateur#

Voici la partie qui justifie la construction de la fixture, et ce n'est pas le score.

v4 n'apporte qu'un seul changement côté Anatoly par rapport à v3, sur la branche rag-index-declarations. Il corrige un trou de récupération que train-dispatch était particulièrement bien placé pour exposer, grâce à une propriété que slot-engine n'a jamais eue : un défaut logé dans un fichier sans la moindre fonction.

Les fichiers de données pures étaient invisibles à l'indexeur#

L'indexeur RAG d'Anatoly transforme les symboles d'un fichier en cartes interrogeables. Le filtre en cause, tiré du code source d'Anatoly sous licence AGPL-3.0, tient en une ligne :

// src/rag/indexer.ts (AGPL-3.0)
const functionSymbols = task.symbols.filter(
  (s) => s.kind === 'function' || s.kind === 'method' || s.kind === 'hook',
);
// Une carte est construite pour chaque functionSymbol, et seulement pour ceux-là.

timetable.ts est un module de données pures : des const, type et enum de premier niveau, sans aucune fonction. Il ne produisait donc aucune carte, et ne stockait donc aucun vecteur NLP. En aval, le récupérateur de documentation par fichier réclame à la base vectorielle le vecteur NLP moyen de ce fichier :

// src/core/docs-resolver.ts (AGPL-3.0)
let queryEmbedding = await vectorStore.getAverageNlpVectorByFile(filePath);

Pour timetable.ts, cet appel renvoyait null, faute de carte à moyenner. La seule requête qu'il restait au récupérateur était le nom du fichier (Module: timetable), bien trop maigre pour amener la section horaire du README jusqu'à la constante qui en avait besoin.

Rapprochez maintenant ce point d'INV-DWELL. INV-DWELL est le défaut trivial : une constante, DWELL_TICKS = 6, qui contredit l'arrêt en gare de 2 ticks documenté dans le README. Pour ne serait-ce que le soupçonner, l'auditeur a besoin que la phrase du README, "Un arrêt en gare dure 2 ticks", soit posée à côté de la constante. Or le fichier qui contenait cette constante était invisible à la récupération de documentation : la contradiction restait hors de portée. Le défaut le plus facile de la fixture était inatteignable pour une raison sans aucun rapport avec la capacité de raisonnement, et entièrement liée à ce que l'indexeur choisissait d'indexer.

Le correctif#

Le changement rag-index-declarations indexe les déclarations non fonctionnelles sous une nouvelle carte kind: 'declaration'. Le résumé est synthétisé à partir de l'AST, sans appel LLM supplémentaire, pour un coût négligeable. La carte de déclaration entre dans la moyenne NLP par fichier, ce qui donne à un fichier de données pures une véritable empreinte sémantique, mais elle est exclue de la recherche de similarité de code et de duplication, pour qu'une simple constante ne soit jamais comptée comme le "doublon" d'une fonction.

Le run de bench apporte la preuve que le trou est bouché. Après le correctif, la revue de correction de timetable.ts porte reference_source: README.md#Timing et l'extrait "A station dwell is 2 ticks...". Avant le correctif, cette documentation ne pouvait physiquement pas atteindre le fichier. Le socle de récupération dont INV-DWELL a besoin est désormais en place, et il apparaît comme un artefact tangible dans le rapport, pas seulement comme un point sur un graphe.

Voilà l'argument en faveur de la fixture, résumé en un exemple. Un benchmark ne se réduit pas à un tableau de scores. Une fixture délibérément construite autour d'un fichier de données pures porteur d'un invariant documenté a révélé un trou de récupération architectural qu'aucune relecture du rapport d'audit n'aurait pu mettre au jour, puisque le document manquant n'apparaissait jamais dans le rapport au départ. La conception à axe unique, centrée sur le comportement, a rendu ce trou lisible.

Ce qui reste manqué, et pourquoi c'est la partie intéressante#

Deux défauts résistent à chaque run, de v1 à v4, et ils échouent pour deux raisons très différentes.

INV-DWELL : la détection fonctionne, pas la classification. C'est le cas subtil. Après le correctif d'indexation des déclarations, l'extrait du README arrive bien, et la contradiction est détectée : elle remonte sous la forme d'un doc_divergence et d'un constat documentation: UNDOCUMENTED. Mais le verdict de l'axe correction sur la constante reste OK, au motif qu'il n'y a pas de défaut au niveau du code, seulement une valeur qui diverge du README. Le catalogue, lui, classe INV-DWELL comme un défaut de correction : la classification en divergence ne rapporte donc aucun point. Le trou de récupération est bouché ; ce qui subsiste est une question de règle. L'axe correction doit-il traiter une constante qui contredit un invariant documenté comme un défaut de correction à part entière, ou s'en tenir à la classification en divergence ? C'est une décision de responsable, pas une amélioration de détection. On retrouve le thème de la boucle d'arbitrage de slot-engine : une contradiction peut être détectée et exposée sans jamais être reportée sur l'axe noté.

INV-DEADLOCK : un vrai raisonnement multi-acteurs. C'est le défaut le plus dur de la fixture, et aucun run n'en est venu à bout. L'attente en cercle ne se manifeste que lorsqu'un train vers l'est et un train vers l'ouest abordent la même section à voie unique en sens inverse et sont considérés ensemble, dans la durée. La ligne qui réserve un bloc paraît correcte. Le bug tient à l'ordre dans lequel deux trains différents acquièrent deux blocs partagés, visible seulement à travers la trace d'exécution des deux. Le faire émerger par revue statique reste une vraie frontière pour un auditeur LLM, et il est honnête de la laisser ouverte.

Les deux oublis persistants délimitent proprement le travail qui reste. L'un relève d'une règle de classification entre axes. L'autre d'un raisonnement multi-acteurs sur la trace d'exécution. Aucun des deux n'est plus un problème de récupération, et c'est exactement le genre de clarté qu'une fixture ciblée doit apporter.

Ce que cela dit des auditeurs de code LLM#

Trois enseignements que je défends volontiers à partir de quatre runs, tout en restant clair : quatre runs sur une fixture à axe unique forment un petit échantillon.

1. Plusieurs invariants comportementaux sont à portée de la revue statique aujourd'hui. L'exclusion mutuelle, la conservation et l'ordre de priorité sont détectés de façon fiable ici, ce qui dément le préjugé selon lequel "les LLM ne font que reconnaître la syntaxe par motif".
2. Les deux écarts difficiles ne sont pas ceux que j'aurais devinés. Ce sont une décision de règle de classification et un raisonnement multi-acteurs sur la trace, pas de la détection brute. Savoir quel écart on a sous les yeux représente l'essentiel de la valeur.
3. Un benchmark gagne sa place quand il met à l'épreuve votre architecture, pas seulement votre score. Le trou d'indexation des déclarations le prouve. Invisible depuis le rapport, évident depuis la fixture : c'est toute la raison de construire des fixtures qui explorent des configurations présentes dans vos vrais dépôts mais que vos tests existants n'isolent pas.

Pour deux résultats voisins issus du même bench, voyez le constat sur la discipline de concision, où un changement de prompt de 12 lignes a amélioré le F1 tout en réduisant les tokens sur slot-engine, et notre question ouverte sur le remplacement du RAG vectoriel par fonction, qui se situe juste en amont du trou de récupération décrit ici.

Reproduire ceci#

La fixture, le catalogue et les baselines par run vivent dans anatoly-bench sous catalog/train-dispatch/. Chaque run est un unique anatoly run contre catalog/train-dispatch/project/, noté avec anatoly-bench score. L'agent d'audit lui-même est Anatoly, et la fixture est générée à partir de sa spécification par Evolve. Comme le bench ne consomme que les artefacts publics du rapport d'Anatoly sans jamais importer ses types, tout changement de format de rapport casse le bench de façon bruyante, ce qui est le bon signal qu'un contrat a bougé.