Quand on interroge aujourd'hui un modèle d'IA hébergé, rien ne permet de vérifier que c'est bien le modèle demandé qui a répondu : il faut croire le fournisseur sur parole. Anthropic veut combler ce vide. Le 2 novembre 2026, l'entreprise a publié FlashProve, un prototype de recherche open source capable de produire une preuve cryptographique qu'une réponse donnée a été générée par un jeu de poids précis, fixé à l'avance, sans dévoiler ces poids.
Les travaux sont signés Roy Rinberg et Alex Allain, chercheurs chez Anthropic, avec des partenaires de l'EPFL, du MIT, de StarkWare et de Succinct, parmi lesquels Alessandro Chiesa, de l'EPFL et de StarkWare. D'après l'entreprise, Claude a lui-même mis au point les améliorations sur lesquelles repose le système, en combinant de façon inédite des techniques connues de la littérature cryptographique. Ce genre d'optimisation produite par une machine étant difficile à relire, l'équipe a formalisé le protocole et ses garanties de sécurité en Lean, un langage de preuve formelle, afin qu'elles soient vérifiables automatiquement.
Le cœur du dispositif est un zkSNARK, un argument succinct à divulgation nulle de connaissance. Lors d'une phase préalable d'environ 39 minutes, le fournisseur publie un engagement, sorte d'empreinte courte qui verrouille un unique jeu de poids. Pour chaque requête ultérieure, il génère une preuve que ce modèle, appliqué à cette invite, renvoie exactement ces tokens. La preuve ne livre rien sur les poids ni sur les experts sollicités dans le réseau, et elle reste compacte : un utilisateur doté d'un matériel modeste peut la contrôler rapidement. L'architecture du modèle n'est en revanche pas masquée.
Les chiffres mis en avant portent sur Llama 4 Maverick, le modèle à mélange d'experts de Meta doté de 400 milliards de paramètres, dans une version publique quantifiée sur 4 bits. Sur un serveur équipé d'un GPU H100 et de 24 cœurs, le prouveur a traité un lot de 24 requêtes de 1 024 tokens en 223 secondes environ, soit près de 110 tokens par seconde, chaque preuve pesant quelque 18,8 Mo. La vérification se passe de GPU : elle a pris 17 secondes sur 24 fils d'exécution. Par rapport au service des mêmes requêtes via vLLM, la génération de preuves coûte de 70 à 95 fois plus de temps GPU, selon Anthropic.
Ce surcoût reste lourd, mais la comparaison avec les travaux antérieurs montre la vitesse des progrès. Dans son tour d'horizon, Anthropic cite VerInf, qui prouvait le même Maverick à environ 0,02 token par seconde, avec 14,3 heures pour mille tokens et une preuve de 93,6 Go. L'entreprise signale aussi que la jeune pousse Attestable revendique 53 à 77 tokens par seconde pour un modèle Gemma dense de 31 milliards de paramètres, sans avoir toutefois publié de code ouvert.
Anthropic présente l'outil comme une réponse à des problèmes de confiance qui s'aggravent avec la diffusion de l'IA. Un client passant par un service de routage pourrait s'assurer d'avoir obtenu le modèle payé. Un opérateur pourrait repérer un serveur d'inférence compromis, ou un modèle qui se ferait passer pour un autre afin d'échapper à la surveillance. Un régulateur pourrait en principe vérifier qu'un fournisseur ne sert que des modèles autorisés, ou que des machines réservées à l'inférence ne servent pas à entraîner autre chose. La publication comprend le code, un vérificateur en C++ et un second, plus lent, écrit en Lean, les preuves formelles et un rapport technique, sous licence Apache 2.0.
Les limites sont clairement exposées. Les preuves portent sur une version du modèle en arithmétique entière et en décodage glouton : des sorties échantillonnées ou calculées en virgule flottante peuvent donc s'en écarter. Le contexte plafonne à 1 024 tokens, bien en deçà des conversations réelles, et la preuve est produite après coup, par lots, et non en temps réel. Le code C++ rapide n'offre aucune garantie formelle de conformité à la spécification Lean, les attaques par canaux auxiliaires comme la mesure du temps sont exclues, et l'engagement doit être renouvelé après environ 16 millions de requêtes. Anthropic parle d'une étape intermédiaire, et ses mesures de performance n'ont pas encore été reproduites de façon indépendante.