Raftを使ってDFSを作るという仕事を数年前ぐらいから続けています。そのためか最近、形式仕様記述（特にTLA+）とかModel checkingとかTheorem provingとかが私の中でアツいです。TLA+とかAlloyとかVDM++とかSpin周りのやつです。 ソフトウェアの仕様を形式仕…

principia.connpass.com Twitter眺めてたら面白そうなセミナーがあったので申し込んだ。 私はオブジェクトストレージではないPOSIX IFな分散ファイルシステムを作るという面白い仕事をもう数年間ぐらい続けている。 その関係で最近TLA+とTLC Model Checkerを…