今年もクリスマスの時期がやってきました。この時期は全国各地で巨大なクリスマスツリー🎄が飾られていることと思います。ツリーで思い出したのですが、AtCoderで2020年に出題されたFoliaという問題の解法をCoqで形式検証していたのでその話を書きます。