# `Selecto.Verification.BoundedModel`

Deterministic, exhaustive checking over an explicitly bounded state space.

This is a small model-checking kernel used by Selecto's verification suites.
It is deliberately dependency-free so verification is available to package
consumers and Mix tasks, not only to the test environment.

A successful report proves that every invariant held for every supplied
state. The proof is bounded by the caller's finite model; the report records
the exact model size and never presents the result as an unbounded theorem.

# `invariant`

```elixir
@type invariant() ::
  {String.t() | atom(), (term() -> :ok | true | {:error, term()} | false)}
```

# `report`

```elixir
@type report() :: %{
  format: String.t(),
  format_version: pos_integer(),
  proof_level: :bounded_exhaustive,
  model: String.t(),
  state_count: non_neg_integer(),
  invariant_count: non_neg_integer(),
  check_count: non_neg_integer(),
  proved?: boolean(),
  counterexamples: [map()]
}
```

# `check`

```elixir
@spec check(String.t() | atom(), Enumerable.t(), [invariant()]) :: report()
```

Checks every invariant against every state and returns a stable proof report.

Invariants should return `:ok` or `true` when satisfied. `{:error, reason}`,
`false`, exceptions, and throws are captured as reproducible
counterexamples.

---

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