Dans l’écosystème Bitcoin, l’adage « Don’t trust, verify » ne s’applique pas qu’aux blocs et aux transactions, mais également au code source lui-même.
Depuis plus d’une décennie, Bitcoin Core fait office de référence de facto : cette implémentation en C++ définit les règles de consensus. Une erreur dans le code peut alors menacer la stabilité du réseau, cela s’est déjà produit en 2013. C’est précisément ce problème que cherche à résoudre btc-verified, un projet rendu public début juillet 2026 par Keagan McClelland (ProofOfKeags). Présenté sur la liste bitcoindev et sur Delving Bitcoin, il ambitionne d’apporter une vérification formelle de certaines parties du protocole Bitcoin.
Le problème : le code fait office de spécification
Malgré la documentation existante, il reste très difficile d’écrire une implémentation alternative qui reproduise exactement le comportement de Bitcoin Core dans tous les cas limites. Les tests classiques permettent de détecter des erreurs connues, mais jamais de démontrer l’absence d’erreurs.
La solution : démontrer plutôt que tester
La vérification formelle utilise les mathématiques pour prouver qu’un programme respecte une spécification. McClelland s’appuie sur Lean 4 et sa bibliothèque mathlib pour construire un modèle mathématique dont les propriétés peuvent être démontrées avec rigueur.
Le projet a déjà formalisé plusieurs briques fondamentales :
- Les structures de base (transactions, blocs et leurs composants) disposent de codecs pour lesquels sont prouvés le round-trip (encodage puis décodage retrouve la valeur d’origine) et la canonicité (une donnée valide n’a qu’un seul encodage minimal).
- Une implémentation de SHA-256 et double SHA-256 (sha256d), vérifiée sur les vecteurs de test officiels (FIPS 180-4 et ceux de Bitcoin), sans axiomes supplémentaires ni preuves incomplètes.
- L’arbre de Merkle : la détection de mutation introduite après la vulnérabilité CVE-2012-2459 garantit qu’une racine identifie de manière unique l’arbre correspondant (ou qu’il existe une collision SHA-256). Cette propriété a été vérifiée sur plusieurs blocs historiques, dont le bloc Genesis, le bloc 170 et le bloc 481824 (activation de SegWit).
Le modèle est directement exécutable : les décodeurs vérifiés peuvent être appliqués à de vrais blocs Bitcoin.
Bitcoin Script n’est pas encore modélisé : il est traité pour l’instant comme une simple suite d’octets.
Les limites du projet
McClelland insiste sur le caractère exploratoire de son travail. Même parfaitement démontré, le modèle Lean ne garantit pas que Bitcoin Core se comporte toujours exactement de la même manière. Plusieurs propriétés essentielles restent à formaliser, notamment la limite des 21 millions de bitcoins et l’algorithme de sélection de la chaîne qui concentre le plus de travail.
Par ailleurs, McClelland, qui ne prétend pas être un expert en vérification formelle, a rédigé l’intégralité du dépôt avec l’aide de modèles d’intelligence artificielle (notamment Claude), dont il a relu et validé lui-même les résultats. Le travail qu’il a fourni devra donc être vérifié et relu par des experts.
Quels bénéfices pour Bitcoin ?
btc-verified propose un modèle formel en Lean 4 de plusieurs composants essentiels du protocole Bitcoin — sérialisation, hachage et arbres de Merkle — dont les propriétés peuvent être démontrées mathématiquement. Ce travail constitue une première étape crédible vers une spécification plus rigoureuse et indépendante de l’implémentation Bitcoin Core.
À terme, ce type d’approche pourrait faciliter la validation d’implémentations alternatives comme btcd, offrir un cadre plus solide pour évaluer les évolutions du protocole (notamment en matière de résistance quantique), et contribuer à la génération de composants vérifiés pour la bibliothèque de consensus libbitcoinkernel. Il ouvre ainsi une voie prometteuse : celle où la robustesse de Bitcoin reposerait non seulement sur les tests et les revues de code, mais aussi sur des preuves mathématiques.
Sources
– Dépôt GitHub
– Annonce sur Delving Bitcoin (3 juillet 2026)
– Bitcoin Development Mailing List
– Bitcoin Optech Newsletter #414 (juillet 2026)
