prune-states · prove

State-machine proof playground

Paste a transition table. The playground infers every terminal-state invariant — once X, always X — and proves it, or hands you the exact step that breaks it. It evaluates the same one-step inductive encoding prune-states dispatches to Z3; copy the generated SMT-LIB to reproduce any verdict with the real solver. Background: the article

A state mapping to [] is terminal. Transitions are state names or { to, event?, when?, not? } — when/not name a guard, checked as free booleans (a sound overapproximation, same as the package).

Todo · 4 states

activeinitialdonearchiveddeletedterminal

Assert terminal

“This state should be terminal — prove it.” The escape hatch for invariants the structure no longer shows.

Invariants · 1

DeletedIsTerminalproved

Once kind = deleted, the machine stays there.

SMT-LIB — reproduce with z3 check.smt2

; DeletedIsTerminal: Once kind = deleted, the machine stays there.
; Verification by inductive negation — unsat means proved.

(set-logic ALL)

(declare-datatypes ((State 0)) (((s_active) (s_done) (s_archived) (s_deleted))))

(declare-const kind State)
(declare-const kind_next State)

; Transition relation: kind' is determined by kind + guards.
(assert (or
  (and (= kind s_active) (= kind_next s_done))
  (and (= kind s_active) (= kind_next s_archived))
  (and (= kind s_active) (= kind_next s_deleted))
  (and (= kind s_done) (= kind_next s_archived))
  (and (= kind s_done) (= kind_next s_deleted))
  (and (= kind s_archived) (= kind_next s_deleted))
  (and (= kind s_deleted) (= kind_next s_deleted))))

; Negation of the invariant — sat means a counterexample exists.
(assert (= kind s_deleted))
(assert (not (= kind_next s_deleted)))

(check-sat)
(get-model)

The full toolkit extracts these tables for you — from AASM and state_machines declarations in Ruby, and from XState machines or typed React props in TypeScript — then proves the invariants with Z3 in CI, plus an opt-in TLA+ export for TLC and TLAPS. github.com/zernie/prune-states