---
title: "Dafny Reference Documentation"
---

**Abstract:**
This is the Dafny reference manual; it describes the Dafny programming
language and how to use the Dafny verification system.
Parts of this manual are more tutorial in nature in order to help the
user understand how to do proofs with Dafny.

[(Link to current document as html)](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef)

Language reference for the [Dafny type system](http://leino.science/papers/krml243.html), which also describes available expressions for each type


```{toctree}
:maxdepth: 1
:numbered:
:titlesonly:

Introduction
Grammar
Programs
Modules
Types
Specifications
Statements
Expressions
Refinement
Attributes
Topics
UserGuide
VSCodeIDE
Plugins
CommandLineOptions
GrammarDetails
SyntaxTests
References
```