OAuth2 のフローを Alloy Analyzer でモデリングする

趣味でウェブの認証 API を地力で設計しようとしていたときに、認証フローの仕様を頑張ってこしらえたとして、その正しさをどうやって保証するんだろう? と疑問に思い、調べていたところ、「形式手法」というのに行き当たった。 形式手法というのはシステムの正しさを上流工程から検証するための方法で、数理論理やロジッ…