From fba3aae197acb1de9b53c724b21da45b81ebdb1d Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Mon, 12 May 2025 21:56:27 +0300
Subject: [PATCH 01/32] added Ranger repo

---
 docs/ranger/index.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 docs/ranger/index.md

diff --git a/docs/ranger/index.md b/docs/ranger/index.md
new file mode 100644
index 000000000..13c019515
--- /dev/null
+++ b/docs/ranger/index.md
@@ -0,0 +1,12 @@
+(ranger-intro)=
+Ranger: Info goes here
+=================================
+
+Text
+
+<!-- ```{toctree}
+:maxdepth: 2
+
+ranger.md
+``` -->
+

From 9bb35c80eba2906549d694318c581ceb7a323517 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Mon, 12 May 2025 22:03:22 +0300
Subject: [PATCH 02/32] added an md besides the index page

---
 docs/ranger/index.md  | 4 ++--
 docs/ranger/ranger.md | 3 +++
 2 files changed, 5 insertions(+), 2 deletions(-)
 create mode 100644 docs/ranger/ranger.md

diff --git a/docs/ranger/index.md b/docs/ranger/index.md
index 13c019515..f8248d78b 100644
--- a/docs/ranger/index.md
+++ b/docs/ranger/index.md
@@ -4,9 +4,9 @@ Ranger: Info goes here
 
 Text
 
-<!-- ```{toctree}
+```{toctree}
 :maxdepth: 2
 
 ranger.md
-``` -->
+```
 
diff --git a/docs/ranger/ranger.md b/docs/ranger/ranger.md
new file mode 100644
index 000000000..3434a271f
--- /dev/null
+++ b/docs/ranger/ranger.md
@@ -0,0 +1,3 @@
+# Ranger
+
+placeholder text
\ No newline at end of file

From 98790922beb24ba16cd25131a549978ac5055bdb Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Mon, 12 May 2025 22:05:04 +0300
Subject: [PATCH 03/32] added Ranger to top level toc tree

---
 index.rst | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/index.rst b/index.rst
index 1bc3ea752..a49e03d33 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` -- TODO
 * :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
 
 

From 2247e566e7c130284ac4bda48924bcab97b8bb57 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Mon, 12 May 2025 22:23:00 +0300
Subject: [PATCH 04/32] adding all files under ranger docs

---
 docs/ranger/how_ranger_works.md     |  0
 docs/ranger/index.md                |  5 ++++-
 docs/ranger/ranger.md               |  3 ---
 docs/ranger/ranger_client.md        |  0
 docs/ranger/ranger_intro.md         | 15 +++++++++++++++
 docs/ranger/starting_with_ranger.md | 10 ++++++++++
 6 files changed, 29 insertions(+), 4 deletions(-)
 create mode 100644 docs/ranger/how_ranger_works.md
 delete mode 100644 docs/ranger/ranger.md
 create mode 100644 docs/ranger/ranger_client.md
 create mode 100644 docs/ranger/ranger_intro.md
 create mode 100644 docs/ranger/starting_with_ranger.md

diff --git a/docs/ranger/how_ranger_works.md b/docs/ranger/how_ranger_works.md
new file mode 100644
index 000000000..e69de29bb
diff --git a/docs/ranger/index.md b/docs/ranger/index.md
index f8248d78b..acd9c5a09 100644
--- a/docs/ranger/index.md
+++ b/docs/ranger/index.md
@@ -7,6 +7,9 @@ Text
 ```{toctree}
 :maxdepth: 2
 
-ranger.md
+ranger_intro.md
+starting_with_ranger.md
+how_ranger_works.md
+ranger_client.md
 ```
 
diff --git a/docs/ranger/ranger.md b/docs/ranger/ranger.md
deleted file mode 100644
index 3434a271f..000000000
--- a/docs/ranger/ranger.md
+++ /dev/null
@@ -1,3 +0,0 @@
-# Ranger
-
-placeholder text
\ No newline at end of file
diff --git a/docs/ranger/ranger_client.md b/docs/ranger/ranger_client.md
new file mode 100644
index 000000000..e69de29bb
diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
new file mode 100644
index 000000000..d2dd2e740
--- /dev/null
+++ b/docs/ranger/ranger_intro.md
@@ -0,0 +1,15 @@
+# Ranger
+
+What is Ranger?
+
+## Bounded Model Checking vs Formal Verification
+
+## Bounded Model Checking vs Fuzzing
+
+## Key benefits
+
+realistic counterexamples, faster feedback
+
+## Scope and limitations
+
+(Solidity only, invariants only)
diff --git a/docs/ranger/starting_with_ranger.md b/docs/ranger/starting_with_ranger.md
new file mode 100644
index 000000000..507c9fcb3
--- /dev/null
+++ b/docs/ranger/starting_with_ranger.md
@@ -0,0 +1,10 @@
+# Getting Started
+
+Quickstart with example config
+
+How to write a basic invariant (with link to CVL docs)
+
+Running your first certoraRanger job
+
+Link to existing installation guide
+

From 2e139a043f60d6edccaed3b7365748889c7a17b1 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Mon, 12 May 2025 22:27:00 +0300
Subject: [PATCH 05/32] forgot to add content

---
 docs/ranger/how_ranger_works.md | 7 +++++++
 docs/ranger/ranger_client.md    | 9 +++++++++
 2 files changed, 16 insertions(+)

diff --git a/docs/ranger/how_ranger_works.md b/docs/ranger/how_ranger_works.md
index e69de29bb..7edc86dba 100644
--- a/docs/ranger/how_ranger_works.md
+++ b/docs/ranger/how_ranger_works.md
@@ -0,0 +1,7 @@
+# How Ranger Works
+
+Bounded search and depth (--bmc)
+
+Initial state selection (constructor vs custom)
+
+Built-in underapproximations (and how to override them)
diff --git a/docs/ranger/ranger_client.md b/docs/ranger/ranger_client.md
index e69de29bb..3dcf50bd3 100644
--- a/docs/ranger/ranger_client.md
+++ b/docs/ranger/ranger_client.md
@@ -0,0 +1,9 @@
+# The Ranger Client
+
+# Usage: certoraRanger
+
+# Ranger-specific flags
+
+# Unsupported Prover flags
+
+# Config file compatibility

From bcfcbd21642a1c837838995090d0c9ee2966657f Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 13 May 2025 16:50:17 +0300
Subject: [PATCH 06/32] base text for Ranger

---
 docs/ranger/ranger_intro.md | 39 +++++++++++++++++++++++++++++--------
 1 file changed, 31 insertions(+), 8 deletions(-)

diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
index d2dd2e740..eedb57595 100644
--- a/docs/ranger/ranger_intro.md
+++ b/docs/ranger/ranger_intro.md
@@ -1,15 +1,38 @@
-# Ranger
+# Introduction
 
-What is Ranger?
+**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 invariants.
 
-## Bounded Model Checking vs Formal Verification
+Unlike the Certora Prover, which explores all reachable states of a program, 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.
 
-## Bounded Model Checking vs Fuzzing
+---
 
-## Key benefits
+## Why Ranger?
 
-realistic counterexamples, faster feedback
+Formal Verification (FV) provides strong guarantees, but it can be slow, complex, and prone to false positives from unreachable states. Fuzzing, on the other hand, is faster and more intuitive, but lacks completeness and soundness.
 
-## Scope and limitations
+Ranger offers a practical middle ground:
 
-(Solidity only, invariants only)
+- ✅ **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.
+
+---
+
+## What Ranger Does
+
+- Starts from a **user-defined initial state** (or uses the constructor by default).
+- Symbolically executes all function call sequences up to depth `K`.
+- Stops once a configurable number of violations are found (default: 10).
+- Generates a dedicated **Ranger Job Report** showing execution ranges, invariant statuses, and violations.
+
+---
+
+## Scope and Limitations
+
+Ranger is in active development and currently supports:
+
+- ✅ Solidity contracts
+- ✅ Invariant checking with CVL
+- ❌ No support for Vyper, CVL rules, or reruns from the UI
+
+> For details on writing CVL invariants, refer to the [Certora Prover language guide](https://docs.certora.com/en/latest/docs/cvl/index.html).

From 821c4095e82ad3ef4dbc72cec26e6e9e3136af0c Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 13 May 2025 19:43:48 +0300
Subject: [PATCH 07/32] first round of upgrades

---
 docs/ranger/ranger_intro.md | 22 +++++-----------------
 1 file changed, 5 insertions(+), 17 deletions(-)

diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
index eedb57595..a512e5ea6 100644
--- a/docs/ranger/ranger_intro.md
+++ b/docs/ranger/ranger_intro.md
@@ -2,37 +2,25 @@
 
 **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 invariants.
 
-Unlike the Certora Prover, which explores all reachable states of a program, 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.
+Unlike the Certora Prover, which explores all states of a program, 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 (FV) provides strong guarantees, but it can be slow, complex, and prone to false positives from unreachable states. Fuzzing, on the other hand, is faster and more intuitive, but lacks completeness and soundness.
+Formal Verification provides strong correctness guarantees, and xhexks more program states, but it can be slow, complex, and prone to false positives from unreachable states. 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.
-
----
-
-## What Ranger Does
-
-- Starts from a **user-defined initial state** (or uses the constructor by default).
-- Symbolically executes all function call sequences up to depth `K`.
-- Stops once a configurable number of violations are found (default: 10).
-- Generates a dedicated **Ranger Job Report** showing execution ranges, invariant statuses, and violations.
+- ✅ **High coverage**: Symbolicly tests all function call sequences from the initial state up to a certain range.
 
 ---
 
 ## Scope and Limitations
 
-Ranger is in active development and currently supports:
-
-- ✅ Solidity contracts
-- ✅ Invariant checking with CVL
-- ❌ No support for Vyper, CVL rules, or reruns from the UI
+Ranger is in active development and currently supports only supports Solidity contracts.
 
-> For details on writing CVL invariants, refer to the [Certora Prover language guide](https://docs.certora.com/en/latest/docs/cvl/index.html).
+Currently, Ranger can only check CVL invariants. Rules will be supported in the future.

From 41a7e8bca12f25922926b2e9b1a827d6a4811b35 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 13 May 2025 19:47:43 +0300
Subject: [PATCH 08/32] trying ref and term tags

---
 docs/ranger/ranger_intro.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
index a512e5ea6..fb48620cf 100644
--- a/docs/ranger/ranger_intro.md
+++ b/docs/ranger/ranger_intro.md
@@ -23,4 +23,4 @@ Ranger offers a practical middle ground:
 
 Ranger is in active development and currently supports only supports Solidity contracts.
 
-Currently, Ranger can only check CVL invariants. Rules will be supported in the future.
+Currently, Ranger can only check CVL {ref}`invariants`. {term}`rules` will be supported in the future.

From 6cd89a5cb086dfb908879a7c1ac71850057289f8 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 13 May 2025 20:00:55 +0300
Subject: [PATCH 09/32] improving links

---
 docs/ranger/ranger_intro.md | 6 +++---
 docs/user-guide/glossary.md | 6 ++++++
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
index fb48620cf..f765fae7e 100644
--- a/docs/ranger/ranger_intro.md
+++ b/docs/ranger/ranger_intro.md
@@ -2,13 +2,13 @@
 
 **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 invariants.
 
-Unlike the Certora Prover, which explores all states of a program, 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.
+Unlike the [Certora Prover](/docs/user-guide/index), which explores all states of a program, 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 xhexks more program states, but it can be slow, complex, and prone to false positives from unreachable states. Fuzzing, on the other hand, is faster, but has a lower coverage as it only checks for specific inputs per run.
+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:
 
@@ -23,4 +23,4 @@ Ranger offers a practical middle ground:
 
 Ranger is in active development and currently supports only supports Solidity contracts.
 
-Currently, Ranger can only check CVL {ref}`invariants`. {term}`rules` will be supported in the future.
+Currently, Ranger can only check [CVL](cvl-language.md) {ref}`invariants`. Rules will be supported in the future.
diff --git a/docs/user-guide/glossary.md b/docs/user-guide/glossary.md
index 6f416588a..24dcd2c28 100644
--- a/docs/user-guide/glossary.md
+++ b/docs/user-guide/glossary.md
@@ -77,6 +77,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 means that variables are assigned values chosen non-deterministically.
   A havoc happens in two cases: the first, at the beginning of the rule all variables

From f21b1823778ce15d16a4fff424c5b86404541cf7 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 13 May 2025 20:02:59 +0300
Subject: [PATCH 10/32] text improvements on intro

---
 docs/ranger/ranger_intro.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
index f765fae7e..943f76148 100644
--- a/docs/ranger/ranger_intro.md
+++ b/docs/ranger/ranger_intro.md
@@ -2,25 +2,25 @@
 
 **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 invariants.
 
-Unlike the [Certora Prover](/docs/user-guide/index), which explores all states of a program, 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.
+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.
+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**: Symbolicly tests all function call sequences from the initial state up to a certain range.
+- ✅ **High coverage**: Symbolically tests all function call sequences from the initial state up to a certain range.
 
 ---
 
 ## Scope and Limitations
 
-Ranger is in active development and currently supports only supports Solidity contracts.
+Ranger is in active development and currently supports only Solidity contracts.
 
 Currently, Ranger can only check [CVL](cvl-language.md) {ref}`invariants`. Rules will be supported in the future.

From 4056511bcacb1b834198283d341dc07481a9292d Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 13 May 2025 20:09:22 +0300
Subject: [PATCH 11/32] fixing link to CVL

---
 docs/ranger/ranger_intro.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
index 943f76148..ef16aacad 100644
--- a/docs/ranger/ranger_intro.md
+++ b/docs/ranger/ranger_intro.md
@@ -23,4 +23,4 @@ Ranger offers a practical middle ground:
 
 Ranger is in active development and currently supports only Solidity contracts.
 
-Currently, Ranger can only check [CVL](cvl-language.md) {ref}`invariants`. Rules will be supported in the future.
+Currently, Ranger can only check [CVL](/docs/cvl/index) {ref}`invariants`. Rules will be supported in the future.

From 669da9ba3525ff6a9d9fefd0cdd22b5edb1df04b Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 13 May 2025 20:23:41 +0300
Subject: [PATCH 12/32] first version of Ranger user guide

---
 docs/ranger/starting_with_ranger.md | 44 ++++++++++++++++++++++++++---
 1 file changed, 40 insertions(+), 4 deletions(-)

diff --git a/docs/ranger/starting_with_ranger.md b/docs/ranger/starting_with_ranger.md
index 507c9fcb3..a16ef391f 100644
--- a/docs/ranger/starting_with_ranger.md
+++ b/docs/ranger/starting_with_ranger.md
@@ -1,10 +1,46 @@
 # Getting Started
 
-Quickstart with example config
+This guide will help you run your first Ranger job using a Solidity contract and a [CVL](/docs/cvl/index) [invariant](/docs/cvl/invariants).
 
-How to write a basic invariant (with link to CVL docs)
+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.
 
-Running your first certoraRanger job
+---
 
-Link to existing installation guide
+## 1. Install Certora Tools
 
+Ranger is part of the `certora` 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 with at least one invariant (e.g. `MyContract.spec`)
+- 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 in your command line when the job is submitted.
+
+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 clicking on the link. 

From 4af3d4175bc559f61c500b641c185eac9cffc8bf Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 13 May 2025 20:30:20 +0300
Subject: [PATCH 13/32] fixing titles

---
 docs/ranger/starting_with_ranger.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/docs/ranger/starting_with_ranger.md b/docs/ranger/starting_with_ranger.md
index a16ef391f..1a41901ca 100644
--- a/docs/ranger/starting_with_ranger.md
+++ b/docs/ranger/starting_with_ranger.md
@@ -15,7 +15,7 @@ pip install certora-cli
 ```
 For full installation instructions and troubleshooting, see the Certora Prover [installation guide](/docs/user-guide/install).
 
-2. Prepare Your Files
+## 2. Prepare Your Files
 You'll need three files:
 
 - A compiled Solidity contract (e.g. `MyContract.sol`)
@@ -27,11 +27,11 @@ Example `ranger.conf`:
 ```json
 {
     "files": ["MyContract.sol"],
-    "verify" "MyContract:MyContract.spec"
+    "verify": "MyContract:MyContract.spec"
 }
 ```
 
-3. Run Ranger
+## 3. Run Ranger
 Use the certoraRanger command to launch the job:
 
 ```bash
@@ -40,7 +40,7 @@ certoraRanger ranger.conf
 
 This will start the Ranger process. A link to the Ranger Job Report in the dashboard will be pasted in your command line when the job is submitted.
 
-4. View the Results
+## 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 clicking on the link. 

From fb127911c3bce742ccdc9a64a97175f2b09185ed Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 13 May 2025 20:32:52 +0300
Subject: [PATCH 14/32] minor improvements to Ranger getting started

---
 docs/ranger/starting_with_ranger.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/ranger/starting_with_ranger.md b/docs/ranger/starting_with_ranger.md
index 1a41901ca..778668506 100644
--- a/docs/ranger/starting_with_ranger.md
+++ b/docs/ranger/starting_with_ranger.md
@@ -38,9 +38,9 @@ Use the certoraRanger command to launch the job:
 certoraRanger ranger.conf
 ```
 
-This will start the Ranger process. A link to the Ranger Job Report in the dashboard will be pasted in your command line when the job is submitted.
+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.
 
 ## 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 clicking on the link. 
+You can explore the results in the web-based Ranger Report by following the link. 

From dafa02684de4897e7ea875312b0828cfea212b83 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 13 May 2025 20:34:40 +0300
Subject: [PATCH 15/32] shorter title for Ranger index page

---
 docs/ranger/index.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/ranger/index.md b/docs/ranger/index.md
index acd9c5a09..3ff80ebd9 100644
--- a/docs/ranger/index.md
+++ b/docs/ranger/index.md
@@ -1,6 +1,6 @@
 (ranger-intro)=
-Ranger: Info goes here
-=================================
+Ranger
+======
 
 Text
 

From 1b686eb01531ab9f9c479aa02f132f6300456c3d Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Sun, 18 May 2025 13:21:14 +0300
Subject: [PATCH 16/32] ranger now also checks rules

---
 docs/ranger/ranger_intro.md | 2 --
 1 file changed, 2 deletions(-)

diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
index ef16aacad..1b02dfb6e 100644
--- a/docs/ranger/ranger_intro.md
+++ b/docs/ranger/ranger_intro.md
@@ -22,5 +22,3 @@ Ranger offers a practical middle ground:
 ## Scope and Limitations
 
 Ranger is in active development and currently supports only Solidity contracts.
-
-Currently, Ranger can only check [CVL](/docs/cvl/index) {ref}`invariants`. Rules will be supported in the future.

From 03f3c08dffddea2583a0b08cec99efc377f62c4c Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Sun, 18 May 2025 13:26:51 +0300
Subject: [PATCH 17/32] added note about using either --rule or --split_rules

---
 docs/ranger/starting_with_ranger.md | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/docs/ranger/starting_with_ranger.md b/docs/ranger/starting_with_ranger.md
index 778668506..adde88a1e 100644
--- a/docs/ranger/starting_with_ranger.md
+++ b/docs/ranger/starting_with_ranger.md
@@ -40,6 +40,15 @@ 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.
 
+```{warn}
+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 rule/invariant 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. 

From 22e5da9b646aa64fb7bab6cda4c4b4e3d90bd38c Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Sun, 18 May 2025 13:29:23 +0300
Subject: [PATCH 18/32] {warn} -> {warning}

---
 docs/ranger/starting_with_ranger.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/ranger/starting_with_ranger.md b/docs/ranger/starting_with_ranger.md
index adde88a1e..ec3e16daf 100644
--- a/docs/ranger/starting_with_ranger.md
+++ b/docs/ranger/starting_with_ranger.md
@@ -40,7 +40,7 @@ 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.
 
-```{warn}
+```{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.

From 6f1bcfd199c40c5c73c2fd68fbcb93b7943c32d1 Mon Sep 17 00:00:00 2001
From: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com>
Date: Sun, 18 May 2025 19:49:21 +0300
Subject: [PATCH 19/32] Yoav/cert 8890 ranger cli docs (#397)

* start

* Added CLI docs

* Fixing ref

* spelling

* CR

* Update docs/ranger/ranger_client.md

Co-authored-by: urikirsh <38188877+urikirsh@users.noreply.github.com>

* Removed "usage" section and commented range_failure_limit attribute until decided otherwise.

* fixed attribute typo

* How Ranger Works (#398)

* how ranger works

* Uri's CR

---------

Co-authored-by: urikirsh <38188877+urikirsh@users.noreply.github.com>
Co-authored-by: Naftali Goldstein <44599898+naftali-g@users.noreply.github.com>
---
 docs/ranger/how_ranger_works.md |  47 +++++++++++++-
 docs/ranger/ranger_client.md    | 112 +++++++++++++++++++++++++++++++-
 2 files changed, 155 insertions(+), 4 deletions(-)

diff --git a/docs/ranger/how_ranger_works.md b/docs/ranger/how_ranger_works.md
index 7edc86dba..4c60b3d47 100644
--- a/docs/ranger/how_ranger_works.md
+++ b/docs/ranger/how_ranger_works.md
@@ -1,7 +1,48 @@
 # How Ranger Works
 
-Bounded search and depth (--bmc)
+**Ranger** is a bounded model checker. This means that, in contrast with "full"
+formal verification, its initial state isn't arbitrary, but is instead reached
+by a sequence of legal function calls.
 
-Initial state selection (constructor vs custom)
+(the-initial-state)=
+## The Initial State
 
-Built-in underapproximations (and how to override them)
+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/ranger_client.md b/docs/ranger/ranger_client.md
index 3dcf50bd3..25f9a1c1c 100644
--- a/docs/ranger/ranger_client.md
+++ b/docs/ranger/ranger_client.md
@@ -1,9 +1,119 @@
 # The Ranger Client
 
-# Usage: certoraRanger
+Ranger introduces a new CLI entry point: `certoraRanger`.
+
+This command is part of the certora 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
+```
+
+[//]: # (&#40;--ranger_failure_limit&#41;=)
+
+[//]: # (## `ranger_failure_limit`)
+
+[//]: # ()
+[//]: # (**What does it do?**)
+
+[//]: # (Sets the minimal number of violations to be found.)
+
+[//]: # (Once we reach this limit, no new Ranger call sequence checks will be started.)
+
+[//]: # (Checks already in progress will continue, thus we are expected to see at least N violations.)
+
+[//]: # ()
+[//]: # (When not assigned, the default value is defined as 1.)
+
+[//]: # ()
+[//]: # (**When to use it?**)
+
+[//]: # (When you wish to assign a different value than the default one.)
+
+[//]: # (Increasing this flag will execute more sequences, until we will reach the desired amount of violations.)
+
+[//]: # ()
+[//]: # (**Example**)
+
+[//]: # ()
+[//]: # (```sh)
+
+[//]: # (certoraRanger ranger.conf --ranger_failure_limit N)
+
+[//]: # (```)
+
+## `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.

From 834dcd9392d1ea0e0baa5cd5a2e26cc70f6c74f9 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Sun, 18 May 2025 19:57:15 +0300
Subject: [PATCH 20/32] trying a new markdown comment style

---
 docs/ranger/ranger_client.md | 38 ++++++++++++++++++------------------
 1 file changed, 19 insertions(+), 19 deletions(-)

diff --git a/docs/ranger/ranger_client.md b/docs/ranger/ranger_client.md
index 25f9a1c1c..517c3d9a1 100644
--- a/docs/ranger/ranger_client.md
+++ b/docs/ranger/ranger_client.md
@@ -32,38 +32,38 @@ Increasing this flag will execute longer sequences, or decreasing when you wish
 certoraRanger ranger.conf --range K
 ```
 
-[//]: # (&#40;--ranger_failure_limit&#41;=)
+[//]: <> (&#40;--ranger_failure_limit&#41;=)
 
-[//]: # (## `ranger_failure_limit`)
+[//]: <> (## `ranger_failure_limit`)
 
-[//]: # ()
-[//]: # (**What does it do?**)
+[//]: <> ()
+[//]: <> (**What does it do?**)
 
-[//]: # (Sets the minimal number of violations to be found.)
+[//]: <> (Sets the minimal number of violations to be found.)
 
-[//]: # (Once we reach this limit, no new Ranger call sequence checks will be started.)
+[//]: <> (Once we reach this limit, no new Ranger call sequence checks will be started.)
 
-[//]: # (Checks already in progress will continue, thus we are expected to see at least N violations.)
+[//]: <> (Checks already in progress will continue, thus we are expected to see at least N violations.)
 
-[//]: # ()
-[//]: # (When not assigned, the default value is defined as 1.)
+[//]: <> ()
+[//]: <> (When not assigned, the default value is defined as 1.)
 
-[//]: # ()
-[//]: # (**When to use it?**)
+[//]: <> ()
+[//]: <> (**When to use it?**)
 
-[//]: # (When you wish to assign a different value than the default one.)
+[//]: <> (When you wish to assign a different value than the default one.)
 
-[//]: # (Increasing this flag will execute more sequences, until we will reach the desired amount of violations.)
+[//]: <> (Increasing this flag will execute more sequences, until we will reach the desired amount of violations.)
 
-[//]: # ()
-[//]: # (**Example**)
+[//]: <> ()
+[//]: <> (**Example**)
 
-[//]: # ()
-[//]: # (```sh)
+[//]: <> ()
+[//]: <> (```sh)
 
-[//]: # (certoraRanger ranger.conf --ranger_failure_limit N)
+[//]: <> (certoraRanger ranger.conf --ranger_failure_limit N)
 
-[//]: # (```)
+[//]: <> (```)
 
 ## `Default Under-approximations`
 

From 4be35a03ccaff9bc5d113145773e1e1bd5dd4e2d Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Sun, 18 May 2025 20:02:17 +0300
Subject: [PATCH 21/32] trying a different style of comment

---
 docs/ranger/ranger_client.md | 31 +++++++++++++++----------------
 1 file changed, 15 insertions(+), 16 deletions(-)

diff --git a/docs/ranger/ranger_client.md b/docs/ranger/ranger_client.md
index 517c3d9a1..98a512d53 100644
--- a/docs/ranger/ranger_client.md
+++ b/docs/ranger/ranger_client.md
@@ -34,10 +34,9 @@ certoraRanger ranger.conf --range K
 
 [//]: <> (&#40;--ranger_failure_limit&#41;=)
 
-[//]: <> (## `ranger_failure_limit`)
-
-[//]: <> ()
-[//]: <> (**What does it do?**)
+[## `ranger_failure_limit`]::
+[
+    **What does it do?**]::
 
 [//]: <> (Sets the minimal number of violations to be found.)
 
@@ -45,25 +44,25 @@ certoraRanger ranger.conf --range K
 
 [//]: <> (Checks already in progress will continue, thus we are expected to see at least N violations.)
 
-[//]: <> ()
-[//]: <> (When not assigned, the default value is defined as 1.)
+[//]: # ()
+[//]: # (When not assigned, the default value is defined as 1.)
 
-[//]: <> ()
-[//]: <> (**When to use it?**)
+[//]: # ()
+[//]: # (**When to use it?**)
 
-[//]: <> (When you wish to assign a different value than the default one.)
+[//]: # (When you wish to assign a different value than the default one.)
 
-[//]: <> (Increasing this flag will execute more sequences, until we will reach the desired amount of violations.)
+[//]: # (Increasing this flag will execute more sequences, until we will reach the desired amount of violations.)
 
-[//]: <> ()
-[//]: <> (**Example**)
+[//]: # ()
+[//]: # (**Example**)
 
-[//]: <> ()
-[//]: <> (```sh)
+[//]: # ()
+[//]: # (```sh)
 
-[//]: <> (certoraRanger ranger.conf --ranger_failure_limit N)
+[//]: # (certoraRanger ranger.conf --ranger_failure_limit N)
 
-[//]: <> (```)
+[//]: # (```)
 
 ## `Default Under-approximations`
 

From d7d4c2af99ed2033a3db614f3d28872d3db5df88 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Sun, 18 May 2025 20:05:56 +0300
Subject: [PATCH 22/32] trying one big multi-line comment

---
 docs/ranger/ranger_client.md | 33 ++++++++++++++-------------------
 1 file changed, 14 insertions(+), 19 deletions(-)

diff --git a/docs/ranger/ranger_client.md b/docs/ranger/ranger_client.md
index 98a512d53..4508123f0 100644
--- a/docs/ranger/ranger_client.md
+++ b/docs/ranger/ranger_client.md
@@ -34,35 +34,30 @@ certoraRanger ranger.conf --range K
 
 [//]: <> (&#40;--ranger_failure_limit&#41;=)
 
-[## `ranger_failure_limit`]::
-[
-    **What does it do?**]::
+[## `ranger_failure_limit`
 
-[//]: <> (Sets the minimal number of violations to be found.)
-
-[//]: <> (Once we reach this limit, no new Ranger call sequence checks will be started.)
+**What does it do?**
 
-[//]: <> (Checks already in progress will continue, thus we are expected to see at least N violations.)
+Sets the minimal number of violations to be found.
 
-[//]: # ()
-[//]: # (When not assigned, the default value is defined as 1.)
+Once we reach this limit, no new Ranger call sequence checks will be started.
 
-[//]: # ()
-[//]: # (**When to use it?**)
+Checks already in progress will continue, thus we are expected to see at least N violations.
 
-[//]: # (When you wish to assign a different value than the default one.)
+When not assigned, the default value is defined as 1.
 
-[//]: # (Increasing this flag will execute more sequences, until we will reach the desired amount of violations.)
+**When to use it?**
 
-[//]: # ()
-[//]: # (**Example**)
+When you wish to assign a different value than the default one.
 
-[//]: # ()
-[//]: # (```sh)
+Increasing this flag will execute more sequences, until we will reach the desired amount of violations.
 
-[//]: # (certoraRanger ranger.conf --ranger_failure_limit N)
+**Example**
 
-[//]: # (```)
+```sh
+certoraRanger ranger.conf --ranger_failure_limit N
+```
+]::
 
 ## `Default Under-approximations`
 

From eaed8930ee30ca8a8c9d2f6657d379b850b5362f Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Sun, 18 May 2025 20:09:00 +0300
Subject: [PATCH 23/32] spelling

---
 docs/ranger/starting_with_ranger.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/ranger/starting_with_ranger.md b/docs/ranger/starting_with_ranger.md
index ec3e16daf..53eefe3d5 100644
--- a/docs/ranger/starting_with_ranger.md
+++ b/docs/ranger/starting_with_ranger.md
@@ -8,7 +8,7 @@ Ranger uses the same installation process, configuration files, and spec files a
 
 ## 1. Install Certora Tools
 
-Ranger is part of the `certora` Python package. You can install or upgrade it using `pip`:
+Ranger is part of the `certora-cli` Python package. You can install or upgrade it using `pip`:
 
 ```bash
 pip install certora-cli
@@ -32,7 +32,7 @@ Example `ranger.conf`:
 ```
 
 ## 3. Run Ranger
-Use the certoraRanger command to launch the job:
+Use the `certoraRanger` command to launch the job:
 
 ```bash
 certoraRanger ranger.conf

From c937873bc2482cd7d70c8b35d978cb722ba5c76b Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Sun, 18 May 2025 20:10:26 +0300
Subject: [PATCH 24/32] fixing title sizes under ranger_linet.md

---
 docs/ranger/ranger_client.md | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/docs/ranger/ranger_client.md b/docs/ranger/ranger_client.md
index 4508123f0..0ea2d6ab0 100644
--- a/docs/ranger/ranger_client.md
+++ b/docs/ranger/ranger_client.md
@@ -10,10 +10,10 @@ The `certoraRanger` client submits jobs to the Certora Cloud, just like the Prov
 
 Ranger uses the same input format and job flow as `certoraRun`, allowing teams to reuse existing configuration and spec files.
 
-# Ranger-specific flags
+## Ranger-specific flags
 
 (--range)=
-## `range`
+### `range`
 
 **What does it do?**
 Sets the maximal length of function call sequences to check (0 ≤ K).
@@ -34,7 +34,7 @@ certoraRanger ranger.conf --range K
 
 [//]: <> (&#40;--ranger_failure_limit&#41;=)
 
-[## `ranger_failure_limit`
+[### `ranger_failure_limit`
 
 **What does it do?**
 
@@ -80,7 +80,7 @@ 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
+## Unsupported Prover flags
 
 
 The following `certoraRun` flags are not supported in Ranger:
@@ -102,7 +102,7 @@ The following `certoraRun` flags are not supported in Ranger:
 If any of these are used, Ranger will emit a warning, ignore the flag, and continue the job.
 
 
-# Config file compatibility
+## Config file compatibility
 
 Ranger supports the same `.conf` format as the Certora Prover.
 You can reuse your existing `.conf` files without changes.

From 48de033b944ffc890c278e48ed6d30b38229c40d Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Sun, 18 May 2025 20:12:51 +0300
Subject: [PATCH 25/32] removing code tags from title

---
 docs/ranger/ranger_client.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/ranger/ranger_client.md b/docs/ranger/ranger_client.md
index 0ea2d6ab0..142b95054 100644
--- a/docs/ranger/ranger_client.md
+++ b/docs/ranger/ranger_client.md
@@ -59,7 +59,7 @@ certoraRanger ranger.conf --ranger_failure_limit N
 ```
 ]::
 
-## `Default Under-approximations`
+## Default Under-approximations
 
 By default, `certoraRanger` enables the following Prover flags to favor usability over full soundness:
 

From 860d84e08fd41ba0baa3c9d8ab7a2c7125095c8d Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Sun, 18 May 2025 20:14:18 +0300
Subject: [PATCH 26/32] certora-cli instead of certora Python package

---
 docs/ranger/ranger_client.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/ranger/ranger_client.md b/docs/ranger/ranger_client.md
index 142b95054..44e0dda9e 100644
--- a/docs/ranger/ranger_client.md
+++ b/docs/ranger/ranger_client.md
@@ -2,11 +2,11 @@
 
 Ranger introduces a new CLI entry point: `certoraRanger`.
 
-This command is part of the certora Python package and provides a streamlined interface for bounded model checking, 
+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
+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.
 

From 22967aef16af4840ad50b74fb00970190b41185b Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Mon, 19 May 2025 12:18:41 +0300
Subject: [PATCH 27/32] Johannes' CR part 1

---
 docs/ranger/ranger_intro.md | 2 +-
 index.rst                   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
index 1b02dfb6e..e42f34144 100644
--- a/docs/ranger/ranger_intro.md
+++ b/docs/ranger/ranger_intro.md
@@ -15,7 +15,7 @@ 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**: Symbolically tests all function call sequences from the initial state up to a certain range.
+- ✅ **High coverage**: Tests all function call sequences on symbolic inputs from the initial state up to a certain range.
 
 ---
 
diff --git a/index.rst b/index.rst
index a49e03d33..94060bcf5 100644
--- a/index.rst
+++ b/index.rst
@@ -11,7 +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` -- TODO
+* :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::

From ab2f870e6dce684d9166f9822b25e9c8409791bf Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Mon, 19 May 2025 12:20:40 +0300
Subject: [PATCH 28/32] isn't -> is not

---
 docs/ranger/how_ranger_works.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/ranger/how_ranger_works.md b/docs/ranger/how_ranger_works.md
index 4c60b3d47..1bf24dd95 100644
--- a/docs/ranger/how_ranger_works.md
+++ b/docs/ranger/how_ranger_works.md
@@ -1,7 +1,7 @@
 # How Ranger Works
 
 **Ranger** is a bounded model checker. This means that, in contrast with "full"
-formal verification, its initial state isn't arbitrary, but is instead reached
+formal verification, its initial state is not arbitrary, but is instead reached
 by a sequence of legal function calls.
 
 (the-initial-state)=

From 0f5f5b483f4b952faa9f54ce7b64f6512bd3f04a Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Mon, 19 May 2025 12:22:52 +0300
Subject: [PATCH 29/32] removing mentions of requuiring invariants

---
 docs/ranger/ranger_intro.md         | 2 +-
 docs/ranger/starting_with_ranger.md | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
index e42f34144..7cbd3eb6c 100644
--- a/docs/ranger/ranger_intro.md
+++ b/docs/ranger/ranger_intro.md
@@ -1,6 +1,6 @@
 # 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 invariants.
+**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.
 
 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.
 
diff --git a/docs/ranger/starting_with_ranger.md b/docs/ranger/starting_with_ranger.md
index 53eefe3d5..cd9382406 100644
--- a/docs/ranger/starting_with_ranger.md
+++ b/docs/ranger/starting_with_ranger.md
@@ -1,6 +1,6 @@
 # Getting Started
 
-This guide will help you run your first Ranger job using a Solidity contract and a [CVL](/docs/cvl/index) [invariant](/docs/cvl/invariants).
+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.
 
@@ -19,7 +19,7 @@ For full installation instructions and troubleshooting, see the Certora Prover [
 You'll need three files:
 
 - A compiled Solidity contract (e.g. `MyContract.sol`)
-- A CVL spec file with at least one invariant (e.g. `MyContract.spec`)
+- A CVL `.spec` file
 - A configuration file (e.g. `ranger.conf`)
 
 Example `ranger.conf`:
@@ -45,7 +45,7 @@ Ranger is compute-intensive: It performs symbolic exploration of many function c
 
 1. Use {ref}`--rule` to focus on a single invariant or rule.
 
-2. Use {ref}`--split_rules` to automatically run each rule/invariant in a separate job.
+2. Use {ref}`--split_rules` to automatically run each invariant/rule in a separate job.
 ```
 
 

From 8f4a1caed205981b69d4b4954eca4aedff1972a8 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Mon, 19 May 2025 17:42:57 +0300
Subject: [PATCH 30/32] removing ranger failure limit

---
 docs/ranger/ranger_client.md | 26 --------------------------
 docs/ranger/ranger_intro.md  |  2 +-
 2 files changed, 1 insertion(+), 27 deletions(-)

diff --git a/docs/ranger/ranger_client.md b/docs/ranger/ranger_client.md
index 44e0dda9e..f1f9823e7 100644
--- a/docs/ranger/ranger_client.md
+++ b/docs/ranger/ranger_client.md
@@ -32,32 +32,6 @@ Increasing this flag will execute longer sequences, or decreasing when you wish
 certoraRanger ranger.conf --range K
 ```
 
-[//]: <> (&#40;--ranger_failure_limit&#41;=)
-
-[### `ranger_failure_limit`
-
-**What does it do?**
-
-Sets the minimal number of violations to be found.
-
-Once we reach this limit, no new Ranger call sequence checks will be started.
-
-Checks already in progress will continue, thus we are expected to see at least N violations.
-
-When not assigned, the default value is defined as 1.
-
-**When to use it?**
-
-When you wish to assign a different value than the default one.
-
-Increasing this flag will execute more sequences, until we will reach the desired amount of violations.
-
-**Example**
-
-```sh
-certoraRanger ranger.conf --ranger_failure_limit N
-```
-]::
 
 ## Default Under-approximations
 
diff --git a/docs/ranger/ranger_intro.md b/docs/ranger/ranger_intro.md
index 7cbd3eb6c..bc2f8fdc7 100644
--- a/docs/ranger/ranger_intro.md
+++ b/docs/ranger/ranger_intro.md
@@ -1,6 +1,6 @@
 # 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.
+**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.
 

From 1a388e93fb441358497531055c1ccfc97303323c Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 27 May 2025 13:16:13 +0300
Subject: [PATCH 31/32] added note for no Ranger support for multi_example to
 test how it looks

---
 docs/prover/cli/options.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md
index 90da46832..8b74f0349 100644
--- a/docs/prover/cli/options.md
+++ b/docs/prover/cli/options.md
@@ -534,6 +534,10 @@ Use this flag when debugging complex rules where multiple, distinct scenarios mi
 certoraRun MyContract.sol --verify MyContract:MyContract.spec --multi_example
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 
 (--project_sanity)=
 ## `project_sanity`

From 5c0cf4bbf7882a263d7cfaf595b6196e14471710 Mon Sep 17 00:00:00 2001
From: urikirsh <uri@certora.com>
Date: Tue, 27 May 2025 17:07:29 +0300
Subject: [PATCH 32/32] added notes on all flags Ranger doesn't support

---
 docs/prover/cli/options.md | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md
index 8b74f0349..a15065c3f 100644
--- a/docs/prover/cli/options.md
+++ b/docs/prover/cli/options.md
@@ -397,6 +397,10 @@ We suggest using this option when you have finished (a subset of) your rules and
 certoraRun Bank.sol --verify Bank:Bank.spec --coverage_info advanced
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 (--foundry)=
 ## `foundry`
 
@@ -421,6 +425,10 @@ When we want to run all Foundry fuzz tests in the project with the Prover.
 certoraRun --foundry
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 (--independent_satisfy)=
 ## `independent_satisfy`
 
@@ -482,6 +490,10 @@ When you have a rule with multiple satisfy statements, and you would like to dem
 certoraRun Bank.sol --verify Bank:Bank.spec --independent_satisfy
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 (--multi_assert_check)=
 ## `multi_assert_check`
 
@@ -519,6 +531,10 @@ When you have a rule with multiple assertions:
 certoraRun Bank.sol --verify Bank:Bank.spec --multi_assert_check
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 (--multi_example)=
 ## `multi_example`
 Show several counterexamples for failed assert statements and several witnesses for verified satisfy statements.
@@ -566,6 +582,10 @@ may be hot spots for summarization etc.
 certoraRun --project_sanity
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 (--rule_sanity)=
 ## `rule_sanity`
 
@@ -588,6 +608,10 @@ useful check if you notice rules passing surprisingly quickly or easily.
 certoraRun Bank.sol --verify Bank:Bank.spec --rule_sanity basic
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 (--short_output)=
 ## `short_output`
 
@@ -874,6 +898,10 @@ certoraRun Bank.sol --verify Bank:Bank.spec --vyper vyper0.3.10
 certoraRun Bank.sol --verify Bank:Bank.spec --vyper /usr/local/bin/vyper0.3.10
 ```
 
+```{note}
+Ranger does not support this option currently.
+```
+
 
 Options regarding source code loops
 ===================================