The Ranger Client

Ranger introduces a new CLI entry point: certoraRanger.

This command is part of the certora-cli Python package and provides a streamlined interface for bounded model checking, specifically designed for exploring concrete execution paths up to a limited range. It comes with new defaults and additional under-approximations to make finding concrete counterexamples easier and faster.

The certoraRanger client submits jobs to the Certora cloud, just like the Prover. You’ll receive a dashboard link with the results once the job is submitted

Ranger uses the same input format and job flow as certoraRun, allowing teams to reuse existing configuration and spec files.

Ranger-specific flags

`range`

What does it do? Sets the maximal length of function call sequences to check (0 ≤ K). This flag controls how deep Ranger explores function call sequences from the initial state. Higher values can uncover deeper bugs but may increase analysis time.

When not assigned, the default value is defined as 5

When to use it? When you wish to assign a different value than the default one. Increasing this flag will execute longer sequences, or decreasing when you wish to execute faster runs.

Example

certoraRanger ranger.conf --range K

Default Under-approximations

By default, certoraRanger enables the following Prover flags to favor usability over full soundness:

These options help prune unrealistic paths, reduce false positives, and improve performance.

Unresolved calls will be treated as nondeterministic.

You can override any of these defaults in your .conf file or via the CLI. Ranger will never fail due to unsupported overrides—it will simply continue and print a warning if needed.