diff --git a/.github/workflows/rmc.yml b/.github/workflows/rmc.yml
index 0ab4fa2ca796..1747eb5e5dd0 100644
--- a/.github/workflows/rmc.yml
+++ b/.github/workflows/rmc.yml
@@ -46,3 +46,16 @@ jobs:
 
       - name: Execute RMC regression
         run: ./scripts/rmc-regression.sh
+
+      # On one OS only, build the documentation, too.
+      - name: Build Documentation
+        if: ${{ matrix.os == 'ubuntu-20.04' }}
+        run: ./rmc-docs/build-docs.sh
+
+      # When we're pushed to main branch, only then actually publish the docs.
+      - name: Publish Documentation
+        if: ${{ matrix.os == 'ubuntu-20.04' && github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }}
+        uses: JamesIves/github-pages-deploy-action@4.1.4
+        with:
+          branch: gh-pages
+          folder: rmc-docs/book/
diff --git a/.gitignore b/.gitignore
index 0f0dfb84b5c8..b2a0099fb5f2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -82,3 +82,5 @@ src/test/rustdoc-gui/src/**.lock
 /src/test/dashboard
 *Cargo.lock
 src/test/rmc-dependency-test/diamond-dependency/build
+/rmc-docs/book
+/rmc-docs/mdbook*
diff --git a/rmc-docs/README.md b/rmc-docs/README.md
new file mode 100644
index 000000000000..2ba0528e9ffd
--- /dev/null
+++ b/rmc-docs/README.md
@@ -0,0 +1,10 @@
+## RMC documentation development
+
+A good trick when developing RMC on a remote machine is to SSH forward to test documentation changes.
+
+```
+ssh -t -L 3000:127.0.0.1:3000 rmc-host 'cd rmc/rmc-docs/ && ./mdbook serve'
+```
+
+This command will connect to `rmc-host` where it assumes RMC is checked out in `rmc/` and the documentation has been built once successfully.
+It will automatically detect changes to the docs and rebuild, allowing you to quickly refresh in your local browser when you visit: `http://127.0.0.1:3000/`
diff --git a/rmc-docs/book.toml b/rmc-docs/book.toml
new file mode 100644
index 000000000000..065ead741e86
--- /dev/null
+++ b/rmc-docs/book.toml
@@ -0,0 +1,15 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[book]
+title = "The Rust Model Checker"
+description = "Documentation for the Rust Model Checker (RMC)"
+authors = ["RMC Developers"]
+src = "src"
+language = "en"
+multilingual = false
+
+[output.html]
+site-url = "/rmc/"
+git-repository-url = "https://github.com/model-checking/rmc"
+# If we get a stable default branch, we can use this feature, but HEAD doesn't work
+#edit-url-template = "https://github.com/model-checking/rmc/edit/HEAD/rmc-docs/{path}"
diff --git a/rmc-docs/build-docs.sh b/rmc-docs/build-docs.sh
new file mode 100755
index 000000000000..7a0e4fb2d947
--- /dev/null
+++ b/rmc-docs/build-docs.sh
@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -eu
+
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )"
+cd $SCRIPT_DIR
+
+# Download mdbook release (vs spending time building it via cargo install)
+FILE="mdbook-v0.4.12-x86_64-unknown-linux-gnu.tar.gz"
+URL="https://github.com/rust-lang/mdBook/releases/download/v0.4.12/$FILE"
+EXPECTED_HASH="2a0953c50d8156e84f193f15a506ef0adbac66f1942b794de5210ca9ca73dd33"
+if [ ! -x mdbook ]; then
+    curl -sSL -o "$FILE" "$URL"
+    echo "$EXPECTED_HASH $FILE" | sha256sum -c -
+    tar zxf $FILE
+fi
+
+# Build the book into ./book/
+mkdir -p book
+./mdbook build
+touch book/.nojekyll
+
+# TODO: Test all the code examples from our documentation
+# TODO: Build the dashboard and publish into our documentation
+
+echo "Finished documentation build successfully."
diff --git a/rmc-docs/src/SUMMARY.md b/rmc-docs/src/SUMMARY.md
new file mode 100644
index 000000000000..fe81e25e629d
--- /dev/null
+++ b/rmc-docs/src/SUMMARY.md
@@ -0,0 +1,12 @@
+# The Rust Model Checker
+
+- [Getting started with RMC](./getting-started.md)
+  - [Installation]()
+  - [Comparison with other tools]()
+  - [RMC on a single file]()
+  - [RMC on a crate]()
+  - [Debugging failures]()
+  
+- [RMC tutorial]()
+
+- [RMC developer documentation]()
diff --git a/rmc-docs/src/getting-started.md b/rmc-docs/src/getting-started.md
new file mode 100644
index 000000000000..662c25f86754
--- /dev/null
+++ b/rmc-docs/src/getting-started.md
@@ -0,0 +1,9 @@
+# Getting started with RMC
+
+Hello, World!
+
+```rust
+fn main() {
+    assert!(1 == 1);
+}
+```