この間、Let's Encryptがバグで300万近くの証明書を失効させたというニュース流れました。 事の詳しい顛末は以下のBlogにかかれています。かなり詳しく書かれており、どのようなコードでバグが出たのか？というところまで解説されています。 jovi0608.hatena…

TLC Model Checkerとは形式仕様記述言語であるTLA+のモデル検査ツールです。TLA+で書かれた仕様の不変式のviolationやLivenessやSafety 特性のviolationの検出などをしてくれます。 そんで、このTLC Model Checkerというのは、CUIで使えたほうが便利だと思う…