name: dafny-verifier
description: "Use Dafny verification language for constructing verified programs with proofs."
version: "1.0.0"
tags: [verification, dafny, proofs, popl]
difficulty: intermediate
languages: [dafny]
dependencies: [hoare-logic-verifier, smt-solver-interface]
Dafny Verifier
Dafny is a verification-aware programming language that supports writing specifications, programs, and proofs together. It compiles to verified code in multiple languages (C#, Java, Go, JavaScript).
When to Use This Skill
- Writing verified programs
- Learning formal verification
- Proving algorithm correctness
- Teaching program proofs
- Developing certified software
What This Skill Does
- Specification Writing: Define pre/post conditions and invariants
- Verification: Automatically verify programs against specs
- Lemma Proving: Write and prove helper lemmas
- Termination: Prove program termination
- Code Extraction: Generate verified code
Key Concepts
| Concept |
Description |
| Method |
Executable code with specifications |
| Function |
Mathematical function (pure, no side effects) |
| Lemma |
Proof that can be called like a function |
| Invariant |
Property that holds at loop header |
| Ensures |
Postcondition specification |
| Requires |
Precondition specification |
Tips
- Start with strong specifications, weaken if needed
- Use lemmas to break complex proofs
- Write loop invariants before the body
- Use
calc statements for calculation proofs
- The
old() function refers to pre-state
Common Use Cases
- Verified algorithms
- Certified libraries
- Teaching formal methods
- Security-critical code
- Protocol verification
Related Skills
hoare-logic-verifier - Theory behind Dafnycoq-proof-assistant - More expressive proof assistantsmt-solver-interface - Z3 powers Dafnyseparation-logician - For heap reasoning
Canonical References
| Reference |
Why It Matters |
| Leino, "Dafny: An Automatic Program Verifier for Functional Correctness" (LPAR 2010) |
Original Dafny paper |
| Leino, "Program Proofs" (MIT Press, 2023) |
Comprehensive Dafny book |
| Dafny documentation (dafny.org) |
Official reference |
Tradeoffs and Limitations
Approach Tradeoffs
| Approach |
Pros |
Cons |
| Dafny |
Automatic, usable |
Limited expressiveness |
| Coq |
Very expressive |
Manual proofs |
| F* |
More features |
Steeper learning |
When NOT to Use This Skill
- When proofs are not needed
- For low-level systems code (use Verus)
- When performance is critical
Limitations
- Heap reasoning can be tricky
- Some proofs need explicit lemmas
- Not as expressive as Coq
Assessment Criteria
A high-quality implementation should have:
| Criterion |
What to Look For |
| Verification |
All proofs check |
| Readability |
Clear specifications |
| Modularity |
Good lemma structure |
| Termination |
All loops/functions terminate |
Quality Indicators
✅ Good: All specs verified, clear invariants, modular lemmas
⚠️ Warning: Some specs need manual hints
❌ Bad: Unverified code, missing invariants
Research Tools & Artifacts
Verification tools:
| Tool |
Language |
What to Learn |
| Verus |
Rust |
Verified Rust |
| F* |
F* |
Verification |
Research Frontiers
1. Automation
- Goal: More automatic proofs
Implementation Pitfalls
| Pitfall |
Real Consequence |
Solution |
| Failed proofs |
Verification fails |
Add lemmas |
By