# `mix selecto.verify`

Runs the Selecto bounded formal-verification suites.

    mix selecto.verify
    mix selecto.verify --output tmp/selecto-verification.json

Exit status is non-zero if any suite produces a counterexample. Reports state
the proof level and finite model size so bounded results cannot be confused
with unbounded theorem proving.

---

*Consult [api-reference.md](api-reference.md) for complete listing*