Que vient de lancer l'Ethereum Foundation ?

L'équipe Formal Verification de l'Ethereum Foundation a ouvert le 20 août 2026 better.codes, un défi de recherche public construit avec Yukon et zkSecurity. Le dispositif prend un problème isolé, le formalise dans le langage de preuve Lean, et place sa borne de sécurité sur un classement que n'importe qui peut faire monter. Le problème s'appelle koalaIRS12. Il porte sur la proximité des codes de Reed-Solomon, une famille de codes correcteurs d'erreurs utilisée dans la construction des preuves succinctes. Les participants pointent leurs propres modèles d'IA sur l'énoncé et tentent de démontrer une borne de robustesse plus élevée, mesurée en bits.

Pourquoi des bits prouvés plutôt que conjecturés ?

Les SNARKs à base de fonctions de hachage, ces preuves qui permettent de vérifier un calcul sans le rejouer, reposent presque tous sur deux résultats: les écarts de proximité et l'accord corrélé pour les codes de Reed-Solomon. On les retrouve dans les systèmes qui sécurisent les zkrollups et les zkVM, ainsi que dans la feuille de route post-quantique d'Ethereum. Ces rollups sont les mêmes qui font tourner les réseaux de seconde couche adossés à Ethereum. Ces systèmes en production visent une sécurité de 128 bits. Selon l'Ethereum Foundation, cette garantie ne tient entièrement que si les conjectures sous-jacentes sont vraies. Or ce qui est aujourd'hui démontré s'arrête en deçà de ce que les chercheurs pensent atteignable. L'écart entre le niveau conjecturé et le niveau prouvé est précisément la cible du défi.

Comment se déroule une soumission ?

La mécanique est décrite par la fondation en quelques étapes fixes.

  • Le participant s'identifie avec GitHub sur better.codes et clone le dépôt du défi.
  • L'énoncé du théorème, le point de paramètres et le harnais de vérification sont figés, le travail se fait dans une zone de soumission dédiée.
  • Un comparateur vérifie que le théorème exporté correspond exactement à l'énoncé figé, puis le noyau de Lean contrôle la preuve.
  • Les résultats acceptés sont promus dans le dépôt public, avec mention du solveur et du modèle d'IA employé.

Les lemmes, techniques de preuve et résultats d'impossibilité issus des soumissions promues sont reversés au dépôt commun. Chacun peut relire les différences passées et les notes de soumission, ce qui évite aux suivants de refaire les impasses.

D'où vient le problème koalaIRS12 ?

Le problème est tiré du programme Proximity Prize, lancé plus tôt cette année par l'Ethereum Foundation pour prouver ou réfuter les conjectures sur les écarts de proximité de Reed-Solomon. Les grands défis du programme sont posés dans un article intitulé Open Problems in List Decoding and Correlated Agreement, signé Gal Arnon, Dan Boneh et Giacomo Fenzi. koalaIRS12 en est extrait et se rattache directement à ces défis. Sa formalisation complète repose sur ArkLib, la bibliothèque Lean 4 dédiée aux arguments de connaissance vérifiés formellement.

Qu'appelle-t-on autorecherche ?

L'Ethereum Foundation décrit better.codes comme un défi d'autorecherche: chaque participant fait tourner ses propres modèles, ses propres harnais et ses propres outils en parallèle contre une même référence vérifiée. L'argument avancé est qu'aucune configuration d'agents n'est optimale sur un problème ouvert, et que la multiplication des approches indépendantes avance plus vite qu'une équipe seule. La fondation cite trois défis bâtis sur ce modèle, ecdsa.fail, zk.golf et snark.fast, qui ont selon elle déjà fait bouger la conception de circuits quantiques et la vitesse de preuve post-quantique. Le lancement ne couvre qu'un seul objectif, porter la borne inférieure démontrée de koalaIRS12 à 128 bits. D'autres défis pourraient s'y ajouter. L'éligibilité, l'évaluation, les récompenses et les paiements dépendent des conditions du programme, que la fondation se réserve le droit d'ajuster en cours de route.

Quel rapport avec le programme de bug bounty ?

L'Ethereum Foundation fait vivre en parallèle un programme de primes aux bugs qui couvre les spécifications des couches d'exécution et de consensus, les clients Besu, Erigon, Geth, Nethermind, Reth, Lighthouse, Lodestar, Nimbus, Teku et Prysm, les compilateurs Solidity et Vyper, ainsi que le contrat de dépôt de la Beacon Chain. La gravité d'une faille s'y mesure à sa capacité à faire slasher des validateurs, un mécanisme propre à la preuve d'enjeu, ou à provoquer des scissions durables du réseau. Ce programme vise du code déployé, là où better.codes vise les fondements mathématiques qui restent à démontrer.