What we’re about
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 (1)
See all- 🔥 Verification Hack and Learn: Tackling Mutable Objects in DafnyLink visible for attendees
### Join us for the next hands-on session of Verification Hack and Learn. We’ll dig into the practical challenges of verifying classes and mutable state in Dafny—and work together to overcome them.
What to Expect:
- Inspiration from the Article
We’ll walk through the “Verified Ordered Set in Dafny” tutorial—exploring how an ordered set is specified, what invariants are needed, and where Dafny verification becomes challenging. - Core Challenges with Mutable Objects
Discussion will spotlight key hurdles: - Maintaining class invariants and correct representation sets (`Repr`) when dealing with mutable fields.
- Managing reads and modifies framing—explicitly declaring what memory can be accessed or changed, and why it's vital for sound verification.
- Learning how loops and heap mutations can unintentionally invalidate invariants and cause verification failures.
- Live Dafny Exploration
We’ll open a sample “ordered set” class and collaboratively: - Identify necessary attributes and invariants.
- Tinker with `modifies` and `reads` clauses.
- Observe where Dafny balks—and why.
- Group Work & Debugging Practice
In small groups, pick a simple Dafny class or mutable structure. Try: - Adding invariants and framing.
- Testing how modifications and loops affect verification.
- Iteratively refining until the code verifies—or tracking why it doesn’t.
- Tips & Lessons Learned
Wrap up with a group debrief: - What patterns helped?
- What common pitfalls did we hit?
- Inspiration from the Article
