To prove properties on Finite State Machines, we can construct a proof: stating an invariant proving that the invarient is true for all states for all transitions: assume invarient is true before transition and prove that its true after So, essentially induction.