# Specification language

Here we formally describe Verus's specification language, which is used for
`assert`, `requires`, `ensures`, and so on.
We start with the semantics
of its [types](./reference-types.md) and then the syntax and semantics of its
[expressions](./spec-expressions.md).