The categories are based on Certora's workshop notes.
-
Valid states Usually, there can be only one valid state at any given time. Such properties ensure the system is always in exactly one of its valid states.
-
State transitions Such properties verify the correctness of transactions between valid states. E.g., confirm valid states change according to their correct order or transitions only occur under the right conditions.
-
Variable transitions Similar to state transitions, but for variables. E.g., verify that Safe nonce is monotonically increasing.
-
High-level properties The most powerful type of properties covering the entire system. E.g., for any given operation, Safe threshold must remain lower or equal to the number of owners.
-
Unit test Such properties target specific function individually to verify their correctness. E.g., verify that a specific function can only be called by a specific address.
-
Risk assessment Such properties verify that worst cases that can happen to the system are handled correctly. E.g., verify that a transaction cannot be replayed.
only permissioned address can do permissioned activities. who can swap owner? who should be able to?
who should be allowed to make contract do delegate calls? contract creator address specified by contract creator
setup only be done once
check signature validation? can't sign a signature that isn't yours... not really something we can prove
module states enabled cancelled always circular checkNSignatures same as checkSignature N times
properties about approved hashes who can approve hashes? Can hashes do more than one thing?
getStorageAt gets storage at
execTransactionFromModuleReturnData