# E0038

Warning name: `missing_invariant`

This warning is emitted for a proof-checked `for` loop that has no
`proof_invariant` clause. A loop invariant records the facts that must hold
before and after every iteration, so the verifier can reason about the loop body
and the `nobreak` result.

## Erroneous example

The loop does not have a `proof_invariant` clause.

```{literalinclude} /sources/error_codes/0038_error/top.mbt
:language: moonbit
```

## Suggestion

Add some proof invariants.

```{literalinclude} /sources/error_codes/0038_fixed/top.mbt
:language: moonbit
```