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