Anvil でつくる証明された勝利の Kubernetes Controller

Kubernetes の Custom Controller のような非同期的なシステムを正しく実装するのは、本来とても難しい作業です。そして実は、この「難しさ」には二通りの側面があります。一つはもちろん「期待する挙動をコードとして実装すること」、そしてもう一つは「期待する挙動をテスト可能な形で表現すること」です。

この「難しさ」に対する回答の一つが、国際カンファレンス OSDI で 2024 年に発表された Anvil です。Anvil は Controller を実装するための Rust 用フレームワークですが、時相論理の一種 TLA を用いて、通常のテストでは検証し難い「任意のタイミングでクラッシュしても Reconcile が収束する」といった仕様を数学的に表現し、証明を行うことができます。

本講演では、小さな Controller を実際に実装しながら、この「証明」がどのような前提のもとで、何を保証しているのかを解説します。さらに「仕様の表現」という観点から、Anvil を使用しない通常の Go の Controller にも持ち帰れるテスト設計上の指針をお伝えします。