Vers des garanties mathématiques pour le logiciel qui fait fonctionner Bitcoin
Dans l'univers Bitcoin, où la moindre faille logicielle peut provoquer des conséquences systémiques, un nouveau projet veut dépasser les tests classiques pour établir des garanties formelles. Baptisé btc-verified et rendu public début juillet 2026 par Keagan McClelland (ProofOfKeags), il vise à prouver mathématiquement que certaines pièces du protocole respectent des spécifications précises.
"Don’t trust, verify"
Cette maxime, familière aux développeurs et utilisateurs du réseau, s'applique aussi au code source qui implémente les règles de consensus. Bitcoin Core est depuis plus d'une décennie l'implémentation de référence, mais l'histoire a montré — notamment avec un incident en 2013 — qu'une erreur peut affecter la stabilité du réseau. Les tests unitaires et d'intégration détectent des régressions connues, mais ne garantissent pas l'absence totale d'anomalies dans tous les cas limites. C'est précisément ce gap que cherche à combler btc-verified.
Méthode : prouver plutôt que tester
Le projet s'appuie sur Lean 4 et sa bibliothèque mathlib pour formaliser des modèles mathématiques du protocole. La vérification formelle consiste ici à démontrer que le traitement d'un objet logiciel respecte une spécification donnée, en s'appuyant sur des preuves assistées par ordinateur plutôt que sur des jeux de tests.
- Structures de base : transactions, blocs et composants disposent de codecs pour lesquels btc-verified a prouvé le round‑trip (encodage puis décodage retrouve la valeur) et la canonicité (aucun encodage invalide supplémentaire).
- Fonctions de hachage : une implémentation de SHA‑256 et du double SHA‑256 (sha256d) a été vérifiée sur les vecteurs de test officiels (FIPS 180‑4 et ceux utilisés par Bitcoin), sans axiomes supplémentaires non justifiés.
- Arbre de Merkle : la détection de mutation corrigée après la vulnérabilité référencée CVE‑2012‑2459 est formalisée ; la preuve montre qu'une racine Merkle identifie de façon unique l'arbre associé, sauf en cas de collision SHA‑256.
État des travaux et validité historique
Les auteurs indiquent avoir vérifié certaines propriétés sur des blocs historiques, ce qui permet de confronter les preuves au passé réel de la chaîne : le bloc Genesis, le bloc 170 et le bloc 481824 (activation de SegWit) sont cités comme cas test. Ces vérifications concrètes renforcent la crédibilité de la formalisation, mais ne signifient pas que l'ensemble du protocole ou de Bitcoin Core soit couvert.
| Composant | Preuve / Vérification |
|---|---|
| Codecs (transactions, blocs) | Round‑trip et canonicité prouvées |
| SHA‑256 / sha256d | Vérification sur vecteurs FIPS 180‑4 et Bitcoin |
| Arbre de Merkle | Détection de mutation et unicité de racine (tests historiques) |
Conséquences et limites
Si btc-verified réussit à étendre ces preuves, plusieurs bénéfices sont possibles : réduction des risques liés aux divergences d'implémentation, facilité pour développer des implémentations alternatives fidèles, et renforcement de l'argument de sécurité pour les acteurs institutionnels. En revanche, la formalisation ne supprime pas tous les risques : elle couvre des propriétés mathématiques précises mais n'empêche ni bugs ailleurs dans le système, ni erreurs d'intégration, ni attaques matérielles ou humaines.
De plus, formaliser l'intégralité d'un logiciel complexe comme Bitcoin Core reste un chantier long et exigeant. Les éléments déjà traités par btc-verified constituent des briques essentielles, mais l'ambition d'une spécification mathématique complète du protocole nécessitera des ressources et du temps, ainsi qu'une validation indépendante de la communauté.
Reste enfin la question de l'adoption : une spécification formelle n'impose pas automatiquement les modifications aux clients en production. Elle offre cependant une base solide pour auditer, comparer et certifier les implémentations futures, ce qui peut influencer positivement la résilience du réseau sur le moyen terme.
En l'état, btc-verified marque une étape significative vers une ingénierie plus rigoureuse de Bitcoin : utile, techniquement poussée, mais encore partielle. La preuve mathématique réduit l'incertitude sur certains composants ; elle n'élimine pas la nécessité d'une vigilance continue sur l'ensemble de l'écosystème.
