TiKV でちょっと面白いというか、微笑ましい issue を見つけてしまいました。

近年、分散 DB を中心に industry でも形式手法が採用されるようになってきました。形式手法は、すごく雑な説明をすると、テストではなく数学をベースにしてシステムの動作を検証しようとする分野です。中でも OSS 界隈では TLA+ というツールがよく採用されています。

この TLA+ は大御所 Lamport の理論が元になっていて、本人も積極的にツールの普及を推進していたり、採用事例をリストしたりしています。

https://lamport.azurewebsites.net/tla/industrial-use.html

で、リンクした issue を見ると、要するに「TiKV / TiDB でも TLA+ を使ってるんだから Lamport のページに載せて宣伝してもらおう」ということなんですね。

結果的には結局 issue も open のままで Lamport のページには載ってないんですが、TLA+ 側からは認知されていて、実際、TLA+ が開催しているレクチャーシリーズ Dr TLA+ で TiDB を扱った回があります。分散アルゴリズムの回が色々ある中、ケーススタディとしては TiDB は Cosmos DB と同格に取り上げられていて、割といい扱いなんじゃないでしょうか。

https://github.com/tlaplus/DrTLAPlus

残念ながらスライドや映像は公開されてないみたいですね。気になる。