2026年6月25日、Ubuntuチームのテックブログが静かに公開された。そのタイトルには、一見矛盾する二つの事実が潜んでいた。SQLite——地球上で最も広く使われているデータベース——にバグが発見された。そのバグは、2010年からコードの中に眠っていた。
つまり、16年間も隠れ続けていたのだ。
16年とはどれほどの時間か。2010年、iPhone 4が発表されたばかりで、WeChatはまだ存在せず、人々はまだボタン式のケータイでSMSを打っていた時代だ。その年に、このバグは一行のコードとともにSQLiteに書き込まれ、それ以来、静かにすべてのスマートフォン、すべてのブラウザ、すべてのOSの中に住み着いた。数十億のデバイス、16年の歳月——誰一人として、それを見つけた者はいなかった。
そして最終的にそれを見つけたのは、人間ではなく、一つの数学の問題だった。
図：UbuntuチームがTLA+でモデル化したSQLite WALのチェックポイント動作。モデルはわずか20ステップで、16年間隠れ続けたバグを再現する。出典：ubuntu.com
まず前提を整理しよう——SQLiteとは何か、なぜあなたのスマホに入っているのか
最初に一つの前提を説明しておきたい。SQLiteは「ソフトウェア」ではない——あなたのスマホに「SQLite」というアイコンは存在しない。SQLiteは「データベースエンジン」だ。スマホ、PC、ブラウザの中でデータを保存・管理するために特化した仕組みである。
例を挙げよう。チャットアプリの会話履歴、スマホの連絡先、ブラウザに保存したパスワード、ショッピングアプリやSNSアプリを使うときに生成される様々なローカルデータ——その背後では、ほぼすべてSQLiteが黙々と動いている。SQLiteは世界で最もインストール台数の多いデータベースであり、これは比喩ではなく事実だ。推定では、全世界で1兆を超えるSQLiteデータベースが稼働している。
そして、そのような「地盤」レベルのソフトウェアに、バグが16年も潜んでいた。この事実だけでも十分に背筋が寒くなる。
しかし、この物語の本当に面白いところはここからだ。このバグは、いったいどうやって発見されたのか？
人間には絶対に見つけられなかった問題
まずバグそのものを見てみよう。SQLiteにはWAL（Write-Ahead Log、先行書き込みログ）という動作モードがある。簡単に理解するなら、複数のプログラムが同時にデータベースを読み書きするとき、WALは「下書き用ノート」の役割を果たす。書き込む側はまず下書きノートに書き、読む側は当面影響を受けない。書き終わったらまとめて正式な台帳に転記する。このプロセスを「チェックポイント（checkpoint）」と呼ぶ。
バグは、この「転記」という動作と「書き込み」という動作が同時に発生したときに起きる。日常の言葉でたとえよう。
あなたと同僚が同時に一つのスプレッドシートを操作している。同僚は「下書きエリア」に新しいデータを追加し続けている。あなたの仕事は、下書きエリアにある確定済みの内容を正式なファイルに転記することだ。あなたは下書きエリアをざっと見て、転記すべきレコードが100件あると確認し、50件を転記した——その瞬間、同僚が新しいレコードを5件追加し、かつ下書きエリアのカウンターを「リセット」した。あなたは残りの50件を転記し続けるが、カウンターがリセットされたために、実際には古いシーケンス番号だけを転記し、本当に転記すべきだったデータの一部を取りこぼしてしまう。
結果：正式なファイルから数件のレコードが消えた。データが失われたのだ。
これがSQLiteの公式ドキュメントが記述するバグである。WALチェックポイント処理における「競合状態（race condition）」——二つの操作が適切に順序付けられず、極めて精確な時間枠の中で衝突したのだ。
カギとなるのは「極めて精確な」という修飾語だ。このバグを誘発するには、一連の厳しい条件が揃わなければならない。書き込み操作とチェックポイント操作が同時に発生しなければならない。チェックポイントがWALサイズを読み取った後、転記を開始する前の、ほんの一瞬の隙間に、別の書き込み操作がちょうど完了し、WALをリセットしなければならない。この時間枠は、おそらく数マイクロ秒しかない。
人間がテストケースを書いてバグを探すとは、本質的に「推測」である——どこで問題が起きそうかを推測し、その場所で繰り返し試行する。しかしこのバグの誘発ウィンドウは、「推測すらできない」ほど狭い。どれだけ多くのテスターを投入しても、どれだけ大量の自動テストスクリプトを書いても、あらゆる操作順序の組み合わせをカバーすることは不可能だ——可能な組み合わせの総数は天文学的数字に達するからだ。
これこそが、このバグが数十億台のデバイスの中で16年間も安穏と眠り続けられた理由である。
TLA+とは何か——テストツールではなく、数学的証明である
Ubuntuチームがこのバグをどうやって発見したかを理解するには、まず一つの概念を理解する必要がある。形式検証（formal verification）だ。
筆者は最もシンプルなたとえで説明しよう。従来のテストは「抜き取り検査」のようなものだ——米袋からランダムに数掴みして、砂が混じっていないか調べる。形式検証は「数学的証明」のようなものだ——この米袋に砂が混じっているかを、一掴みずつ調べなくても、論理的に導き出せる。
TLA+は、まさにその形式検証ツールである。正式名称をTemporal Logic of Actionsといい、コンピュータサイエンス界のレジェンド、レスリー・ランポート（Leslie Lamport）によって考案された。彼はLaTeX（学術論文の組版システム）の生みの親でもあり、Paxos合意アルゴリズム（今日のほぼすべての分散システムの基礎）の設計者でもある。
TLA+が行うことは、言葉にすればシンプルだ。検証したいソフトウェアの振る舞いを数学的モデルに抽象化する——コードを書く必要はない。数学的な言語で「この対象が、さまざまな状況下でどのように変化すべきか」を記述するだけだ。すると、TLA+のモデル検査器（model checker）が、すべての可能な状態の組み合わせを網羅的に調べ上げ、あなたが定義したルールが常に成立するかどうかを検証する。
Ubuntuチームの言葉を借りれば、彼らがTLA+でSQLite WALの振る舞いモデルを構築した後、モデル検査器は「わずか20ステップで反例を見つけた」という。20ステップ。16年 対 20ステップ。
図：TLA+モデルの静的バージョン。書き込み操作とチェックポイント操作の間の競合状態が、どのようにデータ損失を引き起こすかを示している。出典：ubuntu.com
なぜ人間の目視テストはこの戦いに永遠に勝てないのか
ここには、掘り下げる価値のある深い問題がある。なぜ数学的手法は、16年間誰にも見つけられなかったバグを発見できたのか？数学的手法がそれを可能にした根源は、方法論の本質的な違いにある。
人間のテスト手法——手動でポチポチ操作するにせよ、自動テストスクリプトを書くにせよ——は、本質的に「列挙型」だ。問題が起きそうなシナリオをリストアップし、各シナリオで検証する。問題は、ソフトウェアシステムの状態空間が組み合わせ爆発を起こすことだ。100の操作ステップを持つシステムの、可能な状態順序の総数は100の階乗——この数は宇宙の原子の総数よりも大きい。列挙など不可能だ。
一方、TLA+のような形式検証ツールは、理論上「状態爆発」の問題に直面するものの、人間にはできないあることをやってのける。それは、「私が定義したすべての状況下で、問題は発生しうるか」をチェックするということだ。
この文章は二度味わう価値がある。
人間のテストが答える問いは「どのような問題が見つかったか？」である。 形式検証が答える問いは「問題が発生する可能性はあるか？」である。
前者は受動的で、想像力に依存し、容易に漏れが生じる。後者は能動的で、網羅的であり、計算された状態を一つたりとも見落とさない。
UbuntuのエンジニアがSQLiteの開発者より優秀だったわけではない——SQLiteの開発チームは極めて高いコード品質で知られ、テストスイートのカバレッジは業界トップクラスだ。しかし、道具が違う。定規と顕微鏡が見る世界は、同じ次元ではない。
競合他社が影響を受けなかった理由——意図せざる発見
この物語には興味深いスピンオフがある。Ubuntuチームがそもそもこの検証に着手したのは、彼ら自身がDqliteというプロジェクト——SQLiteベースの分散データベース——をメンテナンスしているからだ。彼らが知りたかったのは、SQLiteのこのバグが、Dqliteにも存在するかどうかだった。
そこで彼らはDqliteのTLA+モデルも構築した。結果は——Dqliteは影響を受けない。
理由はシンプルだ。Dqliteの設計はSQLiteよりも「保守的」なのだ。チェックポイントを実行する際、書き込み操作全体をロックし、「転記」と「書き込み」が同時に発生しないようにしている。これにより多少のパフォーマンスは犠牲になるが、まさにこの競合状態を回避していた。
Dqliteの設計がより優れているとは限らない。しかし、自分が無意識に行った保守的な選択が、16年後に突然「正しかった」と証明されることがある。ソフトウェア工学の因果の連鎖とは、かくも奇妙なものだ。
SQLiteの修正——一行のコード
2026年3月5日、SQLiteは公式にバグ修正をリリースした。修正は極めてシンプルだ。チェックポイント処理中にもう一度チェックを加え、WALがリセットされていないことを確認する。もしリセットされていたら、最初からやり直す。
言い換えれば、16年の潜在的なバグが、一行のコードで解決された。
しかし、コードそのものがシンプルだからといって、問題がシンプルだったわけではない——この一行をコードのどこに置くべきか、どのような条件をチェックすべきか。これを見つけ出すプロセスこそが、極めて困難だったのだ。困難すぎて、世界で最もデータベースを理解しているSQLiteのエンジニアたちでさえ、16年間発見できなかったほどに。
この出来事が意味すること——変わりつつある潮流
筆者が伝えたいことは二つある。
第一に、SQLiteのケースは孤例ではない。Amazon、Microsoft、Oracleなどの企業は、すでに重要なインフラストラクチャでTLA+を用いた形式検証を行っている——AWSのS3やDynamoDBといったコアサービスは、設計の初期段階でTLA+によるモデル検査を通過している。ただ、これらの事例のほとんどは企業内部のクローズドなシステムで行われており、一般の目に触れることはなかった。SQLiteは、遍在するオープンソースプロジェクトとして、そのバグが形式検証によって発見された。これは公共の可視性を持つ象徴的な出来事なのである。
第二に、形式検証の「敷居」は下がりつつある。TLA+は誰でも使える道具ではない——数学的思考とシステムモデリングの能力が求められる。しかし、20年前には誰も「自動テストが全員やるべきこと」とは考えていなかったのに、今ではそれが標準装備であるように、形式検証もまた「達人専用」から「チームの標準装備」へと移行しつつある。Ubuntuチームが今回TLA+で発見したのは、業界で最も成熟し、最も広く使われているデータベースのバグだ——この事実そのものが、すべての人間に告げている。あなたが信頼している基盤ソフトウェアにも、その作者すら知らない問題が潜んでいる可能性がある。そして数学こそが、そうした問題を見つける唯一の信頼できる手段なのだ。
16年前、人々は直感と勤勉さでソフトウェアをテストしていた。 16年後、一つの数学の問題が、わずか20ステップで人間の肉眼では永遠に見えなかったバグを発見した。
これは、道具が進歩したということだ。
参考リンク：