From Puzzles to Proofs: Verified Algorithms Hack and Learn

This meetup is a follow-up to both Advent of Code Verified! and Pearls of Functional Algorithm Design in Dafny (Part 2). The theme is the same across both: taking compact, puzzle-style algorithmic problems and pushing them all the way to provably correct implementations.
We’ll continue working on:

• Advent of Code–style puzzles that involve tricky invariants or edge cases, and/or
• Functional algorithm “pearls” (such as the Surpassing Problem or variations on maximum segment sum),

with a focus on specification, invariants, and proof structure in Dafny.
What we’ll do:

• Briefly recap ideas or partial solutions from previous sessions.
• Pick one or two problems to work on in more depth.
• Refine specifications and correctness properties.
• Break proofs into manageable lemmas and invariants.
• Work individually or in small groups, sharing progress and roadblocks.

Why attend:
If you enjoyed turning puzzles into proofs—or want more practice bridging algorithmic intuition and formal verification—this session is for you. It’s especially useful if you want to improve at structuring proofs, reusing lemmas, and scaling small verified solutions into something clean and maintainable.
All experience levels welcome. Bring a problem you’d like to finish verifying, or jump in to help with one already in progress.
Let’s keep going from clever ideas to solid proofs.