Le 25 juin 2026, l’équipe Ubuntu publiait discrètement un billet technique dont le titre renfermait deux faits apparemment contradictoires : SQLite — la base de données la plus utilisée au monde — contenait un bug ; et ce bug était tapi dans le code depuis 2010.
En d’autres termes, il s’y cachait depuis 16 ans.
Seize ans, qu’est-ce que cela représente ? En 2010, l’iPhone 4 venait de sortir, WeChat n’existait pas encore, on envoyait des SMS avec un clavier à touches. Et c’est cette année-là que le bug fut introduit par une ligne de code, pour ensuite s’installer paisiblement dans chaque smartphone, chaque navigateur, chaque système d’exploitation. Des centaines de millions d’appareils, seize années — et personne ne l’avait jamais repéré.
Au bout du compte, ce n’est pas un humain qui l’a trouvé. C’est un problème de mathématiques.
Figure : l’équipe Ubuntu a modélisé en TLA+ le comportement du checkpoint WAL de SQLite. Le modèle n’a besoin que de 20 étapes pour reproduire le bug caché depuis 16 ans. Source : ubuntu.com
Commençons par le commencement : qu’est-ce que SQLite, et pourquoi est-il dans votre téléphone ?
SQLite n’est pas un « logiciel » que vous lancez — vous ne trouverez pas d’icône SQLite sur votre téléphone. C’est un « moteur de base de données », conçu pour stocker et gérer des données sur un téléphone, un ordinateur, un navigateur.
Quelques exemples : l’historique de vos conversations WeChat, les contacts de votre répertoire, les mots de passe enregistrés par votre navigateur, les multiples données locales produites quand vous utilisez Alipay, Taobao ou TikTok — derrière presque tout cela, c’est SQLite qui travaille en silence. C’est la base de données la plus déployée de la planète, sans concurrence. On estime à plus de mille milliards le nombre de bases SQLite actives dans le monde.
Et ce logiciel de niveau « fondation » contenait un bug vieux de 16 ans. Rien que cela donne le vertige.
Mais le plus fascinant dans cette histoire, c’est la manière dont le bug a été trouvé.
Un problème que l’humain ne pouvait pas détecter
Regardons d’abord le bug lui-même. SQLite dispose d’un mode de fonctionnement appelé WAL — Write-Ahead Log, ou « journal des écritures anticipées ». En simplifiant : quand plusieurs programmes lisent et écrivent simultanément dans la base, le WAL sert de « brouillon ». Celui qui écrit note d’abord dans le brouillon ; ceux qui lisent ne sont pas affectés dans l’immédiat. Une fois l’écriture terminée, le contenu est recopié dans le registre officiel. Cette opération s’appelle un « checkpoint ».
Le bug survient au moment précis où l’action de « recopier » et l’action d’« écrire » se produisent en même temps. Pour filer une métaphore de la vie courante :
Vous et un collègue travaillez sur le même tableur. Le collègue est en train d’ajouter des lignes dans la « zone brouillon », tandis que vous êtes chargé de transférer les lignes validées vers le fichier officiel. Vous jetez un œil au brouillon : 100 enregistrements à transférer. Vous en transférez 50 — et là, votre collègue ajoute 5 nouveaux enregistrements et réinitialise le compteur du brouillon. Vous continuez à transférer les 50 restants, mais comme le compteur a été réinitialisé, vous ne transférez en réalité que d’anciens numéros de séquence, en omettant des données qui auraient dû partir.
Résultat : le fichier officiel a perdu quelques enregistrements. Des données ont disparu.
Voilà le bug décrit dans la documentation officielle de SQLite : une « condition de concurrence » (race condition) au cours du checkpoint WAL — deux opérations dont l’ordre n’est pas correctement synchronisé, et qui entrent en collision dans une fenêtre de temps extrêmement précise.
Le mot-clé, c’est « extrêmement précis ». Déclencher ce bug exige une conjonction d’événements très contraignante : l’écriture et le checkpoint doivent survenir simultanément ; et précisément dans l’instant infinitésimal où le checkpoint a lu la taille du WAL mais n’a pas encore commencé le transfert, une autre écriture doit se terminer et réinitialiser le WAL. Cette fenêtre temporelle se mesure en microsecondes.
Quand un humain écrit des cas de test pour traquer les bugs, il procède par conjecture : il devine où quelque chose pourrait mal tourner, puis il teste à cet endroit. Mais la fenêtre de déclenchement de ce bug était si étroite qu’elle échappait à toute conjecture. Quel que soit le nombre de testeurs ou de scripts de tests automatisés, impossible de couvrir toutes les combinaisons possibles d’ordonnancement des opérations — car le nombre de combinaisons est astronomique.
Voilà pourquoi ce bug a dormi tranquillement seize ans dans des centaines de millions d’appareils.
TLA+ : pas un outil de test, une démonstration mathématique
Pour comprendre comment l’équipe Ubuntu a mis la main dessus, il faut saisir une notion : la vérification formelle.
Prenons l’analogie la plus simple possible. Le test traditionnel, c’est un contrôle par échantillonnage : vous plongez la main dans un sac de riz, vous en prélevez quelques poignées pour voir s’il y a des gravillons. La vérification formelle, c’est une preuve mathématique : vous pouvez déduire par la logique si le sac contient ou non des gravillons, sans avoir à retourner chaque grain.
TLA+ est un outil de vérification formelle. Son nom complet : Temporal Logic of Actions. Il a été inventé par Leslie Lamport, figure légendaire de l’informatique — également créateur de LaTeX (le système de composition de documents académiques) et concepteur de l’algorithme de consensus Paxos, sur lequel reposent aujourd’hui presque tous les systèmes distribués.
Ce que fait TLA+ est simple à décrire : vous modélisez le comportement du logiciel que vous voulez vérifier sous forme mathématique — pas besoin d’écrire du code, il suffit de décrire en langage mathématique « comment cette chose doit évoluer dans différentes circonstances ». Ensuite, le vérificateur de modèle de TLA+ énumère exhaustivement toutes les combinaisons d’états possibles, et vérifie si les règles que vous avez définies sont toujours respectées.
Selon l’équipe Ubuntu, après avoir construit le modèle TLA+ du comportement WAL de SQLite, le vérificateur a « trouvé un contre-exemple en seulement 20 étapes ». Vingt étapes. Seize ans versus vingt étapes.
Figure : version statique du modèle TLA+, montrant comment la condition de concurrence entre écriture et checkpoint provoque une perte de données. Source : ubuntu.com
Pourquoi les tests humains ne gagneront jamais cette bataille
Une question de fond mérite d’être creusée : comment une méthode mathématique parvient-elle à dénicher un bug passé inaperçu pendant 16 ans ? La réponse tient à une différence fondamentale de paradigme.
Les méthodes de test humaines — qu’il s’agisse de cliquer manuellement ou d’écrire des scripts automatisés — sont par essence « énumératives » : vous dressez une liste de scénarios qui vous semblent risqués, et vous vérifiez chaque scénario. Le problème, c’est que l’espace d’état d’un système logiciel explose combinatoirement. Pour un système comportant 100 étapes opératoires, le nombre d’ordonnancements possibles est la factorielle de 100 — un nombre supérieur au nombre d’atomes dans l’univers. L’énumération exhaustive est hors de portée.
TLA+ et les outils de vérification formelle, même s’ils se heurtent eux aussi théoriquement au problème de l’« explosion d’états », font une chose qu’aucun humain ne peut faire : ils vérifient si, dans l’ensemble des situations que j’ai définies, un problème peut survenir.
Cette phrase mérite qu’on la pèse deux fois.
Le test humain répond à la question : « Qu’est-ce que j’ai vu qui ne va pas ? » La vérification formelle répond à la question : « Est-ce que ça pourrait ne pas aller ? »
Le premier est passif, tributaire de l’imagination, et laisse facilement filer des angles morts. Le second est actif, exhaustif, et ne rate aucun des états calculés.
Les ingénieurs d’Ubuntu ne sont pas plus brillants que les développeurs de SQLite — l’équipe SQLite est réputée pour la qualité exceptionnelle de son code, et la couverture de ses suites de tests figure parmi les meilleures de l’industrie. Mais les outils diffèrent. Un mètre ruban et un microscope ne perçoivent pas le monde à la même échelle.
Un concurrent épargné : une découverte inattendue
Cette histoire comporte un épilogue savoureux. Si l’équipe Ubuntu s’est lancée dans cette vérification, c’est parce qu’elle maintient son propre projet : Dqlite, une base de données distribuée bâtie sur SQLite. La question : ce bug de SQLite existait-il aussi dans Dqlite ?
Ils ont donc construit un modèle TLA+ de Dqlite. Résultat : Dqlite n’est pas affecté.
La raison est simple : Dqlite a une conception plus « conservatrice ». Lorsqu’il effectue un checkpoint, il verrouille toutes les écritures, garantissant que « transférer » et « écrire » ne peuvent pas se produire simultanément. Cela coûte un peu de performance, mais cela lui a justement permis d’éviter cette condition de concurrence.
Le design de Dqlite n’est pas forcément meilleur. Mais parfois, un choix conservateur fait sans y penser se révèle payant seize ans plus tard. Les chaînes de causalité du génie logiciel ont ce genre de mystère.
Le correctif SQLite : une ligne de code
Le 5 mars 2026, SQLite publiait officiellement le correctif. La correction est d’une simplicité désarmante : pendant le checkpoint, on ajoute une vérification supplémentaire pour s’assurer que le WAL n’a pas été réinitialisé entre-temps. Si c’est le cas, on recommence.
Seize ans de menace latente, et une ligne de code pour la résoudre.
Mais la simplicité de la correction ne dit rien de la difficulté du diagnostic — trouver où placer cette ligne et quelle condition vérifier, voilà ce qui était diaboliquement ardu. Si ardu que les meilleurs spécialistes de bases de données au monde, ceux de SQLite, ne l’avaient pas repéré en seize ans.
Ce que cela signifie : un basculement en cours
Deux choses me frappent.
Premièrement, le cas SQLite n’est pas isolé. Amazon, Microsoft, Oracle utilisent TLA+ depuis des années pour vérifier leurs infrastructures critiques — les services centraux d’AWS comme S3 ou DynamoDB ont été soumis au vérificateur de modèles TLA+ dès leur conception. Mais ces cas restaient confinés aux systèmes fermés des entreprises, invisibles au grand public. Avec SQLite, projet open source omniprésent, la vérification formelle signe un événement à forte visibilité publique.
Deuxièmement, le « seuil d’entrée » de la vérification formelle est en train de baisser. TLA+ n’est pas un outil grand public — il exige une tournure d’esprit mathématique et des compétences en modélisation de systèmes. Mais de même qu’il y a vingt ans personne n’imaginait que les « tests automatisés » deviendraient la norme, alors qu’aujourd’hui ils le sont, la vérification formelle passe du statut d’« outil de gourou » à celui de « standard d’équipe ». Ce que l’équipe Ubuntu a découvert avec TLA+, c’est un bug dans la base de données la plus mature et la plus déployée de la planète — et ce seul fait envoie un message à tous : les logiciels fondamentaux auxquels vous faites confiance peuvent cacher des problèmes que leurs propres auteurs ignorent. Et les mathématiques sont la seule voie fiable pour les trouver.
Il y a seize ans, on testait les logiciels avec de l’intuition et de l’abnégation. Seize ans plus tard, un problème mathématique a trouvé en 20 étapes ce que l’œil humain ne verrait jamais.
C’est l’outil qui a progressé.
Liens de référence :