Hi! I wrote a blogpost exploring a formal specification in Quint [1] for the secret santa game, and verifying some of its properties with Apalache [2].<p>Hope you enjoy it, and any feedback is welcome. Happy holidays!<p>[1]: <a href="https://github.com/informalsystems/quint">https://github.com/informalsystems/quint</a>
[2]: <a href="https://github.com/informalsystems/apalache">https://github.com/informalsystems/apalache</a>