This hack underscores the need for formal modeling systems like TLA+ or Coq. Essentially, you define successor state axioms, where: 1. start with a seed state.

This hack underscores the need for formal modeling systems like TLA+ or Coq. Essentially, you define successor state axioms, where: 1. start with a seed state. 2. non-deterministically choose the next step (e.g. submit a tx) 3. ask the system to prove the inverse of an invariant you want to check (e.g. hash power cannot fall below X% of total network power.) Decentralized protocols have bugs; trust only what you can prove.