Un historique d'IA n'est pas une preuve
Voilà ce que nous avons construit pour essayer de le rendre vérifiable.
En avril dernier, j'écrivais une phrase assez simple :
« Vous n'avez pas de preuves. Vous avez des croyances. »
À l'époque, je parlais surtout d'un problème de fond.
L'intelligence artificielle nous donne de plus en plus de réponses, de recommandations et bientôt de décisions. Mais lorsque ces systèmes commencent à intervenir dans des processus juridiques, financiers, industriels ou stratégiques, une question finit toujours par apparaître :
Comment prouver, plusieurs semaines ou plusieurs mois plus tard, ce qui s'est réellement passé ?
Prouver ce que l'on peut réellement prouver.
Depuis, nous avons essayé de transformer cette question en problème d'ingénierie.
Et nous avons découvert quelque chose d'important :
un dossier peut être cryptographiquement vérifiable… et contenir une information fausse.
Ce n'est pas un échec de notre protocole.
C'est probablement l'un des résultats les plus utiles de nos travaux.
Dans nos tests, nous avons volontairement introduit une source contenant une information sémantiquement fausse.
Le dossier pouvait donc être classé :
VERIFIED
Alors même que son contenu initial était faux.
Cela peut sembler paradoxal.
Ça ne l'est pas.
Une preuve d'intégrité répond à une question :
« Est-ce bien ce qui a été enregistré à ce moment-là ? »
Elle ne répond pas à :
« Ce qui a été enregistré était-il vrai ? »
Confondre les deux permet de faire des promesses spectaculaires.
Les distinguer permet de construire des systèmes auditables.
Nous avons choisi la seconde voie.
Prenons un système qui enregistre 10 000 décisions.
Cela paraît solide.
Mais supposons maintenant que l'opérateur supprime silencieusement les 300 décisions les plus embarrassantes avant de remettre son dossier à l'auditeur.
Les 9 700 décisions restantes peuvent toujours être parfaitement signées.
Chaque enregistrement présenté est authentique.
Et pourtant, la population présentée est incomplète.
C'est le problème qui nous intéressait réellement.
Une preuve ne doit donc pas seulement permettre de demander :
« Ce dossier a-t-il été modifié ? »
Elle doit également permettre de demander :
« Une décision qui avait été admise peut-elle disparaître silencieusement de l'histoire présentée plus tard ? »
C'est à cette deuxième question que nous avons consacré l'essentiel de notre travail.
Nous avons choisi une propriété volontairement étroite.
Lorsqu'une opération franchit une frontière déclarée de notre système et que cette admission est reconnue par notre mécanisme de témoin, elle doit ensuite rester comptabilisée.
Mais elle ne doit pas simplement disparaître.
Pour qu'une population soit classée VERIFIED, chaque admission reconnue doit pouvoir être réconciliée avec un état terminal explicite.
Autrement dit :
une admission connue du témoin doit continuer à exister dans l'histoire que l'on présente comme complète.
Nous appelons cela la continuité de population après admission.
Cet article présente les principaux enseignements de nos travaux. Le protocole, le modèle de menace, les scénarios hostiles, les résultats expérimentaux et les limites sont documentés dans notre note technique complète.
Référence protocole / publication : f7cfe7ede525d5ba1b01f8f44ea8b2b54fe759eb Implémentation durcie après PR #30 : 13524a13bfaa1d312c84fa7dcc588ede742b6388
Une grande partie du problème vient de l'ordre des opérations.
Une architecture classique peut fonctionner ainsi :
Mais que se passe-t-il si le système tombe entre l'étape 1 et l'étape 3 ?
L'action a peut-être eu lieu.
Le dossier, lui, n'en sait rien.
Nous avons donc inversé la logique sur les frontières que nous protégeons.
D'abord, l'intention ou l'admission est enregistrée. Ensuite seulement, l'exécution peut commencer.
Si le système tombe après cette admission, nous conservons une opération non résolue.
C'est moins confortable qu'un historique parfaitement propre.
Mais c'est beaucoup plus honnête.
Un état INCOMPLETE nous semble préférable à une fausse impression de certitude.
Nous avons ensuite rencontré un autre problème.
Si KOREV contrôle le journal et la clé qui signe ce journal, KOREV pourrait théoriquement reconstruire un historique plus court et signer ce nouvel historique.
La signature serait correcte.
La chaîne pourrait être cohérente.
Mais l'histoire aurait changé.
Nous avons donc ajouté un témoin disposant de son propre état et de sa propre clé.
Son rôle n'est pas de connaître le contenu métier des décisions.
Il conserve une référence à l'état de l'histoire qu'il a déjà reconnue.
Lorsqu'une nouvelle étape lui est présentée, elle doit prolonger exactement l'état précédent.
On ne demande alors plus seulement :
« Cet historique est-il cohérent ? »
On peut demander :
« Cet historique prolonge-t-il bien celui qui avait déjà été reconnu ? »
La nuance est fondamentale.
Dans nos expériences actuelles, le témoin est séparé en processus et en clés, mais reste sous la même administration.
Nous ne prétendons donc pas encore avoir démontré une indépendance opérationnelle complète.
C'est une étape suivante.
Notre vérificateur utilise trois états.
Les octets, l'inventaire, l'historique et l'état courant du témoin se réconcilient, et aucune opération requise ne reste ouverte.
Une information nécessaire manque ou une admission reste dans un état non résolu.
Une incohérence cryptographique ou structurelle est détectée : signature, scope, séquence, hachage, fraîcheur ou inventaire.
Il manque volontairement un quatrième état :
« vrai »
Il manque également :
« conforme »
La cryptographie ne doit pas être utilisée pour transformer une propriété technique en conclusion juridique ou métier qu'elle ne démontre pas.
Nous ne voulions pas seulement écrire le protocole.
Nous voulions essayer de le mettre en défaut.
Notre étude ciblée v2 comporte aujourd'hui 67 tests, dont 43 ajoutés autour de la capture durable et du témoin.
Nous avons notamment testé :
Nous avons enregistré deux lots expérimentaux de 10 et 100 recommandations, avec 11 scénarios prédéterminés par lot.
Soit 22 observations enregistrées, dont les classifications observées correspondent aux résultats attendus définis avant exécution.
Ce n'est pas un benchmark de production.
Ce n'est pas une preuve que toutes les attaques possibles sont couvertes.
C'est quelque chose de plus utile :
une propriété précise confrontée à des tentatives précises de la faire échouer.
Il restait un problème beaucoup plus banal.
Et probablement tout aussi dangereux.
Les fichiers.
Dans KOREV Evidence, un utilisateur peut partir d'une conversation, ajouter des documents puis créer un Dossier sécurisé.
À première vue, cela ressemble à un sujet d'interface.
En réalité, c'est une partie de la chaîne de preuve.
Imaginez que nous protégions parfaitement un dossier après son admission, mais que les octets d'un fichier puissent être remplacés juste avant cette admission.
Le journal serait impeccable.
La mauvaise pièce jointe serait parfaitement protégée.
Nous aurions sécurisé la mauvaise chose.
Nous avons donc audité spécifiquement la frontière :
Conversation → Dossier
L'audit a produit neuf constats initiaux. La correction et la relecture hostile ont ensuite fait apparaître d'autres défauts.
Nous avons notamment ajouté :
La leçon est importante :
La qualité de la preuve commence avant la cryptographie, au moment où le système décide ce qui a réellement été admis.
Nous avons également renforcé nos gates CI.
Sur le gel du travail de publication, nos quatre workflows principaux ont terminé avec succès :
Lors du durcissement Conversation → Dossier qui a suivi, les validations rapportées comprennent notamment :
Et nous conservons aussi dans notre rapport les échecs des suites optionnelles qui restent à traiter.
Parce qu'un workflow vert ne doit jamais servir à faire croire que tout le produit est parfait.
Notre capture s'applique à des frontières déclarées et instrumentées.
Aujourd'hui, cela couvre notamment certaines admissions d'agents, appels modèles, streams, embeddings, outils, sorties visibles côté UI, octets HTTP et transitions de fichiers vers les Dossiers.
Cela ne signifie pas que nous voyons tout.
Ces limites font partie du système.
Pas d'une annexe que nous préférions cacher.
Nous ne sommes évidemment pas les seuls à travailler sur cette question.
La supply chain logicielle a déjà développé des mécanismes avancés de provenance et de transparence avec des projets comme Sigstore/Rekor ou SLSA.
Et l'arrivée des agents IA étend désormais cette question aux modèles, outils, API et actions réalisées au nom d'utilisateurs ou d'organisations.
Des acteurs d'infrastructure comme Traefik travaillent par exemple sur une approche centrée gateway, où les appels modèles, MCP et API sont observés au niveau du chemin de communication.
Notre travail actuel porte sur une frontière différente : ce qui est admis par le runtime et l'application, comment cette admission reste comptabilisée, et comment elle se réconcilie avec ce qui s'est ensuite produit.
Les deux problèmes ne sont pas identiques.
Et nous n'avons réalisé aucun benchmark permettant de classer ces architectures.
Ce qui nous intéresse davantage est que l'industrie commence enfin à poser une meilleure question :
non plus seulement
« Que fait mon agent ? »
mais :
« Qu'est-ce que je pourrai réellement démontrer de ce qu'il a fait ? »
Nous pouvons aujourd'hui défendre une propriété limitée :
Lorsqu'une admission franchit une frontière KOREV déclarée, instrumentée et reconnue par le témoin configuré, elle doit ensuite rester comptabilisée et être réconciliée avant que la population puisse être classée VERIFIED.
Nous ne pouvons pas dire que :
Et c'est précisément pour cette raison que nous publions ces limites avec les résultats.
Notre dépôt de développement reste privé.
Mais vérifiable ne doit pas vouloir dire open source.
Nous préparons donc un pack de reproduction contrôlé comprenant notamment :
L'objectif est simple :
permettre à quelqu'un qui n'a aucune raison de nous croire d'essayer de démontrer que notre propriété ne tient pas.
Parce qu'au fond, c'est probablement la meilleure définition d'une preuve technique :
quelque chose que l'on peut tenter de réfuter.
En avril, j'écrivais que nous confondions trop souvent réponse et preuve.
Quelques mois plus tard, notre position a légèrement évolué.
Nous ne cherchons plus à dire :
« KOREV produit des preuves. »
Nous cherchons à pouvoir dire exactement :
voici la propriété que nous revendiquons, voici la frontière dans laquelle elle existe, voici comment nous avons essayé de la casser, voici les résultats, et voici ce qu'elle ne démontre pas.
C'est moins spectaculaire.
Mais à mesure que les agents IA auront accès à nos données, à nos systèmes et à nos processus métier, ce sera probablement beaucoup plus utile.
Parce que dans un système complexe, la confiance n'est pas une fonctionnalité.
C'est la conséquence de ce que l'on est capable de vérifier.
Voyez comment le consensus multi-modèles produit des décisions vérifiables et auditables.