Bounded-exhaustive verification of Selecto read-path scope invariants.

The model enumerates tenant-required and tenant-optional domains, absent, row-scoped, and schema-scoped tenant contexts, explicit scope application, and ordinary user filters. It checks fail-closed validation, preservation of required filters, and SQL parameterization for every state.

A passing result is a proof over this finite model, not a claim about all possible Selecto programs. See Selecto.Verification.BoundedModel.