Vérifiez par vous-même

Comment Vera, le moteur de vérification intégré à Celina, produit des preuves que votre équipe AQ peut contrôler sans nous dans la pièce.

Pour les directions qualité, les responsables de l'intégrité des données et les équipes de validation des systèmes informatisés.

Tout système d'IA en recherche clinique demande qu'on lui fasse confiance. Celui-ci est construit pour ne pas avoir à le demander.

Vera est la partie de Celina qui contrôle l'enregistrement. Pas le raisonnement du modèle, ni sa sortie. Le registre signé que la plateforme produit au fil du travail : chaque événement haché, lié à son prédécesseur et adressé par contenu. Vera parcourt cette chaîne mécaniquement et émet un certificat qui dit exactement ce qu'elle a contrôlé et exactement ce qu'elle n'a pas pu contrôler.

Son verdict tient en une phrase, et il ne change jamais.

No break detected under the following checks.

Aucune rupture détectée sous les contrôles suivants.

Pas « valide ». Pas « propre ». Pas « vérifié » comme un mot nu. Ce qui a tenu, sous quels contrôles, avec les exclusions nommées. Quiconque détient la clé publique peut refaire le calcul.

Ce que Vera est, et ce qu'elle n'est pas

Vera ne contient aucun modèle de langage, nulle part dans son chemin de vérification. Pas de raisonnement probabiliste, pas de scores de confiance, pas d'inférence. Même entrée, même verdict, à chaque fois. Cette propriété n'est pas une préférence de conception. C'est celle qu'une équipe de validation teste réellement, et c'est la raison pour laquelle sa sortie peut être traitée comme une preuve plutôt que comme une opinion.

Elle n'est pas ce qui produit les réponses de Celina. Elle est ce qui contrôle si l'enregistrement de ces réponses est intact. Le modèle propose. La preuve dispose. Vera est la preuve.

Pourquoi Vera n'est pas une preuve formelle

La première conception de Vera était bâtie autour de Lean, l'assistant de preuve. Le plan était de prouver la correction de la logique de vérification et de laisser un petit noyau, contrôlé par machine, porter la garantie. Nous nous en sommes écartés, et la raison mérite d'être dite ouvertement.

Une preuve en Lean s'attache à un modèle de la chaîne. Les entrées-sorties, la base de données, le réseau et la couche d'extraction restent tous hors de la preuve. On prouve le modèle, puis on espère que l'écart entre le modèle et la production est faible. Vera parcourt le flux d'événements de production lui-même : octets réels, base de données réelle, chaîne complète. Un changement de règle est une pull request avec des tests, pas un chantier d'ingénierie de preuve, et un tiers contrôle son travail en récupérant une clé publique, pas en relançant un prouveur.

Ce que cet échange a sacrifié est réel, et nous ne prétendons pas le contraire : une garantie contrôlée par machine que la logique de vérification elle-même est saine. Cette assurance repose désormais sur la simplicité des contrôles, sur une suite de tests liée à une base de données réelle, et sur le fait que n'importe qui peut recalculer le résultat et nous prendre en défaut. Une preuve dit que notre raisonnement est correct. Une clé publiée dit : prouvez que nous avons tort. Les équipes de validation font davantage confiance à la seconde phrase, parce qu'elle a la forme de leur propre métier.

Le parcours

Vera contrôle l'enregistrement à trois niveaux.

Niveau zéro, la chaîne cryptographique. Hachages des événements, liaison au prédécesseur, intégrité des documents. Chaque événement produit-il le hachage qu'il prétend produire, et chacun est-il lié à ce qui le précède.

Niveau un, la structure. Validité du schéma, ordonnancement, cohérence bitemporelle, chaînes de supplantation. Le temps de validité et le temps de transaction sont-ils tous deux enregistrés et cohérents. Lorsqu'un élément a été supplanté, la chaîne de l'original au successeur tient-elle.

Niveau deux, le graphe de provenance. Chaque artefact remonte-t-il à ce qui l'a produit.

Rien n'est échantillonné. Le parcours couvre la chaîne entière, et ce qu'il ne peut pas couvrir est nommé plutôt qu'ignoré.

Le certificat

Chaque certificat énumère les contrôles exécutés. Il porte aussi un registre des exclusions pré-déclaré qui nomme tout contrôle n'ayant pas pu s'exécuter, et pourquoi. Rien n'est omis en silence, et c'est la différence entre un certificat et une réassurance.

Les certificats sont signés en Ed25519 par une identité de vérificateur nommée, vera-audit-v1. Ils sont ensuite ajoutés au registre même qu'ils décrivent, sous forme d'événements signés. L'acte de vérification figure lui-même sur la piste d'audit.

Vérifiez par vous-même

C'est la partie qui compte le plus pour une équipe de validation, alors elle est dite simplement.

Revérifier un certificat requiert la clé publique et rien d'autre. Pas d'accès fournisseur, pas de base de données, pas de secret, pas d'appel avec nous.

L'algorithme, l'identifiant de clé, la clé publique au format PEM, l'encodage de la signature et le contrat de canonicalisation de la charge utile sont publiés sur un point d'accès ouvert :

GET /vera/v1/keys

Un certificat est revérifié contre cette clé à :

GET /vera/v1/certificates/verify

Le contrat de vérification est complet et public. Une fonction sécurité ou AQ peut récupérer la clé, vérifier les certificats de manière indépendante et parvenir à sa propre conclusion avant toute discussion commerciale. C'est l'ordre des opérations prévu.

Le registre en dessous

Insertion seule. L'enregistrement ne peut pas être modifié, seulement complété. La correction est une supplantation : la version antérieure demeure, liée à sa successeure, avec les deux horodatages intacts. Il n'existe aucun chemin qui réécrive l'histoire, y compris pour nous.

Adressé par contenu. Les artefacts sont identifiés par hachage SHA-256. L'enregistrement est l'original par construction, pas par politique.

Bitemporel. Le temps de validité et le temps de transaction sont tous deux enregistrés au moment de l'événement, pas reconstruits après coup.

Clé par juridiction. La signature utilise un trousseau de clés par espace de noms, avec des clés distinctes pour les enregistrements des États-Unis et du Brésil, versionnées, à rotation progressive. Les lignes historiques se vérifient inchangées sous le trousseau, parce que la bascule était identique octet pour octet par construction. Un enregistrement des États-Unis et un enregistrement du Brésil sont cryptographiquement séparables.

Le périmètre

Deux murs indépendants se dressent devant l'enregistrement. L'identité au niveau de la plateforme refuse une requête non authentifiée avant qu'elle n'atteigne le code applicatif, et ce refus est testé. Derrière, les contrôles de principal au niveau applicatif échouent en mode fermé : une dépendance mal configurée refuse au lieu de s'ouvrir par défaut.

L'export de lignage est disponible par artefact et par juridiction, réservé au titulaire de l'enregistrement ou à un rôle d'auditeur. Un résultat vide renvoie un nombre de lignes égal à zéro plutôt qu'un « introuvable » distinguable, de sorte que l'interface ne peut pas servir à sonder ce qui existe.

Les écritures et les émissions sont limitées en débit. Les empreintes des images déployées sont épinglées dans l'infrastructure en code comme enregistrement de déploiement, et tout écart fait échouer le build. La suite de tests stricte de Vera s'exécute contre une base de données réelle à chaque modification. Son code n'est pas livré sans vérification.

Ce que cela donne face à ALCOA+

Nous ne faisons aucune affirmation de conformité. Le tableau décrit ce que fait le substrat. La conclusion vous appartient.

FAQ

Est-ce conforme au 21 CFR Part 11 ou à l'Annexe 11 de l'UE ?

Nous ne faisons pas cette affirmation. La conformité est une évaluation que votre organisation mène selon son propre référentiel. Ce que nous pouvons énoncer, c'est la capacité : un registre en insertion seule, chaîné par hachage, bitemporel, avec attestation humaine nominative et certificats vérifiables de manière indépendante. L'article ci-dessus est rédigé pour que votre équipe de validation puisse l'évaluer directement.

Pourquoi le certificat dit-il « no break detected under the following checks » et non « vérifié » ?

Parce que « vérifié » serait une affirmation portant sur des contrôles qui n'ont pas été exécutés. Le certificat nomme les contrôles exécutés et ceux qui ont été exclus. Sa formulation se limite exactement à cela. Tout ce qui irait au-delà serait une réassurance, non un constat.

Que contient le registre des exclusions ?

Tout contrôle qui n'a pas pu s'exécuter lors d'un parcours donné, nommé explicitement, avec sa raison. Le registre est pré-déclaré : l'ensemble des exclusions possibles est défini à l'avance, pas découvert après coup. Rien n'est passé sous silence.

Mon équipe peut-elle vérifier un certificat sans aucun accès aux systèmes de NexTrial ?

Oui. La vérification ne requiert que la clé publique, publiée avec le contrat complet sur le point d'accès ouvert des clés. Pas de compte, pas d'accès à une base de données, pas d'appel au support.

Vera vérifie-t-elle si les réponses de Celina sont correctes ?

Non. Vera vérifie si l'enregistrement de ces réponses est intact : la cryptographie, la structure et la provenance. L'exactitude d'une détermination est établie par le moteur de verdict déterministe sur un corpus attesté, puis finalisée par une personne nommée. Vera prouve que l'enregistrement n'a pas été altéré depuis.

Que se passe-t-il si le point d'accès de vérification est indisponible ?

Les certificats déjà émis restent vérifiables avec la clé publique, quelle que soit la disponibilité du service, parce que la vérification ne dépend pas du service. Le service lui-même échoue en mode fermé : une dépendance indisponible produit un refus explicite, jamais un passage silencieux.

Si les clés sont renouvelées, les anciens certificats se vérifient-ils encore ?

Oui. Le trousseau de clés est versionné et la rotation est progressive. Les lignes historiques se vérifient inchangées sous le trousseau, par construction.

Pouvons-nous exporter l'enregistrement dans nos propres systèmes ?

Oui. L'export signé de lignage est disponible par artefact et par juridiction pour le titulaire de l'enregistrement ou un rôle d'auditeur. Il circule sous forme de données. Le destinataire n'a besoin de rien de NexTrial pour le contrôler.

Que se passe-t-il lorsqu'un enregistrement est erroné ?

Il est supplanté, jamais modifié. L'original demeure, lié à son successeur, avec les deux horodatages préservés. La chaîne de l'original à la correction fait elle-même partie de l'enregistrement vérifié.

Vera est-elle un modèle de langage ?

Non. Il n'y a aucun modèle dans son chemin de vérification. Elle ne raisonne pas. Elle contrôle.

Comment Vera est-elle elle-même testée ?

Sa suite de tests s'exécute contre une base de données réelle à chaque modification du code, et une suite en échec bloque la fusion. Les empreintes des images déployées sont épinglées comme enregistrement de déploiement, et tout écart entre l'empreinte épinglée et ce qui s'exécute fait échouer le build.

Pouvons-nous l'essayer avant toute discussion commerciale ?

C'est l'ordre prévu. Récupérez la clé, vérifiez un certificat, forgez-vous votre propre avis. Apportez un artefact et regardez-le repartir avec un certificat.

Vera a-t-elle été construite à l'origine sur Lean ?

Oui. La première conception de Vera était bâtie autour de Lean, l'assistant de preuve, avec une logique de vérification à prouver correcte et à contrôler par un petit noyau de confiance. Nous avons déplacé l'assurance vers le déterminisme, la transparence totale et le recalcul indépendant sur la chaîne de production, parce qu'une preuve sur un modèle ne contrôle pas vos données. L'article ci-dessus expose ce que cet échange a sacrifié et ce qu'il a apporté.

Renoncer à la preuve formelle rend-il Vera moins fiable ?

Cela change ce sur quoi la confiance repose. Une preuve en Lean garantit la logique de vérification dans les hypothèses du modèle et ne dit rien de la base de données, du réseau ou de la couche d'extraction déployés. Les contrôles de Vera sont assez courts pour être lus, sa suite de tests s'exécute contre une base de données réelle à chaque modification, et tout tiers peut recalculer son verdict à partir de la clé publique. Si nous réintroduisons un jour de la profondeur formelle, ce sera en prouvant les petits noyaux de spécification, canonicalisation, liaison et supplantation, tout en continuant d'exécuter contre la réalité.

Conçue pour les environnements où l'intégrité des données est auditée, pas affirmée.

NexTrial.ai · Celina · Trial Activation Intelligence