diff --git a/.github/workflows/gambit.yml b/.github/workflows/gambit.yml
index 55ac74a..2aea6b5 100644
--- a/.github/workflows/gambit.yml
+++ b/.github/workflows/gambit.yml
@@ -130,4 +130,24 @@ jobs:
           else
             gh release upload $TAG gambit-linux-$TAG/gambit-linux-$TAG
             gh release upload $TAG gambit-macos-$TAG/gambit-macos-$TAG
-          fi
\ No newline at end of file
+          fi
+
+  check-docs:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v2
+      
+      - name: PIP install
+        run: pip install ansi
+
+      - name: Check that RTD Docs are Up To Date
+        run: python3 scripts/check_rtd_docs_up_to_date.py
+      
+      - name: Check Exit Code
+        run: |
+          if [[ $? -ne 0 ]]; then
+            echo "Error: documentation is not synced"
+            exit 1
+          fi
+
diff --git a/.gitignore b/.gitignore
index 0bfcc3a..5463df2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,3 +18,6 @@ Cargo.lock
 
 # vscode
 .vscode/
+
+# python
+**/__pycache__/
diff --git a/README.md b/README.md
index be97d66..7f48ed3 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,151 @@
 # Gambit: Mutant Generation for Solidity
 
+<!-- SUPPRESS --> 
+
+<!-- NOTE: IF YOU EDIT THIS FILE!!!
+
+  # Keep In Sync With ReadTheDocs
+
+
+  This documentation appears in two locations: 
+  - here (the Gambit repo), and
+  - https://github.com/Certora/Documentation/docs/gambit/gambit.md (used to
+    generate the ReadTheDocs documentation at
+    https://docs.certora.com/en/latest/docs/gambit/gambit.html)
+
+  Unfortunately we cannot simply copy this file the Certora Documentation repo:
+  the formats are slightly different (I describe how below). To solve this we
+  _generate_ the RTD docs from this file.
+
+
+  ## Steps to Sync With RTD
+  
+
+  1. Run `python scripts/generate_rtd_markdown.py README.md`
+
+     This will create `./gambit.md`
+
+  2. Move this generated `gambit.md` to location `docs/gambit/gambit.md` in the
+     Certora Documentation repository (https://github.com/Certora/Documentation)
+  
+  3. Create a new PR in https://github.com/Certora/Documentation with the new
+     Gambit docs
+  
+  4. Create a new PR in Gambit repo. Note that CI will check that the RTD
+     documentation is up to date (see section "Checking RTDs are Up To Date"
+     below). If this fails, CI will also fail, and you will be unable to merge
+     into `master` until changes to the Gambit README are propagated to the RTD
+     docs.
+  
+  5. Once the PR from (3) is merged and CI is passing in this repository, merge
+     the PR from (4) into master.
+
+
+  ## Checking RTDs are Up To Date
+
+  To check that the RTD Gambit docs are in sync with Gambit's README, run
+
+  ```
+  python scripts/check_rtd_docs_upt_to_date.py
+  ```
+
+  This will translate the Gambit README to a string, pull the RTD docs from the
+  Github Repo, and do a equality check on the two strings.
+  
+  You can optionally specify a `--branch` argument to choose another branch in
+  the Certora Documentation repo (default is `'master'`)
+
+
+  ## Markdown Format Differences
+
+
+  1. Internal Links:
+
+     ```markdown
+     [Link Title](#link-title) becomes
+     ```
+     
+     ```markdown
+     {ref}`link-title`
+     ```
+
+     Note that `link-title` needs to target an _anchor_, which we describe in
+     item 2.
+
+  2. Anchors:
+     
+     To link to internal locations the RTD documentation expects an _anchor_:
+
+     ```markdown
+     (heading-title)=
+     ## Heading Title
+     ```
+
+     Then the 
+
+     ```markdown
+     {ref}`heading-title`
+     ```
+     
+    internal link will point to the `## Heading Title` section.
+
+    Raw markdown doesn't support this syntax, so we use an HTML comment
+    containing the contents "ANCHOR (content-title)=":
+
+    ```markdown
+    <!-- ANCHOR (heading-title)=   -- >
+    ```
+
+    Note that I intentionally added a space to the close comment tag because
+    that would terminate this entire comment :)
+  
+  3. Notes:
+
+     RTD uses admonition-style notes:
+
+     ```{note}
+     Some note goes here
+     ```
+
+     We don't have access to this here, so I've implemented a simple system,
+     where all notes begin with a line containing:
+
+     ```markdown
+     _**Note:**
+     ```
+
+     and end with a line ending with `_`:
+
+     ```markdown
+     and this is the last line of my note._
+     ```
+
+     So, a full note would look like:
+
+     ```markdown
+     _**Note:**
+     This is a note. The opening tag is on its own line, and the closing italic
+     is at the end of the final line. This is to make parsing easy, and to keep
+     diffs minimal!_
+     ```
+     
+-->
+
+<!-- END SUPPRESS -->
+
+<!-- EMIT:
+<\!--
+  WARNING: AUTO_GENERATED DOCUMENTATION
+
+  The following documentation is automatlically generated from the Gambit
+  README.md located at https://github.com/Certora/Gambit/README.md. Please view
+  this document for instructions on producing this file.
+--\>
+-->
+
 Gambit is a state-of-the-art mutation system for Solidity.
 By applying predefined syntax transformations called _mutation operators_ (for
-  example, `a + b` -> `a - b`) to a Solidity program's source code, Gambit
+  example, convert `a + b` to `a - b`) to a Solidity program's source code, Gambit
   generates variants of the program called _mutants_.
 Mutants can be used to evaluate test suites or specs used for formal
   verification: each mutant represents a potential bug in the program, and
@@ -12,8 +155,8 @@ Mutants can be used to evaluate test suites or specs used for formal
 
 1. Gambit is written in Rust. You'll need to [install Rust and
    Cargo](https://www.rust-lang.org/tools/install) to build Gambit.
-2. Gambit uses the solc, the Solidity compiler, to generate mutants. You'll need
-   to have solc binary that is compatable with the project you are mutating (see
+2. Gambit uses `solc`, the Solidity compiler, to generate mutants. You'll need
+   to have a `solc` binary that is compatible with the project you are mutating (see
    the `--solc` option in `gambit mutate --help`)
 
 ## Installation
@@ -21,7 +164,7 @@ Mutants can be used to evaluate test suites or specs used for formal
 You can download prebuilt Gambit binaries for Mac and Linux from our
 [releases](https://github.com/Certora/gambit/releases) page.
 
-To build Gambit from source, clone this repository and run
+To build Gambit from source, clone [the Gambit repository](https://github.com/Certora/gambit) and run
 
 ```
 cargo install --path .
@@ -41,13 +184,14 @@ Gambit has two main commands: `mutate` and `summary`. `gambit mutate` is
 responsible for mutating code, and `gambit summary` is a convenience command for
 summarizing generated mutants in a human-readable way.
 
-Running `gambit mutate` will invoke the solidity compiler via `solc`, so make
+Running `gambit mutate` will invoke `solc`, so make
 sure it is visible on your `PATH`. Alternatively, you can specify where Gambit can
 find the Solidity compiler with the option `--solc path/to/solc`, or specify a
-version of solc (e.g., solc8.12) with the option `--solc solc8.12`.
+`solc` binary (e.g., `solc8.12`) with the option `--solc solc8.12`.
 
-_**Note:** All tests (`cargo test`) are currently run using solc8.13. Your tests may fail if your `solc` points at
-  a different version of the compiler._
+_**Note:**
+All tests (`cargo test`) are currently run using `solc8.13`. Your tests may fail
+  if your `solc` points at a different version of the compiler._
 
 ### Running  `gambit mutate` 
 
@@ -65,12 +209,13 @@ instead:
 
 ```bash
 gambit mutate --json gambit_conf.json
-``` 
+```
 
 Run `gambit --help` for more information.
 
-_**Note:** all relative paths specified in a JSON configuration file are interpreted
-to be relative to the config file's parent directory._
+_**Note:**
+All relative paths specified in a JSON configuration file are interpreted
+to be relative to the configuration file's parent directory._
 
 In the following section we provide examples of how to run Gambit using both
 `--filename` and `--json`. We provide more complete documentation in the
@@ -78,27 +223,29 @@ In the following section we provide examples of how to run Gambit using both
 
 ## Examples
 
-Unless otherwise noted, examples use code from `benchmarks/` and are run from
-the root of this repository.
+Unless otherwise noted, examples use code from [benchmarks/](https://github.com/Certora/gambit/tree/master/benchmarks)
+and are run from the root of the [Gambit repository](https://github.com/Certora/gambit).
 
-### Example 1: Mutating a Single File
+### Example 1: Mutating a single file
 
 To mutate a single file, use the `--filename` option (or `-f`), followed by the
 file to mutate.
 
 ```bash
-gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol                          
+gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol
 ```
-<!-- Code output: using `pre` to avoid the Copy To Clipboard feature -->
+
+This will generate:
 <pre>
 Generated 34 mutants in 0.69 seconds
 </pre>
 
-_**Note:** The mutated file must located within your current working directory or
+_**Note:**
+The mutated file must be located within your current working directory or
 one of its subdirectories. If you want to mutate code in an arbitrary directory,
 use the `--sourceroot` option._
 
-### Example 2: Mutating and Downsampling
+### Example 2: Mutating and downsampling
 
 The above command produced 34 mutants which may be more than you need. Gambit
 provides a way to randomly downsample the number of mutants with the
@@ -107,19 +254,23 @@ provides a way to randomly downsample the number of mutants with the
 ```bash
 gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol -n 3
 ```
+
+which will generate:
 <pre>
 Generated 3 mutants in 0.15 seconds
 </pre>
 
-### Example 3: Viewing Gambit Results
-_**Note:** this example assumes you've just completed Example 2_
+### Example 3: Viewing Gambit results
+_**Note:**
+This example assumes you've just completed Example 2._
 
 Gambit outputs all of its results in `gambit_out`:
 
 ```bash
 tree -L 2 gambit_out
 ```
-<!-- Code output: using `pre` to avoid the Copy To Clipboard feature -->
+
+This produces:
 <pre>
 gambit_out
 ├── gambit_results.json
@@ -145,45 +296,45 @@ For instance, `gambit summary --mids 3 4 5`  will only print info for mutant ids
 3 through 5.
 
 
-### Example 4: Specifying solc Pass-through Arguments
-Solc may need some extra information to successfully run on a file or a project.
-Gambit enables this with _pass-through arguments_ that, as the name suggests,
-are passed directly through to the solc compiler.
+### Example 4: Specifying `solc` pass-through arguments
+The Solidity compiler (`solc`) may need some extra information to successfully
+run on a file or a project.  Gambit enables this with _pass-through arguments_
+that, as the name suggests, are passed directly through to the `solc` compiler.
 
 For projects that have complex dependencies and imports, you may need to:
-* **Specify base-paths**: To specify the Solidity [--base-path][basepath]
+* **Specify base paths**: To specify the Solidity [`--base-path`][basepath]
   argument, use `--solc_base_path`:
 
   ```bash
-  gambit mutate --filename path/to/file.sol --solc_base_path base/path/dir/.
+  gambit mutate --filename path/to/file.sol --solc_base_path base/path/dir
   ```
 
 * **Specify remappings:** To indicate where Solidity should find libraries,
-  use solc's [import remapping][remapping] syntax with `--solc_remappings`:
+  use `solc`'s [import remapping][remapping] syntax with `--solc_remappings`:
 
   ```bash
   gambit mutate --filename path/to/file.sol \
     --solc_remappings @openzeppelin=node_modules/@openzeppelin @foo=node_modules/@foo
   ```
 
-* **Specify allow-paths:** To include additional allowed paths via solc's
-  [--allow-paths][allowed] argument, use `--solc_allow_paths`:
+* **Specify allow paths:** To include additional allowed paths via `solc`'s
+  [`--allow-paths`][allowed] argument, use `--solc_allow_paths`:
 
   ```bash
   gambit mutate --filename path/to/file.sol \
-  --solc_allow_paths PATH1 --solc_allow_paths PATH2 ...
+    --solc_allow_paths PATH1 --solc_allow_paths PATH2 ...
   ```
 
 * **Specify include-path:** To make an additional source directory available
-  to the default import callback via solc's [--include-path][included] argument, use
-  `--solc_include_path`:
+  to the default import callback via `solc`'s [--include-path][included] argument,
+  use `--solc_include_path`:
 
   ```bash
   gambit mutate --filename path/to/file.sol --solc_include_path PATH
   ```
 
-* **Use optimization:** To run the solidity compiler with optimizations (solc's
-  `--optimize` argument), use `--solc_optimize`:
+* **Use optimization:** To run the Solidity compiler with optimizations
+  (`solc`'s `--optimize` argument), use `--solc_optimize`:
 
   ```bash
   gambit mutate --filename path/to/file.sol --solc_optimize
@@ -193,22 +344,25 @@ For projects that have complex dependencies and imports, you may need to:
 [basepath]: https://docs.soliditylang.org/en/v0.8.17/path-resolution.html#base-path-and-include-paths
 [allowed]: https://docs.soliditylang.org/en/v0.8.17/path-resolution.html#allowed-paths
 
-### Example 5: The `--sourceroot`  Option
 
-Gambit needs to track the location of sourcefiles that it mutates within a
+<!-- ANCHOR: (gambit-config)= -->
+### Example 5: The `--sourceroot`  option
+
+Gambit needs to track the location of source files that it mutates within a
 project: for instance, imagine there are files `foo/Foo.sol` and `bar/Foo.sol`.
 These are separate files, and their path prefixes are needed to determine this.
-Gambit addresses this with the `--sourceroot` option: the sourceroot indicates
+Gambit addresses this with the `--sourceroot` option: the source root indicates
 to Gambit the root of the files that are being mutated, and all source file
-paths (both original and mutated) are reported relative to this sourceroot.
+paths (both original and mutated) are reported relative to this source root.
 
-_If Gambit encounters a source file that does not belong to the sourceroot it
+_**Note:**
+If Gambit encounters a source file that does not belong to the source root it
 will print an error message and exit._
 
 _When running `gambit mutate` with the `--filename` option,
-sourceroot defaults to the current working directory.
+source root defaults to the current working directory.
 When running `gambit mutate` with the `--json` option,
-sourceroot defaults to the directory containing the configuration JSON._
+source root defaults to the directory containing the configuration JSON._
 
 Here are some examples of using the `--sourceroot` option.
 
@@ -216,35 +370,34 @@ Here are some examples of using the `--sourceroot` option.
 
    ```bash
    gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol -n 1
-   cat gambit_out/mutants.log 
+   cat gambit_out/mutants.log
    find gambit_out/mutants -name "*.sol"
    ```
 
    This should output the following:
-   <!-- Code output: using `pre` to avoid the Copy To Clipboard feature -->
+
    <pre>
    Generated 1 mutants in 0.13 seconds
    1,BinaryOpMutation,benchmarks/BinaryOpMutation/BinaryOpMutation.sol,23:10, % ,*
    gambit_out/mutants/1/benchmarks/BinaryOpMutation/BinaryOpMutation.sol
    </pre>
 
-   The first command generates a single mutant, and its sourcepath is relative to `.`,
-   the default sourceroot. We can see that the reported paths in `mutants.log`,
+   The first command generates a single mutant, and its source path is relative to `.`,
+   the default source root. We can see that the reported paths in `mutants.log`,
    and the mutant file path in `gambit_out/mutants/1`, are the relative to this
-   sourceroot: `benchmarks/BinaryOpMutation/BinaryOpMutation.sol`
-  
+   source root: `benchmarks/BinaryOpMutation/BinaryOpMutation.sol`
+
 2. Suppose we want our paths to be reported relative to
    `benchmarks/BinaryOpMutation`. We can run
 
    ```bash
    gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol -n 1 --sourceroot benchmarks/BinaryOpMutation
-   cat gambit_out/mutants.log 
+   cat gambit_out/mutants.log
    find gambit_out/mutants -name "*.sol"
    ```
 
    which will output:
 
-   <!-- Code output: using `pre` to avoid the Copy To Clipboard feature -->
    <pre>
    Generated 1 mutants in 0.13 seconds
    1,BinaryOpMutation,BinaryOpMutation.sol,23:10, % ,*
@@ -252,25 +405,25 @@ Here are some examples of using the `--sourceroot` option.
    </pre>
 
    The reported filenames, and the offset path inside of
-   `gambit_out/mutants/1/`, are now relative to the sourceroot that we
+   `gambit_out/mutants/1/`, are now relative to the source root that we
    specified.
 
-3. Finally, suppose we use a sourceroot that doesn't contain the source file:
+3. Finally, suppose we use a source root that doesn't contain the source file:
 
    ```bash
    gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol -n 1 --sourceroot scripts
    ```
+
    This will try to find the specified file inside of `scripts`, and since it
    doesn't exist Gambit reports the error:
 
-   <!-- Code output: using `pre` to avoid the Copy To Clipboard feature -->
    <pre>
-   [ERROR gambit] [!!] Illegal Configuration: Resolved filename `/Users/USER/Gambit/benchmarks/BinaryOpMutation/BinaryOpMutation.sol` is not prefixed by the derived sourceroot /Users/USER/Gambit/scripts
+   [ERROR gambit] [!!] Illegal Configuration: Resolved filename `/Users/USER/Gambit/benchmarks/BinaryOpMutation/BinaryOpMutation.sol` is not prefixed by the derived source root /Users/USER/Gambit/scripts
    </pre>
 
    Gambit prints an error and exits.
 
-### Example 6: Running Gambit Through a Configuration File
+### Example 6: Running Gambit using a configuration file
 
 To run gambit with a configuration file, use the `--json` argument:
 ```bash
@@ -292,19 +445,21 @@ The configuration file is a JSON file containing the command line arguments for
 
 In addition to specifying the command line arguments, you can list the specific
 mutants that you want to apply, the specific functions you wish to mutate, and
-more.  See the [`benchmark/config-jsons` directory][config-examples] for
+more. See the [`benchmark/config-jsons` directory][config-examples] for
 examples.
 
-_**Note:** Any paths provided by the configuration file are resolved relative to
-the configuration file's parent directory._
+_**Note:**
+Any paths provided by the configuration file are resolved relative to the
+configuration file's parent directory._
 
+<!-- ANCHOR: (configuration-files)= -->
 ## Configuration Files
 Configuration files allow you to save complex configurations and perform
 multiple mutations at once. Gambit uses a simple JSON object format to store
 mutation options, where each `--option VALUE` specified on the CLI is
 represented as a `"option": VALUE` key/value pair in the JSON object.  Boolean
 `--flag`s are enabled by storing them as true: `"flag": true`. For instance,
-`--no_overwrite` would be written as `"no_overwrite": true"`.
+`--no_overwrite` would be written as `"no_overwrite": true`.
 
 As an example, consider the command from Example 1:
 
@@ -359,6 +514,7 @@ directory of the configuration file_. So if the JSON file listed above was moved
 to the `benchmarks/` directory the `"filename"` would need to be updated to
 `BinaryOpMutation/BinaryOpMutation.sol`.
 
+<!-- ANCHOR: (results-directory)= -->
 ## Results Directory
 
 `gambit mutate` produces all results in an output directory (default:
@@ -368,7 +524,9 @@ to the `benchmarks/` directory the `"filename"` would need to be updated to
 gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol -n 5
 tree gambit_out -L 2
 ```
-<!-- Code output: using `pre` to avoid the Copy To Clipboard feature -->
+
+which produces:
+
 <pre>
 Generated 5 mutants in 0.15 seconds
 
@@ -393,6 +551,7 @@ This has the following structure:
 + `mutants.log`: a log file with all mutant information. This is similar to
   `results.json` but in a different format and with different information
 
+<!-- ANCHOR: (cli-options)= -->
 ## CLI Options
 
  `gambit mutate` supports the following options; for a comprehensive list, run
@@ -404,21 +563,23 @@ This has the following structure:
 | `-o`, `--outdir`      | specify Gambit's output directory (defaults to `gambit_out`)                                                                 |
 | `--no_overwrite`      | do not overwrite an output directory; if the output directory exists, print an error and exit                                |
 | `-n`, `--num_mutants` | randomly downsample to a given number of mutants.                                                                            |
-| `-s`, `--seed`        | specify a random seed. For reproducability, Gambit defaults to using the seed `0`. To randomize the seed use `--random-seed` |
-| `--random_seed`       | use a random seed. Note this overrides any value specified by `--seed`                                                       |
+| `-s`, `--seed`        | specify a random seed. For reproducibility, Gambit defaults to using the seed `0`. To randomize the seed use `--random_seed` |
+| `--random_seed`       | use a random seed. Note that this overrides any value specified by `--seed`                                                  |
 | `--contract`          | specify a specific contract name to mutate; by default mutate all contracts                                                  |
 | `--functions`         | specify one or more functions to mutate; by default mutate all functions                                                     |
 | `--mutations`         | specify one or more mutation operators to use; only generates mutants that are created using the specified operators         |
+| `--skip_validate`     | only generate mutants without validating them by compilation                                                                 |
 
 Gambit also supports _pass-through arguments_, which are arguments that are
-passed directly to solc. All pass-through arguments are prefixed with `solc-`:
+passed directly to the Solidity compiler. All pass-through arguments are
+prefixed with `solc_`:
 
-| Option                | Description                                                                   |
-| :-------------------- | :---------------------------------------------------------------------------- |
-| `--solc_base_path`    | passes a value to solc's `--base-path` argument                               |
-| `--solc_allow_paths`  | passes a value to solc's `--allow-paths` argument                             |
-| `--solc_include_path` | passes a value to solc's `--include-path` argument                           |
-| `--solc_remappings`    | passes a value to directly to solc: this should be of the form `prefix=path`. |
+| Option                | Description                                                                     |
+| :-------------------- | :------------------------------------------------------------------------------ |
+| `--solc_allow_paths`  | passes a value to `solc`'s `--allow-paths` argument                             |
+| `--solc_base_path`    | passes a value to `solc`'s `--base-path` argument                               |
+| `--solc_include_path` | passes a value to `solc`'s `--include-path` argument                            |
+| `--solc_remappings`   | passes a value to directly to `solc`: this should be of the form `prefix=path`. |
 
 ## Mutation Operators
 Gambit implements the following mutation operators
@@ -428,8 +589,8 @@ Gambit implements the following mutation operators
 | **binary-op-mutation**               | Replace a binary operator with another                   | `a+b` -> `a-b`                                 |
 | **unary-operator-mutation**          | Replace a unary operator with another                    | `~a` -> `-a`                                   |
 | **require-mutation**                 | Alter the condition of a `require` statement             | `require(some_condition())` -> `require(true)` |
-| **assignment-mutation**              | Replaces the rhs of a mutation                           | `x = foo();` -> `x = -1;`                      |
-| **delete-expression-mutation**       | Replace an expression statement with `assert(true)`      | `foo();` -> `assert(true);`                    |
+| **assignment-mutation**              | Replaces the right hand side of an assignment            | `x = foo();` -> `x = -1;`                      |
+| **delete-expression-mutation**       | Replaces an expression with a no-op (`assert(true)`)     | `foo();` -> `assert(true);`                    |
 | **if-cond-mutation**                 | Mutate the conditional of an `if` statement              | `if (C) {...}` -> `if (true) {...}`            |
 | **swap-arguments-operator-mutation** | Swap the order of non-commutative operators              | `a - b` -> `b - a`                             |
 | **elim-delegate-mutation**           | Change a `delegatecall()` to a `call()`                  | `_c.delegatecall(...)` -> `_c.call(...)`       |
@@ -438,6 +599,7 @@ Gambit implements the following mutation operators
 
 For more details on each mutation type, refer to the [full documentation](https://docs.certora.com/en/latest/docs/gambit/gambit.html#mutation-types).
 
+<!-- SUPPRESS -->
 ## Contact
 If you have ideas for interesting mutations or other features,
 we encourage you to make a PR or [email](mailto:chandra@certora.com) us.
@@ -448,6 +610,7 @@ We thank
 [Vishal Canumalla](https://homes.cs.washington.edu/~vishalc/)
 for their excellent contributions to an earlier prototype of Gambit.
 
+<!-- END SUPPRESS -->
 
 [config-examples]: https://github.com/Certora/gambit/blob/master/benchmarks/config-jsons/
 [test6]: https://github.com/Certora/gambit/blob/master/benchmarks/config-jsons/test6.json
diff --git a/scripts/check_rtd_docs_up_to_date.py b/scripts/check_rtd_docs_up_to_date.py
new file mode 100644
index 0000000..1ea5545
--- /dev/null
+++ b/scripts/check_rtd_docs_up_to_date.py
@@ -0,0 +1,90 @@
+#!/usr/bin/env python3
+
+from argparse import ArgumentParser
+from urllib.request import urlopen
+import difflib
+import os
+import sys
+import re
+from generate_rtd_markdown import translate_readme_to_rtd
+
+OUR_README_PATH = os.path.join(os.path.dirname(__file__), "..", "README.md")
+
+THEIR_README_URL_NO_BRANCH = (
+    "https://raw.githubusercontent.com/Certora/Documentation/{}/docs/gambit/gambit.md"
+)
+
+
+def main():
+    parser = ArgumentParser()
+    parser.add_argument(
+        "--branch", default="master", help="Branch to check README from"
+    )
+    parser.add_argument(
+        "--no_colors", action="store_true", help="Do not use ansi color on outputs"
+    )
+    args = parser.parse_args()
+
+    exit_code = check_rtd_docs_up_to_date(branch=args.branch, colors=not args.no_colors)
+
+    sys.exit(exit_code)
+
+
+def print_unified_diff(diff, colors=True):
+    color_fn = {}
+    if colors:
+        try:
+            from ansi.color import fg
+
+            color_fn = {"+": fg.green, "-": fg.red, "@": fg.blue}
+        except ImportError:
+            colors = False
+
+    for line in diff:
+        l: str = line
+        if colors:
+            if l.startswith("+++") or l.startswith("---"):
+                l = fg.yellow(l)
+            else:
+                f = color_fn.get(l[0], str)
+                l = f(l)
+        print(l, end="")
+
+
+def check_rtd_docs_up_to_date(branch="master", colors=True) -> int:
+    url = THEIR_README_URL_NO_BRANCH.format(branch)
+
+    with open(OUR_README_PATH) as f:
+        our_readme_contents = f.read()
+
+    try:
+        their_readme_contents = urlopen(url).read().decode("utf-8")
+
+    except RuntimeError as e:
+        print(f"Could not read `gambit.md` from {url}")
+        print(f"Error: {e}")
+        return 127
+
+    print()
+    our_translated_readme_contents = translate_readme_to_rtd(OUR_README_PATH)
+    if our_translated_readme_contents == their_readme_contents:
+        print(f"Docs are in sync!")
+        return 0
+    else:
+        print(f"Docs are out of sync!")
+        print()
+        print("Unified diff: Local vs Remote")
+        print("=============================")
+        print()
+        print_unified_diff(
+            difflib.unified_diff(
+                our_translated_readme_contents.splitlines(keepends=True),
+                their_readme_contents.splitlines(keepends=True),
+            ),
+            colors=colors,
+        )
+        return 1
+
+
+if __name__ == "__main__":
+    main()
diff --git a/scripts/generate_rtd_markdown.py b/scripts/generate_rtd_markdown.py
new file mode 100644
index 0000000..b52d864
--- /dev/null
+++ b/scripts/generate_rtd_markdown.py
@@ -0,0 +1,208 @@
+#!/usr/bin/env python3
+
+"""
+Generate RTD version of the Gambit README
+"""
+
+from argparse import ArgumentParser
+from typing import Optional
+import re
+
+
+def line_is_anchor(line: str) -> bool:
+    return line.startswith("<!-- ANCHOR:")
+
+
+def replace_internal_references(line):
+    """
+    Internal references look like '[Readable Text](#some-header-title)'. We
+    want to repalce this with '{ref}`some-header-title`
+
+    Examples
+    ========
+
+    >>> replace_internal_references("[Test1](#test1")
+    '[Test1](#test1'
+    >>> replace_internal_references("[Test1](#test1)")
+    '{ref}`test1`'
+    >>> replace_internal_references("This is [Test2](#test-2) with [Multiple Matches](#multiple-matches)")
+    'This is {ref}`test-2` with {ref}`multiple-matches`'
+    """
+    pat = r"\[([^\]]+)\]\(#([^\)]+)\)"
+    while True:
+        m = re.search(pat, line)
+        if m is None:
+            return line
+        line = line[: m.start()] + "{ref}" + f"`{m.group(2)}`" + line[m.end() :]
+
+
+def get_anchor(line: str) -> Optional[str]:
+    """
+    Attempt to get an anchor from a comment
+
+    Examples
+    ========
+
+    >>> get_anchor("<!-- ANCHOR: (test-anchor)= -->")
+    '(test-anchor)='
+    >>> get_anchor("# README")
+    """
+
+    if not line.startswith("<!-- ANCHOR: "):
+        return None
+    line = line.strip()
+    anchor = line[len("<!-- ANCHOR:") : -len("-->")].strip()
+    return anchor
+
+
+def is_suppress(line: str) -> bool:
+    return "<!--SUPPRESS-->" == line.upper().replace(" ", "").strip()
+
+
+def is_end_suppress(line: str) -> bool:
+    return "<!--ENDSUPPRESS-->" == line.upper().replace(" ", "").strip()
+
+
+def is_emit(line: str) -> bool:
+    return "<!--EMIT:" == line.upper().replace(" ", "").strip()
+
+
+def is_escaped_open_comment(line: str) -> bool:
+    return line.strip() == r"<\!--"
+
+
+def is_note_end(line: str) -> bool:
+    """
+    A note ends when a line is ended by an underscore. We double check to ensure
+    that the line doesn't end with two underscores.
+    """
+    l = line.strip()
+    if l.endswith("_"):
+        return len(l) == 1 or l[-2] != "_"
+
+
+def is_tag(tag: str, line: str):
+    """
+    Check if a line consists
+    """
+    return line.strip() in (f"<{tag}>", f"</{tag}>")
+
+
+def is_warning_end(line: str) -> bool:
+    """
+    A warning ends when a line is ended by an underscore. We double check to
+    ensure that the line doesn't end with two underscores.
+    """
+    return is_note_end(line)
+
+
+def is_escaped_closed_comment(line: str) -> bool:
+    return line.strip() == r"--\>"
+
+
+def translate_readme_to_rtd(readme_file_path: str) -> str:
+    with open(readme_file_path) as f:
+        original = f.read()
+        lines = original.split("\n")
+    lines2 = []
+
+    suppress_start = -1  # Track if we are suppressing
+    admonition_start = -1
+    admonition_start = -1  # Track if we've started a note
+    emit_start = -1
+    for i, line in enumerate(lines):
+        # First, check if we are suppressing
+        if suppress_start > -1:
+            if is_end_suppress(line):
+                suppress_start = -1
+            continue
+
+        anchor = get_anchor(line)
+        if anchor is not None:
+            lines2.append(anchor)
+        elif "_**note:**" == line.strip().lower():
+            if admonition_start > -1:
+                raise RuntimeError(
+                    f"Already in note from line {admonition_start + 1}, cannot start new note on line {i+1}"
+                )
+            admonition_start = i
+            lines2.append("```{note}")
+        elif "_**note:**" in line.strip().lower():
+            raise RuntimeError(
+                f"Illegal note start on line {i+1}: new note tags '_**Note:**' and their closing '_' must be on their own lines"
+            )
+
+        elif admonition_start > -1 and is_note_end(line):
+            admonition_start = -1
+            lines2.append(line.rstrip().rstrip("_"))
+            lines2.append("```")
+
+        elif "_**warning:**" == line.strip().lower():
+            if admonition_start > -1:
+                raise RuntimeError(
+                    f"Already in warning from line {admonition_start + 1}, cannot start new warning on line {i+1}"
+                )
+            admonition_start = i
+            lines2.append("```{warning}")
+        elif "_**warning:**" in line.strip().lower():
+            raise RuntimeError(
+                f"Illegal warning start on line {i+1}: new warning tags '_**Warning:**' and their closing '_' must be on their own lines"
+            )
+
+        elif admonition_start > -1 and is_warning_end(line):
+            admonition_start = -1
+            lines2.append(line.rstrip().rstrip("_"))
+            lines2.append("```")
+
+        elif is_emit(line):
+            if emit_start > 0:
+                raise RuntimeError(
+                    f"Cannot start a new emit on line {i+1}: already in an emit started at line {emit_start+1}"
+                )
+            emit_start = i
+
+        elif is_tag("pre", line):
+            num_spaces = len(line) - len(line.lstrip(' '))
+            lines2.append(f"{num_spaces * ' '}```")
+
+        elif line.strip() == "-->" and emit_start > -1:
+            emit_start = -1
+
+        # Handle escaped comments from inside of an emit
+        elif is_escaped_open_comment(line) and emit_start > -1:
+            lines2.append("<!--")
+        elif is_escaped_closed_comment(line) and emit_start > -1:
+            lines2.append("-->")
+
+        elif is_suppress(line):
+            if suppress_start > 0:
+                raise RuntimeError(
+                    f"Cannot start a new suppression on line {i+1}: already in a suppression tag started at line {suppress_start+1}"
+                )
+            suppress_start = i
+        elif is_end_suppress(line):
+            raise RuntimeError(
+                f"Illegal end suppress on line {i+1}: not currently in a suppress"
+            )
+        else:
+            # replace internal links
+            lines2.append(line.strip("\n"))
+    combined = "\n".join(lines2) + "\n"
+    combined = replace_internal_references(combined)
+    return combined
+
+
+def main():
+    parser = ArgumentParser()
+    parser.add_argument("readme_file", help="README.md file to translate to RTD")
+    parser.add_argument("--output", "-o", default="gambit.md", help="output file")
+
+    args = parser.parse_args()
+    rtd = translate_readme_to_rtd(args.readme_file)
+    with open(args.output, "w+") as f:
+        print("Writing to", args.output)
+        f.write(rtd)
+
+
+if __name__ == "__main__":
+    main()