btc-verified : vers une vérification formelle du protocole Bitcoin

Dans l’écosystème Bitcoin, l’adage « Don’t trust, verify » ne s’applique pas qu’aux blocs et aux transactions, il s’applique é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 puis relayé sur Delving Bitcoin, il ambitionne d’apporter une vérification formelle de certaines parties du protocole Bitcoin.

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 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 :

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.

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.

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)

• Evénements • Statistiques en temps réel • Acheter et vendre des bitcoins • Bitcoin par son inventeur • Choisir son application "portefeuille" • Générer des bitcoins : le minage • Les sites à éviter • Quelle banque choisir ? • Histoire de Bitcoin • Articles populaires • Statistiques du site

• Opensats.org • Asmae - Sœur Emmanuelle • L'UNICEF France • Human Rights Foundation • Internet Archive

• Plan B Network • L'Institut National de Bitcoin • Le Cercle du Coin (association) • La Voie du Bitcoin

Auteur : La rédaction

Date de publication : 22 July 2026

Lire l'article original