(cvl-language)=
The Certora Verification Language
=================================

The Certora Verification Language (often abbreviated CVL) is the language used
to write specifications for smart contracts.  This chapter describes the syntax
and semantics of CVL Specifications.

```{toctree}
:maxdepth: 2

overview.md
basics.md
types.md
expr.md
statements.md
imports.md
using.md
methods.md
rules.md
builtin.md
functions.md
invariants.md
sorts.md
ghosts.md
defs.md
hooks.md
transient.md
foundry-integration.md
```

Changes Since CVL 1
-------------------

```{toctree}
:maxdepth: 2

cvl2/changes.md
cvl2/migration.md
v5-changes.md
```