Added TLA+ file for the leaderboard use case and TLC snapshot