added Ranger repo

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)

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
+```
+

docs/ranger/ranger_client.md

@@ -0,0 +1,9 @@
+# The Ranger Client
+
+# Usage: certoraRanger
+
+# Ranger-specific flags
+
+# Unsupported Prover flags
+
+# Config file compatibility

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 invariants.
+
+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**: 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 Solidity contracts.

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) [invariant](/docs/cvl/invariants).
+
+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` 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 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 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. 
+You can explore the results in the web-based Ranger Report by following the link. 

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

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