(prover-approximations)=
Prover Approximations
=====================

In order to check programs in an acceptable amount of time, the Prover
simplifies the code being verified. This section describes the mechanisms for
simplification.

```{warning}
The approximations described in this section may be
{term}`underapproximation`s, meaning that they can cause real bugs to be
overlooked by the Prover.
```


```{toctree}

loops.md
summarization.md
harnessing.md
hashing.md
grounding.md
```