takaha.siの技術メモ

勉強したことをお伝えします。ちょっとでも誰かの役に立てればいいな…

2020-03-01から1ヶ月間の記事一覧

Let's Encryptの証明書失効から学ぶループと末尾再帰の関係

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

TLC Model CheckerをCUI(コマンドライン)で使う

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