About us
Interested in writing provably correct software? Join us as we explore the world of software verification, with a focus on the Dafny language and related tools like Lean, TLA+, Quint, P, and more.
We'll meet regularly to:
Study verification languages and their semantics
Work through hands-on exercises and example problems
Share ideas, code, and techniques
Build a library of verified software components
Whether you're a beginner or experienced in formal methods, this group is a space to learn, practice, and collaborate. All curious minds welcome!
Upcoming events
2
Functional Programming & Theorem Proving in Lean
·OnlineOnlineWe’re launching a new series dedicated to verification and formal reasoning in Lean — centered around two excellent Lean resources:
- Functional Programming in Lean, a free Lean book that teaches writing programs in Lean’s pure functional language with proofs built in.
- Theorem Proving in Lean 4, a companion Lean book focused on interactive theorem proving and verifying properties using Lean tactics and dependent types.
Lean uniquely unites programming and proof, allowing you to write real code and formally verify its correctness. This series will help you explore that blend step by step.
In this session, we’ll:- Get familiar with the structure and goals of both books.
- Walk through the beginnings of Functional Programming in Lean, including basic definitions, recursion, and simple proofs.
- Introduce key ideas from Theorem Proving in Lean 4 to support writing proofs about models and programs.
- Work on small Lean exercises together: writing definitions, proving simple properties, and sharing approaches.
Who it’s for:
Anyone curious about using Lean for software verification, algorithm correctness, or proof-driven development — whether you’re new to Lean or have some experience. Bring your laptop, a Lean environment (optional but helpful), and questions!
Let’s dive into Lean, mix programming and proof, and learn together how to build verified software with expressive dependent types.6 attendees
Past events
11
