README.md

Examples for CVL Commands

Category	Links
array	In a statement, In SStore parameter, by function call, Function declaration in method block
assert	assert
assert_uint256	assert_uint256
at	at
builtin rule	builtin rule
calldataarg	calldataarg
cvldoc	cvldoc @param, cvldoc @title
CVL function	CVL function, override
definition	definition
expect	expect
filtered	filtered
forall	forall
Function call	Function call
ghost	simple variable example, ghost mapping, ghost function, init_state, axiom, ghost summary
hook	Sstore, Sload
import	import
invariant	Simple Invariant, strengthening, preserved with (env e), requireInvariant, Teams example (preserved, requireInvariant, Invariant fail without preserved
lastreverted	lastreverted
laststorage	laststorage
methods block	Calls to external contracts, envfree, Summary ALWAYS, CONSTANT, DISPATCHER, NONDET, HAVOC_ALL, Summary Application ALL, UNRESOLVED, direct summarization, wildcard summarization, CVL Function Summary, Ghost Summary, optional, 'expect'
nativeBalances	nativeBalances
override	override, definition, function
require	require
require_uint256	require_uint256
rule	Simple Rule, parameterized Simple Parameters, Method Parameter
satisfy	satisfy
selector	selector
sig	sig
storage	of a contract, of a ghost, of nativeBalances, full storage, laststorage, direct storage access
struct	struct return type, struct in methods block: struct parameter, struct return type, returning a struct as a tuple, struct in a CVL function: struct parameter to a CVL function, struct return type of a CVL function, returning struct as a tuple, assignment to struct, Assigning struct to a tuple
to_mathint	to_mathint
use	rule: with filters, overriding imported filters, invariant: overriding imported preserved, builtin rule
using	using
withrevert	withrevert
CVL Type	mathint, method, env
ercecover	example
TransientStorage	Tstore Hook Tload Hook
executingContract	example
directStorageAccess	example
UnresolvedCallSummarization	example

These examples can serve as an introduction to CVL ( Certora Verification Language ). It also contains examples that are based on real-life code and the spec that have caught critical bugs.

See https://docs.certora.com for a complete guide.