mix selecto.verify (Selecto v0.4.8)

Copy Markdown

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.