Imaginez un agent d’intelligence artificielle capable de résoudre 672 problèmes mathématiques issus d’une compétition universitaire prestigieuse, et ce pour un coût total de seulement 111,85 dollars. C’est exactement ce qu’a accompli l’équipe de Near AI. Derrière ce chiffre impressionnant se cache une ambition bien plus grande : transformer la vérification formelle, longtemps réservée à une élite de spécialistes, en un outil accessible pour sécuriser les protocoles blockchain et les contrats intelligents.
Une percée qui change la donne pour la sécurité des blockchains
Le 16 octobre, Near Protocol a officialisé sa volonté d’appliquer cette technologie à son propre protocole et à ses contrats de base. L’annonce, relayée ensuite sur les réseaux, marque un tournant. Pendant des années, prouver qu’un logiciel se comporte exactement comme prévu restait un exercice long, coûteux et réservé à des experts. Aujourd’hui, l’IA commence à automatiser une partie cruciale de ce travail : la génération de preuves.
La vérification formelle ne se contente pas de tester quelques scénarios. Elle cherche à démontrer mathématiquement qu’un programme respecte toujours certaines règles, quelles que soient les entrées. Dans un univers où des millions de dollars transitent chaque jour via des contrats intelligents, cette différence est capitale. Un bug oublié peut coûter une fortune. Une preuve solide, elle, offre une garantie bien plus robuste.
Ce que signifie vraiment le résultat des 672 problèmes
Le benchmark utilisé s’appelle PutnamBench. Il s’inspire des problèmes de la compétition Putnam, réputée pour sa difficulté parmi les étudiants en mathématiques. Near AI a annoncé avoir résolu 672 de ces problèmes formalisés en Lean, un langage et assistant de preuve open-source. Le coût moyen par problème s’élève à environ 0,17 dollar selon les tarifs des modèles au moment de la soumission.
Le dépôt public du projet précise qu’il s’agit de 670 problèmes originaux plus deux versions corrigées de formalisations défectueuses. Les chercheurs insistent : ce montant ne tient pas compte des coûts de développement de l’agent lui-même, ni de ce qu’il faudrait réellement pour vérifier un contrat de production. En rejouant les mêmes appels avec les tarifs hors pointe de DeepSeek, la facture grimperait à 331 dollars. La méthodologie inclut les tentatives infructueuses, et un essai parallèle avec un autre modèle a été volontairement exclu du calcul.
Certains runs ont duré plus de trois jours. L’agent propose une preuve, interroge Lean, analyse les retours d’erreur, puis recommence. Le noyau de Lean vérifie ensuite si la démonstration respecte strictement les règles logiques. C’est ce contrôle automatique qui donne de la solidité au résultat.
« L’avenir de l’IA et du code généré par IA est excitant, mais seulement une fois que nous aurons des garanties vérifiables et mathématiques de son comportement. »
— Illia Polosukhin, cofondateur de Near Protocol
Cette citation résume parfaitement l’enjeu. Plus l’intelligence artificielle génère de code, plus le risque d’introduire des failles augmente. Les outils d’attaque, eux aussi, gagnent en puissance. D’où l’urgence de disposer de méthodes de vérification à la hauteur.
Les trois étapes indispensables pour passer à la production
Near insiste sur un point : réussir un benchmark mathématique ne revient pas à vérifier un logiciel déployé. Trois étapes sont nécessaires.
D’abord, il faut modéliser le programme de façon mathématique. Ensuite, définir clairement les propriétés que l’on souhaite garantir. Enfin, construire les preuves qui montrent que ces propriétés sont bien respectées. L’équipe a fait d’énormes progrès sur la troisième étape. Les deux premières restent, pour l’instant, un travail humain exigeant.
Un exemple concret illustre bien la nuance. On peut prouver qu’un transfert de tokens préserve toujours le solde total des comptes concernés. C’est utile. Mais cela ne dit rien sur qui a le droit d’initier ce transfert. Une deuxième preuve, distincte, sera nécessaire pour garantir que seuls les comptes autorisés peuvent le faire. La vérification formelle ne couvre que ce que l’on a explicitement demandé de prouver.
Pourquoi Lean est devenu un outil central
Lean n’est pas un simple langage de programmation. C’est un assistant de preuve capable de vérifier, avec une rigueur extrême, que chaque étape d’une démonstration est correcte. L’agent d’IA peut proposer des preuves, les soumettre, recevoir des messages d’erreur précis, puis ajuster sa stratégie. L’humain, ou un autre système, garde le contrôle sur les spécifications de départ.
Un échec de preuve n’indique pas forcément un bug dans le code. La spécification peut être mal formulée, le modèle peut être incomplet, ou l’agent peut simplement ne pas avoir trouvé la bonne démonstration. Cette distinction est essentielle pour éviter les fausses alertes comme les fausses assurances.
Des applications déjà visibles dans l’écosystème Near
La vérification formelle n’est pas une nouveauté absolue sur Near. En mars, Certora a publié une évaluation du protocole de prêt Templar. L’équipe a combiné revue manuelle des contrats Rust et spécification formelle du contrat de marché. Plusieurs propriétés ont été prouvées, et des problèmes ont été identifiés. Ce type de travail reste aujourd’hui rare et coûteux. L’ambition de Near est de le rendre plus abordable grâce à l’automatisation.
D’autres blockchains explorent des pistes similaires. Aptos Labs a présenté en mai un flux de travail où l’IA aide à générer des spécifications pour le Move Prover, notamment autour de la répartition dynamique. Vitalik Buterin a également évoqué l’intérêt de combiner outils d’IA et preuves vérifiées par machine pour sécuriser différentes couches d’Ethereum, de la consensus à la cryptographie post-quantique. Il a toutefois rappelé qu’une preuve sur une couche ne garantit pas le comportement global du système.
La vérification formelle ne remplace pas le reste de la sécurité
Near le souligne clairement : les preuves formelles viennent en complément des tests, des revues de code et des pratiques opérationnelles. Elles ne se substituent à rien. Une preuve ne vaut que pour les propriétés choisies et sous les hypothèses retenues. Si le modèle mathématique omet un aspect important du code réel, la garantie s’effondre.
C’est précisément pour cette raison que le projet insiste sur la nécessité de relier étroitement les preuves à l’implémentation déployée. Les utilisateurs ne se soucient pas d’un modèle abstrait. Ils se soucient du code qui tourne réellement sur le réseau.
Points clés à retenir
- 672 problèmes PutnamBench résolus pour 111,85 $
- Objectif : appliquer la méthode au protocole Near et aux contrats de base
- Trois étapes : modélisation, spécification, preuve
- Lean comme moteur de vérification
- Complément, et non remplacement, des méthodes classiques
Les limites actuelles et les défis à venir
Le coût de 111,85 dollars est spectaculaire pour un benchmark académique. Il ne donne cependant aucune indication fiable sur le prix de vérification d’un vrai contrat de production. La modélisation reste un goulot d’étranglement. Traduire un code Rust ou un protocole complexe en énoncés mathématiques précis demande du temps et de l’expertise.
Par ailleurs, Near AI a également obtenu la première place en nombre total de résolutions sur le classement Lean Eval v1. Ce classement mesure le volume de problèmes formalisés, pas uniquement les premières solutions ou les solutions uniques. C’est un indicateur de capacité, pas encore une preuve de maturité industrielle.
Les runs les plus longs, dépassant parfois trois jours, montrent aussi que l’automatisation n’est pas encore instantanée. L’agent explore, échoue, recommence. Cette boucle de recherche est puissante, mais elle consomme des ressources et du temps de calcul.
Sécurité quantique : un autre chantier parallèle
Near ne se limite pas à la vérification formelle. L’équipe Near One a proposé en mai le support des signatures FIPS-204 basées sur le standard ML-DSA approuvé par le NIST. L’objectif était d’atteindre un testnet d’ici la fin du deuxième trimestre 2026. Ce changement nécessitera des adaptations coordonnées des portefeuilles logiciels, des portefeuilles matériels, des points de terminaison et des API.
La résistance quantique et la vérification formelle forment deux faces d’une même médaille : anticiper les menaces futures tout en renforçant les garanties présentes. Dans un monde où l’IA accélère à la fois la création de code et la découverte de failles, ces deux axes deviennent stratégiques.
Ce que cela change concrètement pour les développeurs
Si Near réussit à industrialiser ces outils, les développeurs de l’écosystème pourraient bientôt disposer de moyens plus abordables pour prouver certaines propriétés de leurs contrats. Aujourd’hui, faire appel à une société spécialisée en vérification formelle reste hors de portée pour beaucoup de projets. Demain, une partie du travail pourrait être assistée par des agents capables de générer et de corriger des preuves sous supervision humaine.
Cela ne signifie pas que le métier de vérificateur formel disparaîtra. Au contraire. Les experts resteront indispensables pour formuler les bonnes spécifications, valider les modèles et interpréter les résultats. L’IA agit comme un multiplicateur de force, pas comme un remplaçant.
Pour les utilisateurs finaux, l’impact sera plus indirect mais tout aussi important. Un protocole dont les propriétés critiques sont prouvées formellement inspire davantage confiance. Dans un marché où les hacks de contrats intelligents font régulièrement la une, cette confiance a une valeur économique réelle.
Une course mondiale à la preuve automatisée
Near n’est pas seul dans cette course. Plusieurs équipes de recherche et d’autres protocoles blockchain explorent des approches proches. L’avantage concurrentiel ira à ceux qui sauront le mieux relier les résultats de benchmarks académiques à des garanties concrètes sur du code en production.
Le message de Near est clair : les benchmarks mathématiques sont un terrain d’entraînement indispensable. Ils forcent les agents à manipuler des énoncés complexes, à gérer des erreurs, à rechercher des stratégies de preuve. Mais le vrai match se joue ailleurs, sur les protocoles réels et les contrats qui gèrent des fonds.
La distinction entre une preuve isolée et une garantie système reste cruciale. Prouver qu’un module de transfert préserve les soldes ne protège pas contre une faille d’autorisation, une attaque de réentrance mal modélisée ou une erreur dans une autre partie du code. La vérification formelle est puissante, mais elle reste partielle par nature.
Vers une culture de la preuve dans la blockchain
Si la démarche de Near se généralise, on pourrait assister à un changement culturel. Aujourd’hui, beaucoup de projets se contentent de tests unitaires, d’audits manuels et de bug bounties. Demain, prouver formellement certaines propriétés critiques pourrait devenir un standard attendu par les investisseurs et les utilisateurs.
Ce n’est pas une révolution du jour au lendemain. Les outils doivent encore mûrir. Les coûts doivent baisser davantage. Les interfaces doivent se simplifier. Mais la direction est tracée. L’automatisation de la génération de preuves ouvre une porte que peu croyaient accessible il y a seulement quelques années.
Dans un secteur où la confiance se gagne durement et se perd en quelques blocs, chaque avancée technique qui renforce les garanties a de la valeur. Near mise sur cette idée. Les 672 problèmes résolus pour 111,85 dollars ne sont qu’un début. La suite se jouera sur la capacité à transformer cette prouesse académique en bouclier concret pour le protocole et ses applications.
La sécurité des blockchains n’a jamais été un sujet purement technique. Elle conditionne l’adoption, la régulation et la pérennité des projets. En rapprochant l’intelligence artificielle et la vérification formelle, Near Protocol tente de répondre à l’un des défis les plus difficiles du domaine : prouver, et non seulement tester, que le code fait exactement ce qu’il est censé faire. Le chemin est encore long, mais la première étape, celle des preuves automatisées à bas coût, vient d’être franchie avec un résultat qui force le respect.
Les prochaines annonces diront si cette approche passe réellement en production et si d’autres protocoles emboîtent le pas. En attendant, le message est lancé : dans un monde où l’IA génère de plus en plus de code, seule une IA capable de prouver le comportement de ce code pourra réellement sécuriser l’avenir des réseaux décentralisés.
