Glossary

Actor

The address that will perform the calls specific to TargetFunctions. See ActorManager for how to use these in a test suite.

CryticTester

The invariant testing contract that's deployed in the Chimera Framework and that the fuzzer will use to explore state and properties with the target functions defined on it.

CryticToFoundry

A Foundry test contract used to implement unit tests of property-breaking call sequences (reproducers) obtained with testing tools (i.e. Echidna, Medusa, Halmos, etc.).

Clamping

Reducing the search space of a fuzzer for a handler function by excluding certain input values that may not provide meaningful coverage.

Dynamic Deployment

A technique that consists of adding custom handlers that will deploy new contracts, by leaving the configuration up to the fuzzer, this can help explore more unintuitive edge cases and configurations.

Dynamic Deployment is the opposite of a hardcoded config in Setup.

Property

A property is a verifiable claim about contract behavior — for example, "total supply equals sum of all balances" or "no withdrawal exceeds the user's deposit." Properties can be tested via fuzzing (random state exploration) or formal verification (mathematical proof).

Invariant Testing

Invariant testing automatically verifies that system properties (expected behaviors) remain valid across all possible sequences of state changes, using random fuzzing or formal verification to explore the state space.

Reproducer

A call trace generated by a tool (fuzzer, formal verifier) that breaks a property of a contract or system.

Invariant

An invariant is a property that must hold true after any operation on the system, regardless of which functions are called or in what order. It represents the strongest form of behavioral guarantee — for example, "the sum of all balances never exceeds totalSupply" must hold after every transaction.

Fuzzer

An engine/solver, a program that can perform stateful tests on a smart contract or system.

Some fuzzers are concrete, others concolic, and others symbolic.

Handler

A handler wraps a target contract function for property testing. It includes the function call itself, optional clamping (input narrowing to focus the fuzzer's search space), and assertions that verify expected state changes after execution.

Target Function

Target functions are the specific contract functions the fuzzer calls during testing to explore different system states and verify properties. You select which state-changing functions to include based on their relevance to the properties being tested.

Shrinking

A process performed by the fuzzer to remove unnecessary calls from a call sequence that don't contribute to breaking a property.

Line Coverage

The ability of the fuzzer to reach a specific line in the targeted contract.

Logical Coverage

The frequency with which the fuzzer reaches all possible logical paths in a function of interest.

Scaffolding

The set of smart contracts put into place to organize the code and tell the fuzzer how to explore states and test properties.

Echidna

A concrete fuzzer written in Haskell, using HEVM as its EVM engine.

Medusa

A concrete fuzzer written in Go, using GETH for the EVM engine.

Halmos

A symbolic fuzzer written in Python, using its own SEVM for the EVM engine.