diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md
index 5beca17ce..56c3c01d3 100644
--- a/docs/prover/cli/options.md
+++ b/docs/prover/cli/options.md
@@ -447,6 +447,10 @@ _Configuration file_
 "coverage_info": "advanced"
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 (--foundry)=
 ## `foundry`
 
@@ -482,6 +486,10 @@ _Configuration file_
 "foundry": true
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 (--independent_satisfy)=
 ## `independent_satisfy`
 
@@ -561,6 +569,10 @@ _Configuration file_
 "independent_satisfy": true
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 (--multi_assert_check)=
 ## `multi_assert_check`
 
@@ -612,6 +624,9 @@ _Configuration file_
 "multi_assert_check": true
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
 
 (--multi_example)=
 ## `multi_example`
@@ -639,6 +654,9 @@ _Configuration file_
 "multi_example": true
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
 
 (--project_sanity)=
 ## `project_sanity`
@@ -678,7 +696,9 @@ _Configuration file_
 "project_sanity": true
 ```
 
-
+```{note}
+Ranger does not support this option currently.
+```
 
 (--rule_sanity)=
 ## `rule_sanity`
@@ -713,6 +733,9 @@ _Configuration file_
 "rule_sanity": "basic"
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
 
 (--short_output)=
 ## `short_output`
@@ -1203,6 +1226,9 @@ _Configuration file_
 "vyper": "/usr/local/bin/vyper0.3.10"
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
 
 Options regarding source code loops
 ===================================
diff --git a/docs/ranger/how_ranger_works.md b/docs/ranger/how_ranger_works.md
new file mode 100644
index 000000000..1bf24dd95
--- /dev/null
+++ b/docs/ranger/how_ranger_works.md
@@ -0,0 +1,48 @@
+# How Ranger Works
+
+**Ranger** is a bounded model checker. This means that, in contrast with "full"
+formal verification, its initial state is not arbitrary, but is instead reached
+by a sequence of legal function calls.
+
+(the-initial-state)=
+## The Initial State
+
+Ranger starts by initializing all storage to 0, assuming all ghosts'
+`init_state` {ref}`axioms <ghost-axioms>`, and then calling the constructors
+of all the contracts in the {term}`scene`. Additionally, if the .spec file has a
+`function setup()` declared then it will run right after the constructors.
+
+## Sequences
+
+In Ranger's terminology, a sequence refers to setting the
+{ref}`initial state <the-initial-state>` followed by a series of contract
+function calls. The depth or range of a sequence is the number of functions the
+sequence calls. Note that a sequence can call the same function twice, and they
+are counted as two distinct calls.
+
+## Ranger's flow
+
+When a Ranger job starts, for each rule/invariant that's to be run it does the
+following:
+
+1. Verify that the initial state rule/invariant holds right after the
+{ref}`initial state <the-initial-state>` (it could also hold vacuously, that's
+fine in this case).
+2. For each range `1 <= i <= N` (`N` is determined by the {ref}`--range`
+option), create a sequence of `i` functions from the scene (could be from any
+contract and could have duplicates), then call them providing each function with
+independent and arbitrary input. Finally, call the rule/invariant and check that
+it holds.
+    * In the invariant case, before each function call we insert an assumption
+    that the invariant is true. This is done for optimization reasons.
+
+For each sequence `f_1 -> ... -> f_n` we first check the subsequence
+`f_1 -> ... -> f_n-1` and only if it verifies will we continue to check the
+longer sequence. This promises that if a violation is found it is the shortest
+sequence with these functions that violates the rule/invariant.
+
+```{note}
+While in principle for a provided range N there are \sum_{i=0}^N a_i sequences,
+in practice Ranger has several optimizations that prune a significant portion of
+these sequences.
+```
diff --git a/docs/ranger/index.md b/docs/ranger/index.md
new file mode 100644
index 000000000..3ff80ebd9
--- /dev/null
+++ b/docs/ranger/index.md
@@ -0,0 +1,15 @@
+(ranger-intro)=
+Ranger
+======
+
+Text
+
+```{toctree}
+:maxdepth: 2
+
+ranger_intro.md
+starting_with_ranger.md
+how_ranger_works.md
+ranger_client.md
+```
+
diff --git a/docs/ranger/ranger_client.md b/docs/ranger/ranger_client.md
new file mode 100644
index 000000000..f1f9823e7
--- /dev/null
+++ b/docs/ranger/ranger_client.md
@@ -0,0 +1,87 @@
+# 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)=
+### `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**
+
+```sh
+certoraRanger ranger.conf --range K
+```
+
+
+## Default Under-approximations
+
+By default, `certoraRanger` enables the following Prover flags to favor usability over full soundness:
+
+{ref}`--optimistic_loop`
+
+{ref}`--loop_iter` 3
+
+{ref}`--optimistic_fallback`
+
+{ref}`--optimistic_hashing`
+
+{ref}`--auto_dispatcher`
+
+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.
+
+
+## Unsupported Prover flags
+
+
+The following `certoraRun` flags are not supported in Ranger:
+
+{ref}`--project_sanity`
+
+{ref}`--rule_sanity`
+
+{ref}`--coverage_info`
+
+{ref}`--multi_example`
+
+{ref}`--foundry`
+
+{ref}`--independent_satisfy`
+
+{ref}`--multi_assert_check`
+
+If any of these are used, Ranger will emit a warning, ignore the flag, and continue the job.
+
+
+## Config file compatibility
+
+Ranger supports the same `.conf` format as the Certora Prover.
+You can reuse your existing `.conf` files without changes.
+
+- Ranger will ignore Prover-only flags in the config file.
+- Prover will ignore Ranger-only flags, like {ref}`--range`.
+
+This ensures that a single configuration file can work for both tools, enabling easier integration and faster iteration across your workflows.
diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
new file mode 100644
index 000000000..bc2f8fdc7
--- /dev/null
+++ b/docs/ranger/ranger_intro.md
@@ -0,0 +1,24 @@
+# Introduction
+
+**Ranger** is Certora’s bounded model checker for smart contracts. It complements formal verification by offering a lightweight, developer-friendly approach for quickly identifying violations of contract expected behaviors defined with [CVL](/docs/cvl/index).
+
+Unlike the [Certora Prover](/docs/user-guide/index), which explores all program states, Ranger starts from a specific initial state and explores all function call sequences up to a bounded depth. This ensures that every violation corresponds to a realistic execution path, removing the need to filter out spurious counterexamples.
+
+---
+
+## Why Ranger?
+
+Formal Verification provides strong correctness guarantees and checks more program states, but it can be slow, complex, and prone to false positives from unreachable states. {term}`fuzzing`, on the other hand, is faster, but has a lower coverage as it only checks for specific inputs per run.
+
+Ranger offers a practical middle ground:
+
+- ✅ **Realistic counterexamples**: All violations are reachable from the initial state.
+- ✅ **Faster time to value**: Minimal setup required to get useful results.
+- ✅ **Fewer false positives**: No need to precondition rules to filter out invalid states.
+- ✅ **High coverage**: Tests all function call sequences on symbolic inputs from the initial state up to a certain range.
+
+---
+
+## Scope and Limitations
+
+Ranger is in active development and currently supports only Solidity contracts.
diff --git a/docs/ranger/starting_with_ranger.md b/docs/ranger/starting_with_ranger.md
new file mode 100644
index 000000000..cd9382406
--- /dev/null
+++ b/docs/ranger/starting_with_ranger.md
@@ -0,0 +1,55 @@
+# Getting Started
+
+This guide will help you run your first Ranger job using a Solidity contract and a [CVL](/docs/cvl/index) `.spec` file.
+
+Ranger uses the same installation process, configuration files, and spec files as the [Certora Prover](/docs/user-guide/index). If you're already familiar with the Prover, getting started with Ranger will feel familiar.
+
+---
+
+## 1. Install Certora Tools
+
+Ranger is part of the `certora-cli` Python package. You can install or upgrade it using `pip`:
+
+```bash
+pip install certora-cli
+```
+For full installation instructions and troubleshooting, see the Certora Prover [installation guide](/docs/user-guide/install).
+
+## 2. Prepare Your Files
+You'll need three files:
+
+- A compiled Solidity contract (e.g. `MyContract.sol`)
+- A CVL `.spec` file
+- A configuration file (e.g. `ranger.conf`)
+
+Example `ranger.conf`:
+
+```json
+{
+    "files": ["MyContract.sol"],
+    "verify": "MyContract:MyContract.spec"
+}
+```
+
+## 3. Run Ranger
+Use the `certoraRanger` command to launch the job:
+
+```bash
+certoraRanger ranger.conf
+```
+
+This will start the Ranger process. A link to the Ranger Job Report in the dashboard will be pasted into your command line when the job is submitted.
+
+```{warning}
+Ranger is compute-intensive: It performs symbolic exploration of many function call sequences. For faster feedback, avoiding timeouts, and better resource usage, consider one of the following:
+
+1. Use {ref}`--rule` to focus on a single invariant or rule.
+
+2. Use {ref}`--split_rules` to automatically run each invariant/rule in a separate job.
+```
+
+
+## 4. View the Results
+A link to the Ranger Job Report in the dashboard will be pasted in your command line 
+when the job is submitted. 
+You can explore the results in the web-based Ranger Report by following the link. 
diff --git a/docs/user-guide/glossary.md b/docs/user-guide/glossary.md
index e4b909e2b..db6a13e2e 100644
--- a/docs/user-guide/glossary.md
+++ b/docs/user-guide/glossary.md
@@ -76,6 +76,12 @@ EVM storage
   the Ethereum blockchain.
   [Official documentation](https://ethereum.org/en/developers/docs/smart-contracts/anatomy)
 
+fuzzing
+  An automated testing technique that sends large volumes of randomized or semi-randomized 
+  inputs to smart contract functions to uncover unexpected behaviors, reverts, or security
+  vulnerabilities. In DeFi, fuzzing is especially useful for discovering edge cases in financial
+  logic, such as precision loss, invalid state transitions, or violations of protocol invariants.
+
 havoc
   Havoc refers to assigning variables arbitrary, non-deterministic values. 
   This occurs in two main cases:
diff --git a/index.rst b/index.rst
index 1bc3ea752..94060bcf5 100644
--- a/index.rst
+++ b/index.rst
@@ -11,6 +11,7 @@ Contents
 * :doc:`docs/sunbeam/index` -- instructions for installing and using *Certora Sunbeam*
   for formal verification of `Soroban`_ contracts.
 * :doc:`docs/solana/index` -- instructions for installing and using *Certora Solana Prover*
+* :doc:`docs/ranger/index` -- explains how to use Ranger, Certora's Bounded Model Checker for EVM
 * :doc:`docs/gambit/index` -- use mutation testing to improve you specifications.
 
 .. toctree::
@@ -23,6 +24,7 @@ Contents
    docs/prover/index.md
    docs/sunbeam/index.rst
    docs/solana/index.rst
+   docs/ranger/index.md
    docs/gambit/index.md