仕様検証言語 TLA+ の AWS における使用事例について向井が話します。