Generate action sequences while checking a property after each step.
LET’S PICTURE IT
A game rule should hold after every move, not only after one opening move.
SEE IT FOR YOURSELF
A valid counter call, step by stepStep 1 / 4
This example begins with count zero and a request to call increment(). No real contract is deployed.
This example begins with count zero and a request to call increment(). No real contract is deployed.Execution follows the code’s input and permission rules. A website button is not the access-control mechanism.The function reads zero, calculates zero plus one, and writes one to persistent storage.The accepted state contains count one. Later reads can inspect it. Events are emitted only if the code implements them.
Animated local teaching model. No wallet, RPC or live blockchain data. Some labels and hashes are abbreviated for readability.
Model a stateful system
A sequence can contain deposits, transfers, withdrawals and rejected attempts. Later actions run against the state produced by earlier ones.
Define the allowed actors
Use multiple accounts and relevant privileged roles. A single friendly actor can miss permission and inter-user accounting failures.
Control handler assumptions
A test handler should not silently exclude the very transitions that could break the property. Document preconditions and avoid excessive filtering.
Minimize failing sequences
A small counterexample such as deposit, donation, withdraw can explain more than a long noisy trace. Preserve the seed and state setup.
Define the test
state S0
action A → S1 → assert invariant
action B → S2 → assert invariant
action C → S3 → assert invariant
Test plans are framework-neutral unless labeled as complete Solidity or JavaScript. Use a local test environment and no real funds.
QUICK CHECK · NO PRESSURE
How does invariant testing differ from one isolated input test?