TLA+で解明：16年間眠っていたSQLite WALモードのバグを追跡する

16年間もの間、ひっそりと潜んでいたSQLiteのWAL（Write-Ahead Logging）モードにおけるバグ。一体なぜ見つからなかったのか、そしてどのようにして形式手法である「TLA+」を駆使してその真相を突き止めたのか。驚異的なデバッグの旅路を解説します。

TLA+ は、Leslie Lamport（ベクトルクロックやPaxosなどで有名）によって作られた、コードより上のレベルのソフトウェアや、回路より上のレベルのハードウェアをモデル化するための形式言語だよ。
https://lamport.azurewebsites.net/tla/tla.html (https://lamport.azurewebsites.net/tla/tla.html)

TLA+ は最高だよね。
誰か Lean に移植して、タクティクスを実装するような試みをしてる人っていないのかな。

この記事の著者です。まさか投稿されてフロントページまで来るとは驚き！何か質問があれば気軽に聞いてね。

この記事のタイトルはあまり好きじゃないな。実際の内容は、TLA+の仕様を使って dqlite が SQLite と同じバグを抱えていないことを証明するプロセスについて書かれているものだよね。SQLite のバグ修正自体は、ここで説明されている内容とは完全に別物だし。