Amazon Releases Dafny-Based Program Verification Course
2025-06-02
Amazon has open-sourced teaching materials for program verification using Dafny. The course goes beyond basic Dafny programming, delving into its capabilities as a proof assistant. It's structured in three parts: Part 1 introduces Dafny as a programming language; Part 2 explores Dafny as a proof assistant, covering formal proof methods like natural deduction; and Part 3 applies this knowledge to program verification, covering functional, imperative, and object-oriented programs. This resource is suitable for beginners and experienced Dafny developers alike, offering a comprehensive approach to program verification.
Development
formal proof