Unlike many real world systems, smart contracts are deterministic state machines. Contracts will move through different states (e.g., uninitialized, initialized, finalized, upgrading, time locked) and state transitions occur under well defined conditions. This review focuses on comparing the state transition behavior of smart contracts with their intended behavior. ### Define a state machine model The first step is to create a written or visual summary of different smart contract states at a high-level. For example, a smart contract representing a physically redeemable good could have the following state machine model. - No active bid or offer - Owner can create offer and move to "Active offer, no active bid" - Anyone can create bid and move to "Active bid, no active offer" - Active bid, no active offer - Owner can sell, transitioning to "No active bid or offer" - Owner can create offer and move to "Active bid and offer" - Active offer, no active bid - Anyone can buy, transitioning to "No active bid or offer" - Anyone can bid and move to "Active bid and offer" - Active bid and offer - Owner can sell, transitioning to "No active bid or offer" - Anyone can buy, transitioning to "No active bid or offer" - From all the above states: - Owner can redeem, transitioning to "Redeemed" - Redeemed - This state is terminal (no more transitions are possible). Initially, it's important to specify the states in user terms rather than smart contract storage terms because the specific storage variables used in the smart contract may be incorrect. Next, attempt to describe each state purely in terms of smart contract storage. E.g., the redeemed state may be described with `redeemed = true`. ### Generate a state change overview Use the `vars-and-auth` printer available in [Slither](/codex/slither) to show which state variables are modified in each function. Below is an example output: ```bash ... $ slither examples/printers/authorization.sol --print vars-and-auth [..] INFO:Printers: Contract MyContract +-------------+-------------------------+----------------------------------------+ | Function | State variables written | Conditions on msg.sender | +-------------+-------------------------+----------------------------------------+ | constructor | ['owner'] | [] | | mint | ['balances'] | ['require(bool)(msg.sender == owner)'] | +-------------+-------------------------+----------------------------------------+ ``` ### Go function-by-function through state machine transitions For each state machine state, go into each function which could be triggered in that state and facilitate a transition out of that state. Verify that it works in line with the specification. ### Review state machine transition coverage State transition behavior is so significant that it should have full coverage in tests. Review tests to make sure that each transition is verified and also test invalid transitions. ### Fuzzing Consider using [Fuzzing](/codex/fuzzing) to obtain more confidence that invalid state transitions are not possible even through longer sequences of transactions.