Material for a logic and set theory course written in the verification-aware programming language Dafny

Using the Dafny verification language to specify the design of a toy imperative language (WHILE-like). The de#cludes the syntax, small step operational semantics, type system and proof system…

Verifying Algorithms and Data Structures in Dafny (TFG)

An embedding of TLA+ in Dafny

Dafny for Metatheory of Programming Languages

Library of formally verified abstract data types in Dafny.

Libraries useful for Dafny programs

Verified algorithms with tools like Dafny

Verified Datalog