Bug Injection
=============

One useful way to check specifications is by injecting bugs into the verified
contracts and checking that the Prover finds the injected bugs.

```{todo}
This section should be expanded.
```