Souveraineté par la preuve : une stratégie défensive pour l'IA européenne

Idée centrale — La course à la frontière de l'IA est perdue pour l'Europe. La course à la défense ne l'est pas, et elle est nécessaire quel que soit le vainqueur. Le terrain à prendre : des modèles qui prouvent mathématiquement que le code tient, face à n'importe quel attaquant, y compris une IA plus puissante. Ce marché se structure en ce moment même, avec des centaines de millions levés aux États-Unis, et sans aucun acteur européen visible.

Pourquoi maintenant#

Le marché de la vérification formelle par IA est passé en 2026 de la recherche aux levées à neuf chiffres. Aucun acteur européen n'apparaît.

Acteur	Levée	Date	Chef de file	Approche
Pramaana Labs	27 M$ (amorçage)	juin 2026	Khosla Ventures	LLM + couche de vérification de type Lean, par secteur (fiscalité, droit, médicament, cyber)
Axiom	200 M$ (série A, valorisation 1,6 Md$)	mars 2026	Menlo Ventures	Modèles qui produisent des preuves en Lean, boucle de données vérifiées
Axiom	64 M$ (amorçage)	octobre 2025	—	idem

Le paradoxe : Pramaana cite comme précédent Catala, projet de l'INRIA qui formalise le code fiscal français. La recherche fondatrice est souvent française (Rocq, CompCert, Catala, méthode B). L'industrialisation se fait ailleurs.

La fenêtre est ouverte, mais elle se referme : les premiers à accumuler des preuves vérifiées prennent une avance qui se cumule.

Le raisonnement, étape par étape#

Chaque étape est une affirmation distincte. Si l'une ne tient pas, la suite tombe : c'est là qu'il faut appuyer.

1. La capacité est en avance sur l'usage. Pour la plupart des métiers, les modèles actuels suffisent ; l'adoption bute sur les données, les processus et la responsabilité, pas sur la puissance.
2. La course à la frontière se justifie donc par la sécurité nationale. Le seul domaine où l'IA donne un avantage immédiat est le numérique, et d'abord la cyber : pas d'usine, un déploiement en heures.
3. Cette course est perdue pour l'Europe. L'écart d'investissement avec les États-Unis et la Chine se compte en ordres de grandeur.
4. La sécurité se prend par les deux bouts. L'enjeu de la course est la sécurité, et la sécurité a deux entrées : l'attaque, qui est la frontière, et la défense. Le même enjeu se prend par l'autre bout, et l'Europe y a un avantage réel : la recherche fondatrice en preuve est souvent française (Rocq, CompCert, Catala, méthode B).
5. La défense est nécessaire quel que soit le vainqueur. Même la puissance en tête doit protéger ses propres systèmes. Un investissement défensif ne devient jamais caduc, contrairement à un modèle dépassé en six mois.
6. La preuve formelle est une défense qui ne dépend pas de la force de l'attaquant. Une propriété prouvée tient face à n'importe quelle IA, quelle que soit sa puissance de calcul.
7. La preuve se prête à l'apprentissage autonome. Un vérificateur tranche automatiquement : le modèle génère, le vérificateur trie, les réussites deviennent le corpus suivant. La rareté des données de départ est un frein, pas un mur. C'est l'étape sur laquelle toute la note repose : si la capacité de preuve suit simplement la capacité générale, l'avance ne se prend pas.
8. C'est à l'échelle européenne. On part d'un modèle de code ouvert et on le post-entraîne ; le calcul nécessaire se chiffre en centaines de milliers d'euros, pas en milliards (ordre de grandeur, à confirmer).
9. La défense se vend ; l'attaque ne se vend pas. Vendre de l'attaque, c'est remettre un potentiel d'attaque à quelqu'un : contrôle des exportations, responsabilité, réputation, une clientèle réduite à des États. La défense se vend à n'importe qui, sans dilemme éthique, de façon récurrente, et la réglementation en crée la demande. Un pays tiers qui cherche un fournisseur sans allégeance à Washington ou Pékin peut acheter de la certitude ; il ne peut pas acheter une arme offensive sans conséquences.

Ce que la preuve couvre, et ce qu'elle ne couvre pas#

La preuve ne ferme pas toutes les portes. Elle ferme les deux plus graves : l'exécution de code à distance et l'élévation de privilèges.

Type d'attaque	Couvert par la preuve ?	Réponse
Bugs mémoire (environ 70 % des failles critiques chez Microsoft et Chrome)	Oui	Rust, par construction
Entrées hostiles, contrats de fonction	Oui	Annotations vérifiées
Cryptographie, authentification, noyaux, contrôle d'accès	Oui, si énoncés	Spécification explicite
Identifiant volé, hameçonnage	Non pour la cause, oui pour la propagation	Cloisonnement prouvé : l'erreur humaine reste locale
Logique métier détournée (suite d'opérations toutes légitimes)	Partiellement	Dépend de la qualité de la spécification
Dépendance compromise en amont	Non	Chaîne d'approvisionnement, hors champ
Déni de service	Non	Capacité réseau ; pas besoin d'IA pour attaquer

Deux limites structurantes. La preuve protège ce qu'on écrit ou réécrit, pas les milliards de lignes existantes : sur un système neuf et critique, on ferme la plupart des portes ; sur l'existant, on grignote. Et elle ne couvre que les propriétés énoncées.

La pile : un choix pragmatique, pas un dogme#

L'invariant de la thèse, c'est la vérification automatique. Les outils, eux, changeront.

Aujourd'hui, le point de départ le plus réaliste pour le code est Rust + Verus. Rust élimine les bugs mémoire par construction. Verus, open source, ajoute des preuves écrites dans la syntaxe Rust, vérifiées en quelques secondes. Trois atouts pour l'entraînement : les modèles connaissent déjà Rust, la boucle de vérification est rapide, et des travaux publiés ont déjà amorcé le terrain (AutoVerus, KVerus).

D'autres voies existent et pourraient l'emporter. Lean, choisi par Axiom et Pramaana, est plus puissant et bénéficie d'un grand corpus mathématique. Rocq (ex-Coq) et la méthode B ont fait leurs preuves en industrie (CompCert, seL4, ligne 14 du métro parisien). Dafny, F*, Kani et Creusot occupent des positions intermédiaires.

Le choix d'outil se révise ; l'actif durable, ce sont les preuves accumulées et la méthode.

Où est le fossé : la spécification#

Le modèle qui écrit les preuves sera vite banalisé. Ce qui ne le sera pas, c'est l'outil qui permet à un ingénieur ordinaire d'exprimer ce qu'il veut garantir.

Une spécification formelle n'exige pas un niveau de mathématicien. C'est une phrase du type : si l'utilisateur n'est pas propriétaire du dossier, la fonction ne renvoie jamais son contenu. La difficulté est l'exhaustivité (couvrir les cas auxquels personne ne pense), pas la théorie. Un modèle peut justement proposer les cas oubliés.

Le fossé naît de la boucle entre les deux briques :

• l'outillage capte l'usage réel et produit des spécifications et des preuves validées ;
• ces données améliorent le modèle ;
• le modèle améliore l'outil.

La taille d'un modèle se rattrape en six mois. Cette boucle s'accumule. Le métier de développeur se déplace en conséquence : il énonce les garanties plutôt qu'il n'écrit les boucles, plus proche de l'architecte ou du juriste.

Ce qu'il faudrait faire#

Pour Mistral. Occuper ce créneau avant qu'il ne soit fermé : un modèle de preuve post-entraîné sur un modèle de code existant, et l'outillage de spécification au-dessus. Il colle à son positionnement : modèles spécialisés, déployables sur site, clients qui ne peuvent pas envoyer leur code critique dans un nuage américain (défense, énergie, banque, santé). Ne pas vendre un logiciel : vendre de la certitude.

Pour un entrepreneur. Le service est accessible dès maintenant : rendre vérifiable une base de code critique existante. L'actif est la méthode, pas les GPU. La demande est créée par la réglementation (NIS 2, règlement européen sur la cyberrésilience).

Points à challenger#

Cette note est écrite par un non-spécialiste. Les points les plus fragiles :

• Le coût du post-entraînement : l'ordre de grandeur de quelques centaines de milliers d'euros est-il réaliste pour un modèle compétitif ?
• La vitesse de banalisation : les modèles généralistes deviendront-ils bons en preuve sans spécialisation, rendant l'avance inutile ?
• Le choix de langage : Verus, Lean, autre chose ? Le marché risque-t-il de converger sur Lean, où les Américains ont déjà l'avance ?
• L'existant : peut-on rendre vérifiable du code ancien à un coût raisonnable, ou faut-il tout réécrire ?
• La demande réelle : les clients paieront-ils pour une garantie formelle, ou la conformité réglementaire suffira-t-elle sans preuve ?

Sources#

• Axiom lève 200 M$ (SiliconANGLE, mars 2026)
• Pramaana Labs lève 27 M$ (TechCrunch, juin 2026)
• Verus, dépôt officiel
• AutoVerus (ACM)
• KVerus (arXiv, mai 2026)
• Catala (INRIA)