Advent of Code Verified!

Advent of Code is almost here — but this year, we’re adding a twist:
We’re going to solve AoC puzzles with formal verification.
Join us for a relaxed, festive Hack and Learn where we’ll pick one or two Advent of Code challenges and work toward provably correct solutions using Dafny (and optionally Lean, TLA+, or other tools if participants bring them).
Whether you want to:

• implement AoC puzzles in Dafny,
• formally specify the problem and expected behavior,
• experiment with ghost code, invariants, or lemmas,
• or collaborate with others to verify tricky logic…

…this is your chance to mix holiday fun with mathematical rigor.
What we’ll do:

• Choose one or more Advent of Code problems (recent or classic).
• Translate the puzzle into a clear specification.
• Implement a solution and iteratively prove it correct.
• Share verification strategies, stuck points, and clever proof tricks.
• Optionally compare approaches across tools (Dafny, Lean, etc.).

All experience levels welcome — whether it’s your first verification lemma or you’re ready to prove Santa’s sleigh safe under all possible inputs.
Bring your laptop, your favorite holiday beverage, and your best proof-engineering spirit.
Let’s celebrate the season by verifying some puzzles! 🎅📐