This documentation has been moved to https://docs.certora.com/
Keywords
Standard identifiers
CVL language includes the following standard identifiers:
bool lastReverted
- true when the last function call reverted, for example “did the transfer revert?”. Note that it can only return true if the last function was marked with@withrevert
.address currentContract
- the address of the current contract that is checked, e.g. the address ofBank
.storage lastStorage
- The current state of the contract. Useful for enforcing hyperproperties of smart contracts.
rule transfer_reverts() {
// A rule with two free variables:
// - to - the address the transfer is passed to
// - amount - the amount of money to pass
address to;
uint256 amount;
env e;
// Get the caller's balance before the invocation of transfer
uint256 balance = getFunds(e.msg.sender);
// invoke function transfer and assume the caller is w.msg.from
transfer@withrevert(e, to, amount);
// check that transfer reverts if the sender does not have enough funds
assert balance < amount => lastReverted , "insufficient funds";
}